{-# OPTIONS --cubical-compatible --safe #-}
module Prelude where
open import Agda.Primitive public
renaming (Set to Type)
using (Prop; Level; _⊔_; lzero; lsuc)
private
variable
a b c ℓ p : Level
@0 A A₁ A₂ B B₁ B₂ C D Whatever : Type a
@0 P Q R : A → Type p
record ↑ ℓ (A : Type a) : Type (a ⊔ ℓ) where
constructor lift
field lower : A
open ↑ public
open import Agda.Builtin.String public using (String)
open import Agda.Builtin.Unit public using (⊤; tt)
data Unit : Type where
unit : Unit
Block : String → Type
Block _ = Unit
pattern ⊠ = unit
block : (Unit → A) → A
block f = f ⊠
unblock : (b : Unit) (@0 P : Unit → Type p) → P ⊠ → P b
unblock ⊠ _ p = p
data ⊥ {ℓ} : Type ℓ where
⊥-elim₀ : @0 ⊥ {ℓ = ℓ} → Whatever
⊥-elim₀ ()
⊥-elim : ⊥ {ℓ = ℓ} → Whatever
⊥-elim x = ⊥-elim₀ x
⊥₀ : Type
⊥₀ = ⊥
infix 3 ¬_
¬_ : Type ℓ → Type ℓ
¬ P = P → ⊥₀
open import Agda.Builtin.Nat public
using (zero; suc; _+_; _*_)
renaming (Nat to ℕ; _-_ to _∸_)
ℕ-rec : P 0 → (∀ n → P n → P (suc n)) → ∀ n → P n
ℕ-rec z s zero = z
ℕ-rec z s (suc n) = s n (ℕ-rec z s n)
ℕ-case : P 0 → (∀ n → P (suc n)) → ∀ n → P n
ℕ-case z s = ℕ-rec z (λ n _ → s n)
infixr 8 _^_
_^_ : ℕ → ℕ → ℕ
m ^ zero = 1
m ^ suc n = m * m ^ n
infix 9 _!
_! : ℕ → ℕ
zero ! = 1
suc n ! = suc n * n !
# : ℕ → Level
# zero = lzero
# (suc n) = lsuc (# n)
infixr 9 _∘_
infixl 1 _on_
infixr 0 _$_
id : A → A
id x = x
_∘_ :
{@0 B : A → Type b} {@0 C : {x : A} → B x → Type c} →
(∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
((x : A) → C (g x))
f ∘ g = λ x → f (g x)
infix -1 finally-→
infixr -2 step-→
step-→ : (@0 A : Type a) → (B → C) → (A → B) → A → C
step-→ _ f g = f ∘ g
syntax step-→ A B→C A→B = A →⟨ A→B ⟩ B→C
finally-→ : (@0 A : Type a) (@0 B : Type b) → (A → B) → A → B
finally-→ _ _ A→B = A→B
syntax finally-→ A B A→B = A →⟨ A→B ⟩□ B □
_$_ :
{@0 B : A → Type b} →
((x : A) → B x) → ((x : A) → B x)
f $ x = f x
const : A → (B → A)
const x = λ _ → x
{-# DISPLAY const x y = x #-}
flip :
{@0 C : A → B → Type c} →
((x : A) (y : B) → C x y) → ((y : B) (x : A) → C x y)
flip f = λ x y → f y x
_on_ :
{@0 C : B → B → Type c} →
((x y : B) → C x y) →
(f : A → B) →
((x y : A) → C (f x) (f y))
_*_ on f = λ x y → f x * f y
Type-of : {A : Type a} → A → Type a
Type-of {A} _ = A
infix 0 type-signature
type-signature : (@0 A : Type a) → A → A
type-signature _ a = a
syntax type-signature A a = a ⦂ A
it : ⦃ _ : A ⦄ → A
it ⦃ (x) ⦄ = x
infix 0 case_return_of_ case_of_
case_return_of_ :
(x : A) (@0 B : A → Type b) → ((x : A) → B x) → B x
case x return B of f = f x
case_of_ : A → (A → B) → B
case x of f = case x return _ of f
infixr 4 _,′_
infixr 2 _×_
open import Agda.Builtin.Sigma public
using (Σ; _,_)
hiding (module Σ)
renaming (fst to proj₁; snd to proj₂)
module Σ where
open Agda.Builtin.Sigma.Σ public
using ()
renaming (fst to proj₁; snd to proj₂)
proj₁₀ :
{@0 B : A → Type b} →
Σ A B → A
proj₁₀ (x , y) = x
proj₂₀ :
{@0 B : A → Type b}
(p : Σ A B) → B (proj₁ p)
proj₂₀ (x , y) = y
open Σ public using (proj₁₀; proj₂₀)
∃ : {A : Type a} → (A → Type b) → Type (a ⊔ b)
∃ = Σ _
_×_ : (A : Type a) (B : Type b) → Type (a ⊔ b)
A × B = Σ A (const B)
_,′_ : A → B → A × B
x ,′ y = x , y
Σ-map :
(f : A → B) → (∀ {x} → P x → Q (f x)) →
Σ A P → Σ B Q
Σ-map f g = λ p → (f (proj₁₀ p) , g (proj₂₀ p))
Σ-zip :
(f : A → B → C) → (∀ {x y} → P x → Q y → R (f x y)) →
Σ A P → Σ B Q → Σ C R
Σ-zip f g = λ p q → (f (proj₁₀ p) (proj₁₀ q) , g (proj₂₀ p) (proj₂₀ q))
curry :
{@0 B : A → Type b} {@0 C : Σ A B → Type c} →
((p : Σ A B) → C p) →
((x : A) (y : B x) → C (x , y))
curry f x y = f (x , y)
uncurry :
{@0 B : A → Type b} {@0 C : Σ A B → Type c} →
((x : A) (y : B x) → C (x , y)) →
((p : Σ A B) → C p)
uncurry f (x , y) = f x y
swap : A × B → B × A
swap (x , y) = y , x
data W (A : Type a) (B : A → Type b) : Type (a ⊔ b) where
sup : (x : A) (f : B x → W A B) → W A B
headᵂ :
{@0 B : A → Type b} →
W A B → A
headᵂ (sup x f) = x
tailᵂ :
{@0 B : A → Type b} →
(x : W A B) → B (headᵂ x) → W A B
tailᵂ (sup x f) = f
W-map :
(f : A → B) →
(∀ {x} → Q (f x) → P x) →
W A P → W B Q
W-map f g (sup x h) = sup (f x) (λ y → W-map f g (h (g y)))
abstract
inhabited⇒W-empty :
{@0 B : A → Type b} →
(∀ x → B x) → ¬ W A B
inhabited⇒W-empty b (sup x f) = inhabited⇒W-empty b (f (b x))
infixr 1 _⊎_
data _⊎_ (A : Type a) (B : Type b) : Type (a ⊔ b) where
inj₁ : (x : A) → A ⊎ B
inj₂ : (y : B) → A ⊎ B
[_,_] :
{@0 C : A ⊎ B → Type c} →
((x : A) → C (inj₁ x)) → ((x : B) → C (inj₂ x)) →
((x : A ⊎ B) → C x)
[ f , g ] (inj₁ x) = f x
[ f , g ] (inj₂ y) = g y
infix 5 if_then_else_
if_then_else_ : A ⊎ B → C → C → C
if x then t else f = [ const t , const f ] x
not : A ⊎ B → B ⊎ A
not (inj₁ x) = inj₂ x
not (inj₂ x) = inj₁ x
⊎-map : (A₁ → A₂) → (B₁ → B₂) → A₁ ⊎ B₁ → A₂ ⊎ B₂
⊎-map f g = [ (λ x → inj₁ (f x)) , (λ x → inj₂ (g x)) ]
From-⊎ : {A B : Type ℓ} → A ⊎ B → Type ℓ
From-⊎ {A} (inj₁ _) = A
From-⊎ {B} (inj₂ _) = B
from-⊎ : (x : A ⊎ B) → From-⊎ x
from-⊎ (inj₁ x) = x
from-⊎ (inj₂ y) = y
Dec : Type p → Type p
Dec P = P ⊎ ¬ P
pattern yes p = inj₁ p
pattern no p = inj₂ p
Decidable : {A : Type a} {B : Type b} →
(A → B → Type ℓ) → Type (a ⊔ b ⊔ ℓ)
Decidable _∼_ = ∀ x y → Dec (x ∼ y)
infixr 1 _Xor_
_Xor_ : Type a → Type b → Type (a ⊔ b)
A Xor B = (A × ¬ B) ⊎ (¬ A × B)
Maybe : Type a → Type a
Maybe A = ⊤ ⊎ A
pattern nothing = inj₁ tt
pattern just x = inj₂ x
T : A ⊎ B → Type
T b = if b then ⊤ else ⊥
Bool : Type
Bool = ⊤ ⊎ ⊤
pattern true = inj₁ tt
pattern false = inj₂ tt
infixr 6 _∧_
_∧_ : Bool → Bool → Bool
b₁ ∧ b₂ = if b₁ then b₂ else false
infixr 5 _∨_
_∨_ : Bool → Bool → Bool
b₁ ∨ b₂ = if b₁ then true else b₂
open import Agda.Builtin.List public using (List; []; _∷_)
Fin : ℕ → Type
Fin zero = ⊥
Fin (suc n) = ⊤ ⊎ Fin n
pattern fzero = inj₁ tt
pattern fsuc i = inj₂ i
_→-rel_ : {A : Type a} {C : Type c} →
(A → C → Type ℓ) → (B → D → Type ℓ) →
(A → B) → (C → D) → Type (a ⊔ c ⊔ ℓ)
(P →-rel Q) f g = ∀ x y → P x y → Q (f x) (g y)
_×-rel_ : (A → C → Type ℓ) → (B → D → Type ℓ) → A × B → C × D → Type ℓ
(P ×-rel Q) (x , u) (y , v) = P x y × Q u v
_⊎-rel_ : (A → C → Type ℓ) → (B → D → Type ℓ) → A ⊎ B → C ⊎ D → Type ℓ
(P ⊎-rel Q) (inj₁ x) (inj₁ y) = P x y
(P ⊎-rel Q) (inj₁ x) (inj₂ v) = ⊥
(P ⊎-rel Q) (inj₂ u) (inj₁ y) = ⊥
(P ⊎-rel Q) (inj₂ u) (inj₂ v) = Q u v