{-# 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 _∧_
; primIMax to _∨_
; primINeg to ~_
; isOneEmpty to empty
; primComp to comp
; primHComp to hcomp
; primTransp to transp
; itIsOne to 1=1 )
import Agda.Builtin.Cubical.Glue
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
infix 4 _[_≡_]
_[_≡_] : ∀ {ℓ} (A : I → Type ℓ) → A i0 → A i1 → Type ℓ
_[_≡_] = PathP
Path : ∀ {ℓ} (A : Type ℓ) → A → A → Type ℓ
Path A a b = PathP (λ _ → A) a b
private
sys : ∀ i → Partial (i ∨ ~ i) Type₁
sys i (i = i0) = Type₀
sys i (i = i1) = Type₀ → Type₀
sys' : ∀ i → Partial (i ∨ ~ i) Type₁
sys' i = λ { (i = i0) → Type₀
; (i = i1) → Type₀ → Type₀
}
sys2 : ∀ i j → Partial (i ∨ (i ∧ j)) Type₁
sys2 i j = λ { (i = i1) → Type₀
; (i = i1) (j = i1) → Type₀
}
sys3 : Partial i0 Type₁
sys3 = λ { () }
_[_↦_] : ∀ {ℓ} (A : Type ℓ) (φ : I) (u : Partial φ A) → _
A [ φ ↦ u ] = Sub A φ u
infix 4 _[_↦_]
private
variable
ℓ : Level
ℓ′ : I → Level
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)
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)
infix 2 Σ-syntax
Σ-syntax : ∀ {ℓ ℓ'} (A : Type ℓ) (B : A → Type ℓ') → Type (ℓ-max ℓ ℓ')
Σ-syntax = Σ
syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B