IdentityPrinciple.v

(** * The Structure Identity Principle *)
Require Import Category.Core Category.Univalent Category.Morphisms.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Structure.Core.
Require Import Types.Sigma Trunc Equivalences.
Require Import Basics.Tactics.

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

Local Open Scope path_scope.
Local Open Scope category_scope.
Local Open Scope morphism_scope.
Local Open Scope structure_scope.

(** Quoting the Homotopy Type Theory Book (with slight changes for
    notational consistency): *)

(** Theorem (Structure identity principle): If [X] is a category and
    [(P, H)] is a standard notion of structure over [X], then the
    precategory [Str_{(P, H)}(X)] is a category. *)
Section sip.
  Variable X : PreCategory.
  Variable P : NotionOfStructure X.
  Context `{IsCategory X}.
  Context `{@IsStandardNotionOfStructure X P}.

  Let StrX := @precategory_of_structures X P.

  Definition sip_isotoid_helper (xa yb : StrX)
             (f : xa <~=~> yb)
  : xa.1 <~=~> yb.1.X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa, yb: StrX
f: xa <~=~> yb
xa.1 <~=~> yb.1
  Proof.X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa, yb: StrX
f: xa <~=~> yb
xa.1 <~=~> yb.1
    exists (PreCategoryOfStructures.f (f : morphism _ _ _)).X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa, yb: StrX
f: xa <~=~> yb
IsIsomorphism (PreCategoryOfStructures.f f)
    exists (PreCategoryOfStructures.f f^-1).X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa, yb: StrX
f: xa <~=~> yb
PreCategoryOfStructures.f f^-1
o PreCategoryOfStructures.f f = 1
X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa, yb: StrX
f: xa <~=~> yb
PreCategoryOfStructures.f f
o PreCategoryOfStructures.f f^-1 = 1
    -X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa, yb: StrX
f: xa <~=~> yb
PreCategoryOfStructures.f f^-1
o PreCategoryOfStructures.f f = 1 exact (ap (@PreCategoryOfStructures.f _ _ _ _) (@left_inverse _ _ _ _ f)).
    -X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa, yb: StrX
f: xa <~=~> yb
PreCategoryOfStructures.f f
o PreCategoryOfStructures.f f^-1 = 1 exact (ap (@PreCategoryOfStructures.f _ _ _ _) (@right_inverse _ _ _ _ f)).
  Defined.

  Lemma sip_isotoid_helper_refl (xa : StrX)
  : @sip_isotoid_helper xa xa (reflexivity _) = reflexivity _.X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa: StrX
sip_isotoid_helper (reflexivity xa) = reflexivity xa.1
  Proof.X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa: StrX
sip_isotoid_helper (reflexivity xa) = reflexivity xa.1
    unfold sip_isotoid_helper, reflexivity, isomorphic_refl.X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa: StrX
{|
  morphism_isomorphic :=
    PreCategoryOfStructures.f
      {|
        morphism_isomorphic := 1;
        isisomorphism_isomorphic :=
          isisomorphism_identity StrX xa
      |};
  isisomorphism_isomorphic :=
    {|
      morphism_inverse :=
        PreCategoryOfStructures.f
          {|
            morphism_isomorphic := 1;
            isisomorphism_isomorphic :=
              isisomorphism_identity StrX xa
          |}^-1;
      left_inverse :=
        ap (PreCategoryOfStructures.f (yb:=xa))
          left_inverse;
      right_inverse :=
        ap (PreCategoryOfStructures.f (yb:=xa))
          right_inverse
    |}
|} =
{|
  morphism_isomorphic := 1;
  isisomorphism_isomorphic :=
    isisomorphism_identity X xa.1
|}
    apply ap.X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa: StrX
{|
  morphism_inverse :=
    PreCategoryOfStructures.f
      {|
        morphism_isomorphic := 1;
        isisomorphism_isomorphic :=
          isisomorphism_identity StrX xa
      |}^-1;
  left_inverse :=
    ap (PreCategoryOfStructures.f (yb:=xa))
      left_inverse;
  right_inverse :=
    ap (PreCategoryOfStructures.f (yb:=xa))
      right_inverse
|} = isisomorphism_identity X xa.1
    apply path_ishprop.
  Defined.

  Lemma sip_helper x y (p : x = y) (a : P x) (b : P y)
  : transport P p a = b
    <-> is_structure_homomorphism P _ _ (idtoiso X p) a b *
        is_structure_homomorphism P _ _ (idtoiso X p)^-1 b a.X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
x, y: X
p: x = y
a: P x
b: P y
transport P p a = b <->
is_structure_homomorphism P x y (idtoiso X p) a b *
is_structure_homomorphism P y x (idtoiso X p)^-1 b a
  Proof.X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
x, y: X
p: x = y
a: P x
b: P y
transport P p a = b <->
is_structure_homomorphism P x y (idtoiso X p) a b *
is_structure_homomorphism P y x (idtoiso X p)^-1 b a
    split.X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
