SomeCombinators

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))