Homogeneous = heterogeneous dependent paths in cooltt 😎

homogeneous.cooltt

import prelude
import coercion

-- De Morgan-style connections, adapted from https://github.com/RedPRL/redtt/blob/master/library/prelude/connection.red
-- Note that these are *strong* connections in the sense that p (i ∧ i) = p i, as
-- opposed to the weak connections defined in https://arxiv.org/abs/1911.05844.

def max
  (A : type)
  (p : 𝕀 → A)
  : ext i j => A with [
    | i=1 ∨ j=1 => p 1
    | i=0 => p j
    | j=0 ∨ i=j => p i
    ]
  := i j =>
    let face : 𝕀 → 𝕀 → A := k =>
      hfill A 1 {∂ k} {l => [
      | k=1 ∨ l=1 => p 1
      | k=0 => p l
      ]}
    in
    hcom 1 0 {k => [
    | i=1 ∨ j=1 ∨ k=1 => p 1
    | i=0 => face k j
    | j=0 ∨ i=j => face k i
    ]}

def min
  (A : type)
  (p : 𝕀 → A)
  : ext i j => A with [
    | j=0 ∨ i=0 => p 0
    | i=1 => p j
    | j=1 ∨ i=j => p i
    ]
  := i j =>
    let face : 𝕀 → 𝕀 → A := k =>
      hfill A 0 {∂ k} {l => [
      | k=0 ∨ l=0 => p 0
      | k=1 => p l
      ]}
    in
    hcom 0 1 {k => [
    | i=0 ∨ j=0 ∨ k=0 => p 0
    | i=1 => face k j
    | j=1 ∨ i=j => face k i
    ]}

-- Homogeneous dependent paths

def path-coe (A : 𝕀 → type) (x : A 0) (y : A 1) : type :=
  path {A 1} {coe/fwd A x} y

-- With connections defined, we can mimic the de Morgan proof that
-- heterogeneous dependent paths are equal to homogeneous dependent
-- paths [1, 2].

def path-p≡path-coe (A : 𝕀 → type) (x : A 0) (y : A 1)
  : path type {path-p A x y} {path-coe A x y}
  := i => path-p {max type A i} {coe A 0 i x} y

-- [1]: https://www.cse.chalmers.se/~nad/listings/equality/Equality.Path.html#heterogeneous%E2%89%A1homogeneous
-- [2]: https://1lab.dev/1Lab.Path.html#PathP%E2%89%A1Path