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

Page last modified on April 13, 2010, at 12:53 pm

Powered by
PmWiki