\import Category
\import Category.Adjoint
\import Category.Functor
\import Category.Product
\import Category.Slice
\import Data.Bool
\import Equiv
\import Function.Meta
\import HLevel
\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
  => 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.hinv ∘ limMap c'
    | limBeta c' j => pmap (`∘ _) (inv (L.limBeta c j)) *> rewriteEq e.f_hinv (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
    | 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 (\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 => 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) : 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 (ret_f {L.isLimit z} h1) *> pmap (ret {L.isLimit z}) (exts f) *> 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 => 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 (ret_f {isEqualizer Z} h1) *> pmap ret (ext p) *> 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
    | hinv => eqMap eql equal
    | hinv_f => eqMono $ rewriteEq (E.eqBeta E'.eql equal) (eqBeta _ _ *> inv id-right)
    | f_hinv => 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 {
      | isSurjMap t => TruncP.map (p t. t.) (\lam q => (q., ext q.))
      | Embedding => Embedding.fromInjection (\lam q => m.isMono $ pmap __. q)
    }

  \func id-equalizer {D : Precat} {X Y : D} {f : Hom X Y} : Equalizer f f X (id X)\cowith
    | equal => idp
    | isEqualizer _ => \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 $ eqMono $ rewriteI o-assoc $ rewrite (eqBeta {eq} _ _, 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

  \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 __ \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 => 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 (ret_f {L.isLimit w} h1) *> pmap (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 {} {} ())
         }) *> 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.hinv ∘ pbMap p1 p2 c
    | pbBeta1 => rewriteEq e.f_hinv $ rewrite id-right pbBeta1
    | pbBeta2 => rewriteEq e.f_hinv $ rewrite id-right pbBeta2
    | pbEta s1 s2 => e.isMono $ pbEta (rewriteEq s1 o-assoc) (rewriteEq 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 P => pbEta {P} {P} {(p-map P' P) ∘ (p-map P P')} {id P}
          (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 {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}

\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 terminal-ind {C : Precat} (a : C) (e : \Pi (b : C) -> Contr (Hom b a))
  : terminal-obj C
  \cowith
    | apex => a
    | 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.univalence.ret (unfold $ terminal-obj-iso a a'), \lam j => absurd j, \lam {Z} f => terminal-unique')

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

\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 ∘ f) (g' ∘ f') = prodMap g g' ∘ prodMap f f' => 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 y') ∘ prodMap (id x) g
    => rewriteI (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 ∘ f) = prodMap (id w) g ∘ prodMap (id w) f => rewriteI {} id-left $ prodMap-comp _ _ _ _

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

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

  \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
        | 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-proj,id-left) pair-proj
    | f_hinv => rewrite (pair-comp,o-assoc,beta1,beta1,pair-comp,beta2,o-assoc,beta1,beta2,inv pair-comp,pair-proj,id-left) pair-proj

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

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

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

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

  \lemma change-inv {x y : Ob} : change ∘ change = 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 change-prod {x y x' y' : Ob} {f : Hom x x'} {g : Hom y y'} : change ∘ prodMap f g = prodMap g f ∘ change =>
    pair-unique (rewrite (inv o-assoc, beta1 _ _, beta2 _ _, inv o-assoc, beta1 _ _, o-assoc, beta1 _ _) idp)
        (rewrite (inv o-assoc, beta2 _ _, beta1 _ _, inv o-assoc, beta2 _ _, o-assoc, beta2 _ _) idp)

  \func bprod-comm {x y : Ob} : Iso (change {_} {x} {y})\cowith
    | hinv => change {_} {y} {x}
    | hinv_f => change-inv {_} {x} {y}
    | f_hinv => change-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 {_} {_} {_} {g} {f} => prodMap-comp f. g. f. g.
}

\class CartesianPrecat \extends PrecatWithTerminal, PrecatWithBprod {
  \func terminal-prod-left {X : Ob} : Iso {\this} {X} {Bprod terminal X}  \cowith
    | f => pair terminalMap (id X)
    | 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 )
  }
}

\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.hinv ∘ 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.hinv_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 $ 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 f.cod
  | equal => rewriteEq f.hinv_f (id-right *> inv id-left)
  | isEqualizer Z => \new QEquiv {
    | ret (h,p) => f.hinv ∘ h
    | ret_f h => rewriteEq 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