------------------------------------------------------------------------
-- Definitions from The Agda standard library
------------------------------------------------------------------------

-- Data.Product

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

open Σ public

-- The syntax declaration below is attached to Σ-syntax, to make it
-- easy to import Σ without the special syntax.

infix  Σ-syntax

Σ-syntax : (A : Set) → (A → Set) → Set
Σ-syntax = Σ

syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B

∃ : ∀ {A : Set} → (A → Set) → Set
∃ = Σ _


-- Data.Empty

data ⊥ : Set where

⊥-elim : ∀ {Whatever : Set} → ⊥ → Whatever
⊥-elim ()

-- Data.Unit

record ⊤ : Set where
  constructor tt

-- Data.Nat

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ

{-# BUILTIN NATURAL ℕ #-}

-- Data.Sum

infixr  _⊎_

data _⊎_ (A B : Set) : Set where
  inj₁ : (x : A) → A ⊎ B
  inj₂ : (y : B) → A ⊎ B

-- Relation.Binary.PropositionalEquality

infix  _≡_

data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x

{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REFL refl #-}

subst : ∀ {a}{A : Set a} → (P : A → Set) → ∀{a b} → a ≡ b → P a → P b
subst P refl p = p

sym : ∀ {a} {A : Set a} → ∀{a b : A} → a ≡ b → b ≡ a
sym refl = refl

trans : ∀ {a} {A : Set a} → ∀{a b c : A} → a ≡ b → b ≡ c → a ≡ c
trans refl eq = eq

cong : ∀ {a b} {A : Set a} {B : Set b}
       (f : A → B) {x y} → x ≡ y → f x ≡ f y
cong f refl = refl


subst₂ : ∀{A : Set} {B : A → Set} (P : (a : A) → B a → Set)
          {x₁ x₂ y₁} → (q : x₁ ≡ x₂) → P x₁ y₁ → P x₂ (subst B q y₁)
subst₂ P refl p = p


cong₃ : ∀{A : Set}{B : A → Set}{C : (a : A) → B a → Set}{D : Set}
        (f : (a : A)(b : B a) → C a b → D ) 
        {x y : A}{u : B x}{s : C x u} → 
        (qa : x ≡ y) → f x u s ≡ f y (subst B qa u) (subst₂ C qa s)
cong₃ f refl = refl

-- Function

id : ∀ {a} {A : Set a} → A → A
id x = x


_∘_ : ∀ {a b c}
        {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} →
        (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
        ((x : A) → C (g x))
f ∘ g = λ x → f (g x)