\import Category
\import Category.Functor
\import Equiv (Equiv, QEquiv, sigmaEquiv, transEquiv)
\import Equiv.Sigma
\import Function.Meta
\import Logic
\import Meta
\import Paths
\import Paths.Meta

\class DPrecat {C : Precat} (DOb : C -> \hType obj)
  | DHom {a b : C} : Hom a b -> DOb a -> DOb b -> \Set hom
  | id^ {a : C} (x : DOb a) : DHom (id a) x x
  | \fixl  o^ \alias \infixl  ∘^ {a b c : C} {g : Hom b c} {f : Hom a b} {x : DOb a} {y : DOb b} {z : DOb c} : DHom g y z -> DHom f x y -> DHom (g ∘ f) x z
  | id^-left {a b : C} {f : Hom a b} {x : DOb a} {y : DOb b} {f^ : DHom f x y} : transport (DHom __ x y) id-left (id^ y ∘^ f^) = f^
  | id^-right {a b : C} {f : Hom a b} {x : DOb a} {y : DOb b} {f^ : DHom f x y} : transport (DHom __ x y) id-right (f^ ∘^ id^ x) = f^
  | o^-assoc {a b c d : C} {h : Hom c d} {g : Hom b c} {f : Hom a b} {x : DOb a} {y : DOb b} {z : DOb c} {w : DOb d} {h^ : DHom h z w} {g^ : DHom g y z} {f^ : DHom f x y} : transport (DHom __ x w) o-assoc ((h^ ∘^ g^) ∘^ f^) = h^ ∘^ (g^ ∘^ f^)

\record DIso {D : DPrecat {}} (e : Iso {D.C}) {dom : D e.dom} {cod : D e.cod} (\coerce f : DHom e.f dom cod)
  | inv^ : DHom e.hinv cod dom
  | inv^-left : transport (DHom __ dom dom) e.hinv_f (inv^ ∘^ f) = id^ dom
  | inv^-right : transport (DHom __ cod cod) e.f_hinv (f ∘^ inv^) = id^ cod

\func idIso^ {D : DPrecat {}} {a : D.C} {x : D a} : DIso idIso {x} {x} \cowith
  | f => id^ x
  | inv^ => id^ x
  | inv^-left => rewrite (prop-isProp idIso.hinv_f id-left) id^-left
  | inv^-right => rewrite (prop-isProp idIso.hinv_f id-right) id^-right

\func totalPrecat (D : DPrecat {}) : Precat \cowith
  | Ob => \Sigma (a : D.C) (D a)
  | Hom (a,x) (b,y) => \Sigma (f : Hom a b) (DHom f x y)
  | id (a,x) => (id a, id^ x)
  | o (g,g^) (f,f^) => (g ∘ f, g^ ∘^ f^)
  | id-left => ext (id-left, id^-left)
  | id-right => ext (id-right, id^-right)
  | o-assoc => ext (o-assoc, o^-assoc)
  \where {
    \func proj : Functor (totalPrecat D) D.C \cowith
      | F x => x.
      | Func f => f.
      | Func-id => idp
      | Func-o => idp
  }

\class DCat \extends DPrecat
  | univalence^ {a : C} {x y : DOb a} : Equiv {x = y} {DIso idIso {x} {y}} idtoiso^
  \where {
    \func idtoiso^ {D : DPrecat {}} {a : D.C} {x y : DOb a} (q : x = y) : DIso idIso {x} {y} \elim q
      | idp => idIso^

    \func totalCat (D : DCat {}) (C-uni : \Pi {a b : D.C} -> Equiv (Precat.idtoiso {_} {a} {b})) : Cat \cowith
      | Precat => totalPrecat D
      | univalence => Cat.univalenceFromEquiv (later \lam {t} {s} => transEquiv (sigmaEquiv DOb t s) $ transEquiv (sigma-right eq-over) $ transEquiv (sigma-left {_} {_} {\lam e => DIso e {t.} {s.}} C-uni) (total-iso D)) (\lam {p} => idp)

    \func total-iso (D : DCat {}) {x y : totalPrecat D} : QEquiv {\Sigma (e : Iso {_} {x.} {y.}) (DIso e {x.} {y.})} {Iso {totalPrecat D} {x} {y}} \cowith
      | f p => \new Iso {
        | f => (p., p.)
        | hinv => (hinv {p.}, DIso.inv^ {p.})
        | hinv_f => ext (hinv_f {p.}, DIso.inv^-left {p.})
        | f_hinv => ext (f_hinv {p.}, DIso.inv^-right {p.})
      }
      | ret (e : Iso) => (totalPrecat.proj.Func-iso e, \new DIso {
        | f => e.f.
        | inv^ => e.hinv.
        | inv^-left => rewrite (prop-isProp (hinv_f {totalPrecat.proj.Func-iso e}) (pmap __. e.hinv_f)) (Equiv.f {sigmaEquiv _ _ _} e.hinv_f).
        | inv^-right => rewrite (prop-isProp (f_hinv {totalPrecat.proj.Func-iso e}) (pmap __. e.f_hinv)) (Equiv.f {sigmaEquiv _ _ _} e.f_hinv).
      })
      | ret_f p => idp
      | f_sec e => idp

    \func eq-over {D : DCat {}} {a b : D.C} {x : D a} {y : D b} (p : a = b) : Equiv {transport D p x = y} {DIso (Precat.idtoiso p) {x} {y}} \elim p
      | idp => univalence^
  }