Skip to content

Commit

Permalink
Merge pull request #1788 from jdchristensen/equivalences-clean-up
Browse files Browse the repository at this point in the history 
Equivalences clean up
  • Loading branch information
@jdchristensen
jdchristensen authored Oct 20, 2023
2 parents 90a338a + b145376 commit ca9ef4b
Showing 1 changed file with 79 additions and 77 deletions.
156 changes: 79 additions & 77 deletions theories/Basics/Equivalences.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,9 +32,9 @@ Arguments reflexive_equiv /.

(** The composition of equivalences is an equivalence. *)
Global Instance isequiv_compose `{IsEquiv A B f} `{IsEquiv B C g}
: IsEquiv (compose g f) | 1000
:= Build_IsEquiv A C (compose g f)
(compose f^-1 g^-1)
: IsEquiv (g o f) | 1000
:= Build_IsEquiv A C (g o f)
(f^-1 o g^-1)
(fun c => ap g (eisretr f (g^-1 c)) @ eisretr g c)
(fun a => ap (f^-1) (eissect g (f a)) @ eissect f a)
(fun a =>
Expand All @@ -58,16 +58,13 @@ Definition isequiv_compose'
Definition equiv_compose {A B C : Type} (g : B -> C) (f : A -> B)
`{IsEquiv B C g} `{IsEquiv A B f}
: A <~> C
:= Build_Equiv A C (compose g f) _.
:= Build_Equiv A C (g o f) _.

Definition equiv_compose' {A B C : Type} (g : B <~> C) (f : A <~> B)
: A <~> C
:= equiv_compose g f.

Definition iff_equiv {A B : Type} (f : A <~> B)
: A <-> B := (equiv_fun f, f^-1).

(** We put [g] and [f] in [equiv_scope] explcitly. This is a partial work-around for https://coq.inria.fr/bugs/show_bug.cgi?id=3990, which is that implicitly bound scopes don't nest well. *)
(** We put [g] and [f] in [equiv_scope] explicitly. This is a partial work-around for https://github.com/coq/coq/issues/3990, which is that implicitly bound scopes don't nest well. *)
Notation "g 'oE' f" := (equiv_compose' g%equiv f%equiv) : equiv_scope.

(* The TypeClass [Transitive] has a different order of parameters than [equiv_compose]. Thus in declaring the instance we have to switch the order of arguments. *)
Expand All @@ -76,12 +73,16 @@ Global Instance transitive_equiv : Transitive Equiv | 0 :=

Arguments transitive_equiv /.

(** A tactic to simplify "oE". See [ev_equiv] below for a more extensive tactic. *)
Ltac change_apply_equiv_compose :=
match goal with
| [ |- context [ equiv_fun (?f oE ?g) ?x ] ] =>
change ((f oE g) x) with (f (g x))
end.

Definition iff_equiv {A B : Type} (f : A <~> B)
: A <-> B := (equiv_fun f, f^-1).

(** Transporting is an equivalence. *)
Section EquivTransport.

Expand Down Expand Up @@ -256,6 +257,41 @@ Definition equiv_pr1 {A : Type} (P : A -> Type) `{forall x, Contr (P x)}
: { x : A & P x } <~> A
:= Build_Equiv _ _ (@pr1 A P) _.

(** Equivalences between path spaces *)

(** If [f] is an equivalence, then so is [ap f]. We are lazy and use [adjointify]. *)
Global Instance isequiv_ap `{IsEquiv A B f} (x y : A)
: IsEquiv (@ap A B f x y) | 1000
:= isequiv_adjointify (ap f)
(fun q => (eissect f x)^ @ ap f^-1 q @ eissect f y)
(fun q =>
ap_pp f _ _
@ whiskerR (ap_pp f _ _) _
@ ((ap_V f _ @ inverse2 (eisadj f _)^)
@@ (ap_compose f^-1 f _)^
@@ (eisadj f _)^)
@ concat_pA1_p (eisretr f) _ _
@ whiskerR (concat_Vp _) _
@ concat_1p _)
(fun p =>
whiskerR (whiskerL _ (ap_compose f f^-1 _)^) _
@ concat_pA1_p (eissect f) _ _
@ whiskerR (concat_Vp _) _
@ concat_1p _).

Definition equiv_ap `(f : A -> B) `{IsEquiv A B f} (x y : A)
: (x = y) <~> (f x = f y)
:= Build_Equiv _ _ (ap f) _.

Global Arguments equiv_ap (A B)%type_scope f%function_scope _ _ _.

Definition equiv_ap' `(f : A <~> B) (x y : A)
: (x = y) <~> (f x = f y)
:= equiv_ap f x y.

Definition equiv_inj `(f : A -> B) `{IsEquiv A B f} {x y : A}
: (f x = f y) -> (x = y)
:= (ap f)^-1.

(** Assuming function extensionality, composing with an equivalence is itself an equivalence *)

Expand Down Expand Up @@ -293,79 +329,33 @@ Definition equiv_postcompose' `{Funext} {A B C : Type} (f : B <~> C)
: (A -> B) <~> (A -> C)
:= Build_Equiv _ _ (fun (g:A->B) => f o g) _.

(** Conversely, if pre- or post-composing with a function is always an equivalence, then that function is also an equivalence. It's convenient to know that we only need to assume the equivalence when the other type is the domain or the codomain. *)
(** Conversely, if pre- or post-composing with a function is always an equivalence, then that function is also an equivalence. This is a form of the Yoneda lemma. It's convenient to know that we only need to assume the equivalence when the other type is the domain or the codomain. *)

Definition isequiv_isequiv_precompose {A B : Type} (f : A -> B)
(precomp := (fun (C : Type) (h : B -> C) => h o f))
(Aeq : IsEquiv (precomp A)) (Beq : IsEquiv (precomp B))
: IsEquiv f.
Proof.
assert (H : forall (C D : Type)
(Ceq : IsEquiv (precomp C)) (Deq : IsEquiv (precomp D))
(k : C -> D) (h : A -> C),
k o (precomp C)^-1 h = (precomp D)^-1 (k o h)).
{ intros C D ? ? k h.
transitivity ((precomp D)^-1 (k o (precomp C ((precomp C)^-1 h)))).
- transitivity ((precomp D)^-1 (precomp D (k o ((precomp C)^-1 h)))).
+ rewrite (eissect (precomp D) _); reflexivity.
+ reflexivity.
- rewrite (eisretr (precomp C) h); reflexivity. }
refine (isequiv_adjointify f ((precomp A)^-1 idmap) _ _).
- intros x.
change ((f o (precomp A)^-1 idmap) x = idmap x).
apply ap10.
rewrite (H A B Aeq Beq).
change ((precomp B)^-1 (precomp B idmap) = idmap).
apply eissect.
- intros x.
change ((precomp A ((precomp A)^-1 idmap)) x = idmap x).
apply ap10, eisretr.
Qed.

(*
set (g:=(precomp A)^-1 idmap).
pose proof (p:=eisretr (precomp A) idmap : g o f = idmap).
refine (isequiv_adjointify f g (ap10 _) (ap10 p)).
apply (equiv_inj (precomp B)).
unfold precomp; cbn.
exact (ap (fun k => f o k) p).
Defined.

Definition isequiv_isequiv_postcompose {A B : Type} (f : A -> B)
(postcomp := (fun (C : Type) (h : C -> A) => f o h))
(feq : forall C:Type, IsEquiv (postcomp C))
(Aeq : IsEquiv (postcomp A)) (Beq : IsEquiv (postcomp B))
: IsEquiv f.
(* TODO *)
*)

(** Equivalences between path spaces *)

(** If [f] is an equivalence, then so is [ap f]. We are lazy and use [adjointify]. *)
Global Instance isequiv_ap `{IsEquiv A B f} (x y : A)
: IsEquiv (@ap A B f x y) | 1000
:= isequiv_adjointify (ap f)
(fun q => (eissect f x)^ @ ap f^-1 q @ eissect f y)
(fun q =>
ap_pp f _ _
@ whiskerR (ap_pp f _ _) _
@ ((ap_V f _ @ inverse2 (eisadj f _)^)
@@ (ap_compose f^-1 f _)^
@@ (eisadj f _)^)
@ concat_pA1_p (eisretr f) _ _
@ whiskerR (concat_Vp _) _
@ concat_1p _)
(fun p =>
whiskerR (whiskerL _ (ap_compose f f^-1 _)^) _
@ concat_pA1_p (eissect f) _ _
@ whiskerR (concat_Vp _) _
@ concat_1p _).

Definition equiv_ap `(f : A -> B) `{IsEquiv A B f} (x y : A)
: (x = y) <~> (f x = f y)
:= Build_Equiv _ _ (ap f) _.

Global Arguments equiv_ap (A B)%type_scope f%function_scope _ _ _.

Definition equiv_ap' `(f : A <~> B) (x y : A)
: (x = y) <~> (f x = f y)
:= equiv_ap f x y.

(* TODO: Is this really necessary? *)
Definition equiv_inj `(f : A -> B) `{IsEquiv A B f} {x y : A}
: (f x = f y) -> (x = y)
:= (ap f)^-1.
Proof.
set (g:=(postcomp B)^-1 idmap).
pose proof (p:=eisretr (postcomp B) idmap : f o g = idmap).
refine (isequiv_adjointify f g (ap10 p) (ap10 _)).
apply (equiv_inj (postcomp A)).
unfold postcomp; cbn.
exact (ap (fun k => k o f) p).
Defined.

(** The inverse of an equivalence is an equivalence. *)
Global Instance isequiv_inverse {A B : Type} (f : A -> B) {feq : IsEquiv f}
Expand Down Expand Up @@ -431,7 +421,7 @@ Definition equiv_ap_inv' `(f : A <~> B) (x y : B)
Definition cancelR_isequiv {A B C} (f : A -> B) {g : B -> C}
`{IsEquiv A B f} `{IsEquiv A C (g o f)}
: IsEquiv g
:= isequiv_homotopic (compose (compose g f) f^-1)
:= isequiv_homotopic ((g o f) o f^-1)
(fun b => ap g (eisretr f b)).

Definition cancelR_equiv {A B C} (f : A -> B) {g : B -> C}
Expand All @@ -443,7 +433,7 @@ Definition cancelR_equiv {A B C} (f : A -> B) {g : B -> C}
Definition cancelL_isequiv {A B C} (g : B -> C) {f : A -> B}
`{IsEquiv B C g} `{IsEquiv A C (g o f)}
: IsEquiv f
:= isequiv_homotopic (compose g^-1 (compose g f))
:= isequiv_homotopic (g^-1 o (g o f))
(fun a => eissect g (f a)).

Definition cancelL_equiv {A B C} (g : B -> C) {f : A -> B}
Expand Down Expand Up @@ -560,12 +550,24 @@ Ltac equiv_via mid :=
(** It's often convenient when constructing a chain of equivalences to use [equiv_compose'], etc. But when we treat an [Equiv] object constructed in that way as a function, via the coercion [equiv_fun], Coq sometimes needs a little help to realize that the result is the same as ordinary composition. This tactic provides that help. *)
Ltac ev_equiv :=
repeat match goal with
| [ |- context[equiv_fun (equiv_inverse (equiv_inverse ?f))] ] =>
change (equiv_fun (equiv_inverse (equiv_inverse f))) with (equiv_fun f)
| [ |- context[(@equiv_inv ?B ?A (equiv_fun (equiv_inverse ?f)) ?iseq)] ] =>
change (@equiv_inv B A (equiv_fun (equiv_inverse f)) iseq) with (equiv_fun f)
| [ |- context[((equiv_fun ?f)^-1)^-1] ] =>
change ((equiv_fun f)^-1)^-1 with (equiv_fun f)
| [ |- context[equiv_fun (equiv_compose' ?g ?f) ?a] ] =>
change ((equiv_compose' g f) a) with (g (f a))
change (equiv_fun (equiv_compose' g f) a) with (g (f a))
| [ |- context[equiv_fun (equiv_compose ?g ?f) ?a] ] =>
change ((equiv_compose g f) a) with (g (f a))
change (equiv_fun (equiv_compose g f) a) with (g (f a))
| [ |- context[equiv_fun (equiv_inverse ?f) ?a] ] =>
change ((equiv_inverse f) a) with (f^-1 a)
change (equiv_fun (equiv_inverse f) a) with (f^-1 a)
| [ |- context[equiv_fun (equiv_compose' ?g ?f)] ] =>
change (equiv_fun (equiv_compose' g f)) with (g o f)
| [ |- context[equiv_fun (equiv_compose ?g ?f)] ] =>
change (equiv_fun (equiv_compose g f)) with (g o f)
| [ |- context[equiv_fun (equiv_inverse ?f)] ] =>
change (equiv_fun (equiv_inverse f)) with (f^-1)
end.

(** ** Building equivalences between nested sigma and record types *)
Expand Down

0 comments on commit ca9ef4b

Please sign in to comment.