\import Category
\import Category.Adjoint
\import Category.Functor
\import Category.Product
\import Category.Slice
\import Data.Bool
\import Equiv
\import Function.Meta
\import Logic.Unique
\import Logic
\import Logic.Meta
\import Meta
\import Paths
\import Paths.Meta
\import Set (in0)

\class Cone {J : Precat} {D : Precat} (G : Functor J D) (\classifying apex : D)
  | coneMap (j : J) : Hom apex (G j)
  | coneCoh {j j' : J} (h : Hom j j') : G.Func h ∘ coneMap j = coneMap j'
  \where {
    \func map {C D : Precat} (F : Functor C D) {J : Precat} {G : Functor J C} (c : Cone G) : Cone (Comp F G) \cowith
      | apex => F c.apex
      | coneMap j => Func (c.coneMap j)
      | coneCoh h => inv Func-o *> pmap Func (c.coneCoh h)

    \func premap {J J' : Precat} (F : Functor J J') (c : Cone {J'} {}) : Cone (Comp c.G F) \cowith
      | apex => c.apex
      | coneMap j => c.coneMap (F j)
      | coneCoh h => c.coneCoh (F.Func h)

    \func mapEquiv {C D : Precat} (F : FullyFaithfulFunctor C D) {J : Precat} {G : Functor J C} (X : C) : QEquiv {Cone G X} {Cone (Comp F G) (F X)} (\lam c => map F c) \cowith
      | ret (c : Cone) => \new Cone {
        | coneMap j => F.inverse (c.coneMap j)
        | coneCoh h => F.isFaithful $ run {
          rewrite F.Func-o,
          repeat {} (rewrite F.inverse-right),
          c.coneCoh h
        }
      }
      | ret_f c => exts (\lam j => F.inverse-left)
      | f_sec c => exts (\lam j => F.inverse-right)
  }

\func conePullback {J : Precat} {D : Precat} {F : Functor J D} (C : Cone F) (z : D) (f : Hom z C.apex) : Cone F z \cowith
  | coneMap j => coneMap j ∘ f
  | coneCoh h => inv o-assoc *> pmap (∘ f) (coneCoh h)

\func IsLimitCone {J D : Precat} {F : Functor J D} (C : Cone F) : \Prop
  => \Pi (z : D) -> IsEquiv (conePullback C z)

\class Limit \extends Cone {
  | isLimit : IsLimitCone \this
  | limMap {z : D} (c : Cone G z) : Hom z apex
  | limBeta {z : D} (c : Cone G z) (j : J) : coneMap j ∘ limMap c = c.coneMap j
  | limUnique {z : D} {f g : Hom z apex} (p : \Pi (j : J) -> coneMap j ∘ f = coneMap j ∘ g) : f = g

  \default limMap \as limMap-impl {z} c : Hom z apex
    => IsEquiv.ret (isLimit z) c

  \default limBeta \as limBeta-impl {z} (c : Cone G z) j : coneMap j ∘ limMap-impl c = c.coneMap j
    => path (\lam i => coneMap {IsEquiv.f_ret (isLimit z) i} j)

  \default limUnique {z} {f} {g} p => IsEquiv.isInj (isLimit z) (exts p)

  \default isLimit z => inP \new QEquiv {
    | ret => limMap
    | ret_f f => limUnique (limBeta (conePullback _ z f))
    | f_sec c => exts (limBeta c)
  }

  \lemma limUniqueBeta {z : D} {c : Cone G z} {g : Hom z apex} (p : \Pi (j : J) -> c.coneMap j = coneMap j ∘ g) : limMap c = g
    => limUnique (\lam j => limBeta c j *> p j)
} \where {
  \use \level levelProp {J : Precat} {D : Precat} (G : Functor J D) (apex : D)
                        (cm : \Pi (j : J) -> Hom apex (G j)) (L L' : Limit G apex cm) : L = L' =>
    exts (\lam c => L.limUnique (\lam j => L.limBeta c j *> inv (L'.limBeta c j)))

  \lemma iso_lim {J : Precat} {D : Precat} {G : Functor J D} (c : Cone G) (L : Limit G) (e : Iso (L.limMap c)) : Limit { | Cone => c } \cowith
    | limMap c' => e.hinv ∘ limMap c'
    | limBeta c' j => pmap (∘ _) (inv (L.limBeta c j)) *> o-assoc *> pmap (_ ∘) (inv o-assoc *> pmap (∘ _) e.f_hinv *> id-left) *> L.limBeta c' j
    | limUnique {z} {f} {g} p => e.isMono $ L.limUnique (\lam j => inv o-assoc *> pmap (∘ f) (L.limBeta c j) *> p j *> pmap (∘ g) (inv (L.limBeta c j)) *> o-assoc)

  \lemma lim_iso {J : Precat} {D : Precat} {G : Functor J D} (L L' : Limit G) : Iso (L.limMap L') \cowith
    | hinv => L'.limMap L
    | hinv_f => limUnique \lam j => inv o-assoc *> pmap (∘ _) (L'.limBeta L j) *> L.limBeta L' j *> inv id-right
    | f_hinv => limUnique \lam j => inv o-assoc *> pmap (∘ _) (L.limBeta L' j) *> L'.limBeta L j *> inv id-right

  \func transFuncMap {D : Precat} (L L' : Limit { | D => D }) (H : Functor L.J L'.J) (a : NatTrans (Comp L'.G H) L.G) : Hom L' L
    => limMap cone
  \where {
    \func cone : Cone L.G L' => \new Cone {
      | coneMap j => a j ∘ L'.coneMap (H j)
      | coneCoh f => inv o-assoc *> pmap (∘ _) (inv (a.natural f)) *> o-assoc *> pmap (_ ∘) (L'.coneCoh (H.Func f))
    }
  }
}

\meta Colimit G => Limit (Functor.op {G})

\class Diagram (G : Graph) (D : Precat) (F : G -> D) (Func : \Pi {x y : G} -> G.E x y -> Hom (F x) (F y)) {
  \protected \func functor : Functor G.FreeCat D \cowith
    | F => F
    | Func {x y : G} (h : G.Paths x y) : Hom (F x) (F y) \elim h {
      | Graph.empty idp => id
      | Graph.cons e h => Func h ∘ Diagram.Func e
    }
    | Func-id => idp
    | Func-o {x y z : G} {q : G.Paths y z} {p : G.Paths x y} : Func (G.concat p q) = Func q ∘ Func p \elim p {
      | Graph.empty idp => inv id-right
      | Graph.cons e p => rewrite Func-o o-assoc
    }
}

\class DiagramCone \extends Diagram, Cone
  | J => G.FreeCat
  | Cone.D => Diagram.D
  | Cone.G => Diagram.functor
  | diagramCoh {g g' : G} (e : G.E g g') : Func e ∘ coneMap g = coneMap g'
  | coneCoh => coneCoh-lem apex coneMap diagramCoh
  \where {
    \lemma coneCoh-lem {D : Diagram} (apex : D.D) (coneMap : \Pi (j : D.G.FreeCat) -> Hom apex (D.functor j)) (p : \Pi {g g' : D.G} (e : D.G.E g g') -> D.Func e ∘ coneMap g = coneMap g') {j j' : D.G.FreeCat} (h : D.G.FreeCat.Hom j j') : D.functor.Func h ∘ coneMap j = coneMap j' \elim h
      | Graph.empty idp => id-left
      | Graph.cons e h => o-assoc *> pmap (_ ∘) (p e) *> coneCoh-lem apex coneMap p h

    \func pullback {G : Graph} {D : Diagram G} {C : DiagramCone { | Diagram => D }} (z : D.D) (f : Hom z C.apex) : DiagramCone \cowith
      | Diagram => D
      | apex => z
      | coneMap j => coneMap j ∘ f
      | diagramCoh e => inv o-assoc *> pmap (∘ f) (diagramCoh e)

    \func equiv {D : Diagram} (Z : D.D) : QEquiv {DiagramCone { | Diagram => D | apex => Z }} {Cone D.functor Z} (\lam d => d) \cowith
      | ret c => \new DiagramCone {
        | coneMap => c.coneMap
        | diagramCoh e => rewrite id-left in c.coneCoh (Graph.cons e (Graph.empty idp))
      }
      | ret_f d => idp
      | f_sec c => idp
  }

\class LimitDiagram \extends DiagramCone, Limit
  | isLimitDiagram (Z : D) : IsEquiv (DiagramCone.pullback Z)
  | isLimit Z => IsEquiv.trans (isLimitDiagram Z) $ inP (DiagramCone.equiv Z)

\class Product {J : \Type} {D : Precat} (G : J -> D) (\classifying apex : D) {
  | proj (j : J) : Hom apex (G j)
  | tupleMap {Z : D} (f : \Pi (j : J) -> Hom Z (G j)) : Hom Z apex
  | tupleBeta {Z : D} {f : \Pi (j : J) -> Hom Z (G j)} {j : J} : proj j ∘ tupleMap f = f j
  | tupleEq {Z : D} {h1 h2 : Hom Z apex} : (\Pi (j : J) -> proj j ∘ h1 = proj j ∘ h2) -> h1 = h2

  \lemma isProduct (Z : D) : IsEquiv (\lam (h : Hom Z apex) => proj __ ∘ h) => inP \new QEquiv {
    | ret => tupleMap
    | ret_f h => tupleEq (\lam j => tupleBeta)
    | f_sec f => ext (\lam j => tupleBeta)
  }

  \lemma tupleMapComp {W Z : D} (f : \Pi (j : J) -> Hom Z (G j)) (h : Hom W Z) : tupleMap f ∘ h = tupleMap (f __ ∘ h)
    => tupleEq \lam j => inv o-assoc *> pmap (∘ h) tupleBeta *> inv tupleBeta

  \lemma tupleEta {Z : D} {f : Hom Z apex} : tupleMap (\lam j => proj j ∘ f) = f
    => tupleEq \lam j => tupleBeta

  \protected \func toLimit : Limit {DiscretePrecat J} {D} \cowith
    | G => functor G
    | apex => apex
    | coneMap => proj
    | coneCoh {j} {j'} (in0 idp) => id-left
    | isLimit Z => IsEquiv.trans {_} {_} {Cone (functor G) Z} (isProduct Z) $ inP \new QEquiv {
      | f p => \new Cone {
        | coneMap => p
        | coneCoh {j} {j'} (in0 idp) => id-left
      }
      | ret => coneMap {__}
      | ret_f p => idp
      | f_sec c => idp
    }
} \where {
  \func functor {J : \Type} {D : Precat} (G : J -> D) : Functor (DiscretePrecat J) D \cowith
    | F => G
    | Func => DiscretePrecat.map G
    | Func-id => idp
    | Func-o {x} {y} {z} {in0 idp} {in0 idp} => inv id-left

  \use \coerce fromLimit {J : \Type} {D : Precat} (L : Limit {DiscretePrecat J} {D}) : Product L.G L.apex L.coneMap \cowith
    | tupleMap c => L.limMap (cone c)
    | tupleBeta => L.limBeta _ _
    | tupleEq {z} {h1} {h2} f => inv (IsEquiv.ret_f (L.isLimit z)) *> pmap (IsEquiv.ret (L.isLimit z)) (exts f) *> IsEquiv.ret_f (L.isLimit z)
    \where {
      \func cone {J : \Type} {D : Precat} {Z : D} {G : Functor (DiscretePrecat J) D} (c : \Pi (j : J) -> Hom Z (G j)) : Cone G Z \cowith
        | coneMap => c
        | coneCoh {_} {j'} (in0 p) => \case \elim j', \elim p \with {
          | _, idp => pmap (∘ _) Func-id *> id-left
        }
    }
}

\class Equalizer {D : Precat} {X Y : D} (f g : Hom X Y) (\classifying apex : D) (eql : Hom apex X) (equal : f ∘ eql = g ∘ eql) {
  | isEqualizer (Z : D) : IsEquiv {Hom Z apex} {\Sigma (h : Hom Z X) (f ∘ h = g ∘ h)} (\lam h => (eql ∘ h, inv o-assoc *> pmap (∘ h) equal *> o-assoc))

  \func eqMap {Z : D} (h : Hom Z X) (p : f ∘ h = g ∘ h) : Hom Z apex
    => IsEquiv.ret (isEqualizer Z) (h,p)

  \lemma eqBeta {Z : D} {h : Hom Z X} {p : f ∘ h = g ∘ h} : eql ∘ eqMap h p = h
    => pmap __. (IsEquiv.f_ret (isEqualizer Z))

  \lemma eqMono {Z : D} {h1 h2 : Hom Z apex} (p : eql ∘ h1 = eql ∘ h2) : h1 = h2
    => inv (IsEquiv.ret_f (isEqualizer Z)) *> pmap (IsEquiv.ret _) (ext p) *> IsEquiv.ret_f (isEqualizer Z)

  \protected \func toLimit : Limit {Shape} {D} \cowith
    | G => functor f g
    | apex => apex
    | coneMap x => \case \elim x \with {
      | false => eql
      | true => g ∘ eql
    }
    | coneCoh {x} {y} h => \case \elim x, \elim y, \elim h \with {
      | false, true, arrow1 => equal
      | false, true, arrow2 => idp
      | false, false, id_false => id-left
      | true, true, id_true => id-left
    }
    | isLimit Z =>
      \have equiv => IsEquiv.trans {_} {_} {Cone (functor f g) Z} (isEqualizer Z) (inP \new QEquiv {
        | f p => \new Cone {
          | coneMap b => \case \elim b \with {
            | false => p.
            | true => g ∘ p.
          }
          | coneCoh {j} {j'} h => \case \elim j, \elim j', \elim h \with {
            | false, true, arrow1 => p.
            | false, true, arrow2 => idp
            | false, false, id_false => id-left
            | true, true, id_true => id-left
          }
        }
        | ret (c : Cone) => (c.coneMap false, c.coneCoh arrow1 *> inv (c.coneCoh arrow2))
        | ret_f p => ext idp
        | f_sec (c : Cone) => exts \case \elim __ \with {
          | false => idp
          | true => c.coneCoh arrow2
        }
      })
      \in transport (IsEquiv __) (ext \lam h => exts \case \elim __ \with {
        | false => idp
        | true => inv o-assoc
      }) equiv
} \where {
  \data Arrows (x y : Bool) \with
    | false, true => { arrow1 | arrow2 }
    | false, false => id_false
    | true, true => id_true

  \func map {D : Precat} {X Y : D} (f g : Hom X Y) {x y : Bool} (a : Arrows x y) : Hom (if x Y X) (if y Y X) \elim x, y, a
    | false, true, arrow1 => f
    | false, true, arrow2 => g
    | false, false, id_false => id
    | true, true, id_true => id

  \func Shape : Precat Bool \cowith
    | Hom => Arrows
    | id {x : Bool} : Arrows x x \elim x {
      | false => id_false
      | true => id_true
    }
    | o {x y z : Bool} (g : Arrows y z) (f : Arrows x y) : Arrows x z \elim x, y, z, g, f {
      | false, _, false, _, _ => id_false
      | true, _, true, _, _ => id_true
      | false, false, true, a, _ => a
      | false, true, true, _, a => a
      | true, false, false, _, ()
    }
    | id-left {x} {y} {f} => cases (x,y,f) idp
    | id-right {x} {y} {f} => cases (x,y,f) idp
    | o-assoc {x} {y} {z} {w} {h} {g} {f} => cases (x,y,z,w,h,g,f) idp

  \func functor {D : Precat} {x y : D} (f g : Hom x y) : Functor Shape D \cowith
    | F => if __ y x
    | Func => map f g
    | Func-id {x} => cases x idp
    | Func-o {x} {y} {z} {h} {k} => cases (x,y,z,h,k) (inv id-left) \with {
      | false, false, true, arrow1, id_false => inv id-right
      | false, false, true, arrow2, id_false => inv id-right
    }

  \use \coerce fromLimit {D : Precat} {x y : D} {f g : Hom x y} (L : Limit (functor f g)) : Equalizer f g
    => \have cone {z : D} (h : Hom z x) (p : f ∘ h = g ∘ h) => \new Cone (functor f g) z {
         | coneMap => \case \elim __ \with {
           | false => h
           | true => g ∘ h
         }
         | coneCoh {j} {j'} k => cases (j,j',k) \with {
           | false, true, arrow1 => p
           | false, true, arrow2 => idp
           | false, false, id_false => id-left
           | true, true, id_true => id-left
         }
       } \in \new Equalizer {
         | apex => L.apex
         | eql => L.coneMap false
         | equal => L.coneCoh arrow1 *> inv (L.coneCoh arrow2)
         | isEqualizer Z => inP \new QEquiv {
           | ret (h,p) => L.limMap (cone h p)
           | ret_f h => L.limUnique \case \elim __ \with {
             | false => L.limBeta _ false
             | true => L.limBeta _ true *> inv o-assoc *> pmap (∘ h) (L.coneCoh arrow2)
           }
           | f_sec (h,p) => ext (L.limBeta (cone h p) false)
         }
    }

  \func unique {D : Precat} {x y : D} {f g : Hom x y} (E E' : Equalizer f g) : Iso {D} {E} {E'} \cowith
    | f => E'.eqMap eql equal
    | hinv => E.eqMap eql equal
    | hinv_f => E.eqMono $ inv o-assoc *> pmap (∘ _) E.eqBeta *> E'.eqBeta *> inv id-right
    | f_hinv => E'.eqMono $ inv o-assoc *> pmap (∘ _) E'.eqBeta *> E.eqBeta *> inv id-right

  \lemma unique-map {D : Precat} {x y : D} {f g : Hom x y} (E E' : Equalizer f g) : E'.eql ∘ Iso.f {unique E E'} = E.eql
    => E'.eqBeta

  \lemma mono=>equalizer {D : Precat} {x y e : D} {f g : Hom x y} {eql : Hom e x} (m : Mono eql) (equal : f ∘ eql = g ∘ eql)
                         (p : \Pi {z : D} (h : Hom z x) -> f ∘ h = g ∘ h -> ∃ (k : Hom z e) (eql ∘ k = h))
    : Equalizer f g e eql equal \cowith
    | isEqualizer z => IsEquiv.fromInjSurj
      (\lam q => m.isMono $ pmap __. q)
      (\lam t => TruncP.map (p t. t.) (\lam q => (q., ext q.)))

  \func id-equalizer {D : Precat} {X Y : D} {f : Hom X Y} : Equalizer f f X id \cowith
    | equal => idp
    | isEqualizer _ => inP \new QEquiv {
      | ret (h, _) => h
      | ret_f _ => id-left
      | f_sec _ => exts id-left
    }

  \func equalizer-iso {D : Precat} {X Y : D} {f : Hom X Y} (eq : Equalizer f f) : Iso {D} {eq} {X} eq.eql
  \cowith
    | hinv => unique id-equalizer eq
    | hinv_f => unfold $ eq.eqMono $ rewriteI o-assoc $ rewrite (eq.eqBeta, id-left, id-right) idp
    | f_hinv => unique-map id-equalizer eq
}

\class Pullback {D : Precat} {x y z : D} (f : Hom x z) (g : Hom y z) (\classifying apex : D) {
  | pbProj1 : Hom apex x
  | pbProj2 : Hom apex y
  | pbCoh : f ∘ pbProj1 = g ∘ pbProj2
  | pbMap {w : D} (p1 : Hom w x) (p2 : Hom w y) : f ∘ p1 = g ∘ p2 -> Hom w apex
  | pbBeta1 {w : D} {p1 : Hom w x} {p2 : Hom w y} {c : f ∘ p1 = g ∘ p2} : pbProj1 ∘ pbMap p1 p2 c = p1
  | pbBeta2 {w : D} {p1 : Hom w x} {p2 : Hom w y} {c : f ∘ p1 = g ∘ p2} : pbProj2 ∘ pbMap p1 p2 c = p2
  | pbEta {w : D} {h1 h2 : Hom w apex} : pbProj1 ∘ h1 = pbProj1 ∘ h2 -> pbProj2 ∘ h1 = pbProj2 ∘ h2 -> h1 = h2

  \lemma pbMap-comp {a b : D} {p1 : Hom b x} {p2 : Hom b y} {c : f ∘ p1 = g ∘ p2} {h : Hom a b} : pbMap p1 p2 c ∘ h = pbMap (p1 ∘ h) (p2 ∘ h) (inv o-assoc *> pmap (∘ h) c *> o-assoc) =>
    pbEta (inv o-assoc *> rewrite pbBeta1 idp *> inv pbBeta1) (inv o-assoc *> rewrite pbBeta2 idp *> inv pbBeta2)

  \func flip : Pullback g f apex pbProj2 pbProj1 (inv pbCoh) \cowith
    | pbMap p1 p2 c => pbMap p2 p1 (inv c)
    | pbBeta1 => pbBeta2
    | pbBeta2 => pbBeta1
    | pbEta q1 q2 => pbEta q2 q1

  \protected \func toLimit : LimitDiagram \cowith
    | Diagram => diagram f g
    | apex => apex
    | coneMap => \case \elim __ \with {
      |  => pbProj1
      |  => pbProj2
      |  => f ∘ pbProj1
    }
    | diagramCoh {g} {g'} e => \case \elim g, \elim g', \elim e \with {
      | , , _ => idp
      | , , _ => inv pbCoh
    }
    | isLimitDiagram z => inP \new QEquiv {
      | ret c => pbMap (c.coneMap ) (c.coneMap ) (c.diagramCoh {} {} () *> inv (c.diagramCoh {} {} ()))
      | ret_f h => pbEta pbBeta1 pbBeta2
      | f_sec c => exts \case \elim __ \with {
        |  => pbBeta1
        |  => pbBeta2
        |  => o-assoc *> rewrite pbBeta1 (diagramCoh {c} ())
      }
    }
} \where {
  \instance Shape : Graph.{,}
    | V => Fin 
    | E => \case __, __ \with {
      | ,  => \Sigma
      | ,  => \Sigma
      | _, _ => Empty
    }

  \func diagram {D : Precat} {x y z : D} (f : Hom x z) (g : Hom y z) : Diagram Shape D \cowith
    | F => \case __ \with {
      |  => x
      |  => y
      |  => z
    }
    | Func {a} {b} e => \case \elim a, \elim b, \elim e \with {
      | , , _ => f
      | , , _ => g
    }

  \use \coerce fromLimit {D : Precat} {x y z : D} {f : Hom x z} {g : Hom y z} (L : Limit (diagram f g).functor) : Pullback f g L.apex
    => \let | d => (DiagramCone.equiv {diagram f g} L.apex).ret L
            | d' {w} p1 p2 c => \new DiagramCone {
              | Diagram => diagram f g
              | apex => w
              | coneMap => \case \elim __ \with {
                |  => p1
                |  => p2
                |  => f ∘ p1
              }
              | diagramCoh {g} {g'} e => \case \elim g, \elim g', \elim e \with {
                | , , _ => idp
                | , , _ => inv c
              }
            }
       \in \new Pullback {
        | pbProj1 => L.coneMap 
        | pbProj2 => L.coneMap 
        | pbCoh => d.diagramCoh {} {} () *> inv (d.diagramCoh {} {} ())
         | pbMap {w} p1 p2 c => L.limMap (d' p1 p2 c)
         | pbBeta1 {w} {p1} {p2} {c} => L.limBeta (d' p1 p2 c) 
         | pbBeta2 {w} {p1} {p2} {c} => L.limBeta (d' p1 p2 c) 
         | pbEta {w} {h1} {h2} p q => inv (IsEquiv.ret_f (L.isLimit w)) *> pmap (IsEquiv.ret (L.isLimit w)) (exts \case \elim __ \with {
           |  => p
           |  => q
           |  => pmap (∘ _) (inv (d.diagramCoh {} {} ())) *> o-assoc *> pmap (f ∘) p *> inv o-assoc *> pmap (∘ _) (d.diagramCoh {} {} ())
         }) *> IsEquiv.ret_f (L.isLimit w)
      }

  \func fromIso (P : Pullback {}) (e : Iso {P.D} { | cod => P }) : Pullback P.f P.g e.dom \cowith
    | pbProj1 => pbProj1 ∘ e
    | pbProj2 => pbProj2 ∘ e
    | pbCoh => inv o-assoc *> pmap (∘ _) pbCoh *> o-assoc
    | pbMap p1 p2 c => e.hinv ∘ pbMap p1 p2 c
    | pbBeta1 => o-assoc *> pmap (_ ∘) (inv o-assoc *> pmap (∘ _) e.f_hinv *> id-left) *> pbBeta1
    | pbBeta2 => o-assoc *> pmap (_ ∘) (inv o-assoc *> pmap (∘ _) e.f_hinv *> id-left) *> pbBeta2
    | pbEta s1 s2 => e.isMono $ pbEta (inv o-assoc *> s1 *> o-assoc) (inv o-assoc *> s2 *> o-assoc)

  \func unique {D : Precat} {x y z : D} (f : Hom x z) (g : Hom y z) (P P' : Pullback f g) : Iso {D} {P} {P'}
  \cowith
    | f => p-map P P'
    | hinv => p-map P' P
    | hinv_f => hinv' P P'
    | f_hinv => hinv' P' P
    \where {
      \func p-map{D : Precat} {x y z : D} {f : Hom x z} {g : Hom y z} (P P' : Pullback f g) : Hom P P' =>
        pbMap {P'} P.pbProj1 P.pbProj2 P.pbCoh

      \func p-beta1 {D : Precat} {x y z : D} {f : Hom x z} {g : Hom y z} (P P' : Pullback f g)
        : pbProj1 {P} ∘ (p-map P' P) = pbProj1 {P'} => pbBeta1 {P} {P'} {pbProj1 {P'}} {pbProj2 {P'}} {pbCoh {P'}}

      \func p-beta2 {D : Precat} {x y z : D} {f : Hom x z} {g : Hom y z} (P P' : Pullback f g)
        : pbProj2 {P} ∘ (p-map P' P) = pbProj2 {P'} => pbBeta2 {P} {P'} {pbProj1 {P'}} {pbProj2 {P'}} {pbCoh {P'}}

      \func hinv'{D : Precat} {x y z : D} {f : Hom x z} {g : Hom y z} (P P' : Pullback f g)
        : (p-map P' P) ∘ (p-map P P') = id => pbEta {P} {P} {(p-map P' P) ∘ (p-map P P')} {id}
          (rewriteI o-assoc $ rewrite (p-beta1 P P', p-beta1 P' P) (inv id-right))
          (rewriteI o-assoc $ rewrite (p-beta2 P P', p-beta2 P' P) (inv id-right))
    }
}

\func limits<=pr+eq.{u} {D : Precat}
  (pr : \Pi (J : \Type u) (G : J -> D) -> Product G)
  (eq : \Pi {X Y : D} (f g : Hom X Y) -> Equalizer f g)
  {J : Precat.{u,u}} (G : Functor J D) : Limit G
  => \have | X => pr J G
           | Y => pr (\Sigma (j j' : J) (J.Hom j j')) (\lam t => G t.)
           | eql => eq {X.apex} {Y.apex}
              (Y.tupleMap (\lam t => G.Func t. ∘ X.proj t.))
              (Y.tupleMap (\lam t => X.proj t.))
     \in \new Limit {
      | apex => eql.apex
      | coneMap j => X.proj j ∘ eql.eql
      | coneCoh {j} {j'} h => inv o-assoc *> inv (pmap (∘ eql.eql) Y.tupleBeta) *> o-assoc *> pmap (Y.proj (j,j',h) ∘) eql.equal *> inv o-assoc *> pmap (∘ eql.eql) Y.tupleBeta
      | isLimit Z => inP \new QEquiv {
        | ret (c : Cone) => eql.eqMap (X.tupleMap c.coneMap) (Y.tupleMapComp _ _ *> pmap Y.tupleMap (ext (\lam j => o-assoc *> pmap (_ ∘) X.tupleBeta *> c.coneCoh j. *> inv X.tupleBeta)) *> inv (Y.tupleMapComp _ _))
        | ret_f h => eql.eqMono (eql.eqBeta *> path (\lam i => X.tupleMap (\lam j => o-assoc {_} {_} {_} {_} {_} {X.proj j} @ i)) *> X.tupleEq (\lam j => X.tupleBeta))
        | f_sec (c : Cone) => exts \lam j => o-assoc *> pmap (_ ∘) eql.eqBeta *> X.tupleBeta
      }
    }


\class PrecatWithPullbacks \extends Precat
  | pullback {x y z : Ob} (f : Hom x z) (g : Hom y z) : Pullback f g

\func pullbackFunctor {C : PrecatWithPullbacks} {x y : C} (f : Hom x y) : Functor (SlicePrecat y) (SlicePrecat x) \cowith
  | F (t : ObOver y) : ObOver x => (pullback f t., (pullback f t.).pbProj1)
  | Func {a b : ObOver y} (g : Hom a b) : Hom (F a) (F b) =>
    \let p : Pullback => pullback f a.
    \in (pbMap p.pbProj1 (g. ∘ p.pbProj2) (p.pbCoh *> pmap (∘ p.pbProj2) (inv g.) *> o-assoc), pbBeta1)
  | Func-id => ext $ pbEta (pbBeta1 *> inv id-right) (pbBeta2 *> id-left *> inv id-right)
  | Func-o => ext $ pbEta (pbBeta1 *> inv (pmap (∘ _) pbBeta1 *> later pbBeta1) *> o-assoc) (pbBeta2 *> inv (pmap (∘ _) pbBeta2 *> o-assoc *> pmap (_ ∘) pbBeta2 *> inv o-assoc) *> o-assoc)

\meta terminal-obj C => Product {Empty} {C} absurd

\func terminal-obj-iso {C : Precat} (a b : terminal-obj C) : Iso {C} {a} {b}
\cowith
  | f => tupleMap (\case __)
  | hinv => tupleMap (\case __)
  | hinv_f => tupleEq (\case __)
  | f_hinv => tupleEq (\case __)

\func terminalMap' {C : Precat} {t : terminal-obj C} {x : C} : Hom x t => tupleMap (\case __)

\func isTerminal {C : Precat} (a : C) (e : \Pi (b : C) -> Contr (Hom b a)) : terminal-obj C a
  \cowith
    | proj j => absurd j
    | tupleMap {Z} _ => Contr.center {e Z}
    | tupleBeta {_} {_} {j} => absurd j
    | tupleEq {Z} {p} {q} _ => isContr=>isProp (e Z) p q

\lemma terminal-unique' {C : Precat} {terminal : terminal-obj C} {x : C} {f g : Hom x terminal} : f = g => tupleEq (\case __)

\func terminal-prop {C : Cat} : isProp (terminal-obj C)
  => \lam a a' => exts (C.isotoid (unfold $ terminal-obj-iso a a'), \lam j => absurd j, \lam {Z} f => terminal-unique')

\func IsTerminal {C : Precat} (t : C) : \Prop
  => \Pi {c : C} -> Contr (Hom c t)

\class PrecatWithTerminal \extends Precat {
  | terminal : terminal-obj \this

  \func terminalMap {x : Ob} : Hom x terminal => tupleMap (\case __)

  \lemma terminal-unique {x : Ob} {f g : Hom x terminal} : f = g => tupleEq (\case __)

  \func point-splitMono {c : Ob} {p : Hom terminal c} : SplitMono p \cowith
    | hinv => terminalMap
    | hinv_f => terminal-unique
}

\class PrecatWithBprod \extends Precat {
  | Bprod (x y : Ob) : Product (x :: y :: nil)

  \func proj1 {x y : Ob} => proj {Bprod x y} 

  \func proj2 {x y : Ob} => proj {Bprod x y} 

  \func pair {x y z : Ob} (f : Hom z x) (g : Hom z y) : Hom z (Bprod x y)
    => tupleMap \case \elim __ \with {
      |  => f
      |  => g
    }

  \func prodMap {x y x' y' : Ob} (f : Hom x y) (f' : Hom x' y') : Hom (Bprod x x') (Bprod y y')
    => pair (f ∘ proj1) (f' ∘ proj2)

  \lemma prodMap-comp {x y x' y' z z' : Ob} {f : Hom x y} {g : Hom y z} {f' : Hom x' y'} {g' : Hom y' z'}
    : prodMap g g' ∘ prodMap f f' = prodMap (g ∘ f) (g' ∘ f')
    => inv $ pair-unique (rewriteI o-assoc $ rewrite (beta1,beta1) $ rewrite {} o-assoc $ rewrite beta1 o-assoc)
                         (rewriteI o-assoc $ rewrite (beta2,beta2) $ rewrite {} o-assoc $ rewrite beta2 o-assoc)

  \func prodMap-split-right {x y x' y' : Ob} (f : Hom x y) (g : Hom x' y')
    : prodMap f g = prodMap f id ∘ prodMap id g
    => rewrite prodMap-comp $ rewrite (id-left, id-right) idp

  \func prod-id-left {x y z w : Ob} {g : Hom y z} {f : Hom x y}
    : prodMap (id {_} {w}) g ∘ prodMap id f = prodMap id (g ∘ f)
    => prodMap-comp *> pmap (prodMap __ _) id-left

  \func prod-id-right {x y z w : Ob} {g : Hom y z} {f : Hom x y}
    : prodMap g (id {_} {w}) ∘ prodMap f id = prodMap (g ∘ f) id
    => prodMap-comp *> pmap (prodMap _) id-left

  \lemma prod-id {x y : Ob} : prodMap id id = id {_} {Bprod x y}
    => unfold prodMap $ rewrite (id-left, id-left) pair-eta

  \lemma beta1 {x y z : Ob} {f : Hom z x} {g : Hom z y} : proj1 ∘ pair f g = f => tupleBeta {Bprod x y}

  \lemma beta2 {x y z : Ob} {f : Hom z x} {g : Hom z y} : proj2 ∘ pair f g = g
    => (Bprod x y).tupleBeta

  \lemma pair-unique {x y z : Ob} {h1 h2 : Hom z (Bprod x y)} (p1 : proj1 ∘ h1 = proj1 ∘ h2) (p2 : proj2 ∘ h1 = proj2 ∘ h2) : h1 = h2
    => tupleEq $ \case \elim __ \with {
      |  => p1
      |  => p2
    }

  \lemma pair-comp {x y z w : Ob} {f : Hom x y} {g : Hom y z} {h : Hom y w} : pair g h ∘ f = pair (g ∘ f) (h ∘ f)
    => pair-unique (inv o-assoc *> pmap (∘ f) beta1 *> inv beta1) (inv o-assoc *> pmap (∘ f) beta2 *> inv beta2)

  \lemma pair-eta {x y : Ob} : pair proj1 proj2 = id {_} {Bprod x y}
    => pair-unique (beta1 *> inv id-right) (beta2 *> inv id-right)

  \func diagonal (x : Ob) : Hom x (Bprod x x)
    => pair id id

  \lemma diagonal-splitMono {x : Ob} : SplitMono (diagonal x) proj1 \cowith
    | hinv_f => beta1

  \func associator {x y z : Ob} : Hom (Bprod (Bprod x y) z) (Bprod x (Bprod y z))
    => pair (proj1 ∘ proj1) (pair (proj2 ∘ proj1) proj2)

  \func associator-iso {x y z : Ob} : Iso (associator {_} {x} {y} {z}) \cowith
    | hinv => pair (pair proj1 (proj1 ∘ proj2)) (proj2 ∘ proj2)
    | hinv_f => rewrite (pair-comp,pair-comp,beta1,o-assoc,beta2,beta1,o-assoc,beta2,beta2,inv pair-comp,pair-eta,id-left) pair-eta
    | f_hinv => rewrite (pair-comp,o-assoc,beta1,beta1,pair-comp,beta2,o-assoc,beta1,beta2,inv pair-comp,pair-eta,id-left) pair-eta

  \lemma associator-pair {x y z w : Ob} {f : Hom w x} {g : Hom w y} {h : Hom w z} : associator ∘ pair (pair f g) h = pair f (pair g h)
    => pair-comp *> pmap2 pair (o-assoc *> pmap (_ ∘) beta1 *> beta1) (pair-comp *> pmap2 pair (o-assoc *> pmap (_ ∘) beta1 *> beta2) beta2)

  \lemma associator-inv-pair {x y z w : Ob} {f : Hom w x} {g : Hom w y} {h : Hom w z} : associator-iso.hinv ∘ pair f (pair g h) = pair (pair f g) h
    => inv (associator-iso.adjointMap associator-pair)

  \lemma associator-prod {x y z : Ob} {x' y' z' : Ob} {f : Hom x x'} {g : Hom y y'} {h : Hom z z'}
    : prodMap f (prodMap g h) ∘ associator = associator ∘ prodMap (prodMap f g) h
    => pair-unique
      (run {
        rewrite (inv o-assoc, beta1, o-assoc, beta1),
        rewriteI {} o-assoc ,
        rewrite (beta1, o-assoc, beta1),
        rewriteI {} o-assoc,
        rewrite beta1,
        inv o-assoc
    })
      (run {
        rewriteI o-assoc,
        rewrite (beta2, o-assoc, beta2, inv o-assoc, beta2, pair-comp, o-assoc, beta1, o-assoc, beta2, pair-comp),
        rewrite (o-assoc, beta1, beta2),
        rewriteI {} o-assoc,
        rewrite (beta2, o-assoc),
        idp
      })

  \lemma associator-inv-prod {x y z : Ob} {x' y' z' : Ob} {f : Hom x x'} {g : Hom y y'} {h : Hom z z'}
    : prodMap (prodMap f g) h ∘ associator-iso.hinv = associator-iso.hinv ∘ prodMap f (prodMap g h)
    => associator-iso.adjointMap $ inv o-assoc *> inv (associator-iso.adjointMap' associator-prod)

  \func bprodFunctorRight (Y : Ob) : Functor \this \this \cowith
    | F X => Bprod X Y
    | Func f => prodMap f id
    | Func-id => unfold prodMap $ rewrite (id-left, id-left) pair-eta
    | Func-o => inv prod-id-right

  \func swap {x y : Ob} : Hom (Bprod x y) (Bprod y x)
    => pair proj2 proj1

  \func swap-iso {x y : Ob} : Iso (swap {_} {x} {y}) \cowith
    | hinv => swap
    | hinv_f => swap-inv
    | f_hinv => swap-inv

  \lemma swap-inv {x y : Ob} : swap ∘ swap = id {_} {Bprod x y}
    => pair-unique (rewriteI o-assoc $ rewrite (beta1, beta2, id-right) idp)
                   (rewriteI o-assoc $ rewrite (beta2, beta1, id-right) idp)

  \lemma swap-pair {z x y : Ob} {f : Hom z x} {g : Hom z y} : swap ∘ pair f g = pair g f
    => pair-unique (inv o-assoc *> pmap (∘ _) beta1 *> beta2 *> inv beta1) (inv o-assoc *> pmap (∘ _) beta2 *> beta1 *> inv beta2)

  \lemma swap-prod {x y x' y' : Ob} {f : Hom x x'} {g : Hom y y'} : swap ∘ prodMap f g = prodMap g f ∘ swap
    => swap-pair *> inv (pair-comp *> pmap2 pair (o-assoc *> pmap (g ∘) beta1) (o-assoc *> pmap (f ∘) beta2))

  \func bprod-comm {x y : Ob} : Iso (swap {_} {x} {y})\cowith
    | hinv => swap {_} {y} {x}
    | hinv_f => swap-inv {_} {x} {y}
    | f_hinv => swap-inv {_} {y} {x}

  \func bprodBiFunctor : Functor (ProductPrecat \this \this) \this \cowith
    | F x => Bprod x. x.
    | Func f => prodMap f. f.
    | Func-id => prod-id
    | Func-o => inv prodMap-comp
}

\class CartesianPrecat \extends PrecatWithTerminal, PrecatWithBprod {
  \func Bprod_terminal-left {X : Ob} : Iso {\this} {X} {Bprod terminal X}  \cowith
    | f => pair terminalMap id
    | hinv => proj2
    | hinv_f => beta2
    | f_hinv => pair-unique (rewrite (inv o-assoc, beta1, id-right) terminal-unique)
        (rewrite (inv o-assoc, beta2, id-right, id-left) idp)
}

\class FinCompletePrecat \extends PrecatWithPullbacks, CartesianPrecat {
  \default Bprod x y => \new Product {
    | apex => pullback (terminal.tupleMap (\case __)) (tupleMap (\case __))
    | proj => \case \elim __ \with {
      |  => pbProj1
      |  => pbProj2
    }
    | tupleMap f => pbMap (f ) (f ) $ tupleEq (\case __)
    | tupleBeta {_} {_} {j} => \case \elim j \with {
      |  => pbBeta1
      |  => pbBeta2
    }
    | tupleEq f => pbEta (f ) (f )
  }

  \func equalizer {x y : Ob} {f g : Hom x y} : Equalizer f g
    => Equalizer.mono=>equalizer (Mono_pullback (pullback (pair f g) (diagonal y)) diagonal-splitMono)
        (pmap (∘ _) (inv beta1) *> o-assoc *> pmap (proj1 ∘) pbCoh *> inv o-assoc *> pmap (∘ _) beta1 *>
         inv (o-assoc *> pmap (proj2 ∘) (pullback (pair f g) (diagonal y)).pbCoh *> inv o-assoc *> pmap (∘ _) beta2) *> pmap (∘ _) beta2)
        \lam h fh=gh => inP (pbMap h (g ∘ h) \box pair-unique
            (inv o-assoc *> pmap (∘ _) beta1 *> fh=gh *> inv id-left *> pmap (∘ _) (inv beta1) *> o-assoc)
            (inv o-assoc *> pmap (∘ _) beta2 *> inv id-left *> pmap (∘ _) (inv beta2) *> o-assoc), pbBeta1)
}

\class CompletePrecat.{u} \extends FinCompletePrecat {
  | limit {J : Precat.{u,u}} (G : Functor J \this) : Limit G
  \default pullback f g => Pullback.fromLimit (limit {_} {Pullback.Shape.FreeCat} (Pullback.diagram f g).functor)
  \default terminal => Product.fromLimit (limit (Product.functor absurd))
  \default Bprod x y => Product.fromLimit (limit (Product.functor (x :: y :: nil)))

  \func product {J : \Type u} (G : J -> Ob) : Product G => Product.fromLimit (limit (Product.functor G))

  \protected \func op : CocompletePrecat.{u} \cowith
    | Precat => Precat.op
    | colimit G => limit $ Functor.op {G}
} \where {
  \func applyEquiv.{u} {D : CompletePrecat.{u}} (E : CatEquiv { | D => D }) {J : Precat.{u,u}} (G : Functor J E.C) : Limit G
    => \have lim : Limit => limit (Comp E.LAdj G)
       \in \new Limit {
        | apex => E.RAdj lim
        | coneMap j => E.eta-iso.hinv ∘ E.RAdj.Func (lim.coneMap j)
        | coneCoh h => rewrite (inv (pmap E.RAdj.Func (lim.coneCoh h)), E.RAdj.Func-o, inv o-assoc, inv o-assoc)
                               (pmap (∘ _) (inv (NatTrans.natural {E.eta.iso-inv E.eta-iso} (G.Func h))))
        | limMap c => E.eta_epsilon-equiv $ lim.limMap (Cone.map E.LAdj c)
        | limBeta c j => o-assoc *> pmap (_ ∘) (inv o-assoc *> pmap (∘ _) (inv E.RAdj.Func-o *> pmap E.RAdj.Func (lim.limBeta (Cone.map E.LAdj c) j)) *> inv (E.eta.natural (coneMap j))) *> inv o-assoc *> pmap (∘ _) E.eta-iso.hinv_f *> id-left
        | limUnique p => (symQEquiv E.eta_epsilon-equiv).isInj $ lim.limUnique \lam j => inv o-assoc *> pmap (∘ _) (inv (E.epsilon.natural _)) *> o-assoc *> pmap (_ ∘) (inv Func-o *> pmap E.LAdj.Func (E.eta-iso.reverse.isMono (inv o-assoc *> p j *> o-assoc)) *> Func-o) *> inv o-assoc *> pmap (∘ _) (E.epsilon.natural _) *> o-assoc
      }
}

\class CompleteCat.{u} \extends CompletePrecat.{u}, Cat {
  \protected \func op : CocompleteCat.{u} \cowith
    | Cat => Cat.op
    | colimit G => limit $ Functor.op {G}
}

\class CocompletePrecat.{u} \extends Precat {
  | colimit {J : Precat.{u,u}} (G : Functor J \this) : Colimit G

  \protected \func op : CompletePrecat.{u} \cowith
    | Precat => Precat.op
    | limit G => colimit $ Functor.op {G}
} \where {
  \func applyEquiv.{u} {D : CocompletePrecat.{u}} (E : CatEquiv { | D => D }) {J : Precat.{u,u}} (G : Functor J E.C) : Colimit G
    => CompletePrecat.applyEquiv {D.op} E.op G.op
}

\class CocompleteCat.{u} \extends CocompletePrecat.{u}, Cat {
  \protected \func op : CompleteCat.{u} \cowith
    | Cat => Cat.op
    | limit G => colimit $ Functor.op {G}
}

\class BicompleteCat.{u} \extends CompleteCat.{u}, CocompleteCat.{u} {
  \protected \func op : BicompleteCat.{u} \cowith
    | Cat => Cat.op
    | limit G => colimit $ Functor.op {G}
    | colimit G => limit $ Functor.op {G}
}

\func PreservesLimit {J C D : Precat} (G : Functor C D) (F : Functor J C)
  => \Pi (c : Cone F) -> IsLimitCone c -> IsLimitCone (Cone.map G c)

\func ReflectsLimit {J C D : Precat} (G : Functor C D) (F : Functor J C)
  => \Pi (c : Cone F) -> IsLimitCone (Cone.map G c) -> IsLimitCone c

\func CreatesLimit {J C D : Precat} (G : Functor C D) (F : Functor J C)
  => Limit (Comp G F) -> \Sigma (Limit F) (PreservesLimit G F) (ReflectsLimit G F)

\lemma Mono_pullback (P : Pullback {}) (m : Mono P.g) : Mono P.pbProj1 \cowith
  | isMono {d} {dP} {dP'} q => P.pbEta q $ m.isMono $ inv o-assoc *> pmap (∘ _) (inv P.pbCoh) *> o-assoc *> pmap (_ ∘) q *> inv o-assoc *> pmap (∘ _) P.pbCoh *> o-assoc

\func IsRegularMono {C : Precat} {x y : C} (f : Hom x y) =>
  TruncP (Equalizer { | D => C | X => y | apex => x | eql => f })

\lemma regularMono_Mono {C : Precat} {x y : C} {f : Hom x y} (reg : IsRegularMono f) : Mono f \elim reg
  | inP E => \new Mono f E.eqMono

\lemma regularMono_pullback (P : Pullback {}) (m : IsRegularMono P.g) : IsRegularMono P.pbProj1 \elim m
  | inP E => inP \new Equalizer {
    | Y => E.Y
    | f => E.f ∘ P.f
    | g => E.g ∘ P.f
    | equal => o-assoc *> pmap (_ ∘) P.pbCoh *> inv o-assoc *> pmap (∘ _) E.equal *> o-assoc *> inv (o-assoc *> pmap (_ ∘) pbCoh)
    | isEqualizer Z => inP \new QEquiv {
      | ret s => P.pbMap s. (E.eqMap (P.f ∘ s.) \box inv o-assoc *> s. *> o-assoc) (inv E.eqBeta)
      | ret_f h => P.pbEta P.pbBeta1 $ P.pbBeta2 *> E.eqMono (E.eqBeta *> inv o-assoc *> pmap (∘ h) P.pbCoh *> o-assoc)
      | f_sec s => ext P.pbBeta1
    }
  }

{- | If both squares are pullbacks, then the outter rectangle is a pullback.
  Q  -->  P  --> P.y
  |       |       |
  |       |       |
  Q.x --> P.x --> P.z
 -}
\func pullback-lemma (P : Pullback {}) (Q : Pullback {P.D} { | y => P | z => P.x | g => P.pbProj1 }) : Pullback (P.f ∘ Q.f) P.g Q Q.pbProj1 (P.pbProj2 ∘ Q.pbProj2) \cowith
  | pbCoh => o-assoc *> pmap (_ ∘) Q.pbCoh *> inv o-assoc *> pmap (∘ _) P.pbCoh *> o-assoc
  | pbMap p1 p2 c => Q.pbMap p1 (P.pbMap (Q.f ∘ p1) p2 $ inv o-assoc *> c) $ inv P.pbBeta1
  | pbBeta1 => Q.pbBeta1
  | pbBeta2 => o-assoc *> pmap (_ ∘) Q.pbBeta2 *> P.pbBeta2
  | pbEta p1 p2 => Q.pbEta p1 $ P.pbEta (inv o-assoc *> rewriteI Q.pbCoh (o-assoc *> pmap (_ ∘) p1 *> inv o-assoc *> pmap (∘ _) Q.pbCoh) *> o-assoc) (inv o-assoc *> p2 *> o-assoc)

{- | If the right square and the outter rectangle are pullbacks, then the left square is a pullback.
  Q  -->  P  --> P.y
  |       |       |
  |       |       |
  Q.x --> P.x --> P.z
 -}
\func pullback-lemma-conv (P : Pullback {}) (Q : Pullback {P.D} { | y => P.y | z => P.z | g => P.g }) (t : Hom Q.x P.x) (fs=Qf : P.f ∘ t = Q.f) : Pullback t P.pbProj1 Q Q.pbProj1 \cowith
  | pbProj2 => P.pbMap (t ∘ Q.pbProj1) Q.pbProj2 (inv o-assoc *> pmap (∘ _) fs=Qf *> Q.pbCoh)
  | pbCoh => inv P.pbBeta1
  | pbMap p1 p2 c => Q.pbMap p1 (P.pbProj2 ∘ p2) $ pmap (∘ p1) (inv fs=Qf) *> o-assoc *> pmap (P.f ∘) c *> inv o-assoc *> pmap (∘ p2) P.pbCoh *> o-assoc
  | pbBeta1 => Q.pbBeta1
  | pbBeta2 {_} {_} {_} {c} => pbEta (inv o-assoc *> rewrite P.pbBeta1 (o-assoc *> pmap (_ ∘) Q.pbBeta1 *> c)) (inv o-assoc *> rewrite P.pbBeta2 Q.pbBeta2)
  | pbEta p1 p2 => Q.pbEta p1 $ rewrite P.pbBeta2 in o-assoc *> pmap (P.pbProj2 ∘) p2 *> inv o-assoc

\lemma splitMono_regular (f : SplitMono {}) : IsRegularMono f.f => inP \new Equalizer {
  | Y => f.cod
  | f => f.f ∘ f.hinv
  | g => id
  | equal => o-assoc *> pmap (_ ∘) f.hinv_f *> id-right *> inv id-left
  | isEqualizer Z => inP \new QEquiv {
    | ret (h,p) => f.hinv ∘ h
    | ret_f h => inv o-assoc *> pmap (∘ h) f.hinv_f *> id-left
    | f_sec (h,p) => ext (inv o-assoc *> p *> id-left)
  }
}

\func isRegularEpi {C : Precat} {x y : C} (f : Hom x y) => IsRegularMono {C.op} f