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
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β©οΈ