Notes on Dependent Types at Work

From here we recall that:
K = λxy.x
S = λxyz.((xz)(yz))

The paper assumes right associativity of both → and ⊃ but that suppresses the visible symmetries with which I learned these formulae. Reinstating some parens we have:

K = λx.(λy.x)
S = λx.(λy.(λz.((xz)(yz))))

P ⊃ (Q ⊃ P)
(P ⊃ (Q ⊃ R)) ⊃ ((P ⊃ Q) ⊃ (P ⊃ R))

A → (B → A)
(A → (B → C)) → ((A → B) → (A → C))

The 2nd correspondence may not be entirely obvious so we ask OCaml: 

# fun x -> (fun y -> (fun z -> ((x z) (y z))));;
- : ('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c = <fun>
OCaml and the authors think that it is obvious. According to them it is rooted in the Curry-Howard isomorphism too.

The paper refers to the two implication formulae as axioms for implication. I recall that the following tautology can not be deduced from them with modus-ponens:
(((A ⊃ B) ⊃ A) ⊃ A)
That was a theorem but required another axiom such as (¬A ⊃ ¬B) ⊃ (B ⊃ A). Wikipedia says that only the ‘intuitionistic implicational logic’ pare produced thus and I think the above tautology is not a theorem there.

what is the type of S = λx.(λy.(λz.((xz)(yz)))) ?
To see that it is (A → (B → C)) → ((A → B) → (A → C))
We presume that the type of x is (A → (B → C)) in (λy.(λz.((xz)(yz))))
We then presume that the type of y is (A → B) in (λz.((xz)(yz)))
and then that the type of z is A in ((xz)(yz))
We note then, using first presumption, that the type of (xz) is (B → C)
Likewise we see that the type of (yz) is B.
We see thus that the type of ((xz)(yz)) is C.
Q.E.D.