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

module 1Lab.Path.Cartesian where

CoercionπŸ”—

Our interval type is equipped with 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 Our De Morgan interval lets us implement an approximation of the coe operation 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

This definition of coe is an approximation because the following equation, saying that staying in the fibre is definitionally the identity, can only be shown propositionally. In Cartesian cubical type theories, coei→i is instead one of the definitional equalities that characterises coe.

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))