Martin Escardo 2011.

\begin{code}

{-# OPTIONS --without-K #-}

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 the type of i
from the context. I prefer to use \ rather than λ in such cases.

\begin{code}

infixr 3 _,_

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 20 _×_

_×_ : 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 20 _+_

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 31 _∘_

_∘_ : {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}