Require Import Category.Core Functor.Core.
Require Import Category.Morphisms.
Require Import SetCategory.Core.
Require Import Grothendieck.ToSet.Core.
Require Import HoTT.Basics HoTT.Types.

Set Implicit Arguments.
Generalizable All Variables.

Local Open Scope morphism_scope.

Section Grothendieck.
  Context `{Funext}.
  Context {C : PreCategory}
          {F : Functor C set_cat}.

  Definition isequiv_sigma_category_isomorphism {s d : category F}
  : (s <~=~> d)%category <~> { e : (s.(c) <~=~> d.(c))%category | (F _1 e s.(x) = d.(x))%category }.
  Proof.
    simple refine (equiv_adjointify _ _ _ _).
    { intro m.
      simple refine (_; _).
      { ∃ (m : morphism _ _ _).1.
        ∃ (m^-1).1.
        { exact (ap proj1 (@left_inverse _ _ _ m _)). }
        { exact (ap proj1 (@right_inverse _ _ _ m _)). } }
      { exact (m : morphism _ _ _).2. } }
    { intro m.
      ∃ (m.1 : morphism _ _ _ ; m.2).
      eexists (m.1^-1;
               ((ap (F _1 (m.1)^-1) m.2)^)
                 @ (ap10 ((((composition_of F _ _ _ _ _)^)
                             @ (ap (fun m ⇒ F _1 m) (@left_inverse _ _ _ m.1 _))
                             @ (identity_of F _))
                          : (F _1 (m.1 : morphism _ _ _)^-1) o F _1 m.1 = idmap) s.(x)));
        apply path_sigma_hprop.
      - exact left_inverse.
      - exact right_inverse. }
    { intro x; apply path_sigma_hprop; apply path_isomorphic.
      reflexivity. }
    { intro x; apply path_isomorphic; reflexivity. }
  Defined.
End Grothendieck.