Extension.agda

{-# OPTIONS --cubical #-}
module Extension where

open import Agda.Primitive
open import Cubical.Core.Everything
open import Agda.Builtin.Nat

infixr 4 _,,_

record I×_ (A : Setω) : Setω where
  constructor _,,_
  field
    fst : I
    snd : A
open I×_ public

record EData l : Setω where
  constructor _∣_
  field
    {face} : I
    type : Set l
    boundary : Partial face type

I^ : Nat → Setω
I^ zero = I
I^ (suc n) = I× I^ n

FunI : Nat → ∀ l → Setω
FunI zero l = EData l
FunI (suc n) l = I → FunI n l

uncurry : ∀ {n} {l} → FunI (suc n) l → I^ n → EData l
uncurry {zero} f c = f c
uncurry {suc n} f c = uncurry {n} (f (c .fst)) (c .snd)

postulate
 primExtension  : ∀ {l n} → (I^ n → EData l) → Set l

Ext : ∀ {n} {l} → FunI (suc n) l → Set l
Ext f = primExtension (uncurry f)


-- The `I` in (i j : I) is needed for inferring the type as Pi rather than PathP.
bar : Set
bar = Ext \ (i j : I) → Nat ∣ \ { (i = i0) → zero; (i = i1) → suc zero }