(** * Classification of morphisms of the Grothendieck Construction of a functor to Set *)
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 }.
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
(s <~=~> d)%category <~>
{e : (c s <~=~> c d)%category & (F _1 e) (x s) = x d}
  Proof.
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
(s <~=~> d)%category <~>
{e : (c s <~=~> c d)%category & (F _1 e) (x s) = x d}
    simple refine (equiv_adjointify _ _ _ _).
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
(s <~=~> d)%category -> {e : (c s <~=~> c d)%category & (F _1 e) (x s) = x d}
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
{e : (c s <~=~> c d)%category & (F _1 e) (x s) = x d} -> (s <~=~> d)%category
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
?f o ?g == idmap
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
?g o ?f == idmap
    {
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
(s <~=~> d)%category -> {e : (c s <~=~> c d)%category & (F _1 e) (x s) = x d} intro m.
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
m: (s <~=~> d)%category
{e : (c s <~=~> c d)%category & (F _1 e) (x s) = x d}
      simple refine (_; _).
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
m: (s <~=~> d)%category
(c s <~=~> c d)%category
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
m: (s <~=~> d)%category
(fun e : (c s <~=~> c d)%category => (F _1 e) (x s) = x d) ?proj1
      {
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
m: (s <~=~> d)%category
(c s <~=~> c d)%category exists (m : morphism _ _ _).1.
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
m: (s <~=~> d)%category
IsIsomorphism m.1
        exists (m^-1).1.
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
m: (s <~=~> d)%category
(m^-1).1 o m.1 = 1
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
m: (s <~=~> d)%category
m.1 o (m^-1).1 = 1
        {
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
m: (s <~=~> d)%category
(m^-1).1 o m.1 = 1 exact (ap proj1 (@left_inverse _ _ _ m _)). }
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
m: (s <~=~> d)%category
m.1 o (m^-1).1 = 1
        {
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
m: (s <~=~> d)%category
m.1 o (m^-1).1 = 1 exact (ap proj1 (@right_inverse _ _ _ m _)). } }
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
m: (s <~=~> d)%category
(fun e : (c s <~=~> c d)%category => (F _1 e) (x s) = x d)
  {|
    morphism_isomorphic := m.1;
    isisomorphism_isomorphic :=
      {|
        morphism_inverse := (m^-1).1;
        left_inverse := ap pr1 left_inverse;
        right_inverse := ap pr1 right_inverse
      |}
  |}
      {
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
m: (s <~=~> d)%category
(fun e : (c s <~=~> c d)%category => (F _1 e) (x s) = x d)
  {|
    morphism_isomorphic := m.1;
    isisomorphism_isomorphic :=
      {|
        morphism_inverse := (m^-1).1;
        left_inverse := ap pr1 left_inverse;
        right_inverse := ap pr1 right_inverse
      |}
  |} exact (m : morphism _ _ _).2. } }
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
{e : (c s <~=~> c d)%category & (F _1 e) (x s) = x d} -> (s <~=~> d)%category
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
(fun m : (s <~=~> d)%category =>
 ({|
    morphism_isomorphic := m.1;
    isisomorphism_isomorphic :=
      {|
        morphism_inverse := (m^-1%morphism).1;
        left_inverse := ap pr1 left_inverse;
        right_inverse := ap pr1 right_inverse
      |}
  |};
 (m : morphism (category F) s d).2))
o ?g == idmap
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
?g
o (fun m : (s <~=~> d)%category =>
   ({|
      morphism_isomorphic := m.1;
      isisomorphism_isomorphic :=
        {|
          morphism_inverse := (m^-1%morphism).1;
          left_inverse := ap pr1 left_inverse;
          right_inverse := ap pr1 right_inverse
        |}
    |};
   (m : morphism (category F) s d).2)) ==
