Slice

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

\func ObOver {C : Precat} (x : C) => \Sigma (y : C) (Hom y x)
  \where {
    \protected \func id : ObOver x => (x, C.id)

    \sfunc equals {y z : ObOver x} (p : y.1 = z.1) (q : y.2 = z.2 ∘ C.idtoiso p) : y = z
      => Jl (\lam z' p' => \Pi (z2 : Hom z' x) -> y.2 = z2 ∘ C.idtoiso p' -> y = (z',z2)) (\lam z2 q' => pmap {_} {ObOver x} (y.1,__) (q' *> id-right)) p z.2 q

    \lemma unequals {y z : ObOver x} (r : y = z) : y.2 = z.2 ∘ C.idtoiso (pmap __.1 r) \elim r
      | idp => inv id-right
  }

\instance SlicePrecat {C : Precat} (x : C) : Precat (ObOver x)
  | Hom (y,f) (z,g) => \Sigma (h : Hom y z) (g ∘ h = f)
  | id => (id, 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 __.1 __.1 \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.2)), simp_coe (Cat.transport_Hom_iso-right e' _ id-right))