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 Ο) β A`

^{1},
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.

domfiniteβ©οΈ