idmap
    {
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
{e : (c s <~=~> c d)%category & (F _1 e) (x s) = x d} -> (s <~=~> d)%category intro m.
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
m: {e : (c s <~=~> c d)%category & (F _1 e) (x s) = x d}
(s <~=~> d)%category
      exists (m.1 : morphism _ _ _ ; m.2).
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
m: {e : (c s <~=~> c d)%category & (F _1 e) (x s) = x d}
IsIsomorphism (m.1; 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.
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
m: {e : (c s <~=~> c d)%category & (F _1 e) (x s) = x d}
(((m.1)^-1;
 (ap (F _1 (m.1)^-1) m.2)^ @
 ap10
   (((composition_of F (c s) (c d) (c s) m.1 (m.1)^-1)^ @
     ap (fun m0 : morphism C (c s) (c s) => F _1 m0) left_inverse) @
    identity_of F (c s))
   (x s))
 o (m.1; m.2)).1 =
1.1
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
m: {e : (c s <~=~> c d)%category & (F _1 e) (x s) = x d}
((m.1; m.2)
 o ((m.1)^-1;
   (ap (F _1 (m.1)^-1) m.2)^ @
   ap10
     (((composition_of F (c s) (c d) (c s) m.1 (m.1)^-1)^ @
       ap (fun m0 : morphism C (c s) (c s) => F _1 m0) left_inverse) @
      identity_of F (c s))
     (x s))).1 =
1.1
      -
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
m: {e : (c s <~=~> c d)%category & (F _1 e) (x s) = x d}
(((m.1)^-1;
 (ap (F _1 (m.1)^-1) m.2)^ @
 ap10
   (((composition_of F (c s) (c d) (c s) m.1 (m.1)^-1)^ @
     ap (fun m0 : morphism C (c s) (c s) => F _1 m0) left_inverse) @
    identity_of F (c s))
   (x s))
 o (m.1; m.2)).1 =
1.1 exact left_inverse.
      -
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
m: {e : (c s <~=~> c d)%category & (F _1 e) (x s) = x d}
((m.1; m.2)
 o ((m.1)^-1;
   (ap (F _1 (m.1)^-1) m.2)^ @
   ap10
     (((composition_of F (c s) (c d) (c s) m.1 (m.1)^-1)^ @
       ap (fun m0 : morphism C (c s) (c s) => F _1 m0) left_inverse) @
      identity_of F (c s))
     (x s))).1 =
1.1 exact right_inverse. }
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
(fun m : (s <~=~> d)%category =>
 ({|
    morphism_isomorphic := m.1;
    isisomorphism_isomorphic :=
      {|
        morphism_inverse := (m^-1%morphism).1;
        left_inverse := ap pr1 left_inverse;
        right_inverse := ap pr1 right_inverse
      |}
  |};
 (m : morphism (category F) s d).2))
o (fun m : {e : (c s <~=~> c d)%category & (F _1 e) (x s) = x d} =>
   {|
     morphism_isomorphic := (m.1; m.2);
     isisomorphism_isomorphic :=
       {|
         morphism_inverse :=
           ((m.1)^-1%morphism;
           (ap (F _1 (m.1)^-1) m.2)^ @
           ap10
             (((composition_of F (c s) (c d) (c s) m.1 (m.1)^-1)^ @
               ap (fun m0 : morphism C (c s) (c s) => F _1 m0) left_inverse) @
              identity_of F (c s))
             (x s));
         left_inverse :=
           path_sigma_hprop
             (((m.1)^-1;
              (ap (F _1 (m.1)^-1) m.2)^ @
              ap10
                (((composition_of F (c s) (c d) (c s) m.1 (m.1)^-1)^ @
                  ap (fun m0 : morphism C (c s) (c s) => F _1 m0)
                    left_inverse) @
                 identity_of F (c s))
                (x s))
              o (m.1; m.2))%morphism
             1 left_inverse;
         right_inverse :=
           path_sigma_hprop
             ((m.1; m.2)
              o ((m.1)^-1;
                (ap (F _1 (m.1)^-1) m.2)^ @
                ap10
                  (((composition_of F (c s) (c d) (c s) m.1 (m.1)^-1)^ @
                    ap (fun m0 : morphism C (c s) (c s) => F _1 m0)
                      left_inverse) @
                   identity_of F (c s))
                  (x s)))%morphism
             1 right_inverse
       |}
   |}) ==
idmap
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
(fun m : {e : (c s <~=~> c d)%category & (F _1 e) (x s) = x d} =>
 {|
   morphism_isomorphic := (m.1; m.2);
   isisomorphism_isomorphic :=
     {|
       morphism_inverse :=
         ((m.1)^-1%morphism;
         (ap (F _1 (m.1)^-1) m.2)^ @
         ap10
           (((composition_of F (c s) (c d) (c s) m.1 (m.1)^-1)^ @
             ap (fun m0 : morphism C (c s) (c s) => F _1 m0) left_inverse) @
            identity_of F (c s))
           (x s));
       left_inverse :=
         path_sigma_hprop
           (((m.1)^-1;
            (ap (F _1 (m.1)^-1) m.2)^ @
            ap10
              (((composition_of F (c s) (c d) (c s) m.1 (m.1)^-1)^ @
                ap (fun m0 : morphism C (c s) (c s) => F _1 m0) left_inverse) @
               identity_of F (c s))
              (x s))
            o (m.1; m.2))%morphism
           1 left_inverse;
       right_inverse :=
         path_sigma_hprop
           ((m.1; m.2)
            o ((m.1)^-1;
              (ap (F _1 (m.1)^-1) m.2)^ @
              ap10
                (((composition_of F (c s) (c d) (c s) m.1 (m.1)^-1)^ @
                  ap (fun m0 : morphism C (c s) (c s) => F _1 m0)
                    left_inverse) @
                 identity_of F (c s))
                (x s)))%morphism
           1 right_inverse
     |}
 |})
o (fun m : (s <~=~> d)%category =>
   ({|
      morphism_isomorphic := m.1;
      isisomorphism_isomorphic :=
        {|
          morphism_inverse := (m^-1%morphism).1;
          left_inverse := ap pr1 left_inverse;
          right_inverse := ap pr1 right_inverse
        |}
    |};
   (m : morphism (category F) s d).2)) ==
idmap
    {
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
(fun m : (s <~=~> d)%category =>
 ({|
    morphism_isomorphic := m.1;
    isisomorphism_isomorphic :=
      {|
        morphism_inverse := (m^-1%morphism).1;
        left_inverse := ap pr1 left_inverse;
        right_inverse := ap pr1 right_inverse
      |}
  |};
 (m : morphism (category F) s d).2))
o (fun m : {e : (c s <~=~> c d)%category & (F _1 e) (x s) = x d} =>
   {|
     morphism_isomorphic := (m.1; m.2);
     isisomorphism_isomorphic :=
       {|
         morphism_inverse :=
           ((m.1)^-1%morphism;
           (ap (F _1 (m.1)^-1) m.2)^ @
           ap10
             (((composition_of F (c s) (c d) (c s) m.1 (m.1)^-1)^ @
               ap (fun m0 : morphism C (c s) (c s) => F _1 m0) left_inverse) @
              identity_of F (c s))
             (x s));
         left_inverse :=
           path_sigma_hprop
             (((m.1)^-1;
              (ap (F _1 (m.1)^-1) m.2)^ @
              ap10
                (((composition_of F (c s) (c d) (c s) m.1 (m.1)^-1)^ @
                  ap (fun m0 : morphism C (c s) (c s) => F _1 m0)
                    left_inverse) @
                 identity_of F (c s))
                (x s))
              o (m.1; m.2))%morphism
             1 left_inverse;
         right_inverse :=
           path_sigma_hprop
             ((m.1; m.2)
              o ((m.1)^-1;
                (ap (F _1 (m.1)^-1) m.2)^ @
                ap10
                  (((composition_of F (c s) (c d) (c s) m.1 (m.1)^-1)^ @
                    ap (fun m0 : morphism C (c s) (c s) => F _1 m0)
                      left_inverse) @
                   identity_of F (c s))
                  (x s)))%morphism
             1 right_inverse
       |}
   |}) ==
idmap intro x; apply path_sigma_hprop; apply path_isomorphic.
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
x: {e : (c s <~=~> c d)%category & (F _1 e) (Core.x s) = Core.x d}
({|
   morphism_isomorphic :=
     {|
       morphism_isomorphic := (x.1; x.2);
       isisomorphism_isomorphic :=
         {|
           morphism_inverse :=
             ((x.1)^-1;
             (ap (F _1 (x.1)^-1) x.2)^ @
             ap10
               (((composition_of F (c s) (c d) (c s) x.1 (x.1)^-1)^ @
                 ap (fun m : morphism C (c s) (c s) => F _1 m) left_inverse) @
                identity_of F (c s))
               (Core.x s));
           left_inverse :=
             path_sigma_hprop
               (((x.1)^-1;
                (ap (F _1 (x.1)^-1) x.2)^ @
                ap10
                  (((composition_of F (c s) (c d) (c s) x.1 (x.1)^-1)^ @
                    ap (fun m : morphism C (c s) (c s) => F _1 m)
                      left_inverse) @
                   identity_of F (c s))
                  (Core.x s))
                o (x.1; x.2))
               1 left_inverse;
           right_inverse :=
             path_sigma_hprop
               ((x.1; x.2)
                o ((x.1)^-1;
                  (ap (F _1 (x.1)^-1) x.2)^ @
                  ap10
                    (((composition_of F (c s) (c d) (c s) x.1 (x.1)^-1)^ @
                      ap (fun m : morphism C (c s) (c s) => F _1 m)
                        left_inverse) @
                     identity_of F (c s))
                    (Core.x s)))
               1 right_inverse
         |}
     |}.1;
   isisomorphism_isomorphic :=
     {|
       morphism_inverse :=
         ({|
            morphism_isomorphic := (x.1; x.2);
            isisomorphism_isomorphic :=
              {|
                morphism_inverse :=
                  ((x.1)^-1;
                  (ap (F _1 (x.1)^-1) x.2)^ @
                  ap10
                    (((composition_of F (c s) (c d) (c s) x.1 (x.1)^-1)^ @
                      ap (fun m : morphism C (c s) (c s) => F _1 m)
                        left_inverse) @
                     identity_of F (c s))
                    (Core.x s));
                left_inverse :=
                  path_sigma_hprop
                    (((x.1)^-1;
                     (ap (F _1 (x.1)^-1) x.2)^ @
                     ap10
                       (((composition_of F (c s) (c d) (c s) x.1 (x.1)^-1)^ @
                         ap (fun m : morphism C (c s) (c s) => F _1 m)
                           left_inverse) @
                        identity_of F (c s))
                       (Core.x s))
                     o (x.1; x.2))
                    1 left_inverse;
                right_inverse :=
                  path_sigma_hprop
                    ((x.1; x.2)
                     o ((x.1)^-1;
                       (ap (F _1 (x.1)^-1) x.2)^ @
                       ap10
                         (((composition_of F (c s) (c d) (c s) x.1 (x.1)^-1)^ @
                           ap (fun m : morphism C (c s) (c s) => F _1 m)
                             left_inverse) @
                          identity_of F (c s))
                         (Core.x s)))
                    1 right_inverse
              |}
          |}^-1).1;
       left_inverse := ap pr1 left_inverse;
       right_inverse := ap pr1 right_inverse
     |}
 |};
{|
  morphism_isomorphic := (x.1; x.2);
  isisomorphism_isomorphic :=
    {|
      morphism_inverse :=
        ((x.1)^-1;
        (ap (F _1 (x.1)^-1) x.2)^ @
        ap10
          (((composition_of F (c s) (c d) (c s) x.1 (x.1)^-1)^ @
            ap (fun m : morphism C (c s) (c s) => F _1 m) left_inverse) @
           identity_of F (c s))
          (Core.x s));
      left_inverse :=
        path_sigma_hprop
          (((x.1)^-1;
           (ap (F _1 (x.1)^-1) x.2)^ @
           ap10
             (((composition_of F (c s) (c d) (c s) x.1 (x.1)^-1)^ @
               ap (fun m : morphism C (c s) (c s) => F _1 m) left_inverse) @
              identity_of F (c s))
             (Core.x s))
           o (x.1; x.2))
          1 left_inverse;
      right_inverse :=
        path_sigma_hprop
          ((x.1; x.2)
           o ((x.1)^-1;
             (ap (F _1 (x.1)^-1) x.2)^ @
             ap10
               (((composition_of F (c s) (c d) (c s) x.1 (x.1)^-1)^ @
                 ap (fun m : morphism C (c s) (c s) => F _1 m) left_inverse) @
                identity_of F (c s))
               (Core.x s)))
          1 right_inverse
    |}
|}.2).1 = x.1
      reflexivity. }
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
(fun m : {e : (c s <~=~> c d)%category & (F _1 e) (x s) = x d} =>
 {|
   morphism_isomorphic := (m.1; m.2);
   isisomorphism_isomorphic :=
     {|
       morphism_inverse :=
         ((m.1)^-1%morphism;
         (ap (F _1 (m.1)^-1) m.2)^ @
         ap10
           (((composition_of F (c s) (c d) (c s) m.1 (m.1)^-1)^ @
             ap (fun m0 : morphism C (c s) (c s) => F _1 m0) left_inverse) @
            identity_of F (c s))
           (x s));
       left_inverse :=
         path_sigma_hprop
           (((m.1)^-1;
            (ap (F _1 (m.1)^-1) m.2)^ @
            ap10
              (((composition_of F (c s) (c d) (c s) m.1 (m.1)^-1)^ @
                ap (fun m0 : morphism C (c s) (c s) => F _1 m0) left_inverse) @
               identity_of F (c s))
              (x s))
            o (m.1; m.2))%morphism
           1 left_inverse;
       right_inverse :=
         path_sigma_hprop
           ((m.1; m.2)
            o ((m.1)^-1;
              (ap (F _1 (m.1)^-1) m.2)^ @
              ap10
                (((composition_of F (c s) (c d) (c s) m.1 (m.1)^-1)^ @
                  ap (fun m0 : morphism C (c s) (c s) => F _1 m0)
                    left_inverse) @
                 identity_of F (c s))
                (x s)))%morphism
           1 right_inverse
     |}
 |})
o (fun m : (s <~=~> d)%category =>
   ({|
      morphism_isomorphic := m.1;
      isisomorphism_isomorphic :=
        {|
          morphism_inverse := (m^-1%morphism).1;
          left_inverse := ap pr1 left_inverse;
          right_inverse := ap pr1 right_inverse
        |}
    |};
   (m : morphism (category F) s d).2)) ==
idmap
    {
H: Funext
C: PreCategory
F: Functor C set_cat
s, d: category F
(fun m : {e : (c s <~=~> c d)%category & (F _1 e) (x s) = x d} =>
 {|
   morphism_isomorphic := (m.1; m.2);
   isisomorphism_isomorphic :=
     {|
       morphism_inverse :=
         ((m.1)^-1%morphism;
         (ap (F _1 (m.1)^-1) m.2)^ @
         ap10
           (((composition_of F (c s) (c d) (c s) m.1 (m.1)^-1)^ @
             ap (fun m0 : morphism C (c s) (c s) => F _1 m0) left_inverse) @
            identity_of F (c s))
           (x s));
       left_inverse :=
         path_sigma_hprop
           (((m.1)^-1;
            (ap (F _1 (m.1)^-1) m.2)^ @
            ap10
              (((composition_of F (c s) (c d) (c s) m.1 (m.1)^-1)^ @
                ap (fun m0 : morphism C (c s) (c s) => F _1 m0) left_inverse) @
               identity_of F (c s))
              (x s))
            o (m.1; m.2))%morphism
           1 left_inverse;
       right_inverse :=
         path_sigma_hprop
           ((m.1; m.2)
            o ((m.1)^-1;
              (ap (F _1 (m.1)^-1) m.2)^ @
              ap10
                (((composition_of F (c s) (c d) (c s) m.1 (m.1)^-1)^ @
                  ap (fun m0 : morphism C (c s) (c s) => F _1 m0)
                    left_inverse) @
                 identity_of F (c s))
                (x s)))%morphism
           1 right_inverse
     |}
 |})
o (fun m : (s <~=~> d)%category =>
   ({|
      morphism_isomorphic := m.1;
      isisomorphism_isomorphic :=
        {|
          morphism_inverse := (m^-1%morphism).1;
          left_inverse := ap pr1 left_inverse;
          right_inverse := ap pr1 right_inverse
        |}
    |};
   (m : morphism (category F) s d).2)) ==
idmap intro x; apply path_isomorphic; reflexivity. }
  Defined.
End Grothendieck.