happy-interval-subtyping.rzk

#lang rzk-1

-- An (t : II) -> A is usable where a (t : 2) -> A is expected:
-- 2 <: II at the cube level, so by contravariance (II -> A) <: (2 -> A).
-- The converse (a 2-arrow where an II-path is expected) is in ill-interval-subtyping.rzk.

#define arr2
  (A : U) (x y : A)
  : U
  := (t : 2) -> A [ t === 0_2 |-> x , t === 1_2 |-> y ]

#define arrII-to-arr2
  (A : U) (x y : A)
  (p : (t : II) -> A [ t === 0_I |-> x , t === 1_I |-> y ])
  : arr2 A x y
  := p