module Prelude where
open import Agda.Primitive public
ℓ₀ : Level
ℓ₀ = lzero
ℓ₁ : Level
ℓ₁ = lsuc ℓ₀
ℓ₂ : Level
ℓ₂ = lsuc ℓ₁
record LiftSet {l l' : Level} (A : Set l) : Set (l ⊔ l') where
constructor ↑set
field ↓set : A
open LiftSet public
record LiftProp {l l' : Level} (P : Prop l) : Set (l ⊔ l') where
constructor ↑prop
field ↓prop : P
open LiftProp public
id :
{l : Level}
{A : Set l}
→
A → A
id x = x
K :
{l m : Level}
{A : Set l}
(B : Set m)
→
A → B → A
K _ x _ = x
infixr 5 _∘_
_∘_ :
{l m n : Level}
{A : Set l}
{B : A → Set m}
{C : (x : A) → B x → Set n}
(g : {x : A}(y : B x) → C x y)
(f : (x : A) → B x)
→
(x : A) → C x (f x)
(g ∘ f) x = g (f x)
data 𝟘 {l : Level} : Set l where
𝟘e :
{l m : Level}
{A : 𝟘 {l} → Set m}
→
∀ x → A x
𝟘e ()
data 𝔹 : Set where
true false : 𝔹
{-# BUILTIN BOOL 𝔹 #-}
{-# BUILTIN TRUE true #-}
{-# BUILTIN FALSE false #-}
data ⊤ {l : Level} : Prop l where
instance ⊤i : ⊤
data ⊥ {l : Level} : Prop l where
infix 3 ¬_
¬_ : {l : Level} → Prop l → Prop l
¬_ {l} P = P → ⊥ {l}
infix 4 _≣_
data _≣_
{l : Level}
{A : Set l}
:
{B : Set l}(x : A)(y : B) → Prop l
where
instance refl : {x : A} → x ≣ x
{-# BUILTIN REWRITE _≣_ #-}
≣irrel :
{l : Level}
{P Q : Prop l}
{p : P}
{q : Q}
→
P ≣ Q → ↑prop{l}{l} p ≣ ↑prop q
≣irrel refl = refl
≣typ :
{l : Level}
{A B : Set l}
{x : A}
{y : B}
→
x ≣ y → A ≣ B
≣typ refl = refl
coeₚ : {l : Level}{P Q : Prop l} → P ≣ Q → P → Q
coeₚ refl x = x
coeₚ⁻¹ : {l : Level}{P Q : Prop l} → P ≣ Q → Q → P
coeₚ⁻¹ refl x = x
ap :
{l m : Level}
{A : Set l}
{B : A → Set m}
(f : (x : A) → B x)
{x y : A}
(_ : x ≣ y)
→
f x ≣ f y
ap _ refl = refl
ap₂ :
{l m n : Level}
{A : Set l}
{B : A → Set m}
{C : (x : A) → B x → Set n}
(f : (x : A)(y : B x) → C x y)
{x x' : A}
(_ : x ≣ x')
{y : B x}
{y' : B x'}
(_ : y ≣ y')
→
f x y ≣ f x' y'
ap₂ _ refl refl = refl
trans :
{l : Level}
{A B C : Set l}
{x : A}
{y : B}
{z : C}
(q : y ≣ z)
(p : x ≣ y)
→
x ≣ z
trans refl p = p
infixl 5 _；_
_；_ :
{l : Level}
{A B C : Set l}
{x : A}
{y : B}
{z : C}
(p : x ≣ y)
(q : y ≣ z)
→
x ≣ z
p ； refl = p
symm :
{l : Level}
{A B : Set l}
{x : A}
{y : B}
(p : x ≣ y)
→
y ≣ x
symm refl = refl
substp :
{l m : Level}
{A A' : Set l}
{P : A → Prop m}
{P' : A' → Prop m}
(_ : P ≣ P')
{x : A}
{x' : A'}
(_ : x ≣ x')
→
P x → P' x'
substp e e' p with ≣typ e'
substp refl refl p | refl = p
substp₂ :
{l m n : Level}
{A A' : Set l}
{B B' : Set m}
{P : A → B → Prop n}
{P' : A' → B' → Prop n}
(_ : P ≣ P')
{x : A}
{x' : A'}
{y : B}
{y' : B'}
(_ : x ≣ x')
(_ : y ≣ y')
→
P x y → P' x' y'
substp₂ e e' e'' p with ≣typ e' | ≣typ e''
substp₂ refl refl refl p | refl | refl = p
infix 1 proof_
proof_ :
{l : Level}
{A B : Set l}
{x : A}
{y : B}
→
x ≣ y → x ≣ y
proof p = p
infixr 2 _=[_]_
_=[_]_ :
{l : Level}
{A B C : Set l}
(x : A)
{y : B}
{z : C}
→
x ≣ y → y ≣ z → x ≣ z
_ =[ p ] q = trans q p
infix 3 _qed
_qed :
{l : Level}
{A : Set l}
(x : A)
→
x ≣ x
_ qed = refl
infix 4 _≡_
_≡_ : {l : Level}{A : Set l}(x y : A) → Prop l
_≡_ = _≣_
infixr 3 _∧_
data _∧_ {l m : Level}(P : Prop l)(Q : Prop m) : Prop (l ⊔ m) where
∧i : P → Q → P ∧ Q
∧e₁ :
{l m : Level}
{P : Prop l}
{Q : Prop m}
→
P ∧ Q → P
∧e₁ (∧i p _) = p
∧e₂ :
{l m : Level}
{P : Prop l}
{Q : Prop m}
→
P ∧ Q → Q
∧e₂ (∧i _ q) = q
infix 3 _↔_
_↔_ : {l : Level} → Prop l → Prop l → Prop l
P ↔ Q = (P → Q) ∧ (Q → P)
infix 1 ∃
data ∃ {l m : Level}(A : Set l)(P : A → Prop m) : Prop (l ⊔ m) where
∃i : (x : A)(p : P x) → ∃ A P
syntax ∃ A (λ x → P) = ∃ x ∶ A , P
infix 1 ∃!
∃! : {l m : Level}(A : Set l)(P : A → Prop m) → Prop (l ⊔ m)
∃! A P = ∃ x ∶ A , (P x ∧ ∀(x' : A) → P x' → x ≡ x')
syntax ∃! A (λ x → P) = ∃! x ∶ A , P
infix 1 ⋀
data ⋀ {l m : Level}(P : Prop l)(Q : P → Prop m) : Prop (l ⊔ m) where
⋀i : (x : P)(p : Q x) → ⋀ P Q
syntax ⋀ P (λ p → Q) = ⋀ p ∶ P , Q
⋀e₁ :
{l m : Level}
{P : Prop l}
{Q : P → Prop m}
→
⋀ P Q → P
⋀e₁ (⋀i p _) = p
⋀e₂ :
{l m : Level}
{P : Prop l}
{Q : P → Prop m}
(⋀pq : ⋀ P Q)
→
Q (⋀e₁ ⋀pq)
⋀e₂ (⋀i _ q) = q
infixr 1 _∨_
data _∨_ {l m : Level}(P : Prop l)(Q : Prop m) : Prop (l ⊔ m) where
∨i₁ : P → P ∨ Q
∨i₂ : Q → P ∨ Q
case :
{l m : Level}
{A : Set l}
{B : A → Set m}
(x : A)
(f : (x : A) → B x)
→
B x
case x f = f x
casep :
{l m : Level}
{A : Set l}
{P : A → Prop m}
(x : A)
(p : (x : A) → P x)
→
P x
casep x p = p x
match :
{l m : Level}
{P : Prop l}
{Q : P → Prop m}
(p : P)
(q : ∀ p → Q p)
→
Q p
match p q = q p
infixl 4 _∣_
record set
{l m : Level}
(A : Set l)
(P : A → Prop m)
:
Set (l ⊔ m)
where
constructor _∣_
field
el : A
pf : P el
open set public
syntax set A (λ x → P) = set x ∶ A , P
setext :
{l m : Level}
{A : Set l}
{P : A → Prop m}
{z z' : set A P}
(_ : el z ≡ el z')
→
z ≡ z'
setext {z = _ ∣ _} {_ ∣ _} refl = refl
injection :
{l m : Level}
{A : Set l}
{B : Set m}
(f : A → B)
→
Prop (l ⊔ m)
injection f = ∀{x x'} → f x ≡ f x' → x ≡ x'
surjection :
{l m : Level}
{A : Set l}
{B : Set m}
(q : B → A)
→
Prop (l ⊔ m)
surjection q = ∀ x → ∃ y ∶ _ , q y ≡ x
Bij :
{l m : Level}
{A : Set l}
{B : Set m}
(f : A → B)
→
Prop (l ⊔ m)
Bij f = injection f ∧ surjection f
∏ :
{l m : Level}
(A : Set l)
(B : A → Set m)
→
Set (l ⊔ m)
∏ A B = (x : A) → B x
syntax ∏ A (λ x → B) = ∏ x ∶ A , B
infixr 4 _,_
record ∑ {l m : Level}(A : Set l)(B : A → Set m) : Set(l ⊔ m) where
constructor _,_
field
π₁ : A
π₂ : B π₁
{-# BUILTIN SIGMA ∑ #-}
open ∑ public
infix 2 ∑-syntax
∑-syntax : {l m : Level}(A : Set l) → (A → Set m) → Set (l ⊔ m)
∑-syntax = ∑
syntax ∑-syntax A (λ x → B) = ∑ x ∶ A , B
pair :
{l m : Level}
{A : Set l}
(B : A → Set m)
(x : A)
(_ : B x)
→
∑ A B
pair _ x y = (x , y)
∑ext :
{l m : Level}
{A : Set l}
{B : A → Set m}
{x x' : A}
{y : B x}
{y' : B x'}
(_ : x ≡ x')
(_ : y ≣ y')
→
pair B x y ≡ pair B x' y'
∑ext refl refl = refl
∑heq₁ :
{l m : Level}
{A A' : Set l}
{B : A → Set m}
{B' : A' → Set m}
{x : A}
{x' : A'}
{y : B x}
{y' : B' x'}
(_ : A ≡ A')
(_ : B ≣ B')
(_ : pair B x y ≣ pair B' x' y')
→
x ≣ x'
∑heq₁ refl refl refl = refl
∑heq₂ :
{l m : Level}
{A A' : Set l}
{B : A → Set m}
{B' : A' → Set m}
{x : A}
{x' : A'}
{y : B x}
{y' : B' x'}
(_ : A ≡ A')
(_ : B ≣ B')
(_ : pair B x y ≣ pair B' x' y')
→
y ≣ y'
∑heq₂ refl refl refl = refl
record ∑ₚ {l m : Level}(P : Prop l)(B : P → Set m) : Set(l ⊔ m) where
constructor _,_
field
π₁ : P
π₂ : B π₁
open ∑ₚ public
infix 2 ∑ₚ-syntax
∑ₚ-syntax : {l m : Level}(P : Prop l) → (P → Set m) → Set (l ⊔ m)
∑ₚ-syntax = ∑ₚ
syntax ∑ₚ-syntax P (λ p → B) = ∑ₚ p ∶ P , B
pairₚ :
{l m : Level}
{P : Prop l}
(B : P → Set m)
(x : P)
(_ : B x)
→
∑ₚ P B
pairₚ _ x y = (x , y)
∑ₚheq :
{l m : Level}
{P P' : Prop l}
{B : P → Set m}
{B' : P' → Set m}
{x : P}
{x' : P'}
{y : B x}
{y' : B' x'}
(_ : P ≡ P')
(_ : B ≣ B')
(_ : pairₚ B x y ≣ pairₚ B' x' y')
→
y ≣ y'
∑ₚheq refl refl refl = refl
infixr 5 _×_
_×_ : {l m : Level} → Set l → Set m → Set (l ⊔ m)
A × B = ∑ A (λ _ → B)
record 𝟙 : Set where
instance constructor tt
{-# BUILTIN UNIT 𝟙 #-}
⟦_⟧ : {l : Level} → Prop l → Set l
⟦ p ⟧ = set _ ∶ 𝟙 , p
infixr 1 _⊎_
data _⊎_ {l m : Level}(A : Set l)(B : Set m) : Set (l ⊔ m) where
ι₁ : (x : A) → A ⊎ B
ι₂ : (y : B) → A ⊎ B
data ℕ : Set where
zero : ℕ
suc : (n : ℕ) → ℕ
{-# BUILTIN NATURAL ℕ #-}
pattern _+1 n = suc n
infix 4 _≐_
_≐_ : ℕ → ℕ → 𝔹
zero ≐ zero = true
zero ≐ (n +1) = false
(m +1) ≐ zero = false
(m +1) ≐ (n +1) = m ≐ n
decidableℕ : (m n : ℕ) → m ≡ n ∨ ¬(m ≡ n)
decidableℕ zero zero = ∨i₁ refl
decidableℕ zero (n +1) = ∨i₂ λ{()}
decidableℕ (m +1) zero = ∨i₂ λ{()}
decidableℕ (m +1) (n +1) with decidableℕ m n
... | ∨i₁ refl = ∨i₁ refl
... | ∨i₂ p = ∨i₂ λ{refl → p refl}
infixr 6 _∷_
data List {l : Level}(A : Set l) : Set l where
[] : List A
_∷_ : (x : A)(xs : List A) → List A
{-# BUILTIN LIST List #-}
module _
{l m : Level}
{A : Set l}
{B : A → Set m}
(f : (x : A) → B x)
where
ker : Set (l ⊔ m)
ker = set (x , x') ∶ A × A , (f x ≣ f x')
πker₁ : ker → A
πker₁ ((x , _) ∣ _) = x
πker₂ : ker → A
πker₂ ((_ , x') ∣ _) = x'
eqker : (z : ker) → f (πker₁ z) ≣ f (πker₂ z)
eqker ((_ , _) ∣ e) = e