Put interpolateI at Cubical.Core.Interpolate (not exposed by default …

…yet)

Cubical/Core/Interpolate.agda

@@ -0,0 +1,76 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Core.Interpolate where
+
+open import Cubical.Core.Primitives
+
+-- An "interpolation" operator on the interval. Interpolates along t
+-- from i to j (see demo properties below)
+interpolateI : I → I → I → I
+interpolateI t i j = (~ t ∧ i) ∨ (t ∧ j) ∨ (i ∧ j)
+
+-- An "equality" operator on the interval. equalI is a simplification
+-- of interpolateI x (~ y) y and interpolateI y (~ x) x, which are
+-- different in De Morgan CCHM. All three would become equal in Kleene
+-- CCHM. This operator is provided here because interpolateI t i j is
+-- constant on equalI i j, which can be useful; see
+-- Cubical.Foundations.CartesianKanOps coei→j for an example
+equalI : I → I → I
+equalI x y = (~ x ∧ ~ y) ∨ (x ∧ y)
+
+-- demo of nice properties satisfied by interpolateI
+private module _ {A : Type} {p : I → A} {t i j k l : I} where
+  -- just for demonstration purposes
+  infix 1 _＝_
+  _＝_ : I → I → Type
+  _＝_ i j = p i ≡ p j
+  refl : {i : I} → i ＝ i
+  refl {i} _ = p i
+
+  _ : interpolateI i0 i j ＝ i
+  _ = refl
+
+  _ : interpolateI i1 i j ＝ j
+  _ = refl
+
+  _ : interpolateI t i0 i1 ＝ t
+  _ = refl
+
+  _ : interpolateI t i i ＝ i
+  _ = refl
+
+  _ : interpolateI (~ t) i j ＝ interpolateI t j i
+  _ = refl
+
+  _ : interpolateI i i0 j ＝ i ∧ j
+  _ = refl
+
+  _ : interpolateI i j i1 ＝ i ∨ j
+  _ = refl
+
+  _ : interpolateI i j i0 ＝ ~ i ∧ j
+  _ = refl
+
+  _ : interpolateI i i1 j ＝ ~ i ∨ j
+  _ = refl
+
+  _ : interpolateI t (i ∧ j) (i ∧ k) ＝ i ∧ interpolateI t j k
+  _ = refl
+
+  _ : interpolateI t (i ∨ j) (i ∨ k) ＝ i ∨ interpolateI t j k
+  _ = refl
+
+  _ : interpolateI t (~ j) (~ k) ＝ ~ interpolateI t j k
+  _ = refl
+
+  _ : interpolateI (interpolateI t i j) k l
+      ＝ interpolateI t (interpolateI i k l) (interpolateI j k l)
+  _ = refl
+
+  _ : interpolateI i (interpolateI t j k) l
+      ＝ interpolateI t (interpolateI i j l) (interpolateI i k l)
+  _ = refl
+
+  _ : interpolateI i j (interpolateI t k l)
+      ＝ interpolateI t (interpolateI i j k) (interpolateI i j l)
+  _ = refl

Cubical/Foundations/CartesianKanOps.agda

@@ -3,6 +3,7 @@
 module Cubical.Foundations.CartesianKanOps where
 
 open import Cubical.Core.Everything
+open import Cubical.Core.Interpolate
 
 private
   refl : ∀ {ℓ} {A : Type ℓ} {x : A} → x ≡ x
@@ -47,23 +48,6 @@ coei0→0 A a = refl
 coei1→0 : ∀ {ℓ} (A : I → Type ℓ) (a : A i1) → coei→0 A i1 a ≡ coe1→0 A a
 coei1→0 A a = refl
 
-private
-  -- "Interpolation" on the interval. Notice:
-  --     interpolateI i0 i j = i
-  --     interpolateI i1 i j = j
-  --     interpolateI (~ t) i j = interpolateI t j i
-  --     interpolateI t i0 i1 = t
-  --     interpolateI t i i = i
-  -- and more...
-  interpolateI : I → I → I → I
-  interpolateI t i j = (~ t ∧ i) ∨ (t ∧ j) ∨ (i ∧ j)
-
-  -- "Equality" on the interval, chosen for the next definition
-  -- (coei→j), because interpolateI k i j is constant in k on
-  -- eqI i j. Note that eqI i i is not i1 but i ∨ ~ i.
-  equalI : I → I → I
-  equalI i j = (i ∧ j) ∨ (~ i ∧ ~ j)
-
 -- "master coe"
 -- unlike in cartesian cubes, we don't get coei→i = id definitionally
 coei→j : ∀ {ℓ} (A : I → Type ℓ) (i j : I) → A i → A j