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 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' (el! Bool)


A diagram of shape in simply consists of two objects of

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

  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 is canonically equal, not just naturally isomorphic, to the one we defined above.

  canonical-functors
: β (F : Functor 2-object-category C)
β 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 {false} {false} p =
F .Fβ p           β‘β¨ ap (F .Fβ) (Bool-is-set _ _ _ _) β©β‘
F .Fβ refl        β‘β¨ F .F-id β©β‘
id                β
q {true} {true} p =
F .Fβ p           β‘β¨ ap (F .Fβ) (Bool-is-set _ _ _ _) β©β‘
F .Fβ refl        β‘β¨ F .F-id β©β‘
id                β
q {false} {true} p = absurd (trueβ false (sym p))
q {true} {false} p = absurd (trueβ false p)