michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/hott) fix equiv_precomp, doesn't look nice now

Browse source
This commit is contained in:
Jakob von Raumer 2014-11-21 18:04:02 -05:00 committed by Leonardo de Moura
parent 1f6b6ff8e6
commit 12429c93c8
1 changed files with 36 additions and 36 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

72
library/hott/equiv_precomp.lean
View file

@ -3,29 +3,30 @@
-- Author: Jakob von Raumer
-- Ported from Coq HoTT
import hott.equiv hott.axioms.funext
open path function
open path function funext
set_option pp.universes true
namespace IsEquiv
context
parameters {A B : Type} (f : A → B)
--Precomposition of arbitrary functions with f
definition precomp (C : Type) (h : B → C) : A → C := h ∘ f
definition precomp {A B : Type} (f : A → B) (C : Type) (h : B → C) : A → C := h ∘ f
--Postcomposition of arbitrary functions with f
definition postcomp (C : Type) (l : C → A) : C → B := f ∘ l
definition postcomp {A B : Type} (f : A → B) (C : Type) (l : C → A) : C → B := f ∘ l
--Precomposing with an equivalence is an equivalence
definition precompose [instance] [Hf : IsEquiv f] (C : Type):
IsEquiv (precomp C) :=
adjointify (precomp C) (λh, h ∘ f⁻¹)
definition precompose [instance] {A B : Type} (f : A → B) [F : funext] [Hf : IsEquiv f] (C : Type):
IsEquiv (precomp f C) :=
adjointify (precomp f C) (λh, h ∘ f⁻¹)
(λ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
definition postcompose [instance] [Hf : IsEquiv f] (C : Type):
IsEquiv (postcomp C) :=
adjointify (postcomp C) (λl, f⁻¹ ∘ l)
definition postcompose [instance] {A B : Type} (f : A → B) [F : funext] [Hf : IsEquiv f] (C : Type):
IsEquiv (postcomp f C) :=
adjointify (postcomp f C) (λl, f⁻¹ ∘ l)
(λh, path_forall _ _ (λx, retr f (h x)))
(λg, path_forall _ _ (λy, sect f (g y)))
@ -33,29 +34,30 @@ namespace IsEquiv
--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.
private definition isequiv_precompose_eq (C D : Type) (Ceq : IsEquiv (precomp C))
(Deq : IsEquiv (precomp D)) (k : C → D) (h : A → C) :
k ∘ (inv (precomp C)) h ≈ (inv (precomp D)) (k ∘ h) :=
let invD := inv (precomp D) in
let invC := inv (precomp C) in
protected definition isequiv_precompose_eq {A B : Type} (f : A → B) (C D : Type) (Ceq : IsEquiv (precomp f C))
(Deq : IsEquiv (precomp f D)) (k : C → D) (h : A → C) :
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
have eq1 : invD (k ∘ h) ≈ k ∘ (invC h),
from calc invD (k ∘ h) ≈ invD (k ∘ (precomp C (invC h))) : retr (precomp C) h
from calc invD (k ∘ h) ≈ invD (k ∘ (precomp f C (invC h))) : retr (precomp f C) h
... ≈ k ∘ (invC h) : !sect,
eq1⁻¹
definition isequiv_precompose (Aeq : IsEquiv (precomp A))
(Beq : IsEquiv (precomp B)) : (IsEquiv f) :=
let invA := inv (precomp A) in
let invB := inv (precomp B) in
universe variable l
definition isequiv_precompose {A B : Type.{l}} (f : A → B) (Aeq : IsEquiv (precomp f A))
(Beq : IsEquiv (precomp f B)) : (IsEquiv f) :=
let invA := inv (precomp f A) in
let invB := inv (precomp f B) in
let sect' : Sect (invA id) f := (λx,
calc f (invA id x) ≈ (f ∘ invA id) x : idp
... ≈ invB (f ∘ id) x : apD10 (!isequiv_precompose_eq)
... ≈ invB (precomp B id) x : idp
... ≈ x : apD10 (sect (precomp B) id))
... ≈ invB (precomp f B id) x : idp
... ≈ x : apD10 (sect (precomp f B) id))
in
let retr' : Sect f (invA id) := (λx,
calc invA id (f x) ≈ precomp A (invA id) x : idp
... ≈ x : apD10 (retr (precomp A) id)) in
calc invA id (f x) ≈ precomp f A (invA id) x : idp
... ≈ x : apD10 (retr (precomp f A) id)) in
adjointify f (invA id) sect' retr'
end
@ -65,20 +67,18 @@ end IsEquiv
--Bundled versions of the previous theorems
namespace Equiv
context
parameters {A B C : Type} {eqf : A ≃ B}
private definition f := equiv_fun eqf
private definition Hf := equiv_isequiv eqf
definition precompose : (B → C) ≃ (A → C) :=
definition precompose [F : funext] {A B C : Type} {eqf : A ≃ B}
: (B → C) ≃ (A → C) :=
let f := equiv_fun eqf in
let Hf := equiv_isequiv eqf in
Equiv.mk (IsEquiv.precomp f C)
(@IsEquiv.precompose A B f Hf C)
(@IsEquiv.precompose A B f F Hf C)
definition postcompose : (C → A) ≃ (C → B) :=
definition postcompose [F : funext] {A B C : Type} {eqf : A ≃ B}
: (C → A) ≃ (C → B) :=
let f := equiv_fun eqf in
let Hf := equiv_isequiv eqf in
Equiv.mk (IsEquiv.postcomp f C)
(@IsEquiv.postcompose A B f Hf C)
end
(@IsEquiv.postcompose A B f F Hf C)
end Equiv