x, y: X
p: x = y
a: P x
b: P y
transport P p a = b ->
is_structure_homomorphism P x y (idtoiso X p) a b *
is_structure_homomorphism P y x (idtoiso X p)^-1 b a
X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
x, y: X
p: x = y
a: P x
b: P y
is_structure_homomorphism P x y (idtoiso X p) a b *
is_structure_homomorphism P y x (idtoiso X p)^-1 b a ->
transport P p a = b
    -X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
x, y: X
p: x = y
a: P x
b: P y
transport P p a = b ->
is_structure_homomorphism P x y (idtoiso X p) a b *
is_structure_homomorphism P y x (idtoiso X p)^-1 b a intros; path_induction; split; apply reflexivity.
    -X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
x, y: X
p: x = y
a: P x
b: P y
is_structure_homomorphism P x y (idtoiso X p) a b *
is_structure_homomorphism P y x (idtoiso X p)^-1 b a ->
transport P p a = b intros [H0 H1]; path_induction; simpl in *.X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
x: X
a, b: P x
H0: a <= b
H1: b <= a
a = b
      apply antisymmetry_structure; assumption.
  Defined.

  Definition sip_isotoid (xa yb : StrX)
             (f : xa <~=~> yb)
  : xa = yb.X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa, yb: StrX
f: xa <~=~> yb
xa = yb
  Proof.X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa, yb: StrX
f: xa <~=~> yb
xa = yb
    refine (path_sigma_uncurried
              _ _ _
              (isotoid
                 X
                 xa.1
                 yb.1
                 (sip_isotoid_helper f);
               _)).X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa, yb: StrX
f: xa <~=~> yb
transport (fun x : X => P x)
  (isotoid X xa.1 yb.1 (sip_isotoid_helper f)) xa.2 =
yb.2
    apply sip_helper; simpl.X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa, yb: StrX
f: xa <~=~> yb
is_structure_homomorphism P xa.1 yb.1
  (idtoiso X
     (isotoid X xa.1 yb.1 (sip_isotoid_helper f)))
  xa.2 yb.2 *
