open import Prim.Type

module Prim.Interval where


# Primitives: The Interval🔗

The interval type, and its associated operations, are also very magical.

{-# BUILTIN CUBEINTERVALUNIV IUniv #-} -- IUniv : SSet₁
{-# BUILTIN INTERVAL I  #-}            -- I : IUniv


Note that the interval (as of Agda 2.6.3) is in its own sort, IUniv. The reason for this is that the interval can serve as the domain of fibrant types:

_ : Type → Type
_ = λ A → (I → A)


The interval has two endpoints, the builtins IZERO and IONE:

{-# BUILTIN IZERO    i0 #-}
{-# BUILTIN IONE     i1 #-}


It also supports a De Morgan algebra structure. Unlike the other built-in symbols, the operations on the interval are defined as primitive, so we must use renaming to give them usable names.

private module X where
infix  30 primINeg
infixr 20 primIMin primIMax
primitive
primIMin : I → I → I
primIMax : I → I → I
primINeg : I → I
open X public
renaming ( primIMin       to _∧_
; primIMax       to _∨_
; primINeg       to ~_
)


## The IsOne predicate🔗

To specify the shape of composition problems, Cubical Agda gives us the predicate IsOne, which can be thought of as an embedding $\mathbb{I} \hookrightarrow \Omega$ of the interval object into the subobject classifier. Of course, we have that IsOne i0 is uninhabited (since 0 is not 1), but note that assuming a term in IsOne i0 collapses the judgemental equality.

{-# BUILTIN ISONE IsOne #-}  -- IsOne : I → Setω

postulate
1=1 : IsOne i1
leftIs1  : ∀ i j → IsOne i → IsOne (i ∨ j)
rightIs1 : ∀ i j → IsOne j → IsOne (i ∨ j)

{-# BUILTIN ITISONE 1=1  #-}
{-# BUILTIN ISONE1 leftIs1  #-}
{-# BUILTIN ISONE2 rightIs1 #-}


The IsOne proposition is used as the domain of the type Partial, where Partial φ A is a refinement of the type .(IsOne φ) → A1, where inhabitants p, q : Partial φ A are equal iff they agree on a decomposition of φ into DNF.

[domfinite]: They’re actually equal, but this is a bug.

{-# BUILTIN PARTIAL  Partial  #-}
{-# BUILTIN PARTIALP PartialP #-}

postulate
isOneEmpty : ∀ {ℓ} {A : Partial i0 (Type ℓ)} → PartialP i0 A

primitive
primPOr : ∀ {ℓ} (i j : I) {A : Partial (i ∨ j) (Type ℓ)}
→ (u : PartialP i (λ z → A (leftIs1 i j z)))
→ (v : PartialP j (λ z → A (rightIs1 i j z)))
→ PartialP (i ∨ j) A

{-# BUILTIN ISONEEMPTY isOneEmpty #-}

syntax primPOr φ ψ u v = [ φ ↦ u , ψ ↦ v ]


Note that the type of primPOr is incomplete: it looks like the eliminator for a coproduct, but i ∨ j behaves more like a pushout. We can represent the accurate type with extension types.

1. domfinite↩︎