(** * Saturation of the Grothendieck Construction of a functor to Set *)
Require Import Category.Core Functor.Core.
Require Import Category.Univalent.
Require Import Category.Morphisms.
Require Import SetCategory.Core.
Require Import Grothendieck.ToSet.Core Grothendieck.ToSet.Morphisms.
Require Import HoTT.Basics.Equivalences HoTT.Basics.Trunc.
Require Import HoTT.Types.Universe HoTT.Types.Sigma.

Set Implicit Arguments.
Generalizable All Variables.

Local Open Scope morphism_scope.

Section Grothendieck.
  Context `{Funext}.

  Variable C : PreCategory.
  Context `{IsCategory C}.
  Variable F : Functor C set_cat.

  Definition category_isotoid_helper {s d} (a : c s = c d)
  : (transport (fun c : C => F c) a (x s) = x d)
      <~> (F _1 (idtoiso C a)) (x s) = x d.
H: Funext
C: PreCategory
IsCategory0: IsCategory C
F: Functor C set_cat
s, d: Pair F
a: c s = c d
transport (fun c : C => (F _0 c)%object) a (x s) = x d <~>
(F _1 (idtoiso C a)) (x s) = x d
  Proof.
H: Funext
C: PreCategory
IsCategory0: IsCategory C
F: Functor C set_cat
s, d: Pair F
a: c s = c d
transport (fun c : C => (F _0 c)%object) a (x s) = x d <~>
(F _1 (idtoiso C a)) (x s) = x d
    apply equiv_path.
H: Funext
C: PreCategory
IsCategory0: IsCategory C
F: Functor C set_cat
s, d: Pair F
a: c s = c d
(transport (fun c : C => (F _0 c)%object) a (x s) = x d) =
((F _1 (idtoiso C a)) (x s) = x d)
    apply ap10, ap.
H: Funext
C: PreCategory
IsCategory0: IsCategory C
F: Functor C set_cat
s, d: Pair F
a: c s = c d
transport (fun c : C => (F _0 c)%object) a (x s) = (F _1 (idtoiso C a)) (x s)
    destruct a; simpl.
H: Funext
C: PreCategory
IsCategory0: IsCategory C
F: Functor C set_cat
s, d: Pair F
x s = (F _1 1) (x s)
    exact (ap10 (identity_of F _)^ _).
  Defined.

  Arguments category_isotoid_helper : simpl never.

  Definition category_isotoid {s d : category F}
  : s = d <~> (s <~=~> d)%category.
H: Funext
C: PreCategory
IsCategory0: IsCategory C
F: Functor C set_cat
s, d: category F
s = d <~> (s <~=~> d)%category
  Proof.
H: Funext
C: PreCategory
IsCategory0: IsCategory C
F: Functor C set_cat
s, d: category F
s = d <~> (s <~=~> d)%category
    refine (isequiv_sigma_category_isomorphism^-1 oE _ oE (equiv_ap' (issig_pair F)^-1 s d)).
H: Funext
C: PreCategory
IsCategory0: IsCategory C
F: Functor C set_cat
s, d: category F
(issig_pair F)^-1%equiv s = (issig_pair F)^-1%equiv d <~>
{e : (c s <~=~> c d)%category & (F _1 e) (x s) = x d}
    refine (_ oE (equiv_path_sigma _ _ _)^-1).
H: Funext
C: PreCategory
IsCategory0: IsCategory C
F: Functor C set_cat
s, d: category F
{p : ((issig_pair F)^-1%equiv s).1 = ((issig_pair F)^-1%equiv d).1 &
transport (fun c : C => (F _0 c)%object) p ((issig_pair F)^-1%equiv s).2 =
((issig_pair F)^-1%equiv d).2} <~>
{e : (c s <~=~> c d)%category & (F _1 e) (x s) = x d}
    simpl.
H: Funext
C: PreCategory
IsCategory0: IsCategory C
F: Functor C set_cat
s, d: category F
{p : c s = c d & transport (fun c : C => (F _0 c)%object) p (x s) = x d} <~>
{e : (c s <~=~> c d)%category & (F _1 e) (x s) = x d}
    simple refine (equiv_functor_sigma' _ _).
H: Funext
C: PreCategory
IsCategory0: IsCategory C
F: Functor C set_cat
s, d: category F
c s = c d <~> (c s <~=~> c d)%category
H: Funext
C: PreCategory
IsCategory0: IsCategory C
F: Functor C set_cat
s, d: category F
forall a : c s = c d,
(fun p : c s = c d => transport (fun c : C => (F _0 c)%object) p (x s) = x d)
  a <~>
(fun e : (c s <~=~> c d)%category => (F _1 e) (x s) = x d) (?f a)
    {
H: Funext
C: PreCategory
IsCategory0: IsCategory C
F: Functor C set_cat
s, d: category F
c s = c d <~> (c s <~=~> c d)%category exists (@idtoiso C _ _).
H: Funext
C: PreCategory
IsCategory0: IsCategory C
F: Functor C set_cat
s, d: category F
IsEquiv (idtoiso C (y:=c d))
      exact _. }
H: Funext
C: PreCategory
IsCategory0: IsCategory C
F: Functor C set_cat
s, d: category F
forall a : c s = c d,
(fun p : c s = c d => transport (fun c : C => (F _0 c)%object) p (x s) = x d)
  a <~>
(fun e : (c s <~=~> c d)%category => (F _1 e) (x s) = x d)
  ({|
     equiv_fun := idtoiso C (y:=c d);
     equiv_isequiv := IsCategory0 (c s) (c d)
   |} a)
    {
H: Funext
C: PreCategory
IsCategory0: IsCategory C
F: Functor C set_cat
s, d: category F
forall a : c s = c d,
(fun p : c s = c d => transport (fun c : C => (F _0 c)%object) p (x s) = x d)
  a <~>
(fun e : (c s <~=~> c d)%category => (F _1 e) (x s) = x d)
  ({|
     equiv_fun := idtoiso C (y:=c d);
     equiv_isequiv := IsCategory0 (c s) (c d)
   |} a) exact category_isotoid_helper. }
  Defined.

  #[export] Instance preservation : IsCategory (category F).
H: Funext
C: PreCategory
IsCategory0: IsCategory C
F: Functor C set_cat
IsCategory (category F)
  Proof.
H: Funext
C: PreCategory
IsCategory0: IsCategory C
F: Functor C set_cat
IsCategory (category F)
    intros s d.
H: Funext
C: PreCategory
IsCategory0: IsCategory C
F: Functor C set_cat
s, d: category F
IsEquiv (idtoiso (category F) (y:=d))
    refine (@isequiv_homotopic _ _ category_isotoid (idtoiso (category F) (x:=s) (y:=d)) _ _).
H: Funext
C: PreCategory
IsCategory0: IsCategory C
F: Functor C set_cat
s, d: category F
category_isotoid == idtoiso (category F) (y:=d)
    intro x.
H: Funext
C: PreCategory
IsCategory0: IsCategory C
F: Functor C set_cat
s, d: category F
x: s = d
category_isotoid x = idtoiso (category F) x
    destruct x; apply path_isomorphic, path_sigma_hprop.
H: Funext
C: PreCategory
IsCategory0: IsCategory C
F: Functor C set_cat
s: category F
(category_isotoid 1%path).1 = (idtoiso (category F) 1).1
    reflexivity.
  Defined.
End Grothendieck.