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}