🔍

Equations Inline Footnotes

open import Cat.Instances.Discrete
open import Cat.Functor.Base
open import Cat.Prelude

open import Data.Bool

open Functor

module Cat.Instances.Shape.Two where

The two-object category🔗

We define the discrete category $2$ on two objects, which is useful for expressing binary products and coproducts as limits and colimits, respectively.

2-object-category : Precategory _ _
2-object-category = Disc! Bool

A diagram of shape $2$ in $\mathcal{C}$ simply consists of two objects of $\mathcal{C}\text{.}$

module _ {o h} {C : Precategory o h} where
  open Precategory C

  2-object-diagram : Ob → Ob → Functor 2-object-category C
  2-object-diagram a b = Disc-diagram λ where
    true  → a
    false → b

Similarly, a natural transformation between two such diagrams consists of two morphisms in $\mathcal{C}\text{.}$

  2-object-nat-trans
    : ∀ {F G : Functor 2-object-category C}
    → Hom (F · true) (G · true) → Hom (F · false) (G · false)
    → F => G
  2-object-nat-trans f g = Disc-natural λ where
    true  → f
    false → g

We note that any functor $F:2\to \mathcal{C}$ is canonically equal, not just naturally isomorphic, to the one we defined above.

  canonical-functors : ∀ F → F ≡ 2-object-diagram (F · true) (F · false)
  canonical-functors F = Functor-path p q where
    p : ∀ x → _
    p false = refl
    p true  = refl

    q : ∀ {x y} (f : x ≡ᵢ y) → _
    q {true}  reflᵢ = F .F-id
    q {false} reflᵢ = F .F-id