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))