# Some Combinators

Explicit definitions of some combinators in Martin-Löf type theory

Here we present some theorems of Martin-Löf type theory from the Bibliopolis book, but adapt the proofs to the intensional version.

``` module MLTT.Combinators where

open import MLTT.Sets
```

We begin with the combinators I, K, S on p 35-37. (We use id for I since the latter was used for the identity set.)

``` id : {A : Set} -> A -> A
id = \x -> x

K : {A : Set} -> {B : A -> Set} -> (x : A) -> B x -> A
K = \x y -> x

S : {A : Set} -> {B : A -> Set} -> {C : (x : A) -> B x -> Set}
-> (g : (x : A) -> (y : B x) -> C x y)
-> (f : (x : A) -> B x)
-> (x : A)
-> C x (f x)
S = \g f x -> g x (f x)
```

In Bibliopolis the E elimination rule for Σ on p 48-49 is derived from the projections. Here we do the reverse. (Note that Agda was not able to deduce all implicit arguments.)

``` p : {A : Set} -> {B : A -> Set} ->  Σ A B -> A
p {A = A} = \c -> E {A = A} {C = \z -> A} (\x y -> x) c

q : {A : Set} -> {B : A -> Set} ->  (c : Σ A B) -> B (p c)
q {B = B} = \c -> E {B = B} {C = \z -> B (p z)} (\x y -> y) c
```

In Bibliopolis application is a primitive and the F elimination rule is only mentioned in the preface. Here we derive application from F.

``` ap' : {A : Set} -> {B : A -> Set} -> (a : A) ->  Π A B -> B a
ap' = \a -> F (\b -> b a)

ap : {A : Set} -> {B : A -> Set} -> Π A B -> (a : A) -> B a
ap = \c a -> ap' a c
```

The axiom of choice is proved on p 50-52 in Bibliopolis:

``` ac : {A : Set} {B : A -> Set} {C : (x : A) -> B x -> Set}
-> ((x : A) -> Σ (B x) (\y -> C x y))
-> Σ ((x : A) -> B x) (\f -> (x : A) -> C x (f x))

ac = \g -> (\x -> p (g x)) , (\x -> q (g x))
```