\import Category
\import Category.Functor
\import Paths
\import Paths.Meta

\type ObOver {C : Precat} (x : C) => \Sigma (y : C) (Hom y x)

\instance SlicePrecat {C : Precat} (x : C) : Precat (ObOver x)
  | Hom (y,f) (z,g) => \Sigma (h : Hom y z) (g ∘ h = f)
  | id (y,f) => (id y, id-right)
  | o (h1,p1) (h2,p2) => (h1 ∘ h2, inv o-assoc *> pmap (`∘ h2) p1 *> p2)
  | id-left => ext id-left
  | id-right => ext id-right
  | o-assoc => ext o-assoc
  \where
    \lemma forget {C : Precat} (x : C) : FaithfulFunctor (SlicePrecat x) C __. __. \cowith
      | Func-id => idp
      | Func-o => idp
      | isFaithful p => ext p

\instance SliceCat {C : Cat} (x : C) : Cat
  | Precat => SlicePrecat x
  | univalence => Cat.makeUnivalence \lam (e : Iso) =>
      \have e' => Functor.Func-iso {SlicePrecat.forget x} e
      \in (ext (Cat.isotoid e', Cat.transport_Hom_iso-left e' _ (inv e.f.)), simp_coe (Cat.transport_Hom_iso-right e' _ id-right))