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

feat(types/sigma): add lemma

Browse source
This commit is contained in:
Floris van Doorn 2015-11-30 19:25:22 -05:00 committed by Leonardo de Moura
parent 50323e5b14
commit 377755e5ab
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
hott/types/sigma.hlean
View file

@ -244,6 +244,10 @@ namespace sigma
: (Σa, B a) ≃ Σa, B' a := : (Σa, B a) ≃ Σa, B' a :=
sigma_equiv_sigma equiv.refl Hg sigma_equiv_sigma equiv.refl Hg
definition sigma_equiv_sigma_left [constructor] (Hf : A ≃ A') :
(Σa, B a) ≃ (Σa', B (to_inv Hf a')) :=
sigma_equiv_sigma Hf (λ a, equiv_ap B !right_inv⁻¹)
definition ap_sigma_functor_eq_dpair (p : a = a') (q : b =[p] b') : definition ap_sigma_functor_eq_dpair (p : a = a') (q : b =[p] b') :
ap (sigma_functor f g) (sigma_eq p q) = sigma_eq (ap f p) (pathover.rec_on q idpo) := ap (sigma_functor f g) (sigma_eq p q) = sigma_eq (ap f p) (pathover.rec_on q idpo) :=
by induction q; reflexivity by induction q; reflexivity