{- This file document and export the main primitives of Cubical Agda. It also defines some basic derived operations (composition and filling). -} {-# OPTIONS --safe #-} module Cubical.Core.Primitives where open import Agda.Builtin.Cubical.Path public open import Agda.Builtin.Cubical.Sub public renaming ( inc to inS ; primSubOut to outS ) open import Agda.Primitive.Cubical public renaming ( primIMin to _∧_ -- I → I → I ; primIMax to _∨_ -- I → I → I ; primINeg to ~_ -- I → I ; isOneEmpty to empty ; primComp to comp ; primHComp to hcomp ; primTransp to transp ; itIsOne to 1=1 ) -- These two are to make sure all the primitives are loaded and ready -- to compute hcomp/transp for the universe. import Agda.Builtin.Cubical.Glue -- HCompU is already imported from Glue, and older Agda versions do -- not have it. So we comment it out for now. -- import Agda.Builtin.Cubical.HCompU open import Agda.Primitive public using ( Level ) renaming ( lzero to ℓ-zero ; lsuc to ℓ-suc ; _⊔_ to ℓ-max ; Set to Type ; Setω to Typeω ) open import Agda.Builtin.Sigma public -- This file document the Cubical Agda primitives. The primitives -- themselves are bound by the Agda files imported above. -- * The Interval -- I : Typeω -- Endpoints, Connections, Reversal -- i0 i1 : I -- _∧_ _∨_ : I → I → I -- ~_ : I → I -- * Dependent path type. (Path over Path) -- Introduced with lambda abstraction and eliminated with application, -- just like function types. -- PathP : ∀ {ℓ} (A : I → Type ℓ) → A i0 → A i1 → Type ℓ infix 4 _[_≡_] _[_≡_] : {} (A : I Type ) A i0 A i1 Type _[_≡_] = PathP -- Non dependent path types Path : {} (A : Type ) A A Type Path A a b = PathP _ A) a b -- PathP (λ i → A) x y gets printed as x ≡ y when A does not mention i. -- _≡_ : ∀ {ℓ} {A : Type ℓ} → A → A → Type ℓ -- _≡_ {A = A} = PathP (λ _ → A) -- * @IsOne r@ represents the constraint "r = i1". -- Often we will use "φ" for elements of I, when we intend to use them -- with IsOne (or Partial[P]). -- IsOne : I → Typeω -- i1 is indeed equal to i1. -- 1=1 : IsOne i1 -- * Types of partial elements, and their dependent version. -- "Partial φ A" is a special version of "IsOne φ → A" with a more -- extensional judgmental equality. -- "PartialP φ A" allows "A" to be defined only on "φ". -- Partial : ∀ {ℓ} → I → Type ℓ → Typeω -- PartialP : ∀ {ℓ} → (φ : I) → Partial φ (Type ℓ) → Typeω -- Partial elements are introduced by pattern matching with (r = i0) -- or (r = i1) constraints, like so: private sys : i Partial (i ~ i) Type₁ sys i (i = i0) = Type₀ sys i (i = i1) = Type₀ Type₀ -- It also works with pattern matching lambdas: -- http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.PatternMatchingLambdas sys' : i Partial (i ~ i) Type₁ sys' i = λ { (i = i0) Type₀ ; (i = i1) Type₀ Type₀ } -- When the cases overlap they must agree. sys2 : i j Partial (i (i j)) Type₁ sys2 i j = λ { (i = i1) Type₀ ; (i = i1) (j = i1) Type₀ } -- (i0 = i1) is actually absurd. sys3 : Partial i0 Type₁ sys3 = λ { () } -- * There are cubical subtypes as in CCHM. Note that these are not -- fibrant (hence in Typeω): _[_↦_] : {} (A : Type ) (φ : I) (u : Partial φ A) _ A [ φ u ] = Sub A φ u infix 4 _[_↦_] -- Any element u : A can be seen as an element of A [ φ ↦ u ] which -- agrees with u on φ: -- inS : ∀ {ℓ} {A : Type ℓ} {φ} (u : A) → A [ φ ↦ (λ _ → u) ] -- One can also forget that an element agrees with u on φ: -- outS : ∀ {ℓ} {A : Type ℓ} {φ : I} {u : Partial φ A} → A [ φ ↦ u ] → A -- * Composition operation according to [CCHM 18]. -- When calling "comp A φ u a" Agda makes sure that "a" agrees with "u i0" on "φ". -- compCCHM : ∀ {ℓ} (A : (i : I) → Type ℓ) (φ : I) (u : ∀ i → Partial φ (A i)) (a : A i0) → A i1 -- Note: this is not recommended to use, instead use the CHM -- primitives! The reason is that these work with HITs and produce -- fewer empty systems. -- * Generalized transport and homogeneous composition [CHM 18]. -- When calling "transp A φ a" Agda makes sure that "A" is constant on "φ" (see below). -- transp : ∀ {ℓ} (A : I → Type ℓ) (φ : I) (a : A i0) → A i1 -- "A" being constant on "φ" means that "A" should be a constant function whenever the -- constraint "φ = i1" is satisfied. For example: -- - If "φ" is "i0" then "A" can be anything, since this condition is vacuously true. -- - If "φ" is "i1" then "A" must be a constant function. -- - If "φ" is some in-scope variable "i" then "A" only needs to be a constant function -- when substituting "i1" for "i". -- When calling "hcomp A φ u a" Agda makes sure that "a" agrees with "u i0" on "φ". -- hcomp : ∀ {ℓ} {A : Type ℓ} {φ : I} (u : I → Partial φ A) (a : A) → A private variable : Level ℓ′ : I Level -- Homogeneous filling hfill : {A : Type } {φ : I} (u : i Partial φ A) (u0 : A [ φ u i0 ]) ----------------------- (i : I) A hfill {φ = φ} u u0 i = hcomp j λ { (φ = i1) u (i j) 1=1 ; (i = i0) outS u0 }) (outS u0) -- Heterogeneous composition can defined as in CHM, however we use the -- builtin one as it doesn't require u0 to be a cubical subtype. This -- reduces the number of inS's a lot. -- comp : (A : ∀ i → Type (ℓ′ i)) -- {φ : I} -- (u : ∀ i → Partial φ (A i)) -- (u0 : A i0 [ φ ↦ u i0 ]) -- → --------------------------- -- A i1 -- comp A {φ = φ} u u0 = -- hcomp (λ i → λ { (φ = i1) → transp (λ j → A (i ∨ j)) i (u _ 1=1) }) -- (transp A i0 (outS u0)) -- Heterogeneous filling defined using comp fill : (A : i Type (ℓ′ i)) {φ : I} (u : i Partial φ (A i)) (u0 : A i0 [ φ u i0 ]) --------------------------- (i : I) A i fill A {φ = φ} u u0 i = comp j A (i j)) j λ { (φ = i1) u (i j) 1=1 ; (i = i0) outS u0 }) (outS u0) -- Σ-types infix 2 Σ-syntax Σ-syntax : { ℓ'} (A : Type ) (B : A Type ℓ') Type (ℓ-max ℓ') Σ-syntax = Σ syntax Σ-syntax A x B) = Σ[ x A ] B