Synthetic category theory

Volume I Β· Experimental web edition

SCT.VolumeI.Chapter01.Section05.Coproducts

Other Agda modules in this section (9)

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

Corresponding book passages
# The coproduct axiom

The restriction functor is constructed from the two inclusions using the
precomposition functors already defined in Section 1.4. Only the equivalence
of this particular functor is assumed (`post:Coproduct_Of_Categories`).

```agda
{-# OPTIONS --safe --without-K #-}
open import Agda.Primitive using (Level) renaming (_βŠ”_ to _βŠ”β„“_)
open import SCT.VolumeI.Chapter01.Theory using (Theory)
import SCT.VolumeI.Chapter01.Section04.MappingAnimae as Mapping
import SCT.VolumeI.Chapter01.Section05.Setup as Setup

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

open Setup 𝒯 M

record CoproductData : Set (c βŠ”β„“ m βŠ”β„“ a) where
  infixr 5 _βŠ”_
  field
    _βŠ”_ : CAT β†’ CAT β†’ CAT
    in₁ : {C D : CAT} β†’ MAP C (C βŠ” D)
    inβ‚‚ : {C D : CAT} β†’ MAP D (C βŠ” D)

  coproductRestriction : (C D E : CAT) β†’ MAP (Map (C βŠ” D) E) (Map C E Γ— Map D E)
  coproductRestriction C D E = pair (mapPre in₁) (mapPre inβ‚‚)

record CoproductLaws (B : CoproductData) : Set (c βŠ”β„“ m) where
  open CoproductData B
  field
    coproductRestriction-isEquiv : (C D E : CAT) β†’ IsEquiv (coproductRestriction C D E)

record CoproductStructure : Set (c βŠ”β„“ m βŠ”β„“ a) where
  field
    dataCoproduct : CoproductData
    lawsCoproduct : CoproductLaws dataCoproduct
  open CoproductData dataCoproduct public
  open CoproductLaws lawsCoproduct public
```