{-# OPTIONS --rewriting #-}
module Prelude where
open import Agda.Primitive public
id :
{l : Level}
{A : Set l}
→
A → A
id x = x
∏ :
{l m : Level}
(A : Set l)
(B : A → Set m)
→
Set (l ⊔ m)
∏ A B = (x : A) → B x
infix 1 ∏-syntax
∏-syntax : {l m : Level}(A : Set l)(B : A → Set m) → Set (l ⊔ m)
∏-syntax = ∏
syntax ∏-syntax A (λ x → B) = ∏ x ∶ A , B
apply :
{l m : Level}
{A : Set l}
{B : A → Set m}
(x : A)
→
∏ A B → B x
apply x f = f x
syntax apply x f = case x of f
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)
K :
{l m : Level}
{A : Set l}
{B : Set m}
→
B → (A → B)
K y _ = y
record 𝟙 : Set where
instance constructor tt
{-# BUILTIN UNIT 𝟙 #-}
data Ø : Set where
Øelim : {l : Level}{A : Set l} → Ø → A
Øelim ()
infixr 5 _⊎_
data _⊎_ {l m : Level}(A : Set l)(B : Set m) : Set (l ⊔ m) where
inl : (x : A) → A ⊎ B
inr : (y : B) → A ⊎ B
open import Agda.Builtin.Bool renaming (Bool to 𝔹) public
infix 0 if_then_else_
if_then_else_ : {l : Level}{A : Set l} → 𝔹 → A → A → A
if true then x else _ = x
if false then _ else y = y
infix 4 _≡≡_
data _≡≡_
{l : Level}
{A : Set l}
:
{B : Set l}(x : A)(y : B) → Set l
where
instance refl : {x : A} → x ≡≡ x
{-# BUILTIN REWRITE _≡≡_ #-}
infix 4 _≡_
_≡_ : {l : Level}{A : Set l}(x y : A) → Set l
_≡_ = _≡≡_
data Id {l : Level}{A : Set l}(x : A) : A → Set l where
instance refl : Id x x
{-# BUILTIN EQUALITY Id #-}
≡≡typ :
{l : Level}
{A B : Set l}
{x : A}
{y : B}
→
x ≡≡ y → A ≡ B
≡≡typ refl = refl
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
symm :
{l : Level}
{A B : Set l}
{x : A}
{y : B}
(p : x ≡≡ y)
→
y ≡≡ x
symm refl = refl
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
_ =[ refl ] q = q
infix 3 _qed
_qed :
{l : Level}
{A : Set l}
(x : A)
→
x ≡≡ x
_ qed = refl
uip :
{l : Level}
{A A' B B' : Set l}
{x : A}
{x' : A'}
{y : B}
{y' : B'}
(u : x ≡≡ x')
{p : x ≡≡ y}
{q : x' ≡≡ y'}
→
p ≡≡ q
uip refl {refl} {refl} = refl
uip' :
{l : Level}
{A A' B B' : Set l}
{x : A}
{x' : A'}
{y : B}
{y' : B'}
(v : y ≡≡ y')
{p : x ≡≡ y}
{q : x' ≡≡ y'}
→
p ≡≡ q
uip' refl {refl} {refl} = refl
infixr 5 _∗_
_∗_ :
{l : Level}
{A B : Set l}
→
A ≡ B → A → B
refl ∗ x = x
∗≡≡ :
{l : Level}
{A B : Set l}
(e : A ≡ B)
(x : A)
→
x ≡≡ e ∗ x
∗≡≡ refl _ = refl
Id2≡ :
{l : Level}
{A : Set l}
{x y : A}
→
Id x y → x ≡ y
Id2≡ refl = refl
≡2Id :
{l : Level}
{A : Set l}
{x y : A}
→
x ≡ y → Id x y
≡2Id refl = refl
Idsymm :
{l : Level}
{A : Set l}
{x y : A}
→
Id x y → Id y x
Idsymm refl = refl
Idtrans :
{l : Level}
{A : Set l}
{x y z : A}
→
Id y z → Id x y → Id x z
Idtrans refl q = q
infixr 4 _,_
record ∑ {l m : Level}(A : Set l)(B : A → Set m) : Set(l ⊔ m) where
constructor _,_
field
fst : A
snd : B fst
{-# BUILTIN SIGMA ∑ #-}
open ∑ public
infix 1 ∑-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)
infix 4 ⟨_,_⟩
⟨_,_⟩ :
{l m n : Level}
{A : Set l}
{B : Set m}
{C : B → Set n}
(f : A → B)
(g : (x : A) → C (f x))
→
A → ∑ B C
⟨ f , g ⟩ x = (f x , g x)
∑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
infixr 5 _×_
_×_ : {l m : Level} → Set l → Set m → Set (l ⊔ m)
A × B = ∑ A (λ _ → B)
open import Agda.Builtin.Size public
Size≤_ : Size → Set
Size≤ i = Size< (↑ i)