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

feat(red_susp): define pelim

Browse source
This commit is contained in:
Floris van Doorn 2017-04-10 20:33:14 -04:00
parent c268731093
commit b998a49ec4
1 changed files with 8 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
hott/homotopy/red_susp.hlean
View file

@ -34,7 +34,7 @@ section
definition red_susp [constructor] : Type* := pointed.MK red_susp' base' definition red_susp [constructor] : Type* := pointed.MK red_susp' base'
parameter {A} parameter {A}
definition base : red_susp := definition base [reducible] : red_susp :=
base' base'
definition equator (a : A) : base = base := definition equator (a : A) : base = base :=
@ -70,7 +70,7 @@ section
induction q, exact Pe induction q, exact Pe
end end
protected definition elim_on [reducible] {P : Type} (x : red_susp') (Pb : P) protected definition elim_on [reducible] {P : Type} (x : red_susp') (Pb : P)
(Pm : Π(a : A), Pb = Pb) (Pe : Pm pt = idp) : P := (Pm : Π(a : A), Pb = Pb) (Pe : Pm pt = idp) : P :=
elim Pb Pm Pe x elim Pb Pm Pe x
@ -94,6 +94,12 @@ attribute red_susp.rec_on red_susp.elim_on [unfold 3]
namespace red_susp namespace red_susp
protected definition pelim' [unfold 4] {A P : Type*} (f : A →* Ω P) : red_susp' A → P :=
red_susp.elim pt f (respect_pt f)
protected definition pelim [constructor] {A P : Type*} (f : A →* Ω P) : red_susp A →* P :=
pmap.mk (red_susp.pelim' f) idp
definition susp_of_red_susp [unfold 2] {A : Type*} (x : red_susp A) : susp A := definition susp_of_red_susp [unfold 2] {A : Type*} (x : red_susp A) : susp A :=
begin begin
induction x, induction x,