------------------------------------------------------------------------
-- Some theorems of 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

------------------------------------------------------------------------
-- Combinators I, K, S on p 35-37

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 = E (\x y -> x)

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

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