open import 1Lab.Path
open import 1Lab.Type

module 1Lab.Path.Cartesian where

CoercionπŸ”—

In Cubical Agda, the interval is given the structure of a De Morgan algebra. This is not the only choice of structure on the interval that gives a model of univalent type theory: We could also subject the interval to no additional structure other than what comes from the structural rules of type theory (introducing variables, ignoring variables, swapping variables, etc). This is a different cubical type theory, called Cartesian cubical type theory.

In Cartesian cubical type theory, rather than our transp operation, the fundamental operation for manipulating paths is coe, which implements an arbitrary change of interval variables In Cubical Agda, we can implement this by transporting along a function of three variables which β€œinterpolates” between and as increases.

The interpolation function we’re using was discovered by Tom Jack, who kindly allowed us to use it here on the 1Lab:

I-eq : I β†’ I β†’ I
I-eq i j = (i ∧ j) ∨ (~ i ∧ ~ j)

I-interp : I β†’ I β†’ I β†’ I
I-interp t x y = (~ t ∧ x) ∨ (t ∧ y) ∨ (x ∧ y)

coe : βˆ€ {β„“ : I β†’ Level} (A : βˆ€ i β†’ Type (β„“ i)) (i j : I) β†’ A i β†’ A j
coe A i j a = transp (Ξ» k β†’ A (I-interp k i j)) (I-eq i j) a

To show that this definition computes as expected, we can compare it to the other coercion operations (squeezes and spreads) we’ve already defined by hand:

coei0β†’0 : βˆ€ {β„“} (A : I β†’ Type β„“) a β†’ coeiβ†’0 A i0 a ≑ a
coei1β†’0 : βˆ€ {β„“} (A : I β†’ Type β„“) a β†’ coeiβ†’0 A i1 a ≑ coe1β†’0 A a

coei0β†’1 : βˆ€ {β„“} (A : I β†’ Type β„“) a β†’ coeiβ†’1 A i0 a ≑ coe0β†’1 A a
coei1β†’1 : βˆ€ {β„“} (A : I β†’ Type β„“) a β†’ coeiβ†’1 A i1 a ≑ a

coeiβ†’i0 : βˆ€ {β„“} (A : I β†’ Type β„“) i a β†’ coe A i i0 a ≑ coeiβ†’0 A i a
coeiβ†’i1 : βˆ€ {β„“} (A : I β†’ Type β„“) i a β†’ coe A i i1 a ≑ coeiβ†’1 A i a

coei0β†’i : βˆ€ {β„“} (A : I β†’ Type β„“) i a β†’ coe A i0 i a ≑ coe0β†’i A i a
coei1β†’i : βˆ€ {β„“} (A : I β†’ Type β„“) i a β†’ coe A i1 i a ≑ coe1β†’i A i a

Impressively, all these computation rules are refl:

coei0β†’1 A a = refl
coei1β†’1 A a = refl
coei1β†’0 A a = refl
coei0β†’0 A a = refl
coei→i0 A i a = refl
coei0β†’i A i a = refl
coei→i1 A i a = refl
coei1β†’i A i a = refl

In Cartesian cubical type theory, the following equation is definitional. However, in Cubical Agda, it is only propositional:

coeiβ†’i : βˆ€ {β„“} (A : I β†’ Type β„“) i x β†’ coe A i i x ≑ x
coeiβ†’i A i x j = transp (Ξ» _ β†’ A i) (j ∨ i ∨ ~ i) x

coe-path : βˆ€ {β„“} (A : I β†’ Type β„“) (p : βˆ€ i β†’ A i) i j β†’ coe A i j (p i) ≑ p j
coe-path A p i j k = transp
  (Ξ» l β†’ A (I-interp k (I-interp l i j) j))
  (I-interp k (I-eq i j) i1)
  (p (I-interp k i j))