Permalink
Browse files

Add flowers

- Plant some flowers, generalized circles.

- Update `README.agda`.
  • Loading branch information...
1 parent c8876f0 commit b134eab4285d44f308bc5c11fe565fc13c8ef1bb @favonia committed Jun 5, 2012
Showing with 67 additions and 1 deletion.
  1. +4 −1 README.agda
  2. +63 −0 Space/Flower.agda
View
@@ -75,7 +75,10 @@ import Space.Bool-alternative
-- Basic facts about Fin
import Space.Fin.Lemmas
--- Definition of free groups (work in progress)
+-- Definition of flowers
+import Space.Flower
+
+-- Definition of free groups
import Space.FreeGroup
-- Definition of integers
View
@@ -0,0 +1,63 @@
+module Space.Flower where
+
+open import Prelude
+
+open import Path
+open import Path.Lemmas
+
+private
+ data Flower′ (n : ℕ) : Set where
+ core : Flower′ n
+
+Flower : Set
+Flower n = Flower′ n
+
+-- Dependent version
+
+postulate
+ petal : {n} Fin n _≡_ {A = Flower n} core core
+
+Flower-elim : {ℓ} {n} (P : Flower n Set ℓ)
+ (pcore : P core)
+ (ppetal : i subst P (petal i) pcore ≡ pcore)
+ f P f
+Flower-elim _ pcore _ core = pcore
+
+postulate
+ Flower-elim-petal : {ℓ} {n} (P : Flower n Set ℓ)
+ (pcore : P core)
+ (ppetal : i subst P (petal i) pcore ≡ pcore)
+ i cong[dep] P (Flower-elim P pcore ppetal) (petal i) ≡ ppetal i
+
+-- Non-dependent version
+
+Flower-elim[simp] : {ℓ} {n} {P : Set ℓ}
+ (pcore : P) (ppetal : (i : Fin n) pcore ≡ pcore)
+ f P
+Flower-elim[simp] {n = n} {P = P} pcore ppetal =
+ Flower-elim (const P) pcore (λ i trans (boring-petal i) (ppetal i))
+ where
+ boring-petal : (i : Fin n) subst (const P) (petal i) pcore ≡ pcore
+ boring-petal i = subst-const (petal i) pcore
+
+-- This propositional equality is derivable from the dependent version.
+Flower-elim[simp]-petal : {ℓ} {n} {P : Set ℓ}
+ (pcore : P)
+ (ppetal : (i : Fin n) pcore ≡ pcore)
+ i cong (Flower-elim[simp] pcore ppetal) (petal i) ≡ ppetal i
+Flower-elim[simp]-petal {n = n} {P = P} pcore ppetal i =
+ cong pflower (petal i)
+ ≡⟨ sym $ trans-sym-trans (boring-petal i) _ ⟩
+ trans (sym $ boring-petal i) (trans (boring-petal i) $ cong pflower $ petal i)
+ ≡⟨ cong (trans $ sym $ boring-petal i) $ sym $ cong[dep]-const pflower (petal i) ⟩
+ trans (sym $ boring-petal i) (cong[dep] (const P) pflower $ petal i)
+ ≡⟨ cong (trans $ sym $ boring-petal i) $ Flower-elim-petal (const P) _ _ i ⟩
+ trans (sym $ boring-petal i) (trans (boring-petal i) $ ppetal i)
+ ≡⟨ trans-sym-trans (boring-petal i) _ ⟩∎
+ ppetal i
+ ∎
+ where
+ boring-petal : (i : Fin n) subst (const P) (petal i) pcore ≡ pcore
+ boring-petal i = subst-const (petal i) pcore
+
+ pflower = Flower-elim[simp] pcore ppetal

0 comments on commit b134eab

Please sign in to comment.