\import Equiv
\import Equiv.Path
\import Function.Meta ($)
\import Logic
\import Meta
\import Paths
\import Paths.Meta
\import Set

\class Precat (Ob : \Type) {
  | Hom : Ob -> Ob -> \Set
  | id {X : Ob} : Hom X X
  | \fixl  o \alias \infixl  ∘ {X Y Z : Ob} : Hom Y Z -> Hom X Y -> Hom X Z
  | id-left {X Y : Ob} {f : Hom X Y} : id ∘ f = f
  | id-right {X Y : Ob} {f : Hom X Y} : f ∘ id = f
  | o-assoc {X Y Z W : Ob} {h : Hom Z W} {g : Hom Y Z} {f : Hom X Y} : (h ∘ g) ∘ f = h ∘ (g ∘ f)

  \func \infixl  >> {x y z : Ob} (f : Hom x y) (g : Hom y z) => g ∘ f

  \protected \func op : Precat \cowith
    | Ob => Ob
    | Hom x y => Hom y x
    | id => id
    | o g f => o f g
    | id-left => id-right
    | id-right => id-left
    | o-assoc => inv o-assoc

  \func idtoiso {a b : Ob} (p : a = b) : Iso {_} {a} {b} \elim p
    | idp => idIso

  \func =_hom {a b : Ob} (p : a = b) : Hom a b
    => (idtoiso p).f

  \lemma transport_Hom {x1 y1 x2 y2 : Ob} (p1 : x1 = y1) (p2 : x2 = y2) {g : Hom x1 x2} {f : Hom y1 y2}
                       (h : transport (Hom x2) p2 id ∘ g = f ∘ transport (Hom x1) p1 id)
    : coe (\lam i => Hom (p1 @ i) (p2 @ i)) g right = f \elim p1, p2
    | idp, idp => inv id-left *> h *> id-right

  \lemma transport_Hom-left {x y z : Ob} (p : x = y) {g : Hom x z} {f : Hom y z} (h : g = f ∘ transport (Hom x) p id) : transport (Hom __ z) p g = f \elim p
    | idp => h *> id-right

  \lemma transport_Hom-right {x y z : Ob} (p : x = y) {g : Hom z x} {f : Hom z y} (h : transport (Hom x) p id ∘ g = f) : transport (Hom z) p g = f \elim p
    | idp => inv id-left *> h
}

\open Precat (>>)

\record Map {C : Precat} {dom cod : C} (\coerce f : Hom dom cod)

\record Mono \extends Map
  | isMono {x : C} {g h : Hom x dom} : f ∘ g = f ∘ h -> g = h
  \where {
    \func comp {C : Precat} {x y z : C} (g : Mono {C} {y} {z}) (f : Mono {C} {x} {y}) : Mono {C} {x} {z} (g.f ∘ f) \cowith
      | isMono p => f.isMono (g.isMono (inv o-assoc *> p *> o-assoc))
  }

\func IsEpi {C : Precat} {x y : C} (f : Hom x y) => \Pi {z : C} {g h : Hom y z} -> g ∘ f = h ∘ f -> g = h

