\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 8 o \alias \infixl 8 ∘ {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 8 >> {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).1
| 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).1 *> (c e).2)
})

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