\import Algebra.Meta
\import Category.Functor
\import Equiv(Equiv, QEquiv, Retraction, transEquiv)
\import Equiv.Path
\import Function.Meta ($)
\import Logic
\import Meta
\import Paths
\import Paths.Meta
\import Set

\plevels obj >= hom

\class Precat (Ob : \hType obj) {
  | Hom : Ob -> Ob -> \Set hom
  | 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 Y ∘ f = f
  | id-right {X Y : Ob} {f : Hom X Y} : f ∘ id X = 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

  \func op : Precat \cowith
    | Ob => Ob
    | Hom x y => Hom y x
    | id x => id x
    | 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
}

\meta SmallPrecat => Precat \lp

\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 dom
  | isMono {_} {g} {h} gf=hf =>
    g               ==< inv id-left >==
    g >> id dom     ==< 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 dom     ==< id-left >==
    h               `qed

  \lemma adjoint {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 cod
  \lemma adjointInv {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 adjoint' {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} : Equiv {Hom cod z} {Hom dom z} (__ ∘ f)
    => \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} : Equiv {Hom z dom} {Hom z cod} (f ∘ __)
    => \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
       }

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

  \func op : Iso => \new Iso {C.op} f hinv f_hinv hinv_f
} \where {
    \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 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 (rewriteEq e3.f_hinv (inv (rewriteEq id-right idp)))

    \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
      => 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 => rewriteEq g.hinv_f (rewriteEq f.hinv_f idp)
      | f_hinv => rewriteEq f.f_hinv (rewriteEq g.f_hinv idp)
}

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

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

  \func op : Cat \cowith
    | Precat => Precat.op
    | univalence => univalenceFromEquiv {Precat.op} (\lam {a} {b} => transEquiv 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
    => univalence.ret e

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

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

  \lemma transport_Hom {x1 y1 x2 y2 : Ob} (p1 : x1 = y1) (p2 : x2 = y2) {g : Hom x1 x2} {f : Hom y1 y2}
                       (h : g >> transport (Hom x2) p2 (id x2) = transport (Hom x1) p1 (id x1) >> f)
    : 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 = transport (Hom x) p (id x) >> f) : 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 : g >> transport (Hom x) p (id x) = f) : transport (Hom z) p g = f \elim p
    | idp => inv id-left *> h


  \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 univalenceFromEquiv {C : Precat} (e : \Pi {a b : C} -> Equiv {a = b} {Iso {C} {a} {b}}) (i : \Pi {a : C} -> Iso.f {e (idpe a)} = id a) {a b : C} : Equiv (idtoiso {C} {a} {b})
    => \let t : e.f = idtoiso {C} {a} {b} => ext (\case \elim b, \elim __ \with {
      | b, idp => Iso.equals _ _ i
    }) \in transport (Equiv __) t e

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

  \lemma transport_Hom_Func {C D E : Precat} {x1 y1 : C} (p1 : x1 = y1) {x2 y2 : D} (p2 : x2 = y2) (F : Functor C E) (G : Functor D E) {g : Hom (F x1) (G x2)} {f : Hom (F y1) (G y2)}
                            (h : transport (Hom (G x2)) (pmap G p2) (id (G x2)) ∘ g = f ∘ transport (Hom (F x1)) (pmap F p1) (id (F x1)))
    : coe (\lam i => Hom (F (p1 @ i)) (G (p2 @ i))) g right = f \elim p1, p2
    | idp, idp => inv id-left *> h *> id-right

  \lemma transport_Hom_Func-right {C D : Precat} {x y : C} (p : x = y) {z : D} (F : Functor C D) {g : Hom z (F x)}
    : transport (Hom z) (pmap F p) g = F.Func (transport (Hom x) p (id x)) ∘ g \elim p
    | idp => inv (pmap (`∘ g) Func-id *> id-left)

  \lemma transport_Hom_Func_iso-right {C : Cat} {D : Precat} (e : Iso {C}) {z : D} (F : Functor C D) {g : Hom z (F e.dom)}
    : transport (Hom z) (pmap F (isotoid e)) g = F.Func e.f ∘ g
    => transport_Hom_Func-right (isotoid e) F *> cong (transport_iso e)

  \lemma transport_Hom_Func_iso {C D : Cat} {E : Precat} (e1 : Iso {C}) (e2 : Iso {D}) (F : Functor C E) (G : Functor D E) {g : Hom (F e1.dom) (G e2.dom)} {f : Hom (F e1.cod) (G e2.cod)}
                                (h : G.Func e2.f ∘ g = f ∘ F.Func e1.f)
    : coe (\lam i => Hom (F (isotoid e1 @ i)) (G (isotoid e2 @ i))) g right = f
    => transport_Hom_Func (isotoid e1) (isotoid e2) F G (pmap (`∘ g) (transport_Hom_Func_iso-right e2 G *> id-right) *> h *> pmap (f ∘) (inv (transport_Hom_Func_iso-right e1 F *> id-right)))
}

\meta SmallCat => Cat \lp

\func DiscretePrecat (X : \Type) : Precat X \cowith
  | Hom x y => Trunc0 (x = y)
  | id x => 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 -> \hType (\suc \lp)) (isHom : \Pi {x y : C} -> Str x -> Str y -> Hom x y -> \hType (\suc \lp))
           (st : \Pi {X : C} {S1 S2 : Str X} -> isHom S1 S2 (id X) -> isHom S2 S1 (id X) -> 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 X) = e)
  => \case \elim Y, \elim e, \elim S2, p, q, Cat.univalenceToTransport e \with {
    | Y, e : Iso, S2, p, q, (idp,s) => (idp, st (transportInv (isHom S1 S2) s p) (transport (isHom S2 S1) (inv id-right *> pmap (∘ e.hinv) s *> e.hinv_f) q), s)
  }

\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 x => 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 => Graph.FreeCat {\new Graph (\Sigma) (\lam _ _ => Empty)}