(** * Classification of morphisms of the Grothendieck Construction of a functor to Set *)
Require Import Category.Core Functor.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Category.Morphisms.
Require Import SetCategory.Core.
Require Import Grothendieck.ToSet.Core.
Require Import HoTT.Basics HoTT.Types.

Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.

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 m : morphism C (c s) (c s) => F _1 m)
       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 m : morphism C (c s) (c s) => F _1 m)
         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 m : morphism C (c s) (c s) => F _1 m)
       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 m : morphism C (c s) (c s) => F _1 m)
         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 (...) (...)
                     => 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 (...) (...)
                       => 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 (...) (...) =>
                   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 (...) (...)
                     => 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 (...) (...)
                     => 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 (...) (...)
                       => 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 ... ... =>
                       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 ... ... =>
                         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 : ... => 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 ... ... ...
                            x.1 ...^-1)^ @
                         ap (...) 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 ... ...
                              ... x.1 ...^-1)^ @
                           ap (...) 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 (...) (...) =>
                   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 (...) (...)
                     => 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 (...) (...) =>
                   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 (...) (...)
                     => 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.