open import Prim.Interval
open import Prim.Type

module Prim.Extension where

Primitives: Extension typesπŸ”—

Using the type of Partial elements lets us specify maps from some sub-object of a power of the interval to a type The cubical subtypes, or extension types, give us the ability to encode that such a partial element fits into a commutative diagram

where is an ordinary element of (with dimension variables). Commutativity means that, where is defined, agrees with it definitionally.

{-# BUILTIN SUB _[_↦_] #-}

postulate
  inS : βˆ€ {β„“} {A : Type β„“} {Ο†} (x : A) β†’ A [ Ο† ↦ (Ξ» _ β†’ x) ]

{-# BUILTIN SUBIN inS #-}

private module X where primitive
  primSubOut : βˆ€ {β„“} {A : Type β„“} {Ο† : I} {u : Partial Ο† A} β†’ A [ Ο† ↦ u ] β†’ A

open X renaming (primSubOut to outS) public

Using extension types, we can represent the accurate type of primPOr, where the two partial elements u and v must agree on the intersection i ∧ j.

partial-pushout
  : βˆ€ {β„“} (i j : I) {A : Partial (i ∨ j) (Type β„“)}
    {ai : PartialP {a = β„“} (i ∧ j) (Ξ» { (j ∧ i = i1) β†’ A 1=1 }) }
  β†’ (.(z : IsOne i) β†’ A (leftIs1 i j z)  [ (i ∧ j) ↦ (Ξ» { (i ∧ j = i1) β†’ ai 1=1 }) ])
  β†’ (.(z : IsOne j) β†’ A (rightIs1 i j z) [ (i ∧ j) ↦ (Ξ» { (i ∧ j = i1) β†’ ai 1=1 }) ])
  β†’ PartialP (i ∨ j) A
partial-pushout i j u v = primPOr i j (Ξ» z β†’ outS (u z)) (Ξ» z β†’ outS (v z))