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

feat(hott/cubical): add fillers and other little lemmas for squares and cubes

Browse source
This commit is contained in:
Jakob von Raumer 2015-10-20 18:49:26 +01:00 committed by Leonardo de Moura
parent 12a498d411
commit bba6ab5a6d
2 changed files with 176 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

160
hott/cubical/cube.hlean
View file

@ -8,7 +8,7 @@ Cubes
import .square
open equiv is_equiv
open equiv equiv.ops is_equiv sigma sigma.ops
namespace eq
@ -38,12 +38,27 @@ namespace eq
{s₁₀₁ : square p₁₀₀ p₁₀₂ p₀₀₁ p₂₀₁}
{s₁₂₁ : square p₁₂₀ p₁₂₂ p₀₂₁ p₂₂₁}
{b₁ b₂ b₃ b₄ : B}
(c : cube s₁₁₀ s₁₁₂ s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁)
definition idc [reducible] [constructor] := @cube.idc
definition idcube [reducible] [constructor] (a : A) := @cube.idc A a
definition rfl1 : cube s₁₁₀ s₁₁₀ vrfl vrfl vrfl vrfl := by induction s₁₁₀; exact idc
definition rfl2 : cube vrfl vrfl s₁₁₀ s₁₁₀ hrfl hrfl := by induction s₁₁₀; exact idc
definition rfl3 : cube hrfl hrfl hrfl hrfl s₁₀₁ s₁₀₁ := by induction s₁₀₁; exact idc
variables (s₁₁₀ s₁₀₁)
definition refl1 : cube s₁₁₀ s₁₁₀ vrfl vrfl vrfl vrfl :=
by induction s₁₁₀; exact idc
definition refl2 : cube vrfl vrfl s₁₁₀ s₁₁₀ hrfl hrfl :=
by induction s₁₁₀; exact idc
definition refl3 : cube hrfl hrfl hrfl hrfl s₁₀₁ s₁₀₁ :=
by induction s₁₀₁; exact idc
variables {s₁₁₀ s₁₀₁}
definition rfl1 : cube s₁₁₀ s₁₁₀ vrfl vrfl vrfl vrfl := !refl1
definition rfl2 : cube vrfl vrfl s₁₁₀ s₁₁₀ hrfl hrfl := !refl2
definition rfl3 : cube hrfl hrfl hrfl hrfl s₁₀₁ s₁₀₁ := !refl3
definition eq_of_cube (c : cube s₁₁₀ s₁₁₂ s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁) :
transpose s₁₀₁⁻¹ᵛ ⬝h s₁₁₀ ⬝h transpose s₁₂₁ =
@ -60,10 +75,145 @@ namespace eq
definition square_pathover [unfold 7]
{f₁ : A → b₁ = b₂} {f₂ : A → b₃ = b₄} {f₃ : A → b₁ = b₃} {f₄ : A → b₂ = b₄}
{p : a = a'}
{q : square (f₁ a) (f₂ a) (f₃ a) (f₄ a)} {r : square (f₁ a') (f₂ a') (f₃ a') (f₄ a')}
{q : square (f₁ a) (f₂ a) (f₃ a) (f₄ a)}
{r : square (f₁ a') (f₂ a') (f₃ a') (f₄ a')}
(s : cube q r (vdeg_square (ap f₁ p)) (vdeg_square (ap f₂ p))
(vdeg_square (ap f₃ p)) (vdeg_square (ap f₄ p))) : q =[p] r :=
by induction p;apply pathover_idp_of_eq;exact eq_of_vdeg_cube s
/- Transporting along a square -/
definition cube_transport110 {s₁₁₀' : square p₀₁₀ p₂₁₀ p₁₀₀ p₁₂₀}
(p : s₁₁₀ = s₁₁₀') (c : cube s₁₁₀ s₁₁₂ s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁) :
cube s₁₁₀' s₁₁₂ s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ :=
by induction p; exact c
definition cube_transport112 {s₁₁₂' : square p₀₁₂ p₂₁₂ p₁₀₂ p₁₂₂}
(p : s₁₁₂ = s₁₁₂') (c : cube s₁₁₀ s₁₁₂ s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁) :
cube s₁₁₀ s₁₁₂' s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ :=
by induction p; exact c
definition cube_transport011 {s₀₁₁' : square p₀₁₀ p₀₁₂ p₀₀₁ p₀₂₁}
(p : s₀₁₁ = s₀₁₁') (c : cube s₁₁₀ s₁₁₂ s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁) :
cube s₁₁₀ s₁₁₂ s₀₁₁' s₂₁₁ s₁₀₁ s₁₂₁ :=
by induction p; exact c
definition cube_transport211 {s₂₁₁' : square p₂₁₀ p₂₁₂ p₂₀₁ p₂₂₁}
(p : s₂₁₁ = s₂₁₁') (c : cube s₁₁₀ s₁₁₂ s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁) :
cube s₁₁₀ s₁₁₂ s₀₁₁ s₂₁₁' s₁₀₁ s₁₂₁ :=
by induction p; exact c
definition cube_transport101 {s₁₀₁' : square p₁₀₀ p₁₀₂ p₀₀₁ p₂₀₁}
(p : s₁₀₁ = s₁₀₁') (c : cube s₁₁₀ s₁₁₂ s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁) :
cube s₁₁₀ s₁₁₂ s₀₁₁ s₂₁₁ s₁₀₁' s₁₂₁ :=
by induction p; exact c
definition cube_transport121 {s₁₂₁' : square p₁₂₀ p₁₂₂ p₀₂₁ p₂₂₁}
(p : s₁₂₁ = s₁₂₁') (c : cube s₁₁₀ s₁₁₂ s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁) :
cube s₁₁₀ s₁₁₂ s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁' :=
by induction p; exact c
/- 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 -/
section
variables {a₀ a₁ : A} {p₀₀ p₀₂ p₂₀ p₂₂ : a₀ = a₁} {s₁₀ : p₀₀ = p₂₀}
{s₁₂ : p₀₂ = p₂₂} {s₀₁ : p₀₀ = p₀₂} {s₂₁ : p₂₀ = p₂₂}
(sq : square s₁₀ s₁₂ s₀₁ s₂₁)
include sq
definition ids1_cube_of_square : cube ids ids (hdeg_square s₀₁)
(hdeg_square s₂₁) (hdeg_square s₁₀) (hdeg_square s₁₂) :=
by induction p₀₀; induction sq; apply idc
definition ids2_cube_of_square : cube (hdeg_square s₀₁) (hdeg_square s₂₁) ids ids
(vdeg_square s₁₀) (vdeg_square s₁₂) :=
by induction p₀₀; induction sq; apply idc
definition ids3_cube_of_square : cube (vdeg_square s₀₁) (vdeg_square s₂₁)
(vdeg_square s₁₀) (vdeg_square s₁₂) ids ids :=
by induction p₀₀; induction sq; apply idc
end
/- Cube fillers -/
section cube_fillers
variables (s₁₁₀ s₁₁₂ s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁)
definition cube_fil110 : Σ lid, cube lid s₁₁₂ s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ :=
begin
induction s₀₁₁, induction s₂₁₁,
let fillsq := square_fill_l (eq_of_vdeg_square s₁₀₁)
(eq_of_hdeg_square s₁₁₂) (eq_of_vdeg_square s₁₂₁),
apply sigma.mk,
apply cube_transport101 (left_inv (vdeg_square_equiv _ _) s₁₀₁),
apply cube_transport112 (left_inv (hdeg_square_equiv _ _) s₁₁₂),
apply cube_transport121 (left_inv (vdeg_square_equiv _ _) s₁₂₁),
apply ids2_cube_of_square, exact fillsq.2
end
definition cube_fill112 : Σ lid, cube s₁₁₀ lid s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ :=
begin
induction s₀₁₁, induction s₂₁₁,
let fillsq := square_fill_r (eq_of_vdeg_square s₁₀₁)
(eq_of_hdeg_square s₁₁₀) (eq_of_vdeg_square s₁₂₁),
apply sigma.mk,
apply cube_transport101 (left_inv (vdeg_square_equiv _ _) s₁₀₁),
apply cube_transport110 (left_inv (hdeg_square_equiv _ _) s₁₁₀),
apply cube_transport121 (left_inv (vdeg_square_equiv _ _) s₁₂₁),
apply ids2_cube_of_square, exact fillsq.2,
end
definition cube_fill011 : Σ lid, cube s₁₁₀ s₁₁₂ lid s₂₁₁ s₁₀₁ s₁₂₁ :=
begin
induction s₁₀₁, induction s₁₂₁,
let fillsq := square_fill_t (eq_of_vdeg_square s₁₁₀) (eq_of_vdeg_square s₁₁₂)
(eq_of_vdeg_square s₂₁₁),
apply sigma.mk,
apply cube_transport110 (left_inv (vdeg_square_equiv _ _) s₁₁₀),
apply cube_transport211 (left_inv (vdeg_square_equiv _ _) s₂₁₁),
apply cube_transport112 (left_inv (vdeg_square_equiv _ _) s₁₁₂),
apply ids3_cube_of_square, exact fillsq.2,
end
definition cube_fill211 : Σ lid, cube s₁₁₀ s₁₁₂ s₀₁₁ lid s₁₀₁ s₁₂₁ :=
begin
induction s₁₀₁, induction s₁₂₁,
let fillsq := square_fill_b (eq_of_vdeg_square s₀₁₁) (eq_of_vdeg_square s₁₁₀)
(eq_of_vdeg_square s₁₁₂),
apply sigma.mk,
apply cube_transport011 (left_inv (vdeg_square_equiv _ _) s₀₁₁),
apply cube_transport110 (left_inv (vdeg_square_equiv _ _) s₁₁₀),
apply cube_transport112 (left_inv (vdeg_square_equiv _ _) s₁₁₂),
apply ids3_cube_of_square, exact fillsq.2,
end
definition cube_fill101 : Σ lid, cube s₁₁₀ s₁₁₂ s₀₁₁ s₂₁₁ lid s₁₂₁ :=
begin
induction s₁₁₀, induction s₁₁₂,
let fillsq := square_fill_t (eq_of_hdeg_square s₀₁₁) (eq_of_hdeg_square s₂₁₁)
(eq_of_hdeg_square s₁₂₁),
apply sigma.mk,
apply cube_transport011 (left_inv (hdeg_square_equiv _ _) s₀₁₁),
apply cube_transport211 (left_inv (hdeg_square_equiv _ _) s₂₁₁),
apply cube_transport121 (left_inv (hdeg_square_equiv _ _) s₁₂₁),
apply ids1_cube_of_square, exact fillsq.2,
end
definition cube_fill121 : Σ lid, cube s₁₁₀ s₁₁₂ s₀₁₁ s₂₁₁ s₁₀₁ lid :=
begin
induction s₁₁₀, induction s₁₁₂,
let fillsq := square_fill_b (eq_of_hdeg_square s₁₀₁) (eq_of_hdeg_square s₀₁₁)
(eq_of_hdeg_square s₂₁₁),
apply sigma.mk,
apply cube_transport101 (left_inv (hdeg_square_equiv _ _) s₁₀₁),
apply cube_transport011 (left_inv (hdeg_square_equiv _ _) s₀₁₁),
apply cube_transport211 (left_inv (hdeg_square_equiv _ _) s₂₁₁),
apply ids1_cube_of_square, exact fillsq.2,
end
end cube_fillers
end eq

24
hott/cubical/square.hlean
View file

@ -6,7 +6,7 @@ Author: Floris van Doorn
Squares in a type
-/
import types.eq
open eq equiv is_equiv
open eq equiv is_equiv sigma
namespace eq
@ -262,7 +262,8 @@ namespace eq
hdeg_square and vdeg_square, respectively.
See example below the definition
-/
definition hdeg_square_equiv [constructor] (p q : a = a') : square idp idp p q ≃ p = q :=
definition hdeg_square_equiv [constructor] (p q : a = a') :
square idp idp p q ≃ p = q :=
begin
fapply equiv_change_fun,
{ fapply equiv_change_inv, apply hdeg_square_equiv', exact hdeg_square,
@ -271,7 +272,8 @@ namespace eq
{ reflexivity}
end
definition vdeg_square_equiv [constructor] (p q : a = a') : square p q idp idp ≃ p = q :=
definition vdeg_square_equiv [constructor] (p q : a = a') :
square p q idp idp ≃ p = q :=
begin
fapply equiv_change_fun,
{ fapply equiv_change_inv, apply vdeg_square_equiv',exact vdeg_square,
@ -481,4 +483,20 @@ namespace eq
-- : square t b l r :=
-- sorry --by induction s
/- Square fillers -/
-- TODO replace by "more algebraic" fillers?
variables (p₁₀ p₁₂ p₀₁ p₂₁)
definition square_fill_t : Σ (p : a₀₀ = a₂₀), square p p₁₂ p₀₁ p₂₁ :=
by induction p₀₁; induction p₂₁; exact ⟨_, !vrefl⟩
definition square_fill_b : Σ (p : a₀₂ = a₂₂), square p₁₀ p p₀₁ p₂₁ :=
by induction p₀₁; induction p₂₁; exact ⟨_, !vrefl⟩
definition square_fill_l : Σ (p : a₀₀ = a₀₂), square p₁₀ p₁₂ p p₂₁ :=
by induction p₁₀; induction p₁₂; exact ⟨_, !hrefl⟩
definition square_fill_r : Σ (p : a₂₀ = a₂₂) , square p₁₀ p₁₂ p₀₁ p :=
by induction p₁₀; induction p₁₂; exact ⟨_, !hrefl⟩
end eq