From cbe547e1fcc0a8e0be2a6beb7ec6cc4497af4839 Mon Sep 17 00:00:00 2001 From: kangrongji Date: Thu, 18 Aug 2022 21:57:52 +0800 Subject: [PATCH 1/6] done --- Cubical/Foundations/Equiv/Dependent.agda | 30 ++++++++++++ Cubical/Foundations/Univalence/Dependent.agda | 48 +++++++++++++++++++ 2 files changed, 78 insertions(+) create mode 100644 Cubical/Foundations/Univalence/Dependent.agda diff --git a/Cubical/Foundations/Equiv/Dependent.agda b/Cubical/Foundations/Equiv/Dependent.agda index cb9bc651f..1d024a22f 100644 --- a/Cubical/Foundations/Equiv/Dependent.agda +++ b/Cubical/Foundations/Equiv/Dependent.agda @@ -222,3 +222,33 @@ equivOver→IsoOver {P = P} {Q = Q} e f equiv = w w .inv = isom .inv w .rightInv = isom .rightInv w .leftInv = isom .leftInv + + +-- Turn isomorphism over HAE into relative equivalence, +-- i.e. the inverse of the previous precedure. + +isoToEquivOver : + {A : Type ℓ } {P : A → Type ℓ'' } + {B : Type ℓ'} {Q : B → Type ℓ'''} + (f : A → B) (hae : isHAEquiv f) + (isom' : IsoOver (isHAEquiv→Iso hae) P Q) + → isEquivOver {Q = Q} (isom' .fun) +isoToEquivOver {A = A} {P} {Q = Q} f hae isom' a = isoToEquiv (fibiso a) .snd + where + isom = isHAEquiv→Iso hae + finv = isom .inv + + fibiso : (a : A) → Iso (P a) (Q (f a)) + fibiso a .fun = isom' .fun a + fibiso a .inv x = transport (λ i → P (isom .leftInv a i)) (isom' .inv (f a) x) + fibiso a .leftInv x = transport + (λ i → transport-filler (λ i → P (isom .leftInv a i)) (isom' .inv (f a) (isom' .fun a x)) i + ≡ isom' .leftInv a x i) refl + fibiso a .rightInv x = transport (λ i → p-path i) (transport (λ i → c-path (~ i)) (isom' .rightInv _ _)) + where + p-path : I → Type _ + p-path j = PathP (λ i → Q (f (isom .leftInv a (i ∨ j)))) + (isom' .fun _ (transp (λ i → P (isom .leftInv a (i ∧ j))) (~ j) (isom' .inv (f a) x))) x + + c-path : I → Type _ + c-path j = PathP (λ i → Q (hae .com a j i)) (isom' .fun _ (isom' .inv (f a) x)) x diff --git a/Cubical/Foundations/Univalence/Dependent.agda b/Cubical/Foundations/Univalence/Dependent.agda new file mode 100644 index 000000000..e0e0da27d --- /dev/null +++ b/Cubical/Foundations/Univalence/Dependent.agda @@ -0,0 +1,48 @@ +{- + +Dependent Version of Univalence + +The univalence corresponds to the dependent equivalences/isomorphisms, +c.f. `Cubical.Foundations.Equiv.Dependent`. + +-} +{-# OPTIONS --safe #-} +module Cubical.Foundations.Univalence.Dependent where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Equiv.HalfAdjoint +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Equiv.Dependent +open import Cubical.Foundations.Univalence + +private + variable + ℓ ℓ' : Level + + +-- Dependent Univalence + +uaOver : + {A B : Type ℓ} {P : A → Type ℓ'} {Q : B → Type ℓ'} + (e : A ≃ B) (F : mapOver (e .fst) P Q) + (equiv : isEquivOver {P = P} {Q = Q} F) + → PathP (λ i → ua e i → Type ℓ') P Q +uaOver {A = A} {P = P} {Q} e F equiv i x = + hcomp (λ j → λ + { (i = i0) → ua (_ , equiv x) (~ j) + ; (i = i1) → Q x }) + (Q (unglue (i ∨ ~ i) x)) + + +-- Dependent `isoToPath` + +open isHAEquiv + +isoToPathOver : + {A B : Type ℓ} {P : A → Type ℓ'} {Q : B → Type ℓ'} + (f : A → B) (hae : isHAEquiv f) + (isom : IsoOver (isHAEquiv→Iso hae) P Q) + → PathP (λ i → ua (_ , isHAEquiv→isEquiv hae) i → Type ℓ') P Q +isoToPathOver f hae isom = uaOver _ _ (isoToEquivOver f hae isom) From 6d03ce1b3fb1b1c2ed4ba118cc9f2492cb5b8e9c Mon Sep 17 00:00:00 2001 From: KANG Rongji Date: Fri, 19 Aug 2022 11:46:12 +0800 Subject: [PATCH 2/6] done --- Cubical/Foundations/Cubes.agda | 190 ++++++++++++++++++++++++++++ Cubical/Foundations/Cubes/Base.agda | 155 +++++++++++++++++++++++ 2 files changed, 345 insertions(+) create mode 100644 Cubical/Foundations/Cubes.agda create mode 100644 Cubical/Foundations/Cubes/Base.agda diff --git a/Cubical/Foundations/Cubes.agda b/Cubical/Foundations/Cubes.agda new file mode 100644 index 000000000..78c0eac18 --- /dev/null +++ b/Cubical/Foundations/Cubes.agda @@ -0,0 +1,190 @@ +{- + +The Internal n-Cubes + +-} +{-# OPTIONS --safe #-} +module Cubical.Foundations.Cubes where + +open import Cubical.Foundations.Prelude hiding (Cube) +open import Cubical.Foundations.Cubes.Base public +open import Cubical.Data.Nat + +private + variable + ℓ : Level + A : Type ℓ + + +{- + +By mutual recursion, one can define the type of + +- n-Cubes: + Cube : (n : ℕ)(A : Type ℓ) → Type ℓ + +- Boundary of n-cubes: + ∂Cube : ℕ → Type ℓ → Type ℓ + +- n-Cubes with Fixed Boundary: + CubeRel : (n : ℕ)(A : Type ℓ) → ∂Cube n A → Type ℓ the type of n-cubes `Cube`, + +Their definitions are put in `Cubical.Foundations.Cubes.Base`, +to avoid cyclic dependence. + +-} + + +{- + + Relation with the external (partial) cubes + +-} + +-- Concatenate two sides and parts in between to get a partial element. +concat : + {φ : I} (a₋ : (i : I) → Partial φ A) + (a₀ : A [ φ ↦ a₋ i0 ]) (a₁ : A [ φ ↦ a₋ i1 ]) + (i : I) → Partial (i ∨ ~ i ∨ φ) A +concat {φ = φ} a₋ a₀ a₁ i (i = i0) = outS a₀ +concat {φ = φ} a₋ a₀ a₁ i (i = i1) = outS a₁ +concat {φ = φ} a₋ a₀ a₁ i (φ = i1) = a₋ i 1=1 + +-- And the reverse procedure. +module _ (φ : I) (a₋ : (i : I) → Partial (i ∨ ~ i ∨ φ) A) where + + detach₀ : A + detach₀ = a₋ i0 1=1 + + detach₁ : A + detach₁ = a₋ i1 1=1 + + detach₋ : (i : I) → Partial φ A + detach₋ i (φ = i1) = a₋ i 1=1 + + +{- Lower Cubes Back and Forth -} + +-- Notice that the functions are meta-inductively defined, +-- except for the first two cases when n = 0 or 1. + +-- TODO : Write macros to generate them!!! + +from0Cube : Cube 0 A → A +from0Cube p = p + +from1Cube : Cube 1 A → (i : I) → A +from1Cube p i = p .snd i + +from2Cube : Cube 2 A → (i j : I) → A +from2Cube p i j = p .snd i j + +from3Cube : Cube 3 A → (i j k : I) → A +from3Cube p i j k = p .snd i j k + +from4Cube : Cube 4 A → (i j k l : I) → A +from4Cube p i j k l = p .snd i j k l + + +to0Cube : A → Cube 0 A +to0Cube p = p + +to1Cube : ((i : I) → A) → Cube 1 A +to1Cube p = (p i0 , p i1) , λ i → p i + +to2Cube : ((i j : I) → A) → Cube 2 A +to2Cube p = pathCube 0 (λ i → (to1Cube (λ j → p i j))) + +to3Cube : ((i j k : I) → A) → Cube 3 A +to3Cube p = pathCube 1 (λ i → (to2Cube (λ j → p i j))) + +to4Cube : ((i j k l : I) → A) → Cube 4 A +to4Cube p = pathCube 2 (λ i → (to3Cube (λ j → p i j))) + + +-- The 0-cube has no (or empty) boundary... + +from∂1Cube : ∂Cube 1 A → (i : I) → Partial (i ∨ ~ i) A +from∂1Cube (a , b) i = λ { (i = i0) → a ; (i = i1) → b } + +from∂2Cube : ∂Cube 2 A → (i j : I) → Partial (i ∨ ~ i ∨ j ∨ ~ j) A +from∂2Cube (a₀ , a₁ , ∂₋) i j = + concat (λ t → from∂1Cube (∂₋ t) j) + (inS (from1Cube a₀ j)) (inS (from1Cube a₁ j)) i + +from∂3Cube : ∂Cube 3 A → (i j k : I) → Partial (i ∨ ~ i ∨ j ∨ ~ j ∨ k ∨ ~ k) A +from∂3Cube (a₀ , a₁ , ∂₋) i j k = + concat (λ t → from∂2Cube (∂₋ t) j k) + (inS (from2Cube a₀ j k)) (inS (from2Cube a₁ j k)) i + +from∂4Cube : ∂Cube 4 A → (i j k l : I) → Partial (i ∨ ~ i ∨ j ∨ ~ j ∨ k ∨ ~ k ∨ l ∨ ~ l) A +from∂4Cube (a₀ , a₁ , ∂₋) i j k l = + concat (λ t → from∂3Cube (∂₋ t) j k l) + (inS (from3Cube a₀ j k l)) (inS (from3Cube a₁ j k l)) i + + +to∂1Cube : ((i : I) → Partial (i ∨ ~ i) A) → ∂Cube 1 A +to∂1Cube p = p i0 1=1 , p i1 1=1 + +to∂2Cube : ((i j : I) → Partial (i ∨ ~ i ∨ j ∨ ~ j) A) → ∂Cube 2 A +to∂2Cube p .fst = to1Cube (λ j → detach₀ (j ∨ ~ j) (λ i → p i j)) +to∂2Cube p .snd .fst = to1Cube (λ j → detach₁ (j ∨ ~ j) (λ i → p i j)) +to∂2Cube p .snd .snd t = to∂1Cube (λ j → detach₋ _ (λ i → p i j) t) + +to∂3Cube : ((i j k : I) → Partial (i ∨ ~ i ∨ j ∨ ~ j ∨ k ∨ ~ k) A) → ∂Cube 3 A +to∂3Cube p .fst = to2Cube (λ j k → detach₀ (j ∨ ~ j ∨ k ∨ ~ k) (λ i → p i j k)) +to∂3Cube p .snd .fst = to2Cube (λ j k → detach₁ (j ∨ ~ j ∨ k ∨ ~ k) (λ i → p i j k)) +to∂3Cube p .snd .snd t = to∂2Cube (λ j k → detach₋ _ (λ i → p i j k) t) + +to∂4Cube : ((i j k l : I) → Partial (i ∨ ~ i ∨ j ∨ ~ j ∨ k ∨ ~ k ∨ l ∨ ~ l) A) → ∂Cube 4 A +to∂4Cube p .fst = to3Cube (λ j k l → detach₀ (j ∨ ~ j ∨ k ∨ ~ k ∨ l ∨ ~ l) (λ i → p i j k l)) +to∂4Cube p .snd .fst = to3Cube (λ j k l → detach₁ (j ∨ ~ j ∨ k ∨ ~ k ∨ l ∨ ~ l) (λ i → p i j k l)) +to∂4Cube p .snd .snd t = to∂3Cube (λ j k l → detach₋ _ (λ i → p i j k l) t) + + +-- They're strict isomorphisms actually. +-- The following is an example. + +private + + ret-2Cube : {A : Type ℓ} (a : Cube 2 A) → to2Cube (from2Cube a) ≡ a + ret-2Cube a = refl + + sec-2Cube : (p : (i j : I) → A) → (i j : I) → from2Cube (to2Cube p) i j ≡ p i j + sec-2Cube p i j = refl + + ret-∂2Cube : {A : Type ℓ} (a : ∂Cube 2 A) → to∂2Cube (from∂2Cube a) ≡ a + ret-∂2Cube a = refl + + sec-∂2Cube : (p : (i j : I) → Partial (i ∨ ~ i ∨ j ∨ ~ j) A) + → (i j : I) → PartialP (i ∨ ~ i ∨ j ∨ ~ j) (λ o → from∂2Cube (to∂2Cube p) i j o ≡ p i j o) + sec-∂2Cube p i j = λ + { (i = i0) → refl ; (i = i1) → refl ; (j = i0) → refl ; (j = i1) → refl } + + +{- + + The n-cubes-can-always-be-filled is equivalent to be of h-level n + +-} + +-- The property that, given an n-boundary, there always exists an n-cube extending this boundary +-- The case n=0 is not very meaningful, so we use `isContr` instead to keep its relation with h-levels. + +isCubeFilled : ℕ → Type ℓ → Type ℓ +isCubeFilled 0 = isContr +isCubeFilled (suc n) A = (∂ : ∂Cube (suc n) A) → CubeRel (suc n) A ∂ + + +{- + +TODO: + +-- It's not too difficult to show this for a specific n, +-- the trickiest part is to make it for all n. + +isOfHLevel→isCubeFilled : (n : HLevel) → isOfHLevel n A → isCubeFilled n A + +isCubeFilled→isOfHLevel : (n : HLevel) → isCubeFilled n A → isOfHLevel n A + +-} diff --git a/Cubical/Foundations/Cubes/Base.agda b/Cubical/Foundations/Cubes/Base.agda new file mode 100644 index 000000000..888fe3eec --- /dev/null +++ b/Cubical/Foundations/Cubes/Base.agda @@ -0,0 +1,155 @@ +{- + +This file contains: + +- The definition of the type of n-cubes; + +- Some basic operations. + +-} +{-# OPTIONS --safe #-} +module Cubical.Foundations.Cubes.Base where + +open import Cubical.Foundations.Prelude hiding (Cube) +open import Cubical.Foundations.Function hiding (const) +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Isomorphism + +open import Cubical.Data.Nat.Base +open import Cubical.Data.Sigma.Base + +private + variable + ℓ : Level + A : Type ℓ + + +-- The Type of n-Cubes + +-- P.S. +-- Only the definitions of `∂Cube` and `CubeRel` essentially use mutual recursion. +-- The case of `Cube` is designed to gain more definitional equality. + +interleaved mutual + + Cube : (n : ℕ)(A : Type ℓ) → Type ℓ + ∂Cube : ℕ → Type ℓ → Type ℓ + CubeRel : (n : ℕ)(A : Type ℓ) → ∂Cube n A → Type ℓ + + Cube 0 A = A + Cube (suc n) A = Σ[ ∂ ∈ ∂Cube (suc n) A ] CubeRel (suc n) A ∂ + + ∂Cube 0 A = Unit* + ∂Cube 1 A = A × A + ∂Cube (suc (suc n)) A = Σ[ a₀ ∈ Cube (suc n) A ] Σ[ a₁ ∈ Cube (suc n) A ] a₀ .fst ≡ a₁ .fst + + CubeRel 0 A _ = A + CubeRel 1 A ∂ = ∂ .fst ≡ ∂ .snd + CubeRel (suc (suc n)) A (a₀ , a₁ , ∂₋) = PathP (λ i → CubeRel (suc n) A (∂₋ i)) (a₀ .snd) (a₁ .snd) + + +-- Some basic operations + +∂_ : {n : ℕ}{A : Type ℓ} → Cube n A → ∂Cube n A +∂_ {n = 0} _ = tt* +∂_ {n = suc n} = fst + +∂₀ : {n : ℕ}{A : Type ℓ} → Cube (suc n) A → Cube n A +∂₀ {n = 0} (_ , p) = p i0 +∂₀ {n = suc n} (_ , p) = _ , p i0 + +∂₁ : {n : ℕ}{A : Type ℓ} → Cube (suc n) A → Cube n A +∂₁ {n = 0} (_ , p) = p i1 +∂₁ {n = suc n} (_ , p) = _ , p i1 + +∂ᵇ₀ : {n : ℕ}{A : Type ℓ} → ∂Cube (suc n) A → Cube n A +∂ᵇ₀ {n = 0} (a₀ , a₁) = a₀ +∂ᵇ₀ {n = suc n} (a₀ , a₁ , ∂₋) = a₀ + +∂ᵇ₁ : {n : ℕ}{A : Type ℓ} → ∂Cube (suc n) A → Cube n A +∂ᵇ₁ {n = 0} (a₀ , a₁) = a₁ +∂ᵇ₁ {n = suc n} (a₀ , a₁ , ∂₋) = a₁ + + +make∂ : {n : ℕ}{A : Type ℓ}{∂₀ ∂₁ : ∂Cube n A} → ∂₀ ≡ ∂₁ → CubeRel n A ∂₀ → CubeRel n A ∂₁ → ∂Cube (suc n) A +make∂ {n = 0} _ a b = a , b +make∂ {n = suc n} ∂₋ a₀ a₁ = (_ , a₀) , (_ , a₁) , ∂₋ + +makeCube : {n : ℕ}{A : Type ℓ}{a₀ a₁ : Cube n A} → a₀ ≡ a₁ → Cube (suc n) A +makeCube {n = 0} a₋ = _ , a₋ +makeCube {n = suc n} a₋ = _ , λ i → a₋ i .snd + +-- A cube is just a path of cubes of one-lower-dimension. +-- Unfortunately the following function cannot begin at 0, +-- because Agda doesn't support pattern matching on ℕ towards pre-types. +pathCube : (n : ℕ) → (I → Cube (suc n) A) → Cube (suc (suc n)) A +pathCube n p = _ , λ i → p i .snd + +CubeRel→Cube : {n : ℕ}{A : Type ℓ}{∂ : ∂Cube n A} → CubeRel n A ∂ → Cube n A +CubeRel→Cube {n = 0} a = a +CubeRel→Cube {n = suc n} cube = _ , cube + + +-- Composition of internal cubes, with specified boundary + +hcomp∂ : + {n : ℕ} {A : Type ℓ} + {∂₀ ∂₁ : ∂Cube n A} (∂₋ : ∂₀ ≡ ∂₁) + (a₀ : CubeRel n A ∂₀) + → CubeRel n A ∂₁ +hcomp∂ ∂₋ = transport (λ i → CubeRel _ _ (∂₋ i)) + +hfill∂ : + {n : ℕ} {A : Type ℓ} + {∂₀ ∂₁ : ∂Cube n A} (∂₋ : ∂₀ ≡ ∂₁) + (a₀ : CubeRel n A ∂₀) + → CubeRel (suc n) A (make∂ ∂₋ a₀ (hcomp∂ ∂₋ a₀)) +hfill∂ {n = 0} ∂₋ a₀ i = transportRefl a₀ (~ i) +hfill∂ {n = suc n} ∂₋ = transport-filler (λ i → CubeRel _ _ (∂₋ i)) + + +-- Constant path of n-cube as (n+1)-cube + +constCube : {n : ℕ}{A : Type ℓ} → Cube n A → Cube (suc n) A +constCube {n = 0} a = _ , λ i → a +constCube {n = suc n} (∂ , cube) = _ , λ i → cube + +retConst : {n : ℕ}{A : Type ℓ} → (cube : Cube n A) → ∂₀ (constCube {n = n} cube) ≡ cube +retConst {n = 0} _ = refl +retConst {n = suc n} _ = refl + +setConst : {n : ℕ}{A : Type ℓ} → (cube : Cube (suc n) A) → constCube (∂₀ cube) ≡ cube +setConst {n = 0} (_ , p) i = _ , λ j → p (i ∧ j) +setConst {n = suc n} (_ , p) i = _ , λ j → p (i ∧ j) + +isEquivConstCube : {n : ℕ}{A : Type ℓ} → isEquiv (constCube {n = n} {A = A}) +isEquivConstCube {n = n} = isoToEquiv (iso constCube ∂₀ setConst (retConst {n = n})) .snd + + +-- Constant cubes + +const : (n : ℕ){A : Type ℓ} → A → Cube n A +const 0 a = a +const (suc n) a = constCube (const n a) + +isEquivConst : {n : ℕ}{A : Type ℓ} → isEquiv (const n {A = A}) +isEquivConst {n = 0} = idIsEquiv _ +isEquivConst {n = suc n} = compEquiv (_ , isEquivConst) (_ , isEquivConstCube) .snd + +cubeEquiv : {n : ℕ}{A : Type ℓ} → A ≃ Cube n A +cubeEquiv = _ , isEquivConst + +makeConst : {n : ℕ}{A : Type ℓ} → (cube : Cube n A) → Σ[ a ∈ A ] cube ≡ const n a +makeConst {n = n} cube = invEq cubeEquiv cube , sym (secEq (cubeEquiv {n = n}) cube) + +makeConstUniq : {n : ℕ}{A : Type ℓ} → (a : A) → makeConst (const n a) ≡ (a , refl) +makeConstUniq {n = n} a i .fst = isEquivConst .equiv-proof (const n a) .snd (a , refl) i .fst +makeConstUniq {n = n} a i .snd j = isEquivConst .equiv-proof (const n a) .snd (a , refl) i .snd (~ j) + + +-- Cube with constant boundary + +const∂ : (n : ℕ){A : Type ℓ} → A → ∂Cube n A +const∂ 0 _ = tt* +const∂ 1 a = a , a +const∂ (suc (suc n)) a = const _ a , const _ a , refl From 6a2b711d2c080100678f0f9a11e86122eb77f537 Mon Sep 17 00:00:00 2001 From: KANG Rongji Date: Fri, 19 Aug 2022 13:09:44 +0800 Subject: [PATCH 3/6] add import to Everything --- Cubical/Foundations/Everything.agda | 1 + 1 file changed, 1 insertion(+) diff --git a/Cubical/Foundations/Everything.agda b/Cubical/Foundations/Everything.agda index 798dd6deb..6f07d383e 100644 --- a/Cubical/Foundations/Everything.agda +++ b/Cubical/Foundations/Everything.agda @@ -50,3 +50,4 @@ open import Cubical.Foundations.Isomorphism public open import Cubical.Foundations.CartesianKanOps open import Cubical.Foundations.Powerset open import Cubical.Foundations.SIP +open import Cubical.Foundations.Cubes From 1412d0da0619d71a5d5cd084ea08aee26b2cda41 Mon Sep 17 00:00:00 2001 From: KANG Rongji Date: Sat, 20 Aug 2022 20:05:00 +0800 Subject: [PATCH 4/6] better ident --- Cubical/Foundations/Cubes.agda | 6 +++--- Cubical/Foundations/Cubes/Base.agda | 16 ++++++++-------- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/Cubical/Foundations/Cubes.agda b/Cubical/Foundations/Cubes.agda index 78c0eac18..f221cf5f7 100644 --- a/Cubical/Foundations/Cubes.agda +++ b/Cubical/Foundations/Cubes.agda @@ -21,13 +21,13 @@ private By mutual recursion, one can define the type of - n-Cubes: - Cube : (n : ℕ)(A : Type ℓ) → Type ℓ + Cube : (n : ℕ) (A : Type ℓ) → Type ℓ - Boundary of n-cubes: - ∂Cube : ℕ → Type ℓ → Type ℓ + ∂Cube : (n : ℕ) (A : Type ℓ) → Type ℓ - n-Cubes with Fixed Boundary: - CubeRel : (n : ℕ)(A : Type ℓ) → ∂Cube n A → Type ℓ the type of n-cubes `Cube`, + CubeRel : (n : ℕ) (A : Type ℓ) → ∂Cube n A → Type ℓ Their definitions are put in `Cubical.Foundations.Cubes.Base`, to avoid cyclic dependence. diff --git a/Cubical/Foundations/Cubes/Base.agda b/Cubical/Foundations/Cubes/Base.agda index 888fe3eec..1c90a8d74 100644 --- a/Cubical/Foundations/Cubes/Base.agda +++ b/Cubical/Foundations/Cubes/Base.agda @@ -32,16 +32,16 @@ private interleaved mutual - Cube : (n : ℕ)(A : Type ℓ) → Type ℓ - ∂Cube : ℕ → Type ℓ → Type ℓ - CubeRel : (n : ℕ)(A : Type ℓ) → ∂Cube n A → Type ℓ + Cube : (n : ℕ) (A : Type ℓ) → Type ℓ + ∂Cube : (n : ℕ) (A : Type ℓ) → Type ℓ + CubeRel : (n : ℕ) (A : Type ℓ) → ∂Cube n A → Type ℓ - Cube 0 A = A - Cube (suc n) A = Σ[ ∂ ∈ ∂Cube (suc n) A ] CubeRel (suc n) A ∂ + Cube 0 A = A + Cube (suc n) A = Σ[ ∂ ∈ ∂Cube (suc n) A ] CubeRel (suc n) A ∂ - ∂Cube 0 A = Unit* - ∂Cube 1 A = A × A - ∂Cube (suc (suc n)) A = Σ[ a₀ ∈ Cube (suc n) A ] Σ[ a₁ ∈ Cube (suc n) A ] a₀ .fst ≡ a₁ .fst + ∂Cube 0 A = Unit* + ∂Cube 1 A = A × A + ∂Cube (suc (suc n)) A = Σ[ a₀ ∈ Cube (suc n) A ] Σ[ a₁ ∈ Cube (suc n) A ] a₀ .fst ≡ a₁ .fst CubeRel 0 A _ = A CubeRel 1 A ∂ = ∂ .fst ≡ ∂ .snd From 1eab83b19ff54118725386738a52ce68f06cc99f Mon Sep 17 00:00:00 2001 From: KANG Rongji Date: Mon, 29 Aug 2022 21:38:32 +0800 Subject: [PATCH 5/6] comment --- Cubical/Foundations/Cubes/Base.agda | 1 + 1 file changed, 1 insertion(+) diff --git a/Cubical/Foundations/Cubes/Base.agda b/Cubical/Foundations/Cubes/Base.agda index 1c90a8d74..16334517f 100644 --- a/Cubical/Foundations/Cubes/Base.agda +++ b/Cubical/Foundations/Cubes/Base.agda @@ -82,6 +82,7 @@ makeCube {n = suc n} a₋ = _ , λ i → a₋ i .snd -- A cube is just a path of cubes of one-lower-dimension. -- Unfortunately the following function cannot begin at 0, -- because Agda doesn't support pattern matching on ℕ towards pre-types. +-- P.S. It will be fixed in Agda 2.9.3 when I → A becomes fibrant. pathCube : (n : ℕ) → (I → Cube (suc n) A) → Cube (suc (suc n)) A pathCube n p = _ , λ i → p i .snd From 5b372f0ded54b39d66548bd10e586b2258d677d8 Mon Sep 17 00:00:00 2001 From: Evan Cavallo Date: Mon, 29 Aug 2022 15:42:33 +0200 Subject: [PATCH 6/6] off-by-three --- Cubical/Foundations/Cubes/Base.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cubical/Foundations/Cubes/Base.agda b/Cubical/Foundations/Cubes/Base.agda index 16334517f..37d1bd1f8 100644 --- a/Cubical/Foundations/Cubes/Base.agda +++ b/Cubical/Foundations/Cubes/Base.agda @@ -82,7 +82,7 @@ makeCube {n = suc n} a₋ = _ , λ i → a₋ i .snd -- A cube is just a path of cubes of one-lower-dimension. -- Unfortunately the following function cannot begin at 0, -- because Agda doesn't support pattern matching on ℕ towards pre-types. --- P.S. It will be fixed in Agda 2.9.3 when I → A becomes fibrant. +-- P.S. It will be fixed in Agda 2.6.3 when I → A becomes fibrant. pathCube : (n : ℕ) → (I → Cube (suc n) A) → Cube (suc (suc n)) A pathCube n p = _ , λ i → p i .snd