{-# OPTIONS --rewriting #-}

module Prelude where

open import Agda.Primitive public

----------------------------------------------------------------------
-- Identity function
----------------------------------------------------------------------
id :
 {l : Level}
 {A : Set l}
  ---------
 A  A
id x = x

----------------------------------------------------------------------
-- Dependent functions
----------------------------------------------------------------------
 :
  {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

----------------------------------------------------------------------
-- Composition
----------------------------------------------------------------------
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)

----------------------------------------------------------------------
-- Constant function
----------------------------------------------------------------------
K :
  {l m : Level}
  {A : Set l}
  {B : Set m}
   -----------
  B  (A  B)
K y _ = y

----------------------------------------------------------------------
-- Unit type
----------------------------------------------------------------------
record 𝟙 : Set where
  instance constructor tt

{-# BUILTIN UNIT 𝟙 #-}

----------------------------------------------------------------------
-- Empty type
----------------------------------------------------------------------
data Ø : Set where

Øelim : {l : Level}{A : Set l}  Ø  A
Øelim ()

----------------------------------------------------------------------
-- Disjoint union
----------------------------------------------------------------------
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

----------------------------------------------------------------------
-- Boolean type
----------------------------------------------------------------------
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

----------------------------------------------------------------------
-- Heteregeneous equality
----------------------------------------------------------------------
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 _≡≡_ #-}

----------------------------------------------------------------------
-- Homogeneous equality
----------------------------------------------------------------------
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 #-}

----------------------------------------------------------------------
-- Properties of ≡≡ and ≡
----------------------------------------------------------------------
≡≡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

----------------------------------------------------------------------
-- Dependent product
----------------------------------------------------------------------
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

----------------------------------------------------------------------
-- Cartesian product
----------------------------------------------------------------------
infixr 5 _×_
_×_ : {l m : Level}  Set l  Set m  Set (l  m)
A × B =  A  _  B)

----------------------------------------------------------------------
-- Sized types
----------------------------------------------------------------------
open import Agda.Builtin.Size public

Size≤_ : Size  Set
Size≤ i = Size< ( i)