Martin Escardo 2011.

\begin{code}

module SetsAndFunctions where

\end{code}

The empty set us defined by induction by an empty set of
clauses: 

\begin{code}

data ∅ : Set where

unique-from-∅ : {A : Set} → ∅ → A
unique-from-∅ = λ ()

\end{code}

The one-element set is defined by induction with one case:
\begin{code}

data ① : Set where
 * : ①

unique-to-① : {A : Set} → A → ①
unique-to-① a = *

\end{code}

Product types are built-in, but I prefer to introduce the standard notation:

\begin{code}

Π : {X : Set} → (Y : X → Set) → Set
Π {X} Y = (x : X) → Y x

\end{code}

Using our conventions below, a sum can be written Σ {I} X or
as Σ \(i : I) → X i, or even Σ \i → X i when Agda can infer
i from the context. I prefer to use \ rather than λ in such
cases.

\begin{code}

infixr  _,_

record Σ {I : Set} (X : I → Set) : Set where
  constructor _,_
  field
   π₀ : I
   π₁ : X π₀


π₀ : {I : Set} {X : I → Set} →

  (Σ \(i : I) → X i) → I

π₀(i , x) = i


π₁ : {I : Set} {X : I → Set} →

  (pair : Σ \(i : I) → X i) → X(π₀ pair)

π₁(i , x) = x


Σ-elim : {X : Set} → {Y : X → Set} →
         {A : (Σ \(x : X) → Y x) → Set}

   → (∀(x : X) → ∀(y : Y x) → A(x , y))
   → ∀(t : (Σ \(x : X) → Y x)) → A t

Σ-elim f (x , y) = f x y


uncurry : {X Z : Set} → {Y : X → Set} →

  ((x : X) → Y x → Z) → (Σ \(x : X) → Y x) → Z

uncurry f (x , y) = f x y


curry : {X Z : Set} → {Y : X → Set} →

  ((Σ \(x : X) → Y x) → Z) → ((x : X) → Y x → Z)

curry f x y = f(x , y)

\end{code}

Equivalently, Σ-elim f t = f (π₀ t) (π₁ t).

As usual in type theory, binary products are particular
cases of dependent sums.

\begin{code}

infixr  _×_

_×_ : Set → Set → Set
X × Y = Σ \(x : X) → Y

\end{code}

This can also be considered as a special case, but I won't
bother:

\begin{code}

infixr  _+_

data _+_ (X₀ X₁ : Set) : Set where
  in₀ : X₀ → X₀ + X₁
  in₁ : X₁ → X₀ + X₁


dep-cases : {X₀ X₁ : Set} → {Y : X₀ + X₁ → Set} →

 ((x₀ : X₀) → Y(in₀ x₀)) → ((x₁ : X₁) → Y(in₁ x₁))
    → ((p : X₀ + X₁) → Y p)

dep-cases f₀ f₁ (in₀ x₀) = f₀ x₀
dep-cases f₀ f₁ (in₁ x₁) = f₁ x₁


cases : {X₀ X₁ Y : Set} → (X₀ → Y) → (X₁ → Y) → X₀ + X₁ → Y
cases = dep-cases

\end{code}

General constructions on functions:

\begin{code}

infixl  _∘_

_∘_ : {X Y : Set} {Z : Y → Set} →

 ((y : Y) → Z y) → (f : X → Y) → (x : X) → Z(f x)

g ∘ f = λ x → g(f x)


id : {X : Set} → X → X
id x = x

\end{code}

I use JJ and KK to avoid confusion with J and K for
equality.

\begin{code}

KK : Set → Set → Set
KK R X = (X → R) → R

contra-variant : {R X Y : Set} → (X → Y) → (Y → R) → (X → R)
contra-variant f p = p ∘ f

K-functor : {R X Y : Set} → (X → Y) → KK R X → KK R Y
K-functor = contra-variant ∘ contra-variant

ηK : {R X : Set} → X → KK R X
ηK x p = p x

\end{code}

K-unshift:

\begin{code}

KU : {R X : Set} {Y : X → Set} →

 KK R ((x : X) → Y x) → (x : X) → KK R (Y x)

KU = λ f x g → f(λ h → g(h x))

\end{code}

Special case, if you like:

\begin{code}

ku : {R X Y : Set} → KK R (X × Y) → KK R X × KK R Y
ku φ = (K-functor π₀ φ , K-functor π₁ φ)

\end{code}

I am not sure were to put the following (product of
quantifiers and selection functions). At the moment it goes
in this module. It is not used, but it is included for the
sake of comparison with similar patterns.

\begin{code}

quant-prod : {X R : Set} {Y : X → Set} →

  KK R X → ((x : X)  → KK R (Y x))
  → KK R ((Σ \(x : X)  → Y x))

quant-prod φ γ p = φ(λ x → γ x (λ y → p(x , y)))


JJ : Set → Set → Set
JJ R X = (X → R) → X

sel-prod : {R : Set} → {X : Set} → {Y : X → Set} →

    JJ R X → ((x : X) → JJ R (Y x))
    → JJ R (Σ \(x : X) → Y x)

sel-prod {R} {X} {Y} ε δ p = (x₀ , y₀)
   where
    next : (x : X) → Y x
    next x = δ x (λ y → p(x , y))

    x₀ : X
    x₀ = ε(λ x → p(x , next x))

    y₀ : Y x₀
    y₀ = next x₀

\end{code}

Alternative, equivalent, construction:

\begin{code}

overline : {X R : Set} → JJ R X → KK R X
overline ε p = p(ε p)


sel-prod' : {R : Set} → {X : Set} → {Y : X → Set} →

    JJ R X → ((x : X) → JJ R (Y x)) → JJ R (Σ \(x : X) → Y x)

sel-prod' {R} {X} {Y} ε δ p = (x₀ , y₀)
   where
    x₀ : X
    x₀ = ε(λ x → overline(δ x) (λ y → p(x , y)))

    y₀ : Y x₀
    y₀ = δ x₀ (λ y → p(x₀ , y))

\end{code}