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

eq_of_shomotopy

Browse source
This commit is contained in:
Egbert Rijke 2017-07-07 20:11:47 +01:00
parent 58b007c873
commit 877bcd889e
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
homotopy/pointed_cubes.hlean
View file

@ -139,6 +139,13 @@ begin
exact ptb,
end
definition ptube_v_eq_bot {A B C D : Type*} {ftop ftop' : A →* B} (htpy_top : ftop ~* ftop') {fbot fbot' : C →* D} {htpy_bot htpy_bot' : fbot ~* fbot'} (p : htpy_bot = htpy_bot') {fleft : A →* C} {fright : B →* D} (psq_back : psquare ftop fbot fleft fright) (psq_front : psquare ftop' fbot' fleft fright) :
ptube_v htpy_top htpy_bot psq_back psq_front → ptube_v htpy_top htpy_bot' psq_back psq_front :=
begin
induction p,
exact id,
end
definition ptube_v_left_inv {A B C D : Type*} {ftop : A ≃* B} {fbot : C ≃* D} {fleft : A →* C} {fright : B →* D}
(psq : psquare ftop fbot fleft fright) :
ptube_v