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

\class Cone {J : SmallPrecat} {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 : SmallPrecat} {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' : SmallPrecat} (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 : SmallPrecat} {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)

\class Limit \extends Cone {
  | isLimit (z : D) : Equiv (conePullback \this z)
  | 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
    => Equiv.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 {Equiv.f_ret {isLimit z} c @ i} j)

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

  \default isLimit z => \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 : SmallPrecat} {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 : SmallPrecat} {D : Precat} {G : Functor J D} (c : Cone G) (L : Limit G) (e : Iso (L.limMap c)) : Limit { | Cone => c } \cowith
    | limMap c' => e.inv ∘ limMap c'
    | limBeta c' j => pmap (`∘ _) (inv (L.limBeta c j)) *> rewriteEq e.f_inv (rewriteEq (L.limBeta c' j) idp)
    | 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 : SmallPrecat} {D : Precat} {G : Functor J D} (L L' : Limit G) : Iso (L.limMap L') \cowith
    | inv => L'.limMap L
    | inv_f => limUnique $ \lam j => inv o-assoc *> pmap (`∘ _) (L'.limBeta L j) *> L.limBeta L' j *> inv id-right
    | f_inv => 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 (\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)) {
  \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 (F x)
      | 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 : G.FreeCat) -> Hom apex (D.functor j)) (p : \Pi {g g' : G} (e : G.E g g') -> Func e ∘ coneMap g = coneMap g') {j j' : D.G.FreeCat} (h : 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 (`o 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 : Cone) => \new DiagramCone {
        | coneMap => c.coneMap
        | diagramCoh e => rewriteF id-left (c.coneCoh (Graph.cons e (Graph.empty idp)))
      }
      | ret_f d => idp
      | f_sec c => idp
  }

