2014-11-05 01:16:51 +00:00
|
|
|
|
-- Copyright (c) 2014 Jakob von Raumer. All rights reserved.
|
2014-11-04 19:23:37 +00:00
|
|
|
|
-- Released under Apache 2.0 license as described in the file LICENSE.
|
2014-11-05 01:16:51 +00:00
|
|
|
|
-- Author: Jakob von Raumer
|
2014-11-04 19:23:37 +00:00
|
|
|
|
-- Ported from Coq HoTT
|
2014-11-06 18:34:57 +00:00
|
|
|
|
import hott.equiv hott.axioms.funext
|
2014-11-21 23:04:02 +00:00
|
|
|
|
open path function funext
|
|
|
|
|
|
2014-11-26 04:30:52 +00:00
|
|
|
|
namespace is_equiv
|
2014-11-04 19:23:37 +00:00
|
|
|
|
context
|
|
|
|
|
|
2014-11-04 23:04:15 +00:00
|
|
|
|
--Precomposition of arbitrary functions with f
|
2014-11-21 23:04:02 +00:00
|
|
|
|
definition precomp {A B : Type} (f : A → B) (C : Type) (h : B → C) : A → C := h ∘ f
|
2014-11-04 19:23:37 +00:00
|
|
|
|
|
2014-11-04 23:04:15 +00:00
|
|
|
|
--Postcomposition of arbitrary functions with f
|
2014-11-21 23:04:02 +00:00
|
|
|
|
definition postcomp {A B : Type} (f : A → B) (C : Type) (l : C → A) : C → B := f ∘ l
|
2014-11-04 23:04:15 +00:00
|
|
|
|
|
|
|
|
|
--Precomposing with an equivalence is an equivalence
|
2014-11-26 04:30:52 +00:00
|
|
|
|
definition precompose [instance] {A B : Type} (f : A → B) [F : funext] [Hf : is_equiv f] (C : Type)
|
|
|
|
|
: is_equiv (precomp f C) :=
|
2014-11-21 23:04:02 +00:00
|
|
|
|
adjointify (precomp f C) (λh, h ∘ f⁻¹)
|
2014-11-04 23:04:15 +00:00
|
|
|
|
(λh, path_forall _ _ (λx, ap h (sect f x)))
|
|
|
|
|
(λg, path_forall _ _ (λy, ap g (retr f y)))
|
|
|
|
|
|
|
|
|
|
--Postcomposing with an equivalence is an equivalence
|
2014-11-26 04:30:52 +00:00
|
|
|
|
definition postcompose [instance] {A B : Type} (f : A → B) [F : funext] [Hf : is_equiv f] (C : Type)
|
|
|
|
|
: is_equiv (postcomp f C) :=
|
2014-11-21 23:04:02 +00:00
|
|
|
|
adjointify (postcomp f C) (λl, f⁻¹ ∘ l)
|
2014-11-04 23:04:15 +00:00
|
|
|
|
(λh, path_forall _ _ (λx, retr f (h x)))
|
|
|
|
|
(λg, path_forall _ _ (λy, sect f (g y)))
|
|
|
|
|
|
|
|
|
|
--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.
|
2014-11-26 04:30:52 +00:00
|
|
|
|
protected definition isequiv_precompose_eq {A B : Type} (f : A → B) (C D : Type)
|
|
|
|
|
(Ceq : is_equiv (precomp f C)) (Deq : is_equiv (precomp f D)) (k : C → D) (h : A → C) :
|
2014-11-21 23:04:02 +00:00
|
|
|
|
k ∘ (inv (precomp f C)) h ≈ (inv (precomp f D)) (k ∘ h) :=
|
|
|
|
|
let invD := inv (precomp f D) in
|
|
|
|
|
let invC := inv (precomp f C) in
|
2014-11-04 19:23:37 +00:00
|
|
|
|
have eq1 : invD (k ∘ h) ≈ k ∘ (invC h),
|
2014-11-21 23:04:02 +00:00
|
|
|
|
from calc invD (k ∘ h) ≈ invD (k ∘ (precomp f C (invC h))) : retr (precomp f C) h
|
2014-11-04 19:23:37 +00:00
|
|
|
|
... ≈ k ∘ (invC h) : !sect,
|
|
|
|
|
eq1⁻¹
|
|
|
|
|
|
2014-11-26 04:30:52 +00:00
|
|
|
|
definition isequiv_precompose {A B : Type} (f : A → B) (Aeq : is_equiv (precomp f A))
|
|
|
|
|
(Beq : is_equiv (precomp f B)) : (is_equiv f) :=
|
2014-11-21 23:04:02 +00:00
|
|
|
|
let invA := inv (precomp f A) in
|
|
|
|
|
let invB := inv (precomp f B) in
|
2014-11-26 04:30:52 +00:00
|
|
|
|
let sect' : f ∘ (invA id) ∼ id := (λx,
|
2014-11-04 19:23:37 +00:00
|
|
|
|
calc f (invA id x) ≈ (f ∘ invA id) x : idp
|
2014-11-04 23:04:15 +00:00
|
|
|
|
... ≈ invB (f ∘ id) x : apD10 (!isequiv_precompose_eq)
|
2014-11-21 23:04:02 +00:00
|
|
|
|
... ≈ invB (precomp f B id) x : idp
|
|
|
|
|
... ≈ x : apD10 (sect (precomp f B) id))
|
2014-11-04 19:23:37 +00:00
|
|
|
|
in
|
2014-11-26 04:30:52 +00:00
|
|
|
|
let retr' : (invA id) ∘ f ∼ id := (λx,
|
2014-11-21 23:04:02 +00:00
|
|
|
|
calc invA id (f x) ≈ precomp f A (invA id) x : idp
|
|
|
|
|
... ≈ x : apD10 (retr (precomp f A) id)) in
|
2014-11-04 19:23:37 +00:00
|
|
|
|
adjointify f (invA id) sect' retr'
|
|
|
|
|
|
|
|
|
|
end
|
|
|
|
|
|
2014-11-26 04:30:52 +00:00
|
|
|
|
end is_equiv
|
2014-11-04 23:04:15 +00:00
|
|
|
|
|
|
|
|
|
--Bundled versions of the previous theorems
|
2014-11-26 04:30:52 +00:00
|
|
|
|
namespace equiv
|
2014-11-04 23:04:15 +00:00
|
|
|
|
|
2014-11-21 23:04:02 +00:00
|
|
|
|
definition precompose [F : funext] {A B C : Type} {eqf : A ≃ B}
|
|
|
|
|
: (B → C) ≃ (A → C) :=
|
2014-11-26 04:30:52 +00:00
|
|
|
|
let f := to_fun eqf in
|
|
|
|
|
let Hf := to_is_equiv eqf in
|
|
|
|
|
equiv.mk (is_equiv.precomp f C)
|
|
|
|
|
(@is_equiv.precompose A B f F Hf C)
|
2014-11-04 23:04:15 +00:00
|
|
|
|
|
2014-11-21 23:04:02 +00:00
|
|
|
|
definition postcompose [F : funext] {A B C : Type} {eqf : A ≃ B}
|
|
|
|
|
: (C → A) ≃ (C → B) :=
|
2014-11-26 04:30:52 +00:00
|
|
|
|
let f := to_fun eqf in
|
|
|
|
|
let Hf := to_is_equiv eqf in
|
|
|
|
|
equiv.mk (is_equiv.postcomp f C)
|
|
|
|
|
(@is_equiv.postcompose A B f F Hf C)
|
2014-11-04 23:04:15 +00:00
|
|
|
|
|
2014-11-26 04:30:52 +00:00
|
|
|
|
end equiv
|