diff --git a/hott/hit/interval.hlean b/hott/hit/interval.hlean new file mode 100644 index 0000000000..e308d56575 --- /dev/null +++ b/hott/hit/interval.hlean @@ -0,0 +1,96 @@ +/- +Copyright (c) 2015 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Authors: Floris van Doorn + +Declaration of the interval +-/ + +import .suspension types.eq types.prod types.square +open eq suspension unit equiv equiv.ops is_trunc nat prod + +definition interval : Type₀ := suspension unit + +namespace interval + + definition zero : interval := !north + definition one : interval := !south + definition seg : zero = one := merid star + + protected definition rec {P : interval → Type} (P0 : P zero) (P1 : P one) + (Ps : P0 =[seg] P1) (x : interval) : P x := + begin + fapply suspension.rec_on x, + { exact P0}, + { exact P1}, + { intro x, cases x, exact Ps} + end + + protected definition rec_on [reducible] {P : interval → Type} (x : interval) + (P0 : P zero) (P1 : P one) (Ps : P0 =[seg] P1) : P x := + interval.rec P0 P1 Ps x + + theorem rec_seg {P : interval → Type} (P0 : P zero) (P1 : P one) (Ps : P0 =[seg] P1) + : apdo (interval.rec P0 P1 Ps) seg = Ps := + !rec_merid + + protected definition elim {P : Type} (P0 P1 : P) (Ps : P0 = P1) (x : interval) : P := + interval.rec P0 P1 (pathover_of_eq Ps) x + + protected definition elim_on [reducible] {P : Type} (x : interval) (P0 P1 : P) + (Ps : P0 = P1) : P := + interval.elim P0 P1 Ps x + + theorem elim_seg {P : Type} (P0 P1 : P) (Ps : P0 = P1) + : ap (interval.elim P0 P1 Ps) seg = Ps := + begin + apply eq_of_fn_eq_fn_inv !(pathover_constant seg), + rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑interval.elim,rec_seg], + end + + protected definition elim_type (P0 P1 : Type) (Ps : P0 ≃ P1) (x : interval) : Type := + interval.elim P0 P1 (ua Ps) x + + protected definition elim_type_on [reducible] (x : interval) (P0 P1 : Type) (Ps : P0 ≃ P1) + : Type := + interval.elim_type P0 P1 Ps x + + theorem elim_type_seg (P0 P1 : Type) (Ps : P0 ≃ P1) + : transport (interval.elim_type P0 P1 Ps) seg = Ps := + by rewrite [tr_eq_cast_ap_fn,↑interval.elim_type,elim_seg];apply cast_ua_fn + + definition is_contr_interval [instance] [priority 900] : is_contr interval := + is_contr.mk zero (λx, interval.rec_on x idp seg !pathover_eq_r_idp) + +end interval open interval + +definition cube : ℕ → Type₀ +| cube 0 := unit +| cube (succ n) := cube n × interval + +abbreviation square := cube (succ (succ nat.zero)) + +definition cube_one_equiv_interval : cube 1 ≃ interval := +!prod_comm_equiv ⬝e !prod_unit_equiv + + +definition prod_square {A B : Type} {a a' : A} {b b' : B} (p : a = a') (q : b = b') + : square (pair_eq p idp) (pair_eq p idp) (pair_eq idp q) (pair_eq idp q) := +by cases p; cases q; exact ids + +namespace square + + definition tl : square := (star, zero, zero) + definition tr : square := (star, one, zero) + definition bl : square := (star, zero, one ) + definition br : square := (star, one, one ) + -- s stands for "square" in the following definitions + definition st : tl = tr := pair_eq (pair_eq idp seg) idp + definition sb : bl = br := pair_eq (pair_eq idp seg) idp + definition sl : tl = bl := pair_eq idp seg + definition sr : tr = br := pair_eq idp seg + definition sfill : square st sb sl sr := !prod_square + definition fill : st ⬝ sr = sl ⬝ sb := !square_equiv_eq sfill + +end square diff --git a/hott/hit/pushout.hlean b/hott/hit/pushout.hlean index 98018619ee..b835ac531d 100644 --- a/hott/hit/pushout.hlean +++ b/hott/hit/pushout.hlean @@ -21,7 +21,7 @@ parameters {TL BL TR : Type} (f : TL → BL) (g : TL → TR) open pushout_rel local abbreviation R := pushout_rel - definition pushout : Type := type_quotient pushout_rel -- TODO: define this in root namespace + definition pushout : Type := type_quotient R -- TODO: define this in root namespace definition inl (x : BL) : pushout := class_of R (inl x) diff --git a/hott/types/eq.hlean b/hott/types/eq.hlean index b9c3ea9677..abc3b240af 100644 --- a/hott/types/eq.hlean +++ b/hott/types/eq.hlean @@ -98,6 +98,16 @@ namespace eq /- Pathovers -/ -- In the comment we give the fibration of the pathover + + definition pathover_eq_r_idp (p : a1 = a2) : idp =[p] p := /-(λx, a1 = x)-/ + by cases p; exact idpo + + definition pathover_eq_l_idp (p : a1 = a2) : idp =[p] p⁻¹ := /-(λx, x = a1)-/ + by cases p; exact idpo + + definition pathover_eq_l_idp' (p : a1 = a2) : idp =[p⁻¹] p := /-(λx, x = a2)-/ + by cases p; exact idpo + definition pathover_eq_l (p : a1 = a2) (q : a1 = a3) : q =[p] p⁻¹ ⬝ q := /-(λx, x = a3)-/ by cases p; cases q; exact idpo diff --git a/hott/types/square.hlean b/hott/types/square.hlean index dbab850e43..a4aed4bc67 100644 --- a/hott/types/square.hlean +++ b/hott/types/square.hlean @@ -8,7 +8,7 @@ Theorems about square open eq equiv is_equiv -namespace cubical +namespace eq variables {A : Type} {a a' a'' a₀₀ a₂₀ a₄₀ a₀₂ a₂₂ a₂₄ a₀₄ a₄₂ a₄₄ : A} /-a₀₀-/ {p₁₀ : a₀₀ = a₂₀} /-a₂₀-/ {p₃₀ : a₂₀ = a₄₀} /-a₄₀-/ @@ -138,4 +138,4 @@ namespace cubical --we can also do the other recursors (lr, tl, tr, bl, br, tbl, tbr, tlr, blr), but let's postpone this until they are needed -end cubical +end eq diff --git a/hott/types/squareover.hlean b/hott/types/squareover.hlean new file mode 100644 index 0000000000..1645d40622 --- /dev/null +++ b/hott/types/squareover.hlean @@ -0,0 +1,47 @@ +/- +Copyright (c) 2015 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Floris van Doorn + +Theorems about squareovers +-/ + +import cubical.pathover cubical.square + +open eq equiv is_equiv equiv.ops + +namespace cubical + + variables {A A' : Type} {B : A → Type} + {a a' a'' a₀₀ a₂₀ a₄₀ a₀₂ a₂₂ a₂₄ a₀₄ a₄₂ a₄₄ : A} + /-a₀₀-/ {p₁₀ : a₀₀ = a₂₀} /-a₂₀-/ {p₃₀ : a₂₀ = a₄₀} /-a₄₀-/ + {p₀₁ : a₀₀ = a₀₂} /-s₁₁-/ {p₂₁ : a₂₀ = a₂₂} /-s₃₁-/ {p₄₁ : a₄₀ = a₄₂} + /-a₀₂-/ {p₁₂ : a₀₂ = a₂₂} /-a₂₂-/ {p₃₂ : a₂₂ = a₄₂} /-a₄₂-/ + {p₀₃ : a₀₂ = a₀₄} /-s₁₃-/ {p₂₃ : a₂₂ = a₂₄} /-s₃₃-/ {p₄₃ : a₄₂ = a₄₄} + /-a₀₄-/ {p₁₄ : a₀₄ = a₂₄} /-a₂₄-/ {p₃₄ : a₂₄ = a₄₄} /-a₄₄-/ + {s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁} + {b₀₀ : B a₀₀} {b₂₀ : B a₂₀} {b₄₀ : B a₄₀} + {b₀₂ : B a₀₂} {b₂₂ : B a₂₂} {b₄₂ : B a₄₂} + {b₀₄ : B a₀₄} {b₂₄ : B a₂₄} {b₄₄ : B a₄₄} + /-b₀₀-/ {q₁₀ : b₀₀ =[p₁₀] b₂₀} /-b₂₀-/ {q₃₀ : b₂₀ =[p₃₀] b₄₀} /-b₄₀-/ + {q₀₁ : b₀₀ =[p₀₁] b₀₂} /-s₁₁-/ {q₂₁ : b₂₀ =[p₂₁] b₂₂} /-s₃₁-/ {q₄₁ : b₄₀ =[p₄₁] b₄₂} + /-b₀₂-/ {q₁₂ : b₀₂ =[p₁₂] b₂₂} /-b₂₂-/ {q₃₂ : b₂₂ =[p₃₂] b₄₂} /-b₄₂-/ + {q₀₃ : b₀₂ =[p₀₃] b₀₄} /-s₁₃-/ {q₂₃ : b₂₂ =[p₂₃] b₂₄} /-s₃₃-/ {q₄₃ : b₄₂ =[p₄₃] b₄₄} + /-b₀₄-/ {q₁₄ : b₀₄ =[p₁₄] b₂₄} /-b₂₄-/ {q₃₄ : b₂₄ =[p₃₄] b₄₄} /-b₄₄-/ + + inductive squareover (B : A → Type) {b₀₀ : B a₀₀} : + Π{a₂₀ a₀₂ a₂₂ : A} {p₁₀ : a₀₀ = a₂₀} {p₁₂ : a₀₂ = a₂₂} {p₀₁ : a₀₀ = a₀₂} {p₂₁ : a₂₀ = a₂₂} + (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) + {b₂₀ : B a₂₀} {b₀₂ : B a₀₂} {b₂₂ : B a₂₂} + (q₁₀ : b₀₀ =[p₁₀] b₂₀) (q₁₂ : b₀₂ =[p₁₂] b₂₂) (q₀₁ : b₀₀ =[p₀₁] b₀₂) (q₂₁ : b₂₀ =[p₂₁] b₂₂), + Type := + idsquareo : squareover B ids idpo idpo idpo idpo + + definition squareo := @squareover A a₀₀ B + definition idsquareo [reducible] [constructor] (b₀₀ : B a₀₀) := @squareover.idsquareo A a₀₀ B b₀₀ + definition idso [reducible] [constructor] := @squareover.idsquareo A a₀₀ B b₀₀ + + + +end cubical