{-# OPTIONS --without-K --rewriting #-}
module lib.Base where
open import Agda.Primitive public using (lzero)
renaming (Level to ULevel; lsuc to lsucc; _⊔_ to lmax)
Type : (i : ULevel) → Set (lsucc i)
Type i = Set i
Type₀ = Type lzero
Type0 = Type lzero
Type₁ = Type (lsucc lzero)
Type1 = Type (lsucc lzero)
of-type : ∀ {i} (A : Type i) (u : A) → A
of-type A u = u
infix 40 of-type
syntax of-type A u = u :> A
infix 30 _==_
data _==_ {i} {A : Type i} (a : A) : A → Type i where
idp : a == a
Path = _==_
{-# BUILTIN EQUALITY _==_ #-}
{-# BUILTIN REFL idp #-}
J : ∀ {i j} {A : Type i} {a : A} (B : (a' : A) (p : a == a') → Type j) (d : B a idp)
{a' : A} (p : a == a') → B a' p
J B d idp = d
J' : ∀ {i j} {A : Type i} {a : A} (B : (a' : A) (p : a' == a) → Type j) (d : B a idp)
{a' : A} (p : a' == a) → B a' p
J' B d idp = d
infix 30 _↦_
postulate
_↦_ : ∀ {i} {A : Type i} → A → A → Type i
{-# BUILTIN REWRITE _↦_ #-}
record ⊤ : Type₀ where
instance constructor unit
Unit = ⊤
{-# BUILTIN UNIT ⊤ #-}
PathOver : ∀ {i j} {A : Type i} (B : A → Type j)
{x y : A} (p : x == y) (u : B x) (v : B y) → Type j
PathOver B idp u v = (u == v)
infix 30 PathOver
syntax PathOver B p u v =
u == v [ B ↓ p ]
ap : ∀ {i j} {A : Type i} {B : Type j} (f : A → B) {x y : A}
→ (x == y → f x == f y)
ap f idp = idp
ap↓ : ∀ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k}
(g : {a : A} → B a → C a) {x y : A} {p : x == y}
{u : B x} {v : B y}
→ (u == v [ B ↓ p ] → g u == g v [ C ↓ p ])
ap↓ g {p = idp} p = ap g p
apd : ∀ {i j} {A : Type i} {B : A → Type j} (f : (a : A) → B a) {x y : A}
→ (p : x == y) → f x == f y [ B ↓ p ]
apd f idp = idp
coe : ∀ {i} {A B : Type i} (p : A == B) → A → B
coe idp x = x
coe! : ∀ {i} {A B : Type i} (p : A == B) → B → A
coe! idp x = x
transport : ∀ {i j} {A : Type i} (B : A → Type j) {x y : A} (p : x == y)
→ (B x → B y)
transport B p = coe (ap B p)
transport! : ∀ {i j} {A : Type i} (B : A → Type j) {x y : A} (p : x == y)
→ (B y → B x)
transport! B p = coe! (ap B p)
Π : ∀ {i j} (A : Type i) (P : A → Type j) → Type (lmax i j)
Π A P = (x : A) → P x
infixr 60 _,_
record Σ {i j} (A : Type i) (B : A → Type j) : Type (lmax i j) where
constructor _,_
field
fst : A
snd : B fst
open Σ public
pair= : ∀ {i j} {A : Type i} {B : A → Type j}
{a a' : A} (p : a == a') {b : B a} {b' : B a'}
(q : b == b' [ B ↓ p ])
→ (a , b) == (a' , b')
pair= idp q = ap (_ ,_) q
pair×= : ∀ {i j} {A : Type i} {B : Type j}
{a a' : A} (p : a == a') {b b' : B} (q : b == b')
→ (a , b) == (a' , b')
pair×= idp q = pair= idp q
data ⊥ : Type₀ where
Empty = ⊥
⊥-elim : ∀ {i} {P : ⊥ → Type i} → ((x : ⊥) → P x)
⊥-elim ()
Empty-elim = ⊥-elim
¬ : ∀ {i} (A : Type i) → Type i
¬ A = A → ⊥
_≠_ : ∀ {i} {A : Type i} → (A → A → Type i)
x ≠ y = ¬ (x == y)
data ℕ : Type₀ where
O : ℕ
S : (n : ℕ) → ℕ
Nat = ℕ
{-# BUILTIN NATURAL ℕ #-}
record Lift {i j} (A : Type i) : Type (lmax i j) where
instance constructor lift
field
lower : A
open Lift public
infixr 10 _=⟨_⟩_
infix 15 _=∎
_=⟨_⟩_ : ∀ {i} {A : Type i} (x : A) {y z : A} → x == y → y == z → x == z
_ =⟨ idp ⟩ idp = idp
_=∎ : ∀ {i} {A : Type i} (x : A) → x == x
_ =∎ = idp
infixl 40 ap
syntax ap f p = p |in-ctx f
idf : ∀ {i} (A : Type i) → (A → A)
idf A = λ x → x
cst : ∀ {i j} {A : Type i} {B : Type j} (b : B) → (A → B)
cst b = λ _ → b
infixr 80 _∘_
_∘_ : ∀ {i j k} {A : Type i} {B : A → Type j} {C : (a : A) → (B a → Type k)}
→ (g : {a : A} → Π (B a) (C a)) → (f : Π A B) → Π A (λ a → C a (f a))
g ∘ f = λ x → g (f x)
infixr 0 _$_
_$_ : ∀ {i j} {A : Type i} {B : A → Type j} → (∀ x → B x) → (∀ x → B x)
f $ x = f x
curry : ∀ {i j k} {A : Type i} {B : A → Type j} {C : Σ A B → Type k}
→ (∀ s → C s) → (∀ x y → C (x , y))
curry f x y = f (x , y)
uncurry : ∀ {i j k} {A : Type i} {B : A → Type j} {C : ∀ x → B x → Type k}
→ (∀ x y → C x y) → (∀ s → C (fst s) (snd s))
uncurry f (x , y) = f x y
data TLevel : Type₀ where
⟨-2⟩ : TLevel
S : (n : TLevel) → TLevel
ℕ₋₂ = TLevel
⟨_⟩₋₂ : ℕ → ℕ₋₂
⟨ O ⟩₋₂ = ⟨-2⟩
⟨ S n ⟩₋₂ = S ⟨ n ⟩₋₂
data Coprod {i j} (A : Type i) (B : Type j) : Type (lmax i j) where
inl : A → Coprod A B
inr : B → Coprod A B
infixr 80 _⊔_
_⊔_ = Coprod
match_withl_withr_ : ∀ {i j k} {A : Type i} {B : Type j}
{C : Coprod A B → Type k}
(x : Coprod A B) (l : (a : A) → C (inl a)) (r : (b : B) → C (inr b)) → C x
match (inl a) withl l withr r = l a
match (inr b) withl l withr r = r b
Dec : ∀ {i} (P : Type i) → Type i
Dec P = P ⊔ ¬ P
infix 60 ⊙[_,_]
record Ptd (i : ULevel) : Type (lsucc i) where
constructor ⊙[_,_]
field
de⊙ : Type i
pt : de⊙
open Ptd public
ptd : ∀ {i} (A : Type i) → A → Ptd i
ptd = ⊙[_,_]
ptd= : ∀ {i} {A A' : Type i} (p : A == A')
{a : A} {a' : A'} (q : a == a' [ idf _ ↓ p ])
→ ⊙[ A , a ] == ⊙[ A' , a' ]
ptd= idp q = ap ⊙[ _ ,_] q
Ptd₀ = Ptd lzero
infixr 0 _⊙→_
_⊙→_ : ∀ {i j} → Ptd i → Ptd j → Type (lmax i j)
⊙[ A , a₀ ] ⊙→ ⊙[ B , b₀ ] = Σ (A → B) (λ f → f a₀ == b₀)
⊙idf : ∀ {i} (X : Ptd i) → X ⊙→ X
⊙idf X = (λ x → x) , idp
⊙cst : ∀ {i j} {X : Ptd i} {Y : Ptd j} → X ⊙→ Y
⊙cst {Y = Y} = (λ x → pt Y) , idp
data Phantom {i} {A : Type i} (a : A) : Type₀ where
phantom : Phantom a
record FromNat {i} (A : Type i) : Type (lsucc i) where
field
in-range : ℕ → Type i
read : ∀ n → ⦃ _ : in-range n ⦄ → A
open FromNat ⦃...⦄ public using () renaming (read to from-nat)
{-# BUILTIN FROMNAT from-nat #-}
record FromNeg {i} (A : Type i) : Type (lsucc i) where
field
in-range : ℕ → Type i
read : ∀ n → ⦃ _ : in-range n ⦄ → A
open FromNeg ⦃...⦄ public using () renaming (read to from-neg)
{-# BUILTIN FROMNEG from-neg #-}
instance
ℕ-reader : FromNat ℕ
FromNat.in-range ℕ-reader _ = ⊤
FromNat.read ℕ-reader n = n
TLevel-reader : FromNat TLevel
FromNat.in-range TLevel-reader _ = ⊤
FromNat.read TLevel-reader n = S (S ⟨ n ⟩₋₂)
TLevel-neg-reader : FromNeg TLevel
FromNeg.in-range TLevel-neg-reader O = ⊤
FromNeg.in-range TLevel-neg-reader 1 = ⊤
FromNeg.in-range TLevel-neg-reader 2 = ⊤
FromNeg.in-range TLevel-neg-reader (S (S (S _))) = ⊥
FromNeg.read TLevel-neg-reader O = S (S ⟨-2⟩)
FromNeg.read TLevel-neg-reader 1 = S ⟨-2⟩
FromNeg.read TLevel-neg-reader 2 = ⟨-2⟩
FromNeg.read TLevel-neg-reader (S (S (S _))) ⦃()⦄