2015-02-21 00:30:32 +00:00
|
|
|
|
/-
|
|
|
|
|
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
|
|
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
|
|
|
Author: Jeremy Avigad, Jakob von Raumer
|
|
|
|
|
|
|
|
|
|
Ported from Coq HoTT
|
|
|
|
|
-/
|
|
|
|
|
|
2014-12-12 18:17:50 +00:00
|
|
|
|
prelude
|
|
|
|
|
import .path .function
|
|
|
|
|
open eq function
|
2014-12-12 04:14:53 +00:00
|
|
|
|
|
2015-02-21 00:30:32 +00:00
|
|
|
|
/- Equivalences -/
|
2014-12-12 04:14:53 +00:00
|
|
|
|
|
|
|
|
|
-- This is our definition of equivalence. In the HoTT-book it's called
|
|
|
|
|
-- ihae (half-adjoint equivalence).
|
|
|
|
|
structure is_equiv [class] {A B : Type} (f : A → B) :=
|
2015-04-24 22:51:16 +00:00
|
|
|
|
mk' ::
|
2014-12-12 04:14:53 +00:00
|
|
|
|
(inv : B → A)
|
2015-04-27 19:39:36 +00:00
|
|
|
|
(right_inv : (f ∘ inv) ∼ id)
|
|
|
|
|
(left_inv : (inv ∘ f) ∼ id)
|
|
|
|
|
(adj : Πx, right_inv (f x) = ap f (left_inv x))
|
2014-12-12 04:14:53 +00:00
|
|
|
|
|
2015-03-05 06:20:20 +00:00
|
|
|
|
attribute is_equiv.inv [quasireducible]
|
2014-12-12 04:14:53 +00:00
|
|
|
|
|
2015-02-21 00:30:32 +00:00
|
|
|
|
-- A more bundled version of equivalence
|
2014-12-12 04:14:53 +00:00
|
|
|
|
structure equiv (A B : Type) :=
|
|
|
|
|
(to_fun : A → B)
|
|
|
|
|
(to_is_equiv : is_equiv to_fun)
|
|
|
|
|
|
|
|
|
|
|
2015-02-21 00:30:32 +00:00
|
|
|
|
namespace is_equiv
|
|
|
|
|
/- Some instances and closure properties of equivalences -/
|
2014-12-12 04:14:53 +00:00
|
|
|
|
postfix `⁻¹` := inv
|
2015-04-24 22:51:16 +00:00
|
|
|
|
/- a second notation for the inverse, which is not overloaded -/
|
2015-05-14 02:01:48 +00:00
|
|
|
|
postfix [parsing-only] `⁻¹ᶠ`:std.prec.max_plus := inv
|
2014-12-12 04:14:53 +00:00
|
|
|
|
|
2015-02-21 00:30:32 +00:00
|
|
|
|
section
|
2014-12-12 04:14:53 +00:00
|
|
|
|
variables {A B C : Type} (f : A → B) (g : B → C) {f' : A → B}
|
|
|
|
|
|
2015-04-24 22:51:16 +00:00
|
|
|
|
-- The variant of mk' where f is explicit.
|
2015-05-14 02:01:48 +00:00
|
|
|
|
protected abbreviation mk [constructor] := @is_equiv.mk' A B f
|
2015-04-24 22:51:16 +00:00
|
|
|
|
|
2014-12-12 04:14:53 +00:00
|
|
|
|
-- The identity function is an equivalence.
|
2015-04-24 22:51:16 +00:00
|
|
|
|
definition is_equiv_id (A : Type) : (@is_equiv A A id) :=
|
|
|
|
|
is_equiv.mk id id (λa, idp) (λa, idp) (λa, idp)
|
2014-12-12 04:14:53 +00:00
|
|
|
|
|
|
|
|
|
-- The composition of two equivalences is, again, an equivalence.
|
2015-03-03 21:37:38 +00:00
|
|
|
|
definition is_equiv_compose [Hf : is_equiv f] [Hg : is_equiv g] : is_equiv (g ∘ f) :=
|
2015-04-24 22:51:16 +00:00
|
|
|
|
is_equiv.mk (g ∘ f) (f⁻¹ ∘ g⁻¹)
|
2015-04-27 19:39:36 +00:00
|
|
|
|
(λc, ap g (right_inv f (g⁻¹ c)) ⬝ right_inv g c)
|
|
|
|
|
(λa, ap (inv f) (left_inv g (f a)) ⬝ left_inv f a)
|
2015-02-21 00:30:32 +00:00
|
|
|
|
(λa, (whisker_left _ (adj g (f a))) ⬝
|
|
|
|
|
(ap_con g _ _)⁻¹ ⬝
|
2015-04-27 19:39:36 +00:00
|
|
|
|
ap02 g ((ap_con_eq_con (right_inv f) (left_inv g (f a)))⁻¹ ⬝
|
2014-12-12 04:14:53 +00:00
|
|
|
|
(ap_compose (inv f) f _ ◾ adj f a) ⬝
|
2015-02-21 00:30:32 +00:00
|
|
|
|
(ap_con f _ _)⁻¹
|
2014-12-12 04:14:53 +00:00
|
|
|
|
) ⬝
|
|
|
|
|
(ap_compose f g _)⁻¹
|
|
|
|
|
)
|
|
|
|
|
|
|
|
|
|
-- Any function equal to an equivalence is an equivlance as well.
|
2015-05-02 21:17:50 +00:00
|
|
|
|
variable {f}
|
2015-02-21 00:30:32 +00:00
|
|
|
|
definition is_equiv_eq_closed [Hf : is_equiv f] (Heq : f = f') : (is_equiv f') :=
|
2014-12-12 18:17:50 +00:00
|
|
|
|
eq.rec_on Heq Hf
|
2014-12-12 04:14:53 +00:00
|
|
|
|
|
|
|
|
|
-- Any function pointwise equal to an equivalence is an equivalence as well.
|
|
|
|
|
definition homotopy_closed [Hf : is_equiv f] (Hty : f ∼ f') : (is_equiv f') :=
|
2015-04-27 19:39:36 +00:00
|
|
|
|
let sect' := (λ b, (Hty (inv f b))⁻¹ ⬝ right_inv f b) in
|
|
|
|
|
let retr' := (λ a, (ap (inv f) (Hty a))⁻¹ ⬝ left_inv f a) in
|
2014-12-12 04:14:53 +00:00
|
|
|
|
let adj' := (λ (a : A),
|
|
|
|
|
let ff'a := Hty a in
|
|
|
|
|
let invf := inv f in
|
2015-04-27 19:39:36 +00:00
|
|
|
|
let secta := left_inv f a in
|
|
|
|
|
let retrfa := right_inv f (f a) in
|
|
|
|
|
let retrf'a := right_inv f (f' a) in
|
2014-12-12 18:17:50 +00:00
|
|
|
|
have eq1 : _ = _,
|
2014-12-12 04:14:53 +00:00
|
|
|
|
from calc ap f secta ⬝ ff'a
|
2015-03-13 00:25:31 +00:00
|
|
|
|
= retrfa ⬝ ff'a : by rewrite adj
|
|
|
|
|
... = ap (f ∘ invf) ff'a ⬝ retrf'a : by rewrite ap_con_eq_con
|
|
|
|
|
... = ap f (ap invf ff'a) ⬝ retrf'a : by rewrite ap_compose,
|
2014-12-12 18:17:50 +00:00
|
|
|
|
have eq2 : _ = _,
|
2014-12-12 04:14:53 +00:00
|
|
|
|
from calc retrf'a
|
2015-04-24 21:00:32 +00:00
|
|
|
|
= (ap f (ap invf ff'a))⁻¹ ⬝ (ap f secta ⬝ ff'a) : eq_inv_con_of_con_eq eq1⁻¹
|
2015-02-28 00:02:18 +00:00
|
|
|
|
... = (ap f (ap invf ff'a))⁻¹ ⬝ (ap f secta ⬝ Hty a) : ap_inv invf ff'a
|
2015-03-13 00:25:31 +00:00
|
|
|
|
... = (ap f (ap invf ff'a))⁻¹ ⬝ (Hty (invf (f a)) ⬝ ap f' secta) : by rewrite ap_con_eq_con_ap
|
|
|
|
|
... = ((ap f (ap invf ff'a))⁻¹ ⬝ Hty (invf (f a))) ⬝ ap f' secta : by rewrite con.assoc
|
|
|
|
|
... = (ap f (ap invf ff'a)⁻¹ ⬝ Hty (invf (f a))) ⬝ ap f' secta : by rewrite ap_inv
|
|
|
|
|
... = (Hty (invf (f' a)) ⬝ ap f' (ap invf ff'a)⁻¹) ⬝ ap f' secta : by rewrite ap_con_eq_con_ap
|
|
|
|
|
... = (Hty (invf (f' a)) ⬝ (ap f' (ap invf ff'a))⁻¹) ⬝ ap f' secta : by rewrite ap_inv
|
|
|
|
|
... = Hty (invf (f' a)) ⬝ ((ap f' (ap invf ff'a))⁻¹ ⬝ ap f' secta) : by rewrite con.assoc,
|
2014-12-12 18:17:50 +00:00
|
|
|
|
have eq3 : _ = _,
|
2014-12-12 04:14:53 +00:00
|
|
|
|
from calc (Hty (invf (f' a)))⁻¹ ⬝ retrf'a
|
2015-04-24 21:00:32 +00:00
|
|
|
|
= (ap f' (ap invf ff'a))⁻¹ ⬝ ap f' secta : inv_con_eq_of_eq_con eq2
|
2015-03-13 00:25:31 +00:00
|
|
|
|
... = (ap f' (ap invf ff'a)⁻¹) ⬝ ap f' secta : by rewrite ap_inv
|
|
|
|
|
... = ap f' ((ap invf ff'a)⁻¹ ⬝ secta) : by rewrite ap_con,
|
2014-12-12 04:14:53 +00:00
|
|
|
|
eq3) in
|
2015-04-24 22:51:16 +00:00
|
|
|
|
is_equiv.mk f' (inv f) sect' retr' adj'
|
2015-02-21 00:30:32 +00:00
|
|
|
|
end
|
2014-12-12 04:14:53 +00:00
|
|
|
|
|
2015-04-22 02:17:59 +00:00
|
|
|
|
section
|
2014-12-12 04:14:53 +00:00
|
|
|
|
parameters {A B : Type} (f : A → B) (g : B → A)
|
|
|
|
|
(ret : f ∘ g ∼ id) (sec : g ∘ f ∼ id)
|
|
|
|
|
|
2015-02-21 00:30:32 +00:00
|
|
|
|
private definition adjointify_sect' : g ∘ f ∼ id :=
|
2014-12-12 04:14:53 +00:00
|
|
|
|
(λx, ap g (ap f (inverse (sec x))) ⬝ ap g (ret (f x)) ⬝ sec x)
|
|
|
|
|
|
2015-02-21 00:30:32 +00:00
|
|
|
|
private definition adjointify_adj' : Π (x : A), ret (f x) = ap f (adjointify_sect' x) :=
|
2014-12-12 04:14:53 +00:00
|
|
|
|
(λ (a : A),
|
|
|
|
|
let fgretrfa := ap f (ap g (ret (f a))) in
|
2015-02-28 00:02:18 +00:00
|
|
|
|
let fgfinvsect := ap f (ap g (ap f (sec a)⁻¹)) in
|
2014-12-12 04:14:53 +00:00
|
|
|
|
let fgfa := f (g (f a)) in
|
|
|
|
|
let retrfa := ret (f a) in
|
2014-12-12 18:17:50 +00:00
|
|
|
|
have eq1 : ap f (sec a) = _,
|
2014-12-12 04:14:53 +00:00
|
|
|
|
from calc ap f (sec a)
|
2015-03-13 00:25:31 +00:00
|
|
|
|
= idp ⬝ ap f (sec a) : by rewrite idp_con
|
|
|
|
|
... = (ret (f a) ⬝ (ret (f a))⁻¹) ⬝ ap f (sec a) : by rewrite con.right_inv
|
|
|
|
|
... = ((ret fgfa)⁻¹ ⬝ ap (f ∘ g) (ret (f a))) ⬝ ap f (sec a) : by rewrite con_ap_eq_con
|
|
|
|
|
... = ((ret fgfa)⁻¹ ⬝ fgretrfa) ⬝ ap f (sec a) : by rewrite ap_compose
|
|
|
|
|
... = (ret fgfa)⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a)) : by rewrite con.assoc,
|
2014-12-12 18:17:50 +00:00
|
|
|
|
have eq2 : ap f (sec a) ⬝ idp = (ret fgfa)⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a)),
|
2015-02-21 00:30:32 +00:00
|
|
|
|
from !con_idp ⬝ eq1,
|
2014-12-12 18:17:50 +00:00
|
|
|
|
have eq3 : idp = _,
|
2014-12-12 04:14:53 +00:00
|
|
|
|
from calc idp
|
2015-04-24 21:00:32 +00:00
|
|
|
|
= (ap f (sec a))⁻¹ ⬝ ((ret fgfa)⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a))) : eq_inv_con_of_con_eq eq2
|
2015-03-13 00:25:31 +00:00
|
|
|
|
... = ((ap f (sec a))⁻¹ ⬝ (ret fgfa)⁻¹) ⬝ (fgretrfa ⬝ ap f (sec a)) : by rewrite con.assoc'
|
|
|
|
|
... = (ap f (sec a)⁻¹ ⬝ (ret fgfa)⁻¹) ⬝ (fgretrfa ⬝ ap f (sec a)) : by rewrite ap_inv
|
|
|
|
|
... = ((ap f (sec a)⁻¹ ⬝ (ret fgfa)⁻¹) ⬝ fgretrfa) ⬝ ap f (sec a) : by rewrite con.assoc'
|
|
|
|
|
... = ((retrfa⁻¹ ⬝ ap (f ∘ g) (ap f (sec a)⁻¹)) ⬝ fgretrfa) ⬝ ap f (sec a) : by rewrite con_ap_eq_con
|
|
|
|
|
... = ((retrfa⁻¹ ⬝ fgfinvsect) ⬝ fgretrfa) ⬝ ap f (sec a) : by rewrite ap_compose
|
|
|
|
|
... = (retrfa⁻¹ ⬝ (fgfinvsect ⬝ fgretrfa)) ⬝ ap f (sec a) : by rewrite con.assoc'
|
|
|
|
|
... = retrfa⁻¹ ⬝ ap f (ap g (ap f (sec a)⁻¹) ⬝ ap g (ret (f a))) ⬝ ap f (sec a) : by rewrite ap_con
|
|
|
|
|
... = retrfa⁻¹ ⬝ (ap f (ap g (ap f (sec a)⁻¹) ⬝ ap g (ret (f a))) ⬝ ap f (sec a)) : by rewrite con.assoc'
|
|
|
|
|
... = retrfa⁻¹ ⬝ ap f ((ap g (ap f (sec a)⁻¹) ⬝ ap g (ret (f a))) ⬝ sec a) : by rewrite -ap_con,
|
2015-02-28 00:02:18 +00:00
|
|
|
|
have eq4 : ret (f a) = ap f ((ap g (ap f (sec a)⁻¹) ⬝ ap g (ret (f a))) ⬝ sec a),
|
2015-04-24 21:00:32 +00:00
|
|
|
|
from eq_of_idp_eq_inv_con eq3,
|
2014-12-12 04:14:53 +00:00
|
|
|
|
eq4)
|
|
|
|
|
|
2015-05-14 02:01:48 +00:00
|
|
|
|
definition adjointify [constructor] : is_equiv f :=
|
|
|
|
|
is_equiv.mk f g ret adjointify_sect' adjointify_adj'
|
2014-12-12 04:14:53 +00:00
|
|
|
|
|
|
|
|
|
end
|
|
|
|
|
|
2015-02-21 00:30:32 +00:00
|
|
|
|
section
|
2015-03-13 22:27:29 +00:00
|
|
|
|
variables {A B C : Type} (f : A → B) {f' : A → B} [Hf : is_equiv f] (g : B → C)
|
2014-12-12 04:14:53 +00:00
|
|
|
|
include Hf
|
|
|
|
|
|
2015-03-13 22:27:29 +00:00
|
|
|
|
--The inverse of an equivalence is, again, an equivalence.
|
2015-05-02 21:17:50 +00:00
|
|
|
|
definition is_equiv_inv [instance] : is_equiv f⁻¹ :=
|
2015-04-27 19:39:36 +00:00
|
|
|
|
adjointify f⁻¹ f (left_inv f) (right_inv f)
|
2015-02-11 20:49:27 +00:00
|
|
|
|
|
2015-02-21 00:30:32 +00:00
|
|
|
|
definition cancel_right (g : B → C) [Hgf : is_equiv (g ∘ f)] : (is_equiv g) :=
|
2015-03-13 22:27:29 +00:00
|
|
|
|
have Hfinv [visible] : is_equiv f⁻¹, from is_equiv_inv f,
|
2015-04-27 19:39:36 +00:00
|
|
|
|
@homotopy_closed _ _ _ _ (is_equiv_compose f⁻¹ (g ∘ f)) (λb, ap g (@right_inv _ _ f _ b))
|
2014-12-12 04:14:53 +00:00
|
|
|
|
|
2015-02-21 00:30:32 +00:00
|
|
|
|
definition cancel_left (g : C → A) [Hgf : is_equiv (f ∘ g)] : (is_equiv g) :=
|
2015-03-13 22:27:29 +00:00
|
|
|
|
have Hfinv [visible] : is_equiv f⁻¹, from is_equiv_inv f,
|
2015-04-27 19:39:36 +00:00
|
|
|
|
@homotopy_closed _ _ _ _ (is_equiv_compose (f ∘ g) f⁻¹) (λa, left_inv f (g a))
|
2014-12-12 04:14:53 +00:00
|
|
|
|
|
2015-02-21 00:30:32 +00:00
|
|
|
|
definition is_equiv_ap [instance] (x y : A) : is_equiv (ap f) :=
|
2014-12-12 04:14:53 +00:00
|
|
|
|
adjointify (ap f)
|
2015-04-27 19:39:36 +00:00
|
|
|
|
(λq, (inverse (left_inv f x)) ⬝ ap f⁻¹ q ⬝ left_inv f y)
|
2015-02-21 00:30:32 +00:00
|
|
|
|
(λq, !ap_con
|
|
|
|
|
⬝ whisker_right !ap_con _
|
2015-02-28 00:02:18 +00:00
|
|
|
|
⬝ ((!ap_inv ⬝ inverse2 (adj f _)⁻¹)
|
|
|
|
|
◾ (inverse (ap_compose f⁻¹ f _))
|
2014-12-12 04:14:53 +00:00
|
|
|
|
◾ (adj f _)⁻¹)
|
2015-04-27 19:39:36 +00:00
|
|
|
|
⬝ con_ap_con_eq_con_con (right_inv f) _ _
|
2015-02-28 00:50:06 +00:00
|
|
|
|
⬝ whisker_right !con.left_inv _
|
2015-02-21 00:30:32 +00:00
|
|
|
|
⬝ !idp_con)
|
2015-02-28 00:02:18 +00:00
|
|
|
|
(λp, whisker_right (whisker_left _ (ap_compose f f⁻¹ _)⁻¹) _
|
2015-04-27 19:39:36 +00:00
|
|
|
|
⬝ con_ap_con_eq_con_con (left_inv f) _ _
|
2015-02-28 00:50:06 +00:00
|
|
|
|
⬝ whisker_right !con.left_inv _
|
2015-02-21 00:30:32 +00:00
|
|
|
|
⬝ !idp_con)
|
2014-12-12 04:14:53 +00:00
|
|
|
|
|
|
|
|
|
-- The function equiv_rect says that given an equivalence f : A → B,
|
|
|
|
|
-- and a hypothesis from B, one may always assume that the hypothesis
|
|
|
|
|
-- is in the image of e.
|
|
|
|
|
|
|
|
|
|
-- In fibrational terms, if we have a fibration over B which has a section
|
|
|
|
|
-- once pulled back along an equivalence f : A → B, then it has a section
|
|
|
|
|
-- over all of B.
|
|
|
|
|
|
2015-02-21 00:30:32 +00:00
|
|
|
|
definition equiv_rect (P : B → Type) :
|
2014-12-12 04:14:53 +00:00
|
|
|
|
(Πx, P (f x)) → (Πy, P y) :=
|
2015-04-27 19:39:36 +00:00
|
|
|
|
(λg y, eq.transport _ (right_inv f y) (g (f⁻¹ y)))
|
2014-12-12 04:14:53 +00:00
|
|
|
|
|
|
|
|
|
definition equiv_rect_comp (P : B → Type)
|
2014-12-12 18:17:50 +00:00
|
|
|
|
(df : Π (x : A), P (f x)) (x : A) : equiv_rect f P df (f x) = df x :=
|
2014-12-12 04:14:53 +00:00
|
|
|
|
calc equiv_rect f P df (f x)
|
2015-04-27 19:39:36 +00:00
|
|
|
|
= transport P (right_inv f (f x)) (df (f⁻¹ (f x))) : by esimp
|
|
|
|
|
... = transport P (eq.ap f (left_inv f x)) (df (f⁻¹ (f x))) : by rewrite adj
|
|
|
|
|
... = transport (P ∘ f) (left_inv f x) (df (f⁻¹ (f x))) : by rewrite -transport_compose
|
|
|
|
|
... = df x : by rewrite (apd df (left_inv f x))
|
2014-12-12 04:14:53 +00:00
|
|
|
|
|
|
|
|
|
end
|
|
|
|
|
|
2015-03-13 22:27:29 +00:00
|
|
|
|
section
|
|
|
|
|
variables {A B : Type} {f : A → B} [Hf : is_equiv f] {a : A} {b : B}
|
|
|
|
|
include Hf
|
|
|
|
|
|
|
|
|
|
--Rewrite rules
|
|
|
|
|
definition eq_of_eq_inv (p : a = f⁻¹ b) : f a = b :=
|
2015-04-27 19:39:36 +00:00
|
|
|
|
ap f p ⬝ right_inv f b
|
2015-03-13 22:27:29 +00:00
|
|
|
|
|
|
|
|
|
definition eq_of_inv_eq (p : f⁻¹ b = a) : b = f a :=
|
|
|
|
|
(eq_of_eq_inv p⁻¹)⁻¹
|
|
|
|
|
|
|
|
|
|
definition inv_eq_of_eq (p : b = f a) : f⁻¹ b = a :=
|
2015-04-27 19:39:36 +00:00
|
|
|
|
ap f⁻¹ p ⬝ left_inv f a
|
2015-03-13 22:27:29 +00:00
|
|
|
|
|
|
|
|
|
definition eq_inv_of_eq (p : f a = b) : a = f⁻¹ b :=
|
|
|
|
|
(inv_eq_of_eq p⁻¹)⁻¹
|
|
|
|
|
end
|
|
|
|
|
|
2014-12-12 04:14:53 +00:00
|
|
|
|
--Transporting is an equivalence
|
2015-02-21 00:30:32 +00:00
|
|
|
|
definition is_equiv_tr [instance] {A : Type} (P : A → Type) {x y : A} (p : x = y) : (is_equiv (transport P p)) :=
|
2015-04-28 21:31:26 +00:00
|
|
|
|
is_equiv.mk _ (transport P p⁻¹) (tr_inv_tr p) (inv_tr_tr p) (tr_inv_tr_lemma p)
|
2015-02-21 00:30:32 +00:00
|
|
|
|
|
2014-12-12 04:14:53 +00:00
|
|
|
|
end is_equiv
|
2015-02-21 00:30:32 +00:00
|
|
|
|
open is_equiv
|
2015-05-07 02:48:11 +00:00
|
|
|
|
|
|
|
|
|
namespace eq
|
|
|
|
|
definition tr_inv_fn {A : Type} {B : A → Type} {a a' : A} (p : a = a') :
|
|
|
|
|
transport B p⁻¹ = (transport B p)⁻¹ := idp
|
|
|
|
|
definition tr_inv {A : Type} {B : A → Type} {a a' : A} (p : a = a') (b : B a') :
|
|
|
|
|
p⁻¹ ▸ b = (transport B p)⁻¹ b := idp
|
|
|
|
|
|
|
|
|
|
definition cast_inv_fn {A B : Type} (p : A = B) : cast p⁻¹ = (cast p)⁻¹ := idp
|
|
|
|
|
definition cast_inv {A B : Type} (p : A = B) (b : B) : cast p⁻¹ b = (cast p)⁻¹ b := idp
|
|
|
|
|
end eq
|
|
|
|
|
|
2014-12-12 04:14:53 +00:00
|
|
|
|
namespace equiv
|
2015-02-26 18:19:54 +00:00
|
|
|
|
namespace ops
|
|
|
|
|
attribute to_fun [coercion]
|
|
|
|
|
end ops
|
|
|
|
|
open equiv.ops
|
2015-01-26 19:31:12 +00:00
|
|
|
|
attribute to_is_equiv [instance]
|
2014-12-12 04:14:53 +00:00
|
|
|
|
|
|
|
|
|
infix `≃`:25 := equiv
|
|
|
|
|
|
2015-02-26 18:19:54 +00:00
|
|
|
|
variables {A B C : Type}
|
2014-12-12 04:14:53 +00:00
|
|
|
|
|
2015-05-14 02:01:48 +00:00
|
|
|
|
protected definition MK [reducible] [constructor] (f : A → B) (g : B → A)
|
2015-04-27 19:39:36 +00:00
|
|
|
|
(right_inv : f ∘ g ∼ id) (left_inv : g ∘ f ∼ id) : A ≃ B :=
|
|
|
|
|
equiv.mk f (adjointify f g right_inv left_inv)
|
2015-02-28 06:16:20 +00:00
|
|
|
|
|
2015-05-14 02:01:48 +00:00
|
|
|
|
definition to_inv [reducible] [unfold-c 3] (f : A ≃ B) : B → A := f⁻¹
|
|
|
|
|
definition to_right_inv [reducible] [unfold-c 3] (f : A ≃ B) : f ∘ f⁻¹ ∼ id := right_inv f
|
|
|
|
|
definition to_left_inv [reducible] [unfold-c 3] (f : A ≃ B) : f⁻¹ ∘ f ∼ id := left_inv f
|
2014-12-12 04:14:53 +00:00
|
|
|
|
|
2015-05-14 02:01:48 +00:00
|
|
|
|
protected definition refl [refl] : A ≃ A :=
|
2015-02-26 18:19:54 +00:00
|
|
|
|
equiv.mk id !is_equiv_id
|
2014-12-12 04:14:53 +00:00
|
|
|
|
|
2015-05-14 02:01:48 +00:00
|
|
|
|
protected definition symm [symm] (f : A ≃ B) : B ≃ A :=
|
2015-02-28 00:02:18 +00:00
|
|
|
|
equiv.mk f⁻¹ !is_equiv_inv
|
2014-12-12 04:14:53 +00:00
|
|
|
|
|
2015-05-14 02:01:48 +00:00
|
|
|
|
protected definition trans [trans] (f : A ≃ B) (g: B ≃ C) : A ≃ C :=
|
2015-02-26 18:19:54 +00:00
|
|
|
|
equiv.mk (g ∘ f) !is_equiv_compose
|
2014-12-12 04:14:53 +00:00
|
|
|
|
|
2015-05-02 21:17:50 +00:00
|
|
|
|
definition equiv_of_eq_fn_of_equiv (f : A ≃ B) {f' : A → B} (Heq : f = f') : A ≃ B :=
|
|
|
|
|
equiv.mk f' (is_equiv_eq_closed Heq)
|
2014-12-12 04:14:53 +00:00
|
|
|
|
|
2015-02-26 18:19:54 +00:00
|
|
|
|
definition eq_equiv_fn_eq (f : A → B) [H : is_equiv f] (a b : A) : (a = b) ≃ (f a = f b) :=
|
|
|
|
|
equiv.mk (ap f) !is_equiv_ap
|
2014-12-12 04:14:53 +00:00
|
|
|
|
|
2015-02-26 18:19:54 +00:00
|
|
|
|
definition eq_equiv_fn_eq_of_equiv (f : A ≃ B) (a b : A) : (a = b) ≃ (f a = f b) :=
|
|
|
|
|
equiv.mk (ap f) !is_equiv_ap
|
|
|
|
|
|
|
|
|
|
definition equiv_ap (P : A → Type) {a b : A} (p : a = b) : (P a) ≃ (P b) :=
|
|
|
|
|
equiv.mk (transport P p) !is_equiv_tr
|
2014-12-12 04:14:53 +00:00
|
|
|
|
|
2015-02-21 00:30:32 +00:00
|
|
|
|
--we need this theorem for the funext_of_ua proof
|
|
|
|
|
theorem inv_eq {A B : Type} (eqf eqg : A ≃ B) (p : eqf = eqg) : (to_fun eqf)⁻¹ = (to_fun eqg)⁻¹ :=
|
2015-02-26 18:19:54 +00:00
|
|
|
|
eq.rec_on p idp
|
2014-12-12 04:14:53 +00:00
|
|
|
|
|
2015-05-01 03:23:12 +00:00
|
|
|
|
definition equiv_of_equiv_of_eq {A B C : Type} (p : A = B) (q : B ≃ C) : A ≃ C := p⁻¹ ▸ q
|
|
|
|
|
definition equiv_of_eq_of_equiv {A B C : Type} (p : A ≃ B) (q : B = C) : A ≃ C := q ▸ p
|
2015-03-03 21:37:38 +00:00
|
|
|
|
|
2015-05-07 02:48:11 +00:00
|
|
|
|
namespace ops
|
|
|
|
|
infixl `⬝e`:75 := equiv.trans
|
2015-05-14 02:01:48 +00:00
|
|
|
|
postfix `⁻¹` := equiv.symm -- overloaded notation for inverse
|
|
|
|
|
postfix `⁻¹ᵉ`:(max + 1) := equiv.symm -- notation for inverse which is not overloaded
|
2015-05-07 02:48:11 +00:00
|
|
|
|
abbreviation erfl := @equiv.refl
|
|
|
|
|
end ops
|
2014-12-12 04:14:53 +00:00
|
|
|
|
end equiv
|