2014-08-12 00:35:25 +00:00
|
|
|
|
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
|
|
|
|
-- Released under Apache 2.0 license as described in the file LICENSE.
|
2014-10-23 05:24:31 +00:00
|
|
|
|
-- Author: Jeremy Avigad, Jakob von Raumer
|
2014-08-12 00:35:25 +00:00
|
|
|
|
-- Ported from Coq HoTT
|
2014-11-03 19:41:42 +00:00
|
|
|
|
import .path .trunc
|
2014-10-23 02:08:47 +00:00
|
|
|
|
open path function
|
2014-08-12 00:35:25 +00:00
|
|
|
|
|
|
|
|
|
-- Equivalences
|
|
|
|
|
-- ------------
|
|
|
|
|
|
2014-09-17 21:39:05 +00:00
|
|
|
|
definition Sect {A B : Type} (s : A → B) (r : B → A) := Πx : A, r (s x) ≈ x
|
2014-08-12 00:35:25 +00:00
|
|
|
|
|
|
|
|
|
-- -- TODO: need better means of declaring structures
|
|
|
|
|
-- -- TODO: note that Coq allows projections to be declared to be coercions on the fly
|
|
|
|
|
|
|
|
|
|
-- Structure IsEquiv
|
|
|
|
|
|
2014-10-23 02:08:47 +00:00
|
|
|
|
inductive IsEquiv [class] {A B : Type} (f : A → B) :=
|
2014-08-22 22:46:10 +00:00
|
|
|
|
IsEquiv_mk : Π
|
2014-10-23 02:08:47 +00:00
|
|
|
|
(inv : B → A)
|
|
|
|
|
(retr : Sect inv f)
|
|
|
|
|
(sect : Sect f inv)
|
|
|
|
|
(adj : Πx, retr (f x) ≈ ap f (sect x)),
|
2014-08-12 00:35:25 +00:00
|
|
|
|
IsEquiv f
|
|
|
|
|
|
|
|
|
|
|
2014-10-23 02:08:47 +00:00
|
|
|
|
namespace IsEquiv
|
2014-08-12 00:35:25 +00:00
|
|
|
|
|
2014-11-04 05:09:43 +00:00
|
|
|
|
definition inv [coercion] {A B : Type} (f : A → B) [H : IsEquiv f] : B → A :=
|
2014-10-23 02:08:47 +00:00
|
|
|
|
IsEquiv.rec (λinv retr sect adj, inv) H
|
2014-08-12 00:35:25 +00:00
|
|
|
|
|
2014-10-23 02:08:47 +00:00
|
|
|
|
-- TODO: note: does not type check without giving the type
|
2014-11-04 05:09:43 +00:00
|
|
|
|
definition retr [coercion] {A B : Type} (f : A → B) [H : IsEquiv f] : Sect (inv f) f :=
|
2014-10-23 02:08:47 +00:00
|
|
|
|
IsEquiv.rec (λinv retr sect adj, retr) H
|
|
|
|
|
|
2014-11-04 05:09:43 +00:00
|
|
|
|
definition sect [coercion] {A B : Type} (f : A → B) [H : IsEquiv f] : Sect f (inv f) :=
|
2014-10-23 02:08:47 +00:00
|
|
|
|
IsEquiv.rec (λinv retr sect adj, sect) H
|
|
|
|
|
|
2014-11-04 05:09:43 +00:00
|
|
|
|
definition adj [coercion] {A B : Type} (f : A → B) [H : IsEquiv f] :
|
|
|
|
|
Πx, retr f (f x) ≈ ap f (sect f x) :=
|
2014-10-23 02:08:47 +00:00
|
|
|
|
IsEquiv.rec (λinv retr sect adj, adj) H
|
|
|
|
|
|
2014-11-04 05:09:43 +00:00
|
|
|
|
notation e `⁻¹` := inv e
|
|
|
|
|
|
2014-10-23 02:08:47 +00:00
|
|
|
|
end IsEquiv
|
2014-08-12 00:35:25 +00:00
|
|
|
|
|
|
|
|
|
-- Structure Equiv
|
|
|
|
|
|
|
|
|
|
inductive Equiv (A B : Type) : Type :=
|
2014-08-22 22:46:10 +00:00
|
|
|
|
Equiv_mk : Π
|
2014-08-12 00:35:25 +00:00
|
|
|
|
(equiv_fun : A → B)
|
|
|
|
|
(equiv_isequiv : IsEquiv equiv_fun),
|
|
|
|
|
Equiv A B
|
|
|
|
|
|
2014-10-23 02:08:47 +00:00
|
|
|
|
namespace Equiv
|
|
|
|
|
|
|
|
|
|
definition equiv_fun [coercion] {A B : Type} (e : Equiv A B) : A → B :=
|
|
|
|
|
Equiv.rec (λequiv_fun equiv_isequiv, equiv_fun) e
|
|
|
|
|
|
|
|
|
|
definition equiv_isequiv [coercion] {A B : Type} (e : Equiv A B) : IsEquiv (equiv_fun e) :=
|
|
|
|
|
Equiv.rec (λequiv_fun equiv_isequiv, equiv_isequiv) e
|
|
|
|
|
|
|
|
|
|
infix `≃`:25 := Equiv
|
|
|
|
|
|
|
|
|
|
end Equiv
|
|
|
|
|
|
|
|
|
|
-- Some instances and closure properties of equivalences
|
|
|
|
|
|
|
|
|
|
namespace IsEquiv
|
|
|
|
|
variables {A B C : Type} {f : A → B} {g : B → C} {f' : A → B}
|
|
|
|
|
|
|
|
|
|
-- The identity function is an equivalence.
|
|
|
|
|
|
2014-10-23 03:25:12 +00:00
|
|
|
|
definition id_closed [instance] : (@IsEquiv A A id) := IsEquiv_mk id (λa, idp) (λa, idp) (λa, idp)
|
2014-10-23 02:08:47 +00:00
|
|
|
|
|
|
|
|
|
-- The composition of two equivalences is, again, an equivalence.
|
|
|
|
|
|
2014-11-04 05:09:43 +00:00
|
|
|
|
definition comp_closed (Hf : IsEquiv f) (Hg : IsEquiv g) : (IsEquiv (g ∘ f)) :=
|
|
|
|
|
IsEquiv_mk ((inv f) ∘ (inv g))
|
|
|
|
|
(λc, ap g (retr f (g⁻¹ c)) ⬝ retr g c)
|
|
|
|
|
(λa, ap (inv f) (sect g (f a)) ⬝ sect f a)
|
|
|
|
|
(λa, (whiskerL _ (adj g (f a))) ⬝
|
2014-10-23 05:24:31 +00:00
|
|
|
|
(ap_pp g _ _)⁻¹ ⬝
|
2014-11-04 05:09:43 +00:00
|
|
|
|
ap02 g (concat_A1p (retr f) (sect g (f a))⁻¹ ⬝
|
|
|
|
|
(ap_compose (inv f) f _ ◾ adj f a) ⬝
|
2014-10-23 05:24:31 +00:00
|
|
|
|
(ap_pp f _ _)⁻¹
|
|
|
|
|
) ⬝
|
|
|
|
|
(ap_compose f g _)⁻¹
|
|
|
|
|
)
|
2014-10-23 02:08:47 +00:00
|
|
|
|
|
|
|
|
|
-- Any function equal to an equivalence is an equivlance as well.
|
|
|
|
|
definition path_closed (Hf : IsEquiv f) (Heq : f ≈ f') : (IsEquiv f') :=
|
2014-10-25 20:36:38 +00:00
|
|
|
|
path.rec_on Heq Hf
|
2014-10-23 02:08:47 +00:00
|
|
|
|
|
|
|
|
|
-- Any function pointwise equal to an equivalence is an equivalence as well.
|
|
|
|
|
definition homotopic (Hf : IsEquiv f) (Heq : f ∼ f') : (IsEquiv f') :=
|
2014-11-04 05:09:43 +00:00
|
|
|
|
let sect' := (λ b, (Heq (inv f b))⁻¹ ⬝ retr f b) in
|
|
|
|
|
let retr' := (λ a, (ap (inv f) (Heq a))⁻¹ ⬝ sect f a) in
|
2014-10-23 02:08:47 +00:00
|
|
|
|
let adj' := (λ (a : A),
|
|
|
|
|
let ff'a := Heq a in
|
2014-11-04 05:09:43 +00:00
|
|
|
|
let invf := inv f in
|
|
|
|
|
let secta := sect f a in
|
|
|
|
|
let retrfa := retr f (f a) in
|
|
|
|
|
let retrf'a := retr f (f' a) in
|
2014-10-23 03:25:12 +00:00
|
|
|
|
have eq1 : _ ≈ _,
|
|
|
|
|
from calc ap f secta ⬝ ff'a
|
2014-11-04 05:09:43 +00:00
|
|
|
|
≈ retrfa ⬝ ff'a : (ap _ (adj f _ ))⁻¹
|
2014-10-23 03:25:12 +00:00
|
|
|
|
... ≈ ap (f ∘ invf) ff'a ⬝ retrf'a : !concat_A1p⁻¹
|
2014-11-04 05:09:43 +00:00
|
|
|
|
... ≈ ap f (ap invf ff'a) ⬝ retr f (f' a) : {ap_compose invf f _},
|
2014-10-23 03:25:12 +00:00
|
|
|
|
have eq2 : _ ≈ _,
|
2014-10-23 02:08:47 +00:00
|
|
|
|
from calc retrf'a
|
2014-10-23 03:25:12 +00:00
|
|
|
|
≈ (ap f (ap invf ff'a))⁻¹ ⬝ (ap f secta ⬝ ff'a) : moveL_Vp _ _ _ (eq1⁻¹)
|
|
|
|
|
... ≈ ap f (ap invf ff'a)⁻¹ ⬝ (ap f secta ⬝ Heq a) : {ap_V invf ff'a}
|
|
|
|
|
... ≈ ap f (ap invf ff'a)⁻¹ ⬝ (Heq (invf (f a)) ⬝ ap f' secta) : {!concat_Ap}
|
|
|
|
|
... ≈ (ap f (ap invf ff'a)⁻¹ ⬝ Heq (invf (f a))) ⬝ ap f' secta : {!concat_pp_p⁻¹}
|
|
|
|
|
... ≈ (ap f ((ap invf ff'a)⁻¹) ⬝ Heq (invf (f a))) ⬝ ap f' secta : {!ap_V⁻¹}
|
|
|
|
|
... ≈ (Heq (invf (f' a)) ⬝ ap f' ((ap invf ff'a)⁻¹)) ⬝ ap f' secta : {!concat_Ap}
|
|
|
|
|
... ≈ (Heq (invf (f' a)) ⬝ (ap f' (ap invf ff'a))⁻¹) ⬝ ap f' secta : {!ap_V}
|
|
|
|
|
... ≈ Heq (invf (f' a)) ⬝ ((ap f' (ap invf ff'a))⁻¹ ⬝ ap f' secta) : !concat_pp_p,
|
|
|
|
|
have eq3 : _ ≈ _,
|
2014-11-04 05:09:43 +00:00
|
|
|
|
from calc (Heq (invf (f' a)))⁻¹ ⬝ retr f (f' a)
|
2014-10-23 03:25:12 +00:00
|
|
|
|
≈ (ap f' (ap invf ff'a))⁻¹ ⬝ ap f' secta : moveR_Vp _ _ _ eq2
|
|
|
|
|
... ≈ (ap f' ((ap invf ff'a)⁻¹)) ⬝ ap f' secta : {!ap_V⁻¹}
|
|
|
|
|
... ≈ ap f' ((ap invf ff'a)⁻¹ ⬝ secta) : !ap_pp⁻¹,
|
2014-10-23 02:08:47 +00:00
|
|
|
|
eq3) in
|
2014-11-04 05:09:43 +00:00
|
|
|
|
IsEquiv_mk (inv f) sect' retr' adj'
|
2014-10-24 23:19:50 +00:00
|
|
|
|
end IsEquiv
|
|
|
|
|
|
|
|
|
|
namespace IsEquiv
|
2014-10-23 05:24:31 +00:00
|
|
|
|
|
2014-10-24 23:19:50 +00:00
|
|
|
|
variables {A B : Type} (f : A → B) (g : B → A)
|
2014-11-04 05:09:43 +00:00
|
|
|
|
(ret : Sect g f) (sec : Sect f g)
|
2014-10-24 23:19:50 +00:00
|
|
|
|
|
2014-10-28 23:08:39 +00:00
|
|
|
|
context
|
|
|
|
|
set_option unifier.max_steps 30000
|
2014-10-24 23:19:50 +00:00
|
|
|
|
--To construct an equivalence it suffices to state the proof that the inverse is a quasi-inverse.
|
|
|
|
|
definition adjointify : IsEquiv f :=
|
2014-11-04 05:09:43 +00:00
|
|
|
|
let sect' := (λx, ap g (ap f (inverse (sec x))) ⬝ ap g (ret (f x)) ⬝ sec x) in
|
2014-10-24 23:19:50 +00:00
|
|
|
|
let adj' := (λ (a : A),
|
2014-11-04 05:09:43 +00:00
|
|
|
|
let fgretrfa := ap f (ap g (ret (f a))) in
|
|
|
|
|
let fgfinvsect := ap f (ap g (ap f ((sec a)⁻¹))) in
|
2014-10-24 23:19:50 +00:00
|
|
|
|
let fgfa := f (g (f a)) in
|
2014-11-04 05:09:43 +00:00
|
|
|
|
let retrfa := ret (f a) in
|
|
|
|
|
have eq1 : ap f (sec a) ≈ _,
|
|
|
|
|
from calc ap f (sec a)
|
|
|
|
|
≈ idp ⬝ ap f (sec a) : !concat_1p⁻¹
|
|
|
|
|
... ≈ (ret (f a) ⬝ (ret (f a)⁻¹)) ⬝ ap f (sec a) : {!concat_pV⁻¹}
|
|
|
|
|
... ≈ ((ret (fgfa))⁻¹ ⬝ ap (f ∘ g) (ret (f a))) ⬝ ap f (sec a) : {!concat_pA1⁻¹}
|
|
|
|
|
... ≈ ((ret (fgfa))⁻¹ ⬝ fgretrfa) ⬝ ap f (sec a) : {ap_compose g f _}
|
|
|
|
|
... ≈ (ret (fgfa))⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a)) : !concat_pp_p,
|
|
|
|
|
have eq2 : ap f (sec a) ⬝ idp ≈ (ret fgfa)⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a)),
|
|
|
|
|
from !concat_p1 ⬝ eq1,
|
2014-10-24 23:19:50 +00:00
|
|
|
|
have eq3 : idp ≈ _,
|
|
|
|
|
from calc idp
|
2014-11-04 05:09:43 +00:00
|
|
|
|
≈ (ap f (sec a))⁻¹ ⬝ ((ret fgfa)⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a))) : moveL_Vp _ _ _ eq2
|
|
|
|
|
... ≈ (ap f (sec a)⁻¹ ⬝ (ret fgfa)⁻¹) ⬝ (fgretrfa ⬝ ap f (sec a)) : !concat_p_pp
|
|
|
|
|
... ≈ (ap f ((sec a)⁻¹) ⬝ (ret fgfa)⁻¹) ⬝ (fgretrfa ⬝ ap f (sec a)) : {!ap_V⁻¹}
|
|
|
|
|
... ≈ ((ap f ((sec a)⁻¹) ⬝ (ret fgfa)⁻¹) ⬝ fgretrfa) ⬝ ap f (sec a) : !concat_p_pp
|
|
|
|
|
... ≈ ((retrfa⁻¹ ⬝ ap (f ∘ g) (ap f ((sec a)⁻¹))) ⬝ fgretrfa) ⬝ ap f (sec a) : {!concat_pA1⁻¹}
|
|
|
|
|
... ≈ ((retrfa⁻¹ ⬝ fgfinvsect) ⬝ fgretrfa) ⬝ ap f (sec a) : {ap_compose g f _}
|
|
|
|
|
... ≈ (retrfa⁻¹ ⬝ (fgfinvsect ⬝ fgretrfa)) ⬝ ap f (sec a) : {!concat_p_pp⁻¹}
|
|
|
|
|
... ≈ retrfa⁻¹ ⬝ ap f (ap g (ap f ((sec a)⁻¹)) ⬝ ap g (ret (f a))) ⬝ ap f (sec a) : {!ap_pp⁻¹}
|
|
|
|
|
... ≈ retrfa⁻¹ ⬝ (ap f (ap g (ap f ((sec a)⁻¹)) ⬝ ap g (ret (f a))) ⬝ ap f (sec a)) : !concat_p_pp⁻¹
|
|
|
|
|
... ≈ retrfa⁻¹ ⬝ ap f ((ap g (ap f ((sec a)⁻¹)) ⬝ ap g (ret (f a))) ⬝ sec a) : {!ap_pp⁻¹},
|
|
|
|
|
have eq4 : ret (f a) ≈ ap f ((ap g (ap f ((sec a)⁻¹)) ⬝ ap g (ret (f a))) ⬝ sec a),
|
2014-10-24 23:19:50 +00:00
|
|
|
|
from moveR_M1 _ _ eq3,
|
|
|
|
|
eq4) in
|
2014-11-04 05:09:43 +00:00
|
|
|
|
IsEquiv_mk g ret sect' adj'
|
2014-10-28 23:08:39 +00:00
|
|
|
|
end
|
2014-10-24 23:19:50 +00:00
|
|
|
|
end IsEquiv
|
|
|
|
|
|
|
|
|
|
namespace IsEquiv
|
2014-11-04 05:09:43 +00:00
|
|
|
|
variables {A B: Type} {f : A → B}
|
|
|
|
|
|
2014-10-24 23:19:50 +00:00
|
|
|
|
--The inverse of an equivalence is, again, an equivalence.
|
2014-11-04 05:09:43 +00:00
|
|
|
|
definition inv_closed (Hf : IsEquiv f) : (IsEquiv (inv f)) :=
|
|
|
|
|
adjointify (inv f) f (sect f) (retr f)
|
2014-10-24 23:19:50 +00:00
|
|
|
|
|
|
|
|
|
end IsEquiv
|
|
|
|
|
|
|
|
|
|
namespace IsEquiv
|
|
|
|
|
variables {A B C : Type} {f : A → B} {g : B → C} {f' : A → B}
|
2014-10-23 02:08:47 +00:00
|
|
|
|
|
|
|
|
|
definition cancel_R (Hf : IsEquiv f) (Hgf : IsEquiv (g ∘ f)) : (IsEquiv g) :=
|
2014-11-04 05:09:43 +00:00
|
|
|
|
homotopic (comp_closed (inv_closed Hf) Hgf) (λb, ap g (retr f b))
|
2014-10-23 02:08:47 +00:00
|
|
|
|
|
|
|
|
|
definition cancel_L (Hg : IsEquiv g) (Hgf : IsEquiv (g ∘ f)) : (IsEquiv f) :=
|
2014-11-04 05:09:43 +00:00
|
|
|
|
homotopic (comp_closed Hgf (inv_closed Hg)) (λa, sect g (f a))
|
2014-10-23 02:08:47 +00:00
|
|
|
|
|
2014-11-03 19:41:42 +00:00
|
|
|
|
--Transporting is an equivalence
|
|
|
|
|
definition transport [instance] (P : A → Type) {x y : A} (p : x ≈ y) : (IsEquiv (transport P p)) :=
|
2014-10-23 03:25:12 +00:00
|
|
|
|
IsEquiv_mk (transport P (p⁻¹)) (transport_pV P p) (transport_Vp P p) (transport_pVp P p)
|
2014-10-23 02:08:47 +00:00
|
|
|
|
|
|
|
|
|
--Rewrite rules
|
|
|
|
|
section
|
2014-11-04 05:09:43 +00:00
|
|
|
|
variables (Hf : IsEquiv f)
|
2014-10-23 05:24:31 +00:00
|
|
|
|
|
2014-11-04 05:09:43 +00:00
|
|
|
|
definition moveR_M (Hf : IsEquiv f) {x : A} {y : B} (p : x ≈ (inv f) y) : (f x ≈ y) :=
|
|
|
|
|
(ap f p) ⬝ (retr f y)
|
2014-10-23 02:08:47 +00:00
|
|
|
|
|
2014-11-04 05:09:43 +00:00
|
|
|
|
definition moveL_M (Hf : IsEquiv f) {x : A} {y : B} (p : (inv f) y ≈ x) : (y ≈ f x) :=
|
|
|
|
|
(moveR_M Hf (p⁻¹))⁻¹
|
2014-10-23 02:08:47 +00:00
|
|
|
|
|
2014-11-04 05:09:43 +00:00
|
|
|
|
definition moveR_V (Hf : IsEquiv f) {x : B} {y : A} (p : x ≈ f y) : (inv f) x ≈ y :=
|
|
|
|
|
ap (inv f) p ⬝ sect f y
|
2014-10-23 02:08:47 +00:00
|
|
|
|
|
2014-11-04 05:09:43 +00:00
|
|
|
|
definition moveL_V (Hf : IsEquiv f) {x : B} {y : A} (p : f y ≈ x) : y ≈ (inv f) x :=
|
|
|
|
|
(moveR_V Hf (p⁻¹))⁻¹
|
2014-10-23 05:24:31 +00:00
|
|
|
|
|
2014-11-04 05:09:43 +00:00
|
|
|
|
definition contr (Hf : IsEquiv f) (HA: Contr A) : (Contr B) :=
|
|
|
|
|
Contr.Contr_mk (f (center HA)) (λb, moveR_M Hf (contr HA (inv f b)))
|
2014-11-03 19:41:42 +00:00
|
|
|
|
|
2014-11-05 00:50:30 +00:00
|
|
|
|
definition ap (Hf : IsEquiv f) (x y : A) : IsEquiv (@ap A B f x y) :=
|
|
|
|
|
adjointify (ap f)
|
2014-11-05 01:03:12 +00:00
|
|
|
|
(λq, (inverse (sect f x)) ⬝ ap (f⁻¹) q ⬝ sect f y)
|
|
|
|
|
(λq, !ap_pp
|
|
|
|
|
⬝ whiskerR !ap_pp _
|
|
|
|
|
⬝ ((!ap_V ⬝ inverse2 ((adj f _)⁻¹))
|
2014-11-05 00:50:30 +00:00
|
|
|
|
◾ (inverse (ap_compose (f⁻¹) f _))
|
|
|
|
|
◾ (adj f _)⁻¹)
|
|
|
|
|
⬝ concat_pA1_p (retr f) _ _
|
2014-11-05 01:03:12 +00:00
|
|
|
|
⬝ whiskerR !concat_Vp _
|
|
|
|
|
⬝ !concat_1p)
|
|
|
|
|
(λp, whiskerR (whiskerL _ ((ap_compose f (f⁻¹) _)⁻¹)) _
|
2014-11-05 00:50:30 +00:00
|
|
|
|
⬝ concat_pA1_p (sect f) _ _
|
2014-11-05 01:03:12 +00:00
|
|
|
|
⬝ whiskerR !concat_Vp _
|
|
|
|
|
⬝ !concat_1p)
|
2014-11-05 00:50:30 +00:00
|
|
|
|
|
2014-11-03 19:41:42 +00:00
|
|
|
|
end
|
|
|
|
|
|
2014-10-23 02:08:47 +00:00
|
|
|
|
end IsEquiv
|
|
|
|
|
|
|
|
|
|
namespace Equiv
|
|
|
|
|
variables {A B C : Type} (eqf : A ≃ B)
|
|
|
|
|
|
2014-11-04 05:09:43 +00:00
|
|
|
|
definition f : A → B := equiv_fun eqf
|
|
|
|
|
|
2014-11-03 19:41:42 +00:00
|
|
|
|
definition id : A ≃ A := Equiv_mk id IsEquiv.id_closed
|
2014-10-23 02:08:47 +00:00
|
|
|
|
|
|
|
|
|
theorem compose (eqg: B ≃ C) : A ≃ C :=
|
|
|
|
|
Equiv_mk ((equiv_fun eqg) ∘ (equiv_fun eqf))
|
2014-10-23 05:24:31 +00:00
|
|
|
|
(IsEquiv.comp_closed (equiv_isequiv eqf) (equiv_isequiv eqg))
|
2014-10-23 02:08:47 +00:00
|
|
|
|
|
|
|
|
|
theorem path_closed (f' : A → B) (Heq : equiv_fun eqf ≈ f') : A ≃ B :=
|
|
|
|
|
Equiv_mk f' (IsEquiv.path_closed (equiv_isequiv eqf) Heq)
|
|
|
|
|
|
|
|
|
|
theorem inv_closed : B ≃ A :=
|
2014-11-04 05:09:43 +00:00
|
|
|
|
Equiv_mk (@IsEquiv.inv _ _ (equiv_fun eqf) (equiv_isequiv eqf))
|
|
|
|
|
(IsEquiv.inv_closed (equiv_isequiv eqf))
|
2014-10-23 02:08:47 +00:00
|
|
|
|
|
2014-10-23 05:24:31 +00:00
|
|
|
|
theorem cancel_L {f : A → B} {g : B → C}
|
2014-10-23 02:08:47 +00:00
|
|
|
|
(Hf : IsEquiv f) (Hgf : IsEquiv (g ∘ f)) : B ≃ C :=
|
|
|
|
|
Equiv_mk g (IsEquiv.cancel_R _ _)
|
2014-10-23 05:24:31 +00:00
|
|
|
|
|
2014-10-23 02:08:47 +00:00
|
|
|
|
theorem cancel_R {f : A → B} {g : B → C}
|
|
|
|
|
(Hg : IsEquiv g) (Hgf : IsEquiv (g ∘ f)) : A ≃ B :=
|
|
|
|
|
Equiv_mk f (!IsEquiv.cancel_L _ _)
|
2014-08-12 00:35:25 +00:00
|
|
|
|
|
2014-10-23 02:08:47 +00:00
|
|
|
|
theorem transport (P : A → Type) {x y : A} {p : x ≈ y} : (P x) ≃ (P y) :=
|
|
|
|
|
Equiv_mk (transport P p) (IsEquiv.transport P p)
|
2014-08-12 00:35:25 +00:00
|
|
|
|
|
2014-11-03 19:41:42 +00:00
|
|
|
|
theorem contr_closed (HA: Contr A) : (Contr B) :=
|
|
|
|
|
@IsEquiv.contr A B (equiv_fun eqf) (equiv_isequiv eqf) HA
|
|
|
|
|
|
|
|
|
|
end Equiv
|
|
|
|
|
|
|
|
|
|
namespace Equiv
|
|
|
|
|
variables {A B : Type} {HA : Contr A} {HB : Contr B}
|
|
|
|
|
|
|
|
|
|
--Each two contractible types are equivalent.
|
|
|
|
|
definition contr_contr : A ≃ B :=
|
|
|
|
|
Equiv_mk
|
|
|
|
|
(λa, center HB)
|
|
|
|
|
(IsEquiv.adjointify (λa, center HB) (λb, center HA)
|
|
|
|
|
(contr HB) (contr HA))
|
|
|
|
|
|
2014-10-23 02:08:47 +00:00
|
|
|
|
end Equiv
|