SCT.VolumeI.Chapter01.Section05.Setup

Complete compiler-highlighted source. Follow a symbol to its declaration.

# The language used for initial categories and coproducts

We keep the mapping-anima interface as a separate parameter. This module
only collects previously proved operations; it introduces no assumptions.

```agda
{-# OPTIONS --safe --without-K #-}
open import Agda.Primitive using (Level)
open import SCT.VolumeI.Chapter01.Theory using (Theory)
import SCT.VolumeI.Chapter01.Section04.MappingAnimae as Mapping

module SCT.VolumeI.Chapter01.Section05.Setup
  {c m a : Level} (𝒯 : Theory c m a) (M : Mapping.MappingAnimae 𝒯) where

open import SCT.VolumeI.Chapter01.Section04.Setup 𝒯 public
open Mapping.MappingAnimae M public
open import SCT.VolumeI.Chapter01.Section04.Currying 𝒯 M public
open import SCT.VolumeI.Chapter01.Section04.Points 𝒯 M public
open import SCT.VolumeI.Chapter01.Section04.Functoriality 𝒯 M public
open import SCT.VolumeI.Chapter01.Section04.EquivalenceDetection 𝒯 M public
  using (unnamedIso; mapPre-name; mapPost-name)
```