Permalink
Browse files

Add torus (donuts)

- Also add some symbols to make the types nicer.
  • Loading branch information...
favonia committed Jun 8, 2012
1 parent 2614d9e commit df07788f331514801db76f38b5767107743514e8
Showing with 133 additions and 1 deletion.
  1. +19 −0 Path/Symbol.agda
  2. +5 −1 README.agda
  3. +109 −0 Space/Torus.agda
View
@@ -0,0 +1,19 @@
+------------------------------------------------------------------------
+-- Symbols for paths
+------------------------------------------------------------------------
+
+-- Copyright (c) 2012 Favonia
+
+{-# OPTIONS --without-K #-}
+
+module Path.Symbol where
+
+open import Path
+
+!_ : {ℓ} {A : Set ℓ} {x y : A} x ≡ y y ≡ x
+!_ = sym
+
+_◇_ : {ℓ} {A : Set ℓ} {x y z : A} x ≡ y y ≡ z x ≡ z
+_◇_ = trans
+
+infixr 6 _◇_
View
@@ -49,6 +49,10 @@ import Path
-- Some really basic lemmas for equivalence of paths
import Path.Lemmas
+-- Fancy Unicode symbols for writing incomprehensible proofs
+-- (Subjecting to changes.)
+import Path.Symbol
+
-- Higher-order paths and loops
import Path.HigherOrder
@@ -111,7 +115,7 @@ import Space.Sphere.HopfJunior
import Space.Sphere.Omega1
-- Definition of torus
---import Space.Torus
+import Space.Torus
------------------------------------------------------------------------
-- The Univalence axiom
View
@@ -0,0 +1,109 @@
+------------------------------------------------------------------------
+-- Torus
+------------------------------------------------------------------------
+
+-- Copyright (c) 2012 Favonia
+
+{-# OPTIONS --without-K #-}
+
+module Space.Torus where
+
+open import Prelude
+
+open import Path
+open import Path.Lemmas
+open import Path.Symbol
+
+import Space.Sphere as S
+
+private
+ data T²′ : Set where
+ base′ : T²′
+
+ : Set
+T² = T²′
+
+base :
+base = base′
+
+postulate
+ loopα : base ≡ base
+ loopβ : base ≡ base
+ cell : loopα ◇ loopβ ≡ loopβ ◇ loopα
+
+T²-elim : {ℓ} (P : T² Set ℓ) (pbase : P base)
+ (ploopα : subst P loopα pbase ≡ pbase)
+ (ploopβ : subst P loopβ pbase ≡ pbase)
+ (pcell : subst (λ p subst P p pbase ≡ pbase) cell
+ (subst-trans P loopα loopβ pbase ◇ cong (subst P loopβ) ploopα ◇ ploopβ) ≡
+ (subst-trans P loopβ loopα pbase ◇ cong (subst P loopα) ploopβ ◇ ploopα))
+ x P x
+T²-elim _ pbase′ _ _ _ base′ = pbase′
+
+cong[dep]-trans : {ℓ₁} {ℓ₂} {A : Set ℓ₁} (B : A Set ℓ₂) (f : (x : A) B x)
+ {x y} (loop₁ : x ≡ y) {z} (loop₂ : y ≡ z)
+ cong[dep] B f (loop₁ ◇ loop₂) ≡
+ subst-trans B loop₁ loop₂ (f x) ◇ cong (subst B loop₂) (cong[dep] B f loop₁) ◇ cong[dep] B f loop₂
+cong[dep]-trans B f {x} =
+ elim′
+ (λ {y} p₁ {z} (p₂ : y ≡ z)
+ cong[dep] B f (p₁ ◇ p₂) ≡
+ subst-trans B p₁ p₂ (f x) ◇ cong (subst B p₂) (cong[dep] B f p₁) ◇ cong[dep] B f p₂)
+ (elim′
+ (λ {z} p₂
+ cong[dep] B f p₂ ≡
+ subst-trans B (refl _) p₂ (f x) ◇ cong[dep] B f p₂)
+ (refl _))
+
+cong[dep]-trans′ : {ℓ₁} {ℓ₂} {A : Set ℓ₁} (B : A Set ℓ₂) (f : (x : A) B x)
+ {x y} (loop₁ : x ≡ y) {z} (loop₂ : y ≡ z)
+ {bloop₁} (bloop₁-eq : cong[dep] B f loop₁ ≡ bloop₁)
+ {bloop₂} (bloop₂-eq : cong[dep] B f loop₂ ≡ bloop₂)
+ cong[dep] B f (loop₁ ◇ loop₂) ≡
+ subst-trans B loop₁ loop₂ (f x) ◇ cong (subst B loop₂) bloop₁ ◇ bloop₂
+cong[dep]-trans′ B f {x} =
+ elim′
+ (λ {y} p₁ {z} (p₂ : y ≡ z) {bp₁} (bp₁-eq : cong[dep] B f p₁ ≡ bp₁) {bp₂} (bp₂-eq : cong[dep] B f p₂ ≡ bp₂)
+ cong[dep] B f (p₁ ◇ p₂) ≡
+ subst-trans B p₁ p₂ (f x) ◇ cong (subst B p₂) bp₁ ◇ bp₂)
+ (elim′
+ (λ {z} p₂ {bp₁} (bp₁-eq : refl (f x) ≡ bp₁) {bp₂} (bp₂-eq : cong[dep] B f p₂ ≡ bp₂)
+ cong[dep] B f p₂ ≡
+ cong (subst B p₂) bp₁ ◇ bp₂)
+ (λ {bp₁} bp₁-eq {bp₂} bp₂-eq
+ bp₂-eq ◇ cong (λ p p ◇ bp₂) (bp₁-eq ◇ sym (cong-id bp₁))))
+
+postulate
+ T²-elim-loopα : {ℓ} (P : T² Set ℓ) (pbase : P base)
+ (ploopα : subst P loopα pbase ≡ pbase)
+ (ploopβ : subst P loopβ pbase ≡ pbase)
+ (pcell : subst (λ p subst P p pbase ≡ pbase) cell
+ (subst-trans P loopα loopβ pbase ◇ cong (subst P loopβ) ploopα ◇ ploopβ) ≡
+ (subst-trans P loopβ loopα pbase ◇ cong (subst P loopα) ploopβ ◇ ploopα))
+ cong[dep] P (T²-elim P pbase ploopα ploopβ pcell) loopα ≡ ploopα
+
+ T²-elim-loopβ : {ℓ} (P : T² Set ℓ) (pbase : P base)
+ (ploopα : subst P loopα pbase ≡ pbase)
+ (ploopβ : subst P loopβ pbase ≡ pbase)
+ (pcell : subst (λ p subst P p pbase ≡ pbase) cell
+ (subst-trans P loopα loopβ pbase ◇ cong (subst P loopβ) ploopα ◇ ploopβ) ≡
+ (subst-trans P loopβ loopα pbase ◇ cong (subst P loopα) ploopβ ◇ ploopα))
+ cong[dep] P (T²-elim P pbase ploopα ploopβ pcell) loopβ ≡ ploopβ
+
+ T²-elim-cell : {ℓ} (P : T² Set ℓ) (pbase : P base)
+ (ploopα : subst P loopα pbase ≡ pbase)
+ (ploopβ : subst P loopβ pbase ≡ pbase)
+ (pcell : subst (λ p subst P p pbase ≡ pbase) cell
+ (subst-trans P loopα loopβ pbase ◇ cong (subst P loopβ) ploopα ◇ ploopβ) ≡
+ (subst-trans P loopβ loopα pbase ◇ cong (subst P loopα) ploopβ ◇ ploopα))
+ let
+ eliminator = T²-elim P pbase ploopα ploopβ pcell
+ elim-loopα = T²-elim-loopα P pbase ploopα ploopβ pcell
+ elim-loopβ = T²-elim-loopβ P pbase ploopα ploopβ pcell
+ convertαβ = cong[dep]-trans′ P eliminator loopα loopβ elim-loopα elim-loopβ
+ convertβα = cong[dep]-trans′ P eliminator loopβ loopα elim-loopβ elim-loopα
+ in
+ cong (subst (λ p subst P p pbase ≡ pbase) cell) (sym convertαβ) ◇
+ cong[dep] (λ p subst P p pbase ≡ pbase) (cong[dep] P eliminator) cell ◇
+ convertβα ≡
+ pcell

0 comments on commit df07788

Please sign in to comment.