module Cat.Instances.Shape.Parallel where

The “parallel arrows” category🔗

The parallel arrows category is the category with two objects, and two parallel arrows between them. It is the shape of equaliser and coequaliser diagrams.

·⇉· : Precategory lzero lzero
·⇉· = precat where
  open Precategory
  precat : Precategory _ _
  precat .Ob = Bool

  precat .Hom false false = 
  precat .Hom false true  = Bool
  precat .Hom true  false = 
  precat .Hom true  true  = 
module _ {o } {C : Precategory o } where
  open Cat.Reasoning C
  open Functor
  open _=>_

  Fork :  {a b} (f g : Hom a b)  Functor ·⇉· C
  Fork f g = funct where
    funct : Functor _ _
    funct .F₀ false = _
    funct .F₀ true = _
    funct .F₁ {false} {false} _ = id
    funct .F₁ {false} {true}  false = f
    funct .F₁ {false} {true}  true = g
    funct .F₁ {true} {true}   _ = id
    funct .F-id {false} = refl
    funct .F-id {true} = refl
    funct .F-∘ {false} {false} {false} f g   = sym (idr _)
    funct .F-∘ {false} {false} {true}  f g   = sym (idr _)
    funct .F-∘ {false} {true}  {true}  tt _  = sym (idl _)
    funct .F-∘ {true}  {true}  {true}  tt tt = sym (idl _)

  forkl : (F : Functor ·⇉· C)  Hom (F .F₀ false) (F .F₀ true)
  forkl F = F .F₁ {false} {true} false

  forkr : (F : Functor ·⇉· C)  Hom (F .F₀ false) (F .F₀ true)
  forkr F = F .F₁ {false} {true} true

  Fork→Cone
    :  {e} (F : Functor ·⇉· C) {equ : Hom e (F .F₀ false)}
     forkl F  equ  forkr F  equ
     Const e => F
  Fork→Cone {e = e} F {equ = equ} equal = nt where
    nt : Const e => F
    nt .η true = forkl F  equ
    nt .η false = equ
    nt .is-natural true true tt = idr _  introl (F .F-id)
    nt .is-natural false true true = idr _  equal
    nt .is-natural false true false = idr _
    nt .is-natural false false tt = idr _  introl (F .F-id)

  Cofork→Cocone
    :  {e} (F : Functor ·⇉· C) {coequ : Hom (F .F₀ true) e}
     coequ  forkl F  coequ  forkr F
     F => Const e
  Cofork→Cocone {e = e} F {coequ} coequal = nt where
    nt : F => Const e
    nt .η true = coequ
    nt .η false = coequ  forkl F
    nt .is-natural true true tt = elimr (F .F-id)  sym (idl _)
    nt .is-natural false true true = sym coequal  sym (idl _)
    nt .is-natural false true false = sym (idl _)
    nt .is-natural false false tt = elimr (F .F-id)  sym (idl _)