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 Iβ†ͺΞ©\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.

{-# 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. They’re actually equal, but this is a bug.β†©οΈŽ