\class LimitDiagram \extends DiagramCone, Limit
  | isLimitDiagram (Z : D) : Equiv (DiagramCone.pullback Z)
  | isLimit Z => transEquiv (isLimitDiagram Z) (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) : Equiv (\lam (h : Hom Z apex) => proj __ ∘ h) => \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)

  \func toLimit : Limit {DiscretePrecat J} {D} \cowith
    | G => functor G
    | apex => apex
    | coneMap => proj
    | coneCoh {j} {j'} (in0 idp) => id-left
    | isLimit Z => transEquiv {_} {_} {Cone (functor G) Z} (isProduct Z) (\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 (Equiv.ret_f {L.isLimit z} h1) *> pmap (Equiv.ret {L.isLimit z}) (exts f) *> Equiv.ret_f {L.isLimit z} h2
    \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) : Equiv {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
    => Equiv.ret {isEqualizer Z} (h,p)

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

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

  \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 => transEquiv {_} {_} {Cone (functor f g) Z} (isEqualizer Z) (\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 (Equiv __) (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 X
    | true, true, id_true => id Y

  \func Shape : Precat Bool \cowith
    | Hom => Arrows
    | id (x : Bool) : Arrows x x \with {
      | 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 => \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 => eqMap eql equal
    | inv => eqMap eql equal
    | inv_f => eqMono $ rewriteEq (E.eqBeta E'.eql equal) (eqBeta _ _ *> inv id-right)
    | f_inv => eqMono $ rewriteEq (E'.eqBeta E.eql equal) (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
    => eqBeta eql equal

  \lemma mono=>equalizer {D : Precat} {x y e : D} {f g : Hom x y} {eql : Hom e x} (equal : f ∘ eql = g ∘ eql)
                         (m : Mono eql) (p : \Pi {z : D} (h : Hom z x) -> f ∘ h = g ∘ h -> ∃ (k : Hom z e) (eql ∘ k = h))
    : \Pi (z : D) -> Equiv {Hom z e} {\Sigma (h : Hom z x) (f ∘ h = g ∘ h)} (\lam h => (eql ∘ h, inv o-assoc *> pmap (`∘ h) equal *> o-assoc))
    => \lam z => \new ESEquiv {
      | isSurj t => TruncP.map (p t. t.) (\lam q => (q., ext q.))
      | Embedding => Embedding.fromInjection (\lam q => m.isMono $ pmap __. q)
    }
}

\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

  \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 => \new QEquiv {
      | ret (c : DiagramCone) => 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 => \new Graph (Fin ) $ \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 \elim __ \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.functor {diagram f g})) : Pullback f g L.apex
    => \let | d : DiagramCone => Equiv.ret {DiagramCone.equiv {diagram f g} L.apex} 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 (Equiv.ret_f {L.isLimit w} h1) *> pmap (Equiv.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 {} {} ())
         }) *> Equiv.ret_f {L.isLimit w} h2
      }

  \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 => rewriteEq pbCoh o-assoc
    | pbMap p1 p2 c => e.inv ∘ pbMap p1 p2 c
    | pbBeta1 => rewriteEq e.f_inv $ rewrite id-right pbBeta1
    | pbBeta2 => rewriteEq e.f_inv $ rewrite id-right pbBeta2
    | pbEta s1 s2 => e.isMono $ pbEta (rewriteEq s1 o-assoc) (rewriteEq s2 o-assoc)
}

\func limits<=pr+eq {D : Precat}
  (pr : \Pi (J : \hType) (G : J -> D) -> Product G)
  (eq : \Pi {X Y : D} (f g : Hom X Y) -> Equalizer f g)
  {J : SmallPrecat} (G : Functor J D) : Limit G
  => \have | X : Product => pr J G
           | Y : Product => pr (\Sigma (j j' : J) (Hom j j')) (\lam t => G t.)
           | eql : Equalizer => 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 => \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) =>
  \let | F (t : SlicePrecat y) : SlicePrecat x => (pullback f t., map t.)
       | Func {a} {b} (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)
  \in \new Functor {
    | F => F
    | Func => Func
    | 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)
  } \where
  \func map {z : C} (g : Hom z y) : Hom (pullback f g) x
    => pbProj1 {pullback f g}

\class CartesianPrecat \extends Precat {
  | terminal : Product {Empty} {\this} absurd
  | Bprod (x y : Ob) : Product (x :: y :: nil)

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

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

  \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 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
    => tupleBeta {Bprod x y}

  \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 (rewriteEq (beta1 g h) $ inv (beta1 _ _)) (rewriteEq (beta2 g h) $ inv (beta2 _ _))

  \lemma pair-proj {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 x) (id x)
    \where
      \lemma isSplitMono (x : Ob) : SplitMono (diagonal x) proj1 \cowith
        | inv_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
    | inv => pair (pair proj1 (proj1 ∘ proj2)) (proj2 ∘ proj2)
    | inv_f => rewrite (pair-comp,pair-comp,beta1,o-assoc,beta2,beta1,o-assoc,beta2,beta2,inv pair-comp,pair-proj,id-left) pair-proj
    | f_inv => rewrite (pair-comp,o-assoc,beta1,beta1,pair-comp,beta2,o-assoc,beta1,beta2,inv pair-comp,pair-proj,id-left) pair-proj
}

\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 )
  }
}

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

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

  \func equalizer {x y : Ob} (f g : Hom x y) : Equalizer f g
    => Equalizer.fromLimit (limit (Equalizer.functor f g))

  \func op : CocompletePrecat \cowith
    | Precat => Precat.op
    | colimit (G : Functor) => limit G.op
} \where {
  \func applyEquiv {C : CompletePrecat} (E : CatEquiv C) {J : SmallPrecat} (G : Functor J E.D) : Limit G
    => \have lim : Limit => limit (Comp E.LAdj G)
       \in \new Limit {
        | apex => E lim
        | coneMap j => E.eta-iso.inv ∘ E.Func (lim.coneMap j)
        | coneCoh h => rewrite (inv (pmap E.Func (lim.coneCoh h)), Func-o, inv o-assoc, inv o-assoc)
                               (pmap (`∘ _) (inv (NatTrans.natural {E.eta.iso E.eta-iso} (G.Func h))))
        | limMap c => E.isAdjoint $ lim.limMap (Cone.map E.LAdj c)
        | limBeta c j => o-assoc *> pmap (_ ∘) (inv o-assoc *> pmap (`∘ _) (inv E.Func-o *> pmap E.Func (lim.limBeta (Cone.map E.LAdj c) j)) *> inv (E.eta.natural (coneMap j))) *> inv o-assoc *> pmap (`∘ _) E.eta-iso.inv_f *> id-left
        | limUnique p => Equiv.isInj {symQEquiv E.eta_eps_equiv} $ 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 \extends CompletePrecat, Cat {
  \func op : CocompleteCat \cowith
    | Cat => Cat.op
    | colimit (G : Functor) => limit G.op
}

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

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

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

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

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

\func ReflectsLimit {J C D : Precat} (G : Functor C D) (F : Functor J C)
  => \Pi (c : Cone F) -> Limit { | Cone => Cone.map G c } -> Limit { | Cone => 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)

\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 : Equalizer) => \new Mono f E.eqMono

\lemma regularMono_pullback (P : Pullback {}) (m : isRegularMono P.g) : isRegularMono P.pbProj1
  => {?}

{- | 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 => rewriteEq (Q.pbCoh,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 => rewriteEq Q.pbBeta2 P.pbBeta2
  | pbEta p1 p2 => Q.pbEta p1 $ P.pbEta (inv o-assoc *> rewriteI Q.pbCoh (rewriteEq 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 (rewriteEq Q.pbBeta1 c)) (inv o-assoc *> rewrite P.pbBeta2 Q.pbBeta2)
  | pbEta p1 p2 => Q.pbEta p1 $ rewriteF P.pbBeta2 $ 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.inv
    | g => id f.cod
    | equal => rewriteEq f.inv_f (id-right *> inv id-left)
    | isEqualizer Z => \new QEquiv {
      | ret (h,p) => f.inv ∘ h
      | ret_f h => rewriteEq f.inv_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