\record SplitMono \extends Mono {
  | hinv : Hom cod dom
  | hinv_f : hinv ∘ f = id
  | isMono {_} {g} {h} gf=hf =>
    g               ==< inv id-left >==
    g >> id         ==< pmap (g >>) (inv hinv_f) >==
    g >> (f >> hinv) ==< o-assoc >==
    (g >> f) >> hinv ==< pmap (o hinv) gf=hf >==
    (h >> f) >> hinv ==< inv o-assoc >==
    h >> (f >> hinv) ==< pmap (h >>) hinv_f >==
    h >> id         ==< id-left >==
    h               `qed

  \lemma adjointMap {z : C} {g : Hom z dom} {h : Hom z cod} (p : f ∘ g = h) : g = hinv ∘ h
    => inv id-left *> pmap (∘ g) (inv hinv_f) *> o-assoc *> pmap (hinv ∘) p
}

\record Iso \extends SplitMono {
  | f_hinv : f ∘ hinv = id

  \lemma adjointMapInv {z : C} {g : Hom z dom} {h : Hom z cod} (p : g = hinv ∘ h) : f ∘ g = h
    => pmap (f ∘) p *> inv o-assoc *> pmap (∘ h) f_hinv *> id-left

  \lemma adjointMap' {z : C} {g : Hom cod z} {h : Hom dom z} (p : g ∘ f = h) : g = h ∘ hinv
    => inv id-right *> pmap (g ∘) (inv f_hinv) *> inv o-assoc *> pmap (∘ hinv) p

  \lemma -o_Equiv {z : C} : IsEquiv {Hom cod z} {Hom dom z} (__ ∘ f)
    => inP \new QEquiv {
         | ret h => h ∘ hinv
         | ret_f h => o-assoc *> pmap (h ∘) f_hinv *> id-right
         | f_sec h => o-assoc *> pmap (h ∘) hinv_f *> id-right
       }

  \lemma o-_Equiv {z : C} : IsEquiv {Hom z dom} {Hom z cod} (f ∘ __)
    => inP \new QEquiv {
         | ret h => hinv ∘ h
         | ret_f h => inv o-assoc *> pmap (∘ _) hinv_f *> id-left
         | f_sec h => inv o-assoc *> pmap (∘ _) f_hinv *> id-left
       }

  \protected \func reverse : Iso => \new Iso hinv f f_hinv hinv_f

  \protected \func op : Iso => \new Iso {C.op} f hinv f_hinv hinv_f
} \where {
    \use \func equals {C : Precat} {x y : C} (e e' : Iso {C} {x} {y}) (p : e.f = e'.f) : e = e'
      => ext (p, isMono {e} (e.f_hinv *> inv e'.f_hinv *> inv (pmap (e'.hinv >>) p)))

    \use \level levelProp {C : Precat} {x y : C} (f : Hom x y) (e e' : Iso f) => equals e e' idp

    \lemma hinv-unique {C : Precat} {x y : C} (e : SplitMono {C} {x} {y}) (e' : Iso {C} {x} {y}) (p : e.f = e'.f) : e.hinv = e'.hinv
      => inv (o-assoc *> pmap (_ ∘) (pmap (∘ _) p *> e'.f_hinv) *> id-right) *> pmap (∘ _) e.hinv_f *> id-left

    \lemma rightFactor {C : Precat} {x y z : C} (f : Hom x y) (e2 : Mono {C} {y} {z}) (e3 : Iso (e2.f ∘ f)) : Iso f \cowith
      | hinv => e3.hinv ∘ e2
      | hinv_f => o-assoc *> e3.hinv_f
      | f_hinv => e2.isMono $ inv o-assoc *> inv o-assoc *> pmap (∘ _) e3.f_hinv *> id-left *> inv id-right

    \lemma leftFactor {C : Precat} {x y z : C} {f : Hom x y} (e : IsEpi f) (g : Hom y z) (e3 : Iso (g ∘ f)) : Iso g
      => Iso.op {rightFactor {C.op} g (\new Mono f e) e3.op}

    \lemma composite {C : Precat} {x y z : C} (f : Iso {C} {x} {y}) (g : Iso {C} {y} {z}) : Iso (g.f ∘ f.f) \cowith
      | hinv => f.hinv ∘ g.hinv
      | hinv_f => o-assoc *> pmap (_ ∘) (inv o-assoc *> pmap (∘ _) g.hinv_f *> id-left) *> f.hinv_f
      | f_hinv => o-assoc *> pmap (_ ∘) (inv o-assoc *> pmap (∘ _) f.f_hinv *> id-left) *> g.f_hinv
}

\func idIso {C : Precat} {x : C} : Iso (id {_} {x}) \cowith
  | hinv => id
  | f_hinv => id-left
  | hinv_f => id-right

\func oIso {C : Precat} {x y z : C} (e : Iso {C} {x} {y}) (f : Iso {C} {y} {z}) : Iso {C} {x} {z} \cowith
  | f => f.f ∘ e.f
  | hinv => e.hinv ∘ f.hinv
  | f_hinv => o-assoc *> pmap (_ ∘) (inv o-assoc *> pmap (∘ _) e.f_hinv *> id-left) *> f.f_hinv
  | hinv_f => o-assoc *> pmap (_ ∘) (inv o-assoc *> pmap (∘ _) f.hinv_f *> id-left) *> e.hinv_f

\class Cat \extends Precat {
  | univalence {a b : Ob} : IsEquiv (idtoiso {_} {a} {b})

  \protected \func op : Cat \cowith
    | Precat => Precat.op
    | univalence => univalenceFromQEquiv {Precat.op} (\lam {a} {b} => transQEquiv (IsEquiv.toQEquiv univalence) $ later \new QEquiv {
      | f (e : Iso) => e.op.reverse
      | ret (e : Iso) => e.op.reverse
      | ret_f => idpe
      | f_sec => idpe
    }) (\lam {c} => idp)

  \func isotoid {a b : Ob} (e : Iso {\this} {a} {b}) : a = b
    => IsEquiv.ret univalence e

  \lemma idtoiso_isotoid {a b : Ob} {e : Iso {\this} {a} {b}} : (idtoiso (isotoid e)).f = e.f
    => path \lam i => (IsEquiv.f_ret univalence i).f

  \lemma transport_iso (e : Iso {\this}) : transport (Hom e.dom) (isotoid e) id = e
    => Jl (\lam b p => transport (Hom e.dom) p id = idtoiso p) idp (isotoid e) *> path (\lam i => (IsEquiv.f_ret univalence i).f)

  \func univalenceToTransport (e : Iso {\this}) : \Sigma (p : e.dom = e.cod) (transport (Hom e.dom) p id = e)
    => (isotoid e, transport_iso e)


  \lemma transport_Hom_iso (e1 e2 : Iso {\this}) {g : Hom e1.dom e2.dom} {f : Hom e1.cod e2.cod}
                           (h : g >> e2.f = e1.f >> f)
    : coe (\lam i => Hom (isotoid e1 @ i) (isotoid e2 @ i)) g right = f
    => transport_Hom (isotoid e1) (isotoid e2) (pmap (g >>) (transport_iso e2) *> h *> pmap (>> f) (inv (transport_iso e1)))

  \lemma transport_Hom_iso-left (e : Iso {\this}) {z : Ob} (g : Hom e.dom z) {f : Hom e.cod z} (h : g = e.f >> f) : transport (Hom __ z) (isotoid e) g = f
    => transport_Hom-left (isotoid e) (h *> pmap (>> f) (inv (transport_iso e)))

  \lemma transport_Hom_iso-right (e : Iso {\this}) {z : Ob} (g : Hom z e.dom) {f : Hom z e.cod} (h : g >> e.f = f) : transport (Hom z) (isotoid e) g = f
    => transport_Hom-right (isotoid e) (pmap (g >>) (transport_iso e) *> h)
} \where {
  \lemma univalenceFromQEquiv {C : Precat} (e : \Pi {a b : C} -> QEquiv {a = b} {Iso {C} {a} {b}}) (i : \Pi {a : C} -> (e (idpe a)).f = id) {a b : C} : IsEquiv (C.idtoiso {a} {b})
    => \have t : e.f = C.idtoiso {a} {b} => ext (\case \elim b, \elim __ \with {
      | b, idp => Iso.equals _ _ i
    }) \in transport (IsEquiv __) t (inP e)

  \lemma makeUnivalence {C : Precat} (c : \Pi (e : Iso {C}) -> \Sigma (p : e.dom = e.cod) (transport (Hom e.dom) p id = e)) {a b : C} : IsEquiv (C.idtoiso {a} {b})
    => inP $ pathEquiv (\lam a b => Iso {C} {a} {b}) (\lam {a} {b} => \new Retraction {
      | f => C.idtoiso
      | sec e => (c e).
      | f_sec (e : Iso) => Iso.equals _ _ (Jl (\lam b p => C.=_hom p = transport (Hom e.dom) p id) idp (c e). *> (c e).)
    })

  \lemma makeUnivalenceFromPath {C : Precat} (c : \Pi (e : Iso {C}) -> \Sigma (p : e.dom = e.cod) (Path (\lam i => Hom e.dom (p i)) id e)) {a b : C} : IsEquiv (C.idtoiso {a} {b})
    => makeUnivalence \lam e => ((c e)., pathOver.conv (c e).)
}

\func DiscretePrecat (X : \Type) : Precat X \cowith
  | Hom x y => Trunc0 (x = y)
  | id => in0 idp
  | o {x y z : X} (t : Trunc0 (y = z)) (s : Trunc0 (x = y)) : Trunc0 (x = z) \elim t, s {
    | in0 y=z, in0 x=y => in0 (x=y *> y=z)
  }
  | id-left {_} {_} {p} => cases p idp
  | id-right {_} {_} {p} => cases p (pmap in0 (idp_*> _))
  | o-assoc {_} {_} {_} {_} {p} {q} {r} => cases (p,q,r) (pmap in0 (inv (*>-assoc _ _ _)))
  \where {
    \func map {X : \Type} {D : Precat} (f : X -> D) {x y : X} (h : Hom {DiscretePrecat X} x y) : Hom (f x) (f y) \elim h
      | in0 idp => id
  }

\sfunc SIP (C : Cat) (Str : C -> \Type) (isHom : \Pi {x y : C} -> Str x -> Str y -> Hom x y -> \Type)
           (st : \Pi {x : C} {S1 S2 : Str x} -> isHom S1 S2 id -> isHom S2 S1 id -> S1 = S2)
           {x y : C} (e : Iso {C} {x} {y}) (S1 : Str x) (S2 : Str y) (p : isHom S1 S2 e) (q : isHom S2 S1 e.hinv)
  : \Sigma (p : x = y) (Path (\lam i => Str (p i)) S1 S2) (transport (Hom x) p id = e)
  => \case \elim y, \elim e, \elim S2, p, q, Cat.univalenceToTransport e \with {
    | y, (_,g,gf,fg), S2, p, q, (idp,idp) => (idp, st p $ transport (isHom S2 S1) (inv id-right *> gf) q, idp)
  }

\sfunc SIP-gen (C : Cat)
  (Str : C -> \Type) (dHom : \Pi {x y : C} -> Str x -> Str y -> Hom x y -> \Type) (dHom_id : \Pi {x : C} {S : Str x} -> dHom S S id)
  (isIso : \Pi {x y : C} {S1 : Str x} {S2 : Str y} {f : Hom x y} -> dHom S1 S2 f -> \Type)
  (st : \Pi {x : C} {S1 S2 : Str x} {f : dHom S1 S2 id} -> isIso f -> \Sigma (p : S1 = S2) (Path (\lam i => dHom S1 (p i) id) dHom_id f))
  {x y : C} (e : Iso {C} {x} {y}) (S1 : Str x) (S2 : Str y) (p : dHom S1 S2 e) (pi : isIso p)
  : \Sigma (r1 : x = y) (r2 : Path (\lam i => Str (r1 i)) S1 S2) (r3 : Path (\lam i => Hom x (r1 i)) id e) (Path (\lam i => dHom S1 (r2 i) (r3 i)) dHom_id p)
  => \case \elim y, \elim e, \elim S2, \elim p, \elim pi, Cat.univalenceToTransport e \with {
    | y, (_,g,g=id,_), S2, p, pi, (idp,idp) => (idp, (st pi)., idp, (st pi).)
  }

\sfunc SIP-comb (C : Cat) (D : C -> Cat)
  (Str : C -> \Type) (dHom : \Pi {x y : C} -> Str x -> Str y -> Hom x y -> \Type)
  (isIso : \Pi {x y : C} {S1 : Str x} {S2 : Str y} {f : Hom x y} -> dHom S1 S2 f -> \Type)
  (dHom_id : \Pi {x : C} {S : Str x} -> dHom S S id) (dHom_idIso : \Pi {x : C} {S : Str x} -> isIso (dHom_id {x} {S}))
  (do : \Pi {x : C} -> Embedding {Str x} {D x}) (dh : \Pi {x : C} {S1 S2 : Str x} (f : dHom S1 S2 id) (fi : isIso f) -> Iso {D x} {do S1} {do S2})
  (dh_id : \Pi {x : C} {S : Str x} -> (dh (dHom_id {x} {S}) dHom_idIso).f = id)
  (dhi : \Pi {x : C} {S1 S2 : Str x} (f g : dHom S1 S2 id) (fi : isIso f) (gi : isIso g) -> (dh f fi).f = (dh g gi).f -> f = g)
  {x y : C} (e : Iso {C} {x} {y}) (S1 : Str x) (S2 : Str y) (p : dHom S1 S2 e) (pi : isIso p)
  : \Sigma (r1 : x = y) (r2 : Path (\lam i => Str (r1 i)) S1 S2) (r3 : Path (\lam i => Hom x (r1 i)) id e) (Path (\lam i => dHom S1 (r2 i) (r3 i)) dHom_id p)
  => SIP-gen C Str dHom dHom_id isIso (\lam {x} {S1} fi =>
    \let | S1=S2 => do.pmap-isEquiv.ret $ Cat.isotoid (dh _ fi)
         | g {S : Str x} (p : S1 = S) => transport (dHom S1 __ id) p dHom_id
         | gi {S : Str x} (p : S1 = S) => Jl (\lam S S1=S => isIso (g S1=S)) dHom_idIso p
    \in (S1=S2, pathOver $ dhi (g S1=S2) _ (gi S1=S2) fi $ Jl (\lam S p => (dh (g p) (gi p)).f = transport (Hom (do S1)) (do.pmap-isEquiv p) id) dh_id S1=S2 *>
                  pmap (transport (Hom _) __ _) (do.pmap-isEquiv.f_ret _) *> Cat.transport_iso _)) e S1 S2 p pi

\class Graph (\coerce V : \Set) (E : V -> V -> \Set) {
  \data Paths (x y : V)
    | empty (x = y)
    | cons {z : V} (E x z) (Paths z y)

  \func concat {x y z : V} (p : Paths x y) (q : Paths y z) : Paths x z \elim p
    | empty idp => q
    | cons e p => cons e (concat p q)

  \lemma concat_idp {x y : V} {p : Paths x y} : concat p (empty idp) = p \elim p
    | empty idp => idp
    | cons e p => pmap (cons e) concat_idp

  \lemma concat-assoc {x y z w : V} {p : Paths x y} {q : Paths y z} {r : Paths z w} : concat (concat p q) r = concat p (concat q r) \elim p
    | empty idp => idp
    | cons e p => pmap (cons e) concat-assoc

  \func FreeCat : Cat V \cowith
    | Hom => Paths
    | id => empty idp
    | o q p => concat p q
    | id-left => concat_idp
    | id-right => idp
    | o-assoc => inv concat-assoc
    | univalence => Cat.makeUnivalence $ later \case \elim __ \with {
      | (x, y, empty idp, _, _, _) => (idp,idp)
      | (x, y, cons e p, _, (), _)
    }
}

\func TrivialCat : Cat => (\new Graph (\Sigma) (\lam _ _ => Empty)).FreeCat