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

feat(hott/cubical): add cubes which are degenerate in one dimension

Browse source
This commit is contained in:
Jakob von Raumer 2015-10-21 15:52:32 +01:00 committed by Leonardo de Moura
parent bba6ab5a6d
commit 2bc45f4de1
1 changed files with 15 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
hott/cubical/cube.hlean
View file

@ -113,6 +113,21 @@ namespace eq
cube s₁₁₀ s₁₁₂ s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁' :=
by induction p; exact c
/- Each equality between squares leads to a cube which is degenerate in one
dimension. -/
definition deg1_cube {s₁₁₀' : square p₀₁₀ p₂₁₀ p₁₀₀ p₁₂₀} (p : s₁₁₀ = s₁₁₀') :
cube s₁₁₀ s₁₁₀' vrfl vrfl vrfl vrfl :=
by induction p; exact rfl1
definition deg2_cube {s₁₁₀' : square p₀₁₀ p₂₁₀ p₁₀₀ p₁₂₀} (p : s₁₁₀ = s₁₁₀') :
cube vrfl vrfl s₁₁₀ s₁₁₀' hrfl hrfl :=
by induction p; exact rfl2
definition deg3_cube {s₁₁₀' : square p₀₁₀ p₂₁₀ p₁₀₀ p₁₂₀} (p : s₁₁₀ = s₁₁₀') :
cube hrfl hrfl hrfl hrfl s₁₁₀ s₁₁₀' :=
by induction p; exact rfl3
/- For each square of parralel equations, there are cubes where the square's
sides appear in a degenerated way and two opposite sides are ids's -/