Skip to content
Browse files

Sn and revamped tools for higher-order paths

(1) Sn and its dependent elimination rule
(2) Revamped library for higher-order paths
  • Loading branch information...
1 parent 609a4af commit a3795e76e94fa6602471d0c59839d4478e4d37d7 @favonia committed
Showing with 269 additions and 113 deletions.
  1. 0 LICENCE → LICENSE
  2. +53 −69 Path/Higher-order.agda
  3. +5 −7 Path/Omega2-abelian.agda
  4. +8 −2 README.agda
  5. +20 −0 Space/Nat/Lemmas.agda
  6. +183 −35 Space/Sphere.agda
View
0 LICENCE → LICENSE
File renamed without changes.
View
122 Path/Higher-order.agda
@@ -9,17 +9,15 @@ module Path.Higher-order where
open import Prelude
open import Path
open import Path.Lemmas
+open import Space.Nat.Lemmas
--- TODO Generic boring paths for the case that B is a constant function.
--- TODO Build a nicer interface for Env. (Although the hidden definition
--- the one suitable for induction...) Make sure definitional equalities
--- hold for all finite cases.
+-- TODO Generalized cong[dep]-const lemma
------------------------------------------------------------------------
-- Higher-order loop spaces
Ω : {ℓ} n {A : Set ℓ} A Set ℓ
-Ω-refl : {ℓ} n {A : Set ℓ} (base : A) Ω n base
+private Ω-refl : {ℓ} n {A : Set ℓ} (base : A) Ω n base
Ω 0 {A} _ = A
Ω (suc n) {A} base = Ω-refl n base ≡ Ω-refl n base
@@ -30,71 +28,57 @@ open import Path.Lemmas
------------------------------------------------------------------------
-- Higher-order path spaces
--- This definition is not suitable for inductive definition of cong[dep]⇑
---Paths⇑ : {ℓ} n Set ℓ Set ℓ
---Paths⇑ 0 A = A
---Paths⇑ (suc i) A = Σ A (λ x Σ A (λ y Paths⇑ i (x ≡ y)))
-
--- Env 0 = tt
--- Env 1 = (tt , (x₁ , y₁))
--- Env 2 = ((tt , (x₁ , y₁)) , (x₂ , y₂))
--- Env 3 = (((tt , (x₁ , y₁)) , (x₂ , y₂)) , (x₃ , y₃))
-private
- Env⇑ : {ℓ} n Set ℓ Set ℓ
- Path⇑ : {ℓ} n (A : Set ℓ) Env⇑ n A Set ℓ
-
- Env⇑ {ℓ} 0 A = ↑ ℓ ⊤
- Env⇑ {ℓ} 1 A = A × A
- Env⇑ (suc (suc i)) A = Σ (Env⇑ i A) (λ e Path⇑ i A e × Path⇑ i A e)
-
- Path⇑ 0 A _ = A
- Path⇑ 1 A (x , y) = x ≡ y
- Path⇑ (suc (suc i)) A (_ , (x , y)) = x ≡ y
-
---usable but useless
---Paths⇑ : {ℓ} n Set ℓ Set ℓ
---Paths⇑ n A = Σ (Env⇑ n A) (Path⇑ n A)
-
--- These interfaces will be changed
-Cong[dep]-env⇑ : {ℓ} n Set ℓ Set ℓ
-Cong[dep]-env⇑ = Env⇑
-
-Cong[dep]⇑ : {ℓ₁ ℓ₂} n {A : Set ℓ₁} (B : A Set ℓ₂) (f : (x : A) B x)
- (e : Env⇑ n A) (p : Path⇑ n A e) Set ℓ₂
+-- Endpoints[d] 0 = tt
+-- Endpoints[d] 1 = (tt, x₁ , y₁)
+-- Endpoints[d] 2 = ((tt, x₁ , y₂) , x₂ , y₂)
+
+-- This definition is perfect for induction but probably not user-friendly
+Endpoints⇑ : {ℓ} n Set ℓ Set ℓ
+Path⇑ : {ℓ} n {A : Set ℓ} Endpoints⇑ n A Set ℓ
+
+Endpoints⇑ {ℓ} 0 A = ↑ ℓ ⊤
+Endpoints⇑ (suc n) A = Σ (Endpoints⇑ n A) (λ c Path⇑ n c × Path⇑ n c)
+
+Path⇑ 0 {A} _ = A
+Path⇑ (suc n) (_ , x , y) = x ≡ y
+
+-- This definition is terrible for induction, but seems nicer to use?
+Endpoints′⇑ : {ℓ} n Set ℓ Set ℓ
+Endpoints′⇑ {ℓ} 0 A = ↑ ℓ ⊤
+Endpoints′⇑ (suc n) A = Σ A (λ x Σ A ( λ y Endpoints′⇑ n (x ≡ y)))
+
+-- A helper function to convert the above definition
+endpoints′⇒endpoints⇑ : {ℓ} n m {A : Set ℓ} (cA : Endpoints⇑ n A) Endpoints′⇑ m (Path⇑ n cA) Endpoints⇑ (m + n) A
+endpoints′⇒endpoints⇑ n 0 c _ = c
+endpoints′⇒endpoints⇑ n (suc m) {A} c (x , y , p) =
+ subst (λ n Endpoints⇑ n A) (n+suc m n) $ endpoints′⇒endpoints⇑ (suc n) m (_ , (x , y)) p
+
+-- A section that parametrized by a high-order path
+-- Endpoints[d] 0 = tt
+-- Endpoints[d] 1 = (tt, bx₁ , by₁)
+-- Endpoints[d] 2 = ((tt, bx₁ , by₂) , bx₂ , by₂)
+Endpoints[dep]⇑ : {ℓ₁ ℓ₂} n {A : Set ℓ₁} (B : A Set ℓ₂) Endpoints⇑ n A Set ℓ₂
+Path[dep]⇑ : {ℓ₁ ℓ₂} n {A : Set ℓ₁} (B : A Set ℓ₂) {cA : Endpoints⇑ n A} Path⇑ n cA Endpoints[dep]⇑ n B cA Set ℓ₂
+
+Endpoints[dep]⇑ {ℓ₁} {ℓ₂} 0 _ _ = ↑ ℓ₂ ⊤
+Endpoints[dep]⇑ (suc n) B (cA , x , y) = Σ (Endpoints[dep]⇑ n B cA)
+ (λ c Path[dep]⇑ n B x c × Path[dep]⇑ n B y c)
+
+Path[dep]⇑ 0 B a _ = B a
+Path[dep]⇑ (suc n) B a (cB , bx , by) = subst (λ x Path[dep]⇑ n B x cB) a bx ≡ by
+
+-- Higher-order cong(ruence) that takes high-order paths
+-- Reuse Path[dep] to avoid all sorts of problems in Space.Sphere
+cong-endpoints[dep]⇑ : {ℓ₁ ℓ₂} n {A : Set ℓ₁} (B : A Set ℓ₂) (f : (x : A) B x)
+ (cA : Endpoints⇑ n A) Endpoints[dep]⇑ n B cA
cong[dep]⇑ : {ℓ₁ ℓ₂} n {A : Set ℓ₁} (B : A Set ℓ₂) (f : (x : A) B x)
- (e : Env⇑ n A) (p : Path⇑ n A e) Cong[dep]⇑ n B f _ p
+ (cA : Endpoints⇑ n A) (pA : Path⇑ n cA) Path[dep]⇑ n B pA (cong-endpoints[dep]⇑ n B f cA)
-Cong[dep]⇑ 0 B f _ p = B p
-Cong[dep]⇑ 1 B f (x , y) p = subst B p (f x) ≡ (f y)
-Cong[dep]⇑ (suc (suc i)) B f (_ , (x , y)) p = subst (Cong[dep]⇑ i B f _) p (cong[dep]⇑ i B f _ x) ≡ cong[dep]⇑ i B f _ y
+cong-endpoints[dep]⇑ 0 B f _ = lift tt
+cong-endpoints[dep]⇑ (suc n) B f (cA , x , y) = (cong-endpoints[dep]⇑ n B f cA ,
+ cong[dep]⇑ n B f cA x ,
+ cong[dep]⇑ n B f cA y)
-cong[dep]⇑ 0 B f _ p = f p
-cong[dep]⇑ 1 B f (x , y) p = cong[dep] B f p
-cong[dep]⇑ (suc (suc i)) B f (_ , (x , y)) p = cong[dep] (Cong[dep]⇑ i B f _) (cong[dep]⇑ i B f _) p
-
--- Env 0 = tt
--- Env 1 = (tt , ((ax₁ , bx₁) , (ay₁ , by₁)))
--- Env 2 = ((tt , ((ax₁ , bx₁) , (ay₁ , by₂))) , ((ax₂ , bx₂) , (ay₂ , by₂)))
-private
- Env[d]⇑ : {ℓ₁ ℓ₂} n {A : Set ℓ₁} (B : A Set ℓ₂) Set (ℓ₁ ⊔ ℓ₂)
- PathA[d]⇑ : {ℓ₁ ℓ₂} n {A : Set ℓ₁} (B : A Set ℓ₂) Env[d]⇑ n B Set ℓ₁
- PathB[d]⇑ : {ℓ₁ ℓ₂} n {A : Set ℓ₁} (B : A Set ℓ₂) (e : Env[d]⇑ n B) PathA[d]⇑ n B e Set ℓ₂
-
- Env[d]⇑ {ℓ₁} {ℓ₂} 0 B = ↑ (ℓ₁ ⊔ ℓ₂) ⊤
- Env[d]⇑ (suc i) B = Σ (Env[d]⇑ i B) (λ e Σ (PathA[d]⇑ i B e) (PathB[d]⇑ i B e) ×
- Σ (PathA[d]⇑ i B e) (PathB[d]⇑ i B e))
-
- PathA[d]⇑ 0 {A} _ _ = A
- PathA[d]⇑ (suc i) _ (_ , ((ax , _) , (ay , _))) = ax ≡ ay
-
- PathB[d]⇑ 0 B _ a = B a
- PathB[d]⇑ (suc i) B (_ , ((_ , bx) , (_ , by))) a = subst (PathB[d]⇑ i B _) a bx ≡ by
-
--- This interface will be changed
-PathB[dep]⇑-env : {ℓ₁ ℓ₂} n {A : Set ℓ₁} (B : A Set ℓ₂) Set (ℓ₁ ⊔ ℓ₂)
-PathB[dep]⇑-env = Env[d]⇑
-
--- This interface will be changed
-PathB[dep]⇑ : {ℓ₁ ℓ₂} n {A : Set ℓ₁} (B : A Set ℓ₂) (e : Env[d]⇑ n B) PathA[d]⇑ n B e Set ℓ₂
-PathB[dep]⇑ = PathB[d]⇑
+cong[dep]⇑ 0 B f t p = f p
+cong[dep]⇑ (suc n) B f (cA , (x , y)) p = cong[dep] (λ x Path[dep]⇑ n B x (cong-endpoints[dep]⇑ n B f cA)) (cong[dep]⇑ n B f cA) p
View
12 Path/Omega2-abelian.agda
@@ -23,12 +23,10 @@ module Path.Omega2-abelian {ℓ} {A : Set ℓ} (base : A) where
open import Prelude hiding (_∘_)
open import Path
open import Path.Lemmas
+open import Path.Higher-order
private
- Ω₁A = base ≡ base
- Ω₂A = refl base ≡ refl base
-
- lemma₁ : (p : Ω₂A) cong (λ p′ trans p′ (refl base)) p ≡ p
+ lemma₁ : (p : Ω 2 base) cong (λ p′ trans p′ (refl base)) p ≡ p
lemma₁ p = elim″ (λ {x} p cong (λ p trans p (refl _)) p ≡ trans (trans-reflʳ x) p) (refl _) p
lemma₂ : {ℓ₁ ℓ₂ ℓ₃} {A : Set ℓ₁} {B : Set ℓ₂} {C : Set ℓ₃}
@@ -36,7 +34,7 @@ private
(p : x ≡ y) (q : u ≡ v) cong₂ f p q ≡ cong₂′ f p q
lemma₂ f p q = elim (λ {_ _} p cong₂ f p q ≡ cong₂′ f p q) (λ _ sym $ trans-reflʳ _) p
-abelian : (p q : Ω₂A) trans p q ≡ trans q p
+abelian : (p q : Ω 2 base) trans p q ≡ trans q p
abelian p q =
trans p q ≡⟨ cong (trans p) $ sym $ cong-id q ⟩
trans p (cong id q) ≡⟨ cong (flip trans (cong id q)) $ sym $ lemma₁ p ⟩
@@ -93,14 +91,14 @@ private
_∙_ = cong₂ trans
unit = refl (refl base)
- trans-unital : IsUnital Ω₂A _∘_ unit
+ trans-unital : IsUnital 2 base) _∘_ unit
trans-unital = record
{ unitʳ = trans-reflʳ
; unitˡ = λ _ refl _
--; assoc = trans-assoc
}
- cong₂-trans-unital : IsUnital Ω₂A _∙_ unit
+ cong₂-trans-unital : IsUnital 2 base) _∙_ unit
cong₂-trans-unital = record
{ unitʳ = unitʳ
; unitˡ = unitˡ
View
10 README.agda
@@ -5,10 +5,12 @@
------------------------------------------------------------------------
-- Copyright (c) 2012 Favonia
--- Copyright (c) 2011-2012 Nils Anders Danielsson
+-- released under BSD-like license (See LICENSE)
--- A large portion of code was shamelessly copied from Nils' library
+-- A large portion of code was shamelessly copied from Nils Anders Danielsson'
+-- library released under BSD-like license (See LICENCE-Nils)
-- http://www.cse.chalmers.se/~nad/repos/equality/
+-- Copyright (c) 2011-2012 Nils Anders Danielsson
{-# OPTIONS --without-K #-}
@@ -78,6 +80,10 @@ import Space.Integer
-- Definition of intervals
import Space.Interval
+-- Some basic facts about Nat
+-- (Definition of Nat is in the Prelude)
+import Space.Nat.Lemmas
+
-- Definition of spheres (base + loop)
import Space.Sphere
View
20 Space/Nat/Lemmas.agda
@@ -0,0 +1,20 @@
+------------------------------------------------------------------------
+-- Basic facts about natural numbers.
+------------------------------------------------------------------------
+
+-- Copyright (c) 2012 Favonia
+
+{-# OPTIONS --without-K #-}
+
+module Space.Nat.Lemmas where
+
+open import Prelude
+open import Path
+
+n+0 : n n + 0 ≡ n
+n+0 0 = refl _
+n+0 (suc n) = cong suc $ n+0 n
+
+n+suc : n m n + suc m ≡ suc n + m
+n+suc 0 m = refl _
+n+suc (suc n) m = cong suc $ n+suc n m
View
218 Space/Sphere.agda
@@ -13,6 +13,12 @@ module Space.Sphere where
open import Prelude
open import Path
open import Path.Lemmas
+open import Path.Sum
+open import Path.Higher-order
+
+------------------------------------------------------------------------
+-- Safe area: S¹ only
+------------------------------------------------------------------------
------------------------------------------------------------------------
-- Formation rules and introduction rules
@@ -44,76 +50,218 @@ loop = loop¹
-- Dependent version
-S¹-elim : {ℓ} (P : S¹ Set ℓ) (dbase : P base) subst P loop¹ dbasedbase (x : S¹) P x
-S¹-elim _ dbase _ base¹′ = dbase
+S¹-elim : {ℓ} (P : S¹ Set ℓ) (pbase : P base) subst P loop¹ pbasepbase (x : S¹) P x
+S¹-elim _ pbase _ base¹′ = pbase
-- This is actually definitionally equality...
postulate
- S¹-elim-loop : {ℓ} (P : S¹ Set ℓ) (dbase : P base) (dloop : subst P loop¹ dbasedbase)
- cong[dep] P (S¹-elim P dbase dloop) loop¹ ≡ dloop
+ S¹-elim-loop : {ℓ} (P : S¹ Set ℓ) (pbase : P base) (ploop : subst P loop¹ pbasepbase)
+ cong[dep] P (S¹-elim P pbase ploop) loop¹ ≡ ploop
-- Non-dependent version
-S¹-elim[simp] : {ℓ} {P : Set ℓ} (dbase : P) dbasedbase P
-S¹-elim[simp] {P = P} dbase dloop = S¹-elim (const P) dbase (trans boring-loop dloop)
+S¹-elim[simp] : {ℓ} {P : Set ℓ} (pbase : P) pbasepbase P
+S¹-elim[simp] {P = P} pbase ploop = S¹-elim (const P) pbase (trans boring-loop ploop)
where
- boring-loop = subst-const loop dbase
+ boring-loop = subst-const loop pbase
-- This propositional equality is derivable from the dependent version.
-S¹-elim[simp]-loop : {ℓ} {P : Set ℓ} (dbase : P) (dloop : dbasedbase)
- cong (S¹-elim[simp] dbase dloop) loop¹ ≡ dloop
-S¹-elim[simp]-loop {P = P} dbase dloop =
+S¹-elim[simp]-loop : {ℓ} {P : Set ℓ} (pbase : P) (ploop : pbasepbase)
+ cong (S¹-elim[simp] pbase ploop) loop¹ ≡ ploop
+S¹-elim[simp]-loop {P = P} pbase ploop =
cong dcircle loop¹ ≡⟨ sym $ trans-sym-trans boring-loop _ ⟩
trans (sym $ boring-loop) (trans boring-loop $ cong dcircle loop¹) ≡⟨ cong (trans $ sym $ boring-loop) $ sym $ cong[dep]-const dcircle loop¹ ⟩
trans (sym $ boring-loop) (cong[dep] (const P) dcircle loop¹) ≡⟨ cong (trans $ sym $ boring-loop) $ S¹-elim-loop (const P) _ _ ⟩
- trans (sym $ boring-loop) (trans boring-loop dloop) ≡⟨ trans-sym-trans boring-loop _ ⟩∎
- dloop
+ trans (sym $ boring-loop) (trans boring-loop ploop) ≡⟨ trans-sym-trans boring-loop _ ⟩∎
+ ploop
where
- boring-loop = subst-const loop¹ dbase
- dcircle = S¹-elim[simp] dbase dloop
+ boring-loop = subst-const loop¹ pbase
+ dcircle = S¹-elim[simp] pbase ploop
------------------------------------------------------------------------
--- WARNING : S² is still experimental
+-- Experimental area: S² and beyond!
+------------------------------------------------------------------------
------------------------------------------------------------------------
-- Formation rules and introduction rules
private
- data S²′ : Set where
- base²′ : S²′
+ data Sⁿ′ (n : ℕ) : Set where
+ baseⁿ′ : Sⁿ′ n
+
+Sⁿ : Set
+Sⁿ = Sⁿ′
+
+baseⁿ : n Sⁿ n
+baseⁿ n = baseⁿ′
+
+private
+ S-endpoints⇑ : n {S : Set} S Endpoints⇑ n S
+ S-loop⇑ : n {S : Set} (base : S) Path⇑ n (S-endpoints⇑ n base)
- : Set
-= S²′
+ S-endpoints⇑ 0 base = lift tt
+ S-endpoints⇑ (suc n) base = (S-endpoints⇑ n base , S-loop⇑ n base , S-loop⇑ n base)
-base² :
-base² = base²′
+ S-loop⇑ 0 base = base
+ S-loop⇑ (suc n) base = refl (S-loop⇑ n base)
+
+ Sⁿ-endpoints : n Endpoints⇑ n (Sⁿ n)
+ Sⁿ-endpoints n = S-endpoints⇑ n (baseⁿ n)
-- Agda seems to think these are NOT definitionally equal
abstract
- loop² : refl base² ≡ refl base²
- loop² = refl (refl base²)
+ loopⁿ : n Path⇑ n (Sⁿ-endpoints n)
+ loopⁿ n = S-loop⇑ n (baseⁿ n)
+
+private
+ -- Some test cases for "Path⇑ n (Sⁿ-endpoints n)"
+ -- Things need to be definitionally equal to what we expect in all finite cases.
+ module Test where
+ test₀ : Path⇑ 0 (Sⁿ-endpoints 0) ≡ Sⁿ 0
+ test₀ = refl _
+
+ test₁ : Path⇑ 1 (Sⁿ-endpoints 1) ≡ (baseⁿ 1 ≡ baseⁿ 1)
+ test₁ = refl _
+
+ test₂ : Path⇑ 2 (Sⁿ-endpoints 2) ≡ (refl (baseⁿ 2) ≡ refl (baseⁿ 2))
+ test₂ = refl _
+
+private
+ S-endpoints[dep]⇑ : {ℓ} n {S : Set} (P : S Set ℓ) (base : S) (pbase : P base)
+ Endpoints[dep]⇑ n P (S-endpoints⇑ n base)
+ S-loop[dep]⇑ : {ℓ} n {S : Set} (P : S Set ℓ) (base : S) (pbase : P base)
+ Path[dep]⇑ n P (S-loop⇑ n base) (S-endpoints[dep]⇑ n P base pbase)
+
+ S-endpoints[dep]⇑ 0 P base pbase = lift tt
+ S-endpoints[dep]⇑ (suc n) P base pbase = (S-endpoints[dep]⇑ n P base pbase ,
+ S-loop[dep]⇑ n P base pbase ,
+ S-loop[dep]⇑ n P base pbase)
+
+ S-loop[dep]⇑ 0 P base pbase = pbase
+ S-loop[dep]⇑ (suc n) P base pbase = refl (S-loop[dep]⇑ n P base pbase)
+
+ Sⁿ-endpoints[dep] : {ℓ} n (P : Sⁿ n Set ℓ) P (baseⁿ n) Endpoints[dep]⇑ n P (Sⁿ-endpoints n)
+ Sⁿ-endpoints[dep] n P pbase = S-endpoints[dep]⇑ n P (baseⁿ n) pbase
------------------------------------------------------------------------
-- Elimination rules and computation rules
-- Dependent version
+Sⁿ-elim : {ℓ} n (P : Sⁿ n Set ℓ) (pbase : P (baseⁿ n)) Path[dep]⇑ n P (loopⁿ n) (Sⁿ-endpoints[dep] n P pbase) x P x
+Sⁿ-elim n P pbase _ baseⁿ′ = pbase
-S²-elim : {ℓ} (P : S² Set ℓ) (dbase : P base²) subst (λ p subst P p dbase ≡ dbase) loop² (refl dbase) ≡ refl dbase (x : S²) P x
-S²-elim _ dbase _ base²′ = dbase
+private
+ -- Some test cases for "Path[dep]⇑ n P (loopⁿ n) (Sⁿ-endpoints[dep] n P pbase)"
+ module Test where
+ test₀ : {ℓ} (P : Sⁿ 0 Set ℓ) (pbase : P (baseⁿ 0))
+ Path[dep]⇑ 0 P (loopⁿ 0) (Sⁿ-endpoints[dep] 0 P pbase) ≡ P (loopⁿ 0)
+ test₀ _ _ = refl _
--- This is actually definitionally equality...
-postulate
- S²-elim-loop : {ℓ} (P : S² Set ℓ) (dbase : P base²) (dloop : subst (λ p subst P p dbase ≡ dbase) loop² (refl dbase) ≡ refl dbase)
- cong[dep] (λ p subst P p dbase ≡ dbase) (cong[dep] P (S²-elim P dbase dloop)) loop² ≡ dloop
+ test₁ : {ℓ} (P : Sⁿ 1 Set ℓ) (pbase : P (baseⁿ 1))
+ Path[dep]⇑ 1 P (loopⁿ 1) (Sⁿ-endpoints[dep] 1 P pbase) ≡ (subst P (loopⁿ 1) pbase ≡ pbase)
+ test₁ _ _ = refl _
--- Non-dependent version
+ test₂ : {ℓ} (P : Sⁿ 2 Set ℓ) (pbase : P (baseⁿ 2))
+ Path[dep]⇑ 2 P (loopⁿ 2) (Sⁿ-endpoints[dep] 2 P pbase) ≡ (subst (λ p subst P p pbase ≡ pbase) (loopⁿ 2) (refl pbase) ≡ refl pbase)
+ test₂ _ _ = refl _
+
+private
+ cong-,, : {ℓ₁ ℓ₂} {A : Set ℓ₁} (B : A Set ℓ₂) {x y : A} (p : x ≡ y)
+ {x₁ : B x} {y₁ : B y} (p₁ : subst B p x₁ ≡ y₁)
+ {x₂ : B x} {y₂ : B y} (p₂ : subst B p x₂ ≡ y₂)
+ (x , x₁ , x₂) ≡ (y , y₁ , y₂)
+ cong-,, B = elim
+ (λ {x y} (p : x ≡ y)
+ {x₁} {y₁} (p₁ : subst B p x₁ ≡ y₁)
+ {x₂} {y₂} (p₂ : subst B p x₂ ≡ y₂)
+ (x , x₁ , x₂) ≡ (y , y₁ , y₂))
+ (λ x p₁ p₂ cong₂ (λ x₁ x₂ (x , x₁ , x₂)) p₁ p₂)
+
+ subst-cong-,, : {ℓ₁ ℓ₂} {A : Set ℓ₁} (B : A Set ℓ₂) {x y : A} (p : x ≡ y)
+ {x₁₂ : B x} {y₁₂ : B y} (p₁₂ : subst B p x₁₂ ≡ y₁₂)
+ subst (λ s proj₁ (proj₂ s) ≡ proj₂ (proj₂ s)) (cong-,, B p p₁₂ p₁₂) (refl x₁₂) ≡ refl y₁₂
+ subst-cong-,, B = elim
+ (λ {x y} p
+ {x₁₂ : B x} {y₁₂ : B y} (p₁₂ : subst B p x₁₂ ≡ y₁₂)
+ subst (λ s proj₁ (proj₂ s) ≡ proj₂ (proj₂ s)) (cong-,, B p p₁₂ p₁₂) (refl x₁₂) ≡ refl y₁₂)
+ (λ x elim
+ (λ {x₁₂ y₁₂} p₁₂
+ subst (λ s proj₁ (proj₂ s) ≡ proj₂ (proj₂ s)) (cong-,, B (refl x) p₁₂ p₁₂) (refl x₁₂) ≡ refl y₁₂)
+ (λ x₁₂ refl _))
+
+ lemma₁ : {ℓ} m {S} (P : S Set ℓ) (f : (x : S) P x) (b : S)
+ cong-endpoints[dep]⇑ m P f (S-endpoints⇑ m b) ≡ S-endpoints[dep]⇑ m P b (f b)
+ lemma₂ : {ℓ} m {S} (P : S Set ℓ) (f : (x : S) P x) (b : S)
+ subst (Path[dep]⇑ m P (S-loop⇑ m b)) (lemma₁ m P f b)
+ (cong[dep]⇑ m P f (S-endpoints⇑ m b) (S-loop⇑ m b)) ≡
+ S-loop[dep]⇑ m P b (f b)
+
+ lemma₁ 0 _ _ _ = refl _
+ lemma₁ (suc m) P f b = cong-,, (Path[dep]⇑ m P (S-loop⇑ m b)) (lemma₁ m P f b) (lemma₂ m P f b) (lemma₂ m P f b)
+
+ lemma₂ 0 _ _ _ = refl _
+ lemma₂ (suc m) P f b = subst-cong-,, (Path[dep]⇑ m P (S-loop⇑ m b)) (lemma₁ m P f b) (lemma₂ m P f b)
+
+ lemma-main : {ℓ} n (P : Sⁿ n Set ℓ) (pbase : P (baseⁿ n)) (ploop : Path[dep]⇑ n P (loopⁿ n) (Sⁿ-endpoints[dep] n P pbase))
+ cong-endpoints[dep]⇑ n P (Sⁿ-elim n P pbase ploop) (Sⁿ-endpoints n) ≡ Sⁿ-endpoints[dep] n P pbase
+ lemma-main n P pbase ploop = lemma₁ n P (Sⁿ-elim n P pbase ploop) (baseⁿ n)
-S²-elim[simp] : {ℓ} {P : Set ℓ} (dbase : P) refl dbase ≡ refl dbase P
-S²-elim[simp] {P = P} dbase dloop = S²-elim (const P) dbase (trans boring-loop dloop)
+private
+ -- Some test cases for the type of "lemma-main"
+ module Test where
+ test₀ : {ℓ} (P : Sⁿ 0 Set ℓ) (pbase : P (baseⁿ 0)) (ploop : Path[dep]⇑ 0 P (loopⁿ 0) (Sⁿ-endpoints[dep] 0 P pbase))
+ lemma-main 0 P pbase ploop ≡ refl _
+ test₀ _ _ _ = refl _
+
+ test₁ : {ℓ} (P : Sⁿ 1 Set ℓ) (pbase : P (baseⁿ 1)) (ploop : Path[dep]⇑ 1 P (loopⁿ 1) (Sⁿ-endpoints[dep] 1 P pbase))
+ lemma-main 1 P pbase ploop ≡ refl _
+ test₁ _ _ _ = refl _
+
+ test₂ : {ℓ} (P : Sⁿ 2 Set ℓ) (pbase : P (baseⁿ 2)) (ploop : Path[dep]⇑ 2 P (loopⁿ 2) (Sⁿ-endpoints[dep] 2 P pbase))
+ lemma-main 2 P pbase ploop ≡ refl _
+ test₂ _ _ _ = refl _
+
+ test₁₀ : {ℓ} (P : Sⁿ 10 Set ℓ) (pbase : P (baseⁿ 10)) (ploop : Path[dep]⇑ 10 P (loopⁿ 10) (Sⁿ-endpoints[dep] 10 P pbase))
+ lemma-main 10 P pbase ploop ≡ refl _
+ test₁₀ _ _ _ = refl _
+
+postulate
+ Sⁿ-elim-loop : {ℓ} n (P : Sⁿ n Set ℓ) (pbase : P (baseⁿ n)) (ploop : Path[dep]⇑ n P (loopⁿ n) (Sⁿ-endpoints[dep] n P pbase))
+ subst (Path[dep]⇑ n P (loopⁿ n)) (lemma-main n P pbase ploop)
+ (cong[dep]⇑ n P (Sⁿ-elim n P pbase ploop) (Sⁿ-endpoints n) (loopⁿ n)) ≡
+ ploop
+
+private
+ -- Some test cases for the type of the LHS of "Sⁿ-elim-loop"
+ module Test where
+ test₀ : {ℓ} (P : Sⁿ 0 Set ℓ) (pbase : P (baseⁿ 0)) (ploop : Path[dep]⇑ 0 P (loopⁿ 0) (Sⁿ-endpoints[dep] 0 P pbase))
+ subst (Path[dep]⇑ 0 P (loopⁿ 0)) (lemma-main 0 P pbase ploop)
+ (cong[dep]⇑ 0 P (Sⁿ-elim 0 P pbase ploop) (Sⁿ-endpoints 0) (loopⁿ 0))
+ ≡ (Sⁿ-elim 0 P pbase ploop) (loopⁿ 0)
+ test₀ _ _ _ = refl _
+
+ test₁ : {ℓ} (P : Sⁿ 1 Set ℓ) (pbase : P (baseⁿ 1)) (ploop : Path[dep]⇑ 1 P (loopⁿ 1) (Sⁿ-endpoints[dep] 1 P pbase))
+ subst (Path[dep]⇑ 1 P (loopⁿ 1)) (lemma-main 1 P pbase ploop)
+ (cong[dep]⇑ 1 P (Sⁿ-elim 1 P pbase ploop) (Sⁿ-endpoints 1) (loopⁿ 1))
+ ≡ cong[dep] P (Sⁿ-elim 1 P pbase ploop) (loopⁿ 1)
+ test₁ _ _ _ = refl _
+
+ test₂ : {ℓ} (P : Sⁿ 2 Set ℓ) (pbase : P (baseⁿ 2)) (ploop : Path[dep]⇑ 2 P (loopⁿ 2) (Sⁿ-endpoints[dep] 2 P pbase))
+ subst (Path[dep]⇑ 2 P (loopⁿ 2)) (lemma-main 2 P pbase ploop)
+ (cong[dep]⇑ 2 P (Sⁿ-elim 2 P pbase ploop) (Sⁿ-endpoints 2) (loopⁿ 2))
+ ≡ cong[dep] (λ p subst P p pbase ≡ pbase) (cong[dep] P (Sⁿ-elim 2 P pbase ploop)) (loopⁿ 2)
+ test₂ _ _ _ = refl _
+
+{-
+-- TODO Non-dependent version for Sⁿ
+
+S²-elim[simp] : ∀ {ℓ} {P : Set ℓ} (pbase : P) → refl pbase ≡ refl pbase → S² → P
+S²-elim[simp] {P = P} pbase ploop = S²-elim (const P) pbase (trans boring-loop ploop)
where
- boring-loop = cong[dep] (λ p subst (const P) p dbasedbase) (λ p subst-const p dbase) loop²
+ boring-loop = cong[dep] (λ p → subst (const P) p pbasepbase) (λ p → subst-const p pbase) loop²
-- TODO This rule should be derivable from the dependent one
postulate
- S²-elim[simp]-loop : {ℓ} {P : Set ℓ} (dbase : P) (dloop : refl dbase ≡ refl dbase)
- cong (cong (S²-elim[simp] dbase dloop)) loop² ≡ dloop
+ S²-elim[simp]-loop : ∀ {ℓ} {P : Set ℓ} (pbase : P) (ploop : refl pbase ≡ refl pbase)
+ → cong (cong (S²-elim[simp] pbase ploop)) loop² ≡ ploop
+-}

0 comments on commit a3795e7

Please sign in to comment.
Something went wrong with that request. Please try again.