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

    : βˆ€ {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.

    : βˆ€ (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)