Mltt

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

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