\begin{code}
module SetsAndFunctions where
\end{code}
\begin{code}
data ∅ : Set where
unique-from-∅ : {A : Set} → ∅ → A
unique-from-∅ = λ ()
\end{code}
\begin{code}
data ① : Set where
* : ①
unique-to-① : {A : Set} → A → ①
unique-to-① a = *
\end{code}
\begin{code}
Π : {X : Set} → (Y : X → Set) → Set
Π {X} Y = (x : X) → Y x
\end{code}
\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}
\begin{code}
infixr 20 _×_
_×_ : Set → Set → Set
X × Y = Σ \(x : X) → Y
\end{code}
\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}
\begin{code}
infixl 30 _∘_
_∘_ : {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}
\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}
\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}
\begin{code}
ku : {R X Y : Set} → KK R (X × Y) → KK R X × KK R Y
ku φ = (K-functor π₀ φ , K-functor π₁ φ)
\end{code}
\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}
\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}