is_structure_homomorphism P yb.1 xa.1
  (idtoiso X
     (isotoid X xa.1 yb.1 (sip_isotoid_helper f)))^-1
  yb.2 xa.2
    split;
      lazymatch goal with
        | [ |- context[idtoiso ?X ((isotoid ?X ?x ?y) ?m)] ]
          => pose proof (eisretr (@idtoiso X x y) m) as H';
             pattern (idtoiso X ((isotoid X x y) m))
      end;
      refine (transport _ H'^ _); clear H'; simpl;
      apply PreCategoryOfStructures.h.
  Defined.

  Lemma sip_isotoid_refl xa
  : @sip_isotoid xa xa (reflexivity _) = reflexivity _.X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa: StrX
sip_isotoid (reflexivity xa) = reflexivity xa
  Proof.X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa: StrX
sip_isotoid (reflexivity xa) = reflexivity xa
    refine (_ @ eta_path_sigma_uncurried _).X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa: StrX
sip_isotoid (reflexivity xa) =
path_sigma_uncurried (fun x : X => P x) xa xa
  ((reflexivity xa) ..1; (reflexivity xa) ..2)
    refine (ap (path_sigma_uncurried _ _ _) _).X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa: StrX
(isotoid X xa.1 xa.1
   (sip_isotoid_helper (reflexivity xa));
let X0 :=
  fun (x y : X) (p : x = y) (a : P x) (b : P y) =>
  snd (sip_helper p a b) in
X0 xa.1 xa.1
  (isotoid X xa.1 xa.1
     (sip_isotoid_helper (reflexivity xa))) xa.2 xa.2
  (let H' :=
     eisretr (idtoiso X (y:=xa.1))
       (sip_isotoid_helper (reflexivity xa)) in
   transport
     (fun i : xa.1 <~=~> xa.1 =>
      is_structure_homomorphism P xa.1 xa.1 i xa.2
        xa.2) H'^
     (PreCategoryOfStructures.h (reflexivity xa)),
  let H' :=
    eisretr (idtoiso X (y:=xa.1))
      (sip_isotoid_helper (reflexivity xa)) in
  transport
    (fun i : xa.1 <~=~> xa.1 =>
     is_structure_homomorphism P xa.1 xa.1 i^-1 xa.2
       xa.2) H'^
    (PreCategoryOfStructures.h (reflexivity xa)^-1))) =
((reflexivity xa) ..1; (reflexivity xa) ..2)
    apply equiv_path_sigma_hprop.X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa: StrX
(isotoid X xa.1 xa.1
   (sip_isotoid_helper (reflexivity xa));
let X0 :=
  fun (x y : X) (p : x = y) (a : P x) (b : P y) =>
  snd (sip_helper p a b) in
X0 xa.1 xa.1
  (isotoid X xa.1 xa.1
     (sip_isotoid_helper (reflexivity xa))) xa.2 xa.2
  (let H' :=
     eisretr (idtoiso X (y:=xa.1))
       (sip_isotoid_helper (reflexivity xa)) in
   transport
     (fun i : xa.1 <~=~> xa.1 =>
      is_structure_homomorphism P xa.1 xa.1 i xa.2
        xa.2) H'^
     (PreCategoryOfStructures.h (reflexivity xa)),
  let H' :=
    eisretr (idtoiso X (y:=xa.1))
      (sip_isotoid_helper (reflexivity xa)) in
  transport
    (fun i : xa.1 <~=~> xa.1 =>
     is_structure_homomorphism P xa.1 xa.1 i^-1 xa.2
       xa.2) H'^
    (PreCategoryOfStructures.h (reflexivity xa)^-1))).1 =
((reflexivity xa) ..1; (reflexivity xa) ..2).1
    simpl.X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa: StrX
isotoid X xa.1 xa.1
  (sip_isotoid_helper (isomorphic_refl StrX xa)) =
1%path
    refine (_ @ eisretr (isotoid X xa.1 xa.1) 1%path).X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa: StrX
isotoid X xa.1 xa.1
  (sip_isotoid_helper (isomorphic_refl StrX xa)) =
isotoid X xa.1 xa.1
  (((isotoid X xa.1 xa.1)^-1)%function 1%path)
    apply ap.X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa: StrX
sip_isotoid_helper (isomorphic_refl StrX xa) =
((isotoid X xa.1 xa.1)^-1)%function 1%path
    apply sip_isotoid_helper_refl.
  Defined.

  Lemma path_f_idtoiso_precategory_of_structures xa yb (p : xa = yb)
  : PreCategoryOfStructures.f (idtoiso (precategory_of_structures P) p : morphism _ _ _)
    = idtoiso X p..1.X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa, yb: precategory_of_structures P
p: xa = yb
PreCategoryOfStructures.f
  (idtoiso (precategory_of_structures P) p
   :
   morphism (precategory_of_structures P) xa yb) =
idtoiso X p ..1
  Proof.X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa, yb: precategory_of_structures P
p: xa = yb
PreCategoryOfStructures.f
  (idtoiso (precategory_of_structures P) p
   :
   morphism (precategory_of_structures P) xa yb) =
idtoiso X p ..1
    induction p; reflexivity.
  Defined.

  Lemma structure_identity_principle_helper
        (xa yb : StrX)
        (x : xa <~=~> yb)
  : PreCategoryOfStructures.f
      (idtoiso (precategory_of_structures P) (sip_isotoid x) : morphism _ _ _)
    = PreCategoryOfStructures.f (x : morphism _ _ _).X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa, yb: StrX
x: xa <~=~> yb
PreCategoryOfStructures.f
  (idtoiso (precategory_of_structures P)
     (sip_isotoid x)
   :
   morphism (precategory_of_structures P) xa yb) =
PreCategoryOfStructures.f (x : morphism StrX xa yb)
  Proof.X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa, yb: StrX
x: xa <~=~> yb
PreCategoryOfStructures.f
  (idtoiso (precategory_of_structures P)
     (sip_isotoid x)
   :
   morphism (precategory_of_structures P) xa yb) =
PreCategoryOfStructures.f (x : morphism StrX xa yb)
    refine (path_f_idtoiso_precategory_of_structures _ @ _).X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa, yb: StrX
x: xa <~=~> yb
idtoiso X (sip_isotoid x) ..1 =
PreCategoryOfStructures.f x
    refine ((ap _ (ap _ _))
              @ (ap (@morphism_isomorphic _ _ _)
                    (eisretr (@idtoiso X xa.1 yb.1) (sip_isotoid_helper _)))).X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa, yb: StrX
x: xa <~=~> yb
(sip_isotoid x) ..1 =
isotoid X xa.1 yb.1 (sip_isotoid_helper x)
    exact (pr1_path_sigma_uncurried _).
  Defined.

  Global Instance structure_identity_principle
  : IsCategory (precategory_of_structures P).X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
IsCategory (precategory_of_structures P)
  Proof.X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
IsCategory (precategory_of_structures P)
    intros xa yb.X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa, yb: precategory_of_structures P
IsEquiv
  (idtoiso (precategory_of_structures P) (y:=yb))
    refine (isequiv_adjointify
              _ (@sip_isotoid xa yb)
              _ _);
      intro; simpl in *.X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa, yb: {x : X & P x}
x: xa <~=~> yb
idtoiso (precategory_of_structures P) (sip_isotoid x) =
x
X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa, yb: {x : X & P x}
x: xa = yb
sip_isotoid (idtoiso (precategory_of_structures P) x) =
x
    -X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa, yb: {x : X & P x}
x: xa <~=~> yb
idtoiso (precategory_of_structures P) (sip_isotoid x) =
x abstract (
          apply path_isomorphic; simpl;
          apply PreCategoryOfStructures.path_morphism;
          apply structure_identity_principle_helper
        ).
    -X: PreCategory
P: NotionOfStructure X
IsCategory0: IsCategory X
H: IsStandardNotionOfStructure P
StrX:= precategory_of_structures P: PreCategory
xa, yb: {x : X & P x}
x: xa = yb
sip_isotoid (idtoiso (precategory_of_structures P) x) =
x abstract (induction x; apply sip_isotoid_refl).
  Defined.
End sip.