# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1486621923 0
# Node ID a2e6f61d5f2b991593f5faa8507c8b8e2a40adf4
# Parent  29a3a4b79d4df32151d3ba11dec2c34c3ac769f6
Add modus-ponens

diff -r 29a3a4b79d4d -r a2e6f61d5f2b sandbox/modus-ponens.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/sandbox/modus-ponens.agda	Thu Feb 09 06:32:03 2017 +0000
@@ -0,0 +1,13 @@
+module modus-ponens where
+
+data _×_ (A B : Set) : Set where
+  <_,_> : A -> B -> A × B
+
+fst : {A B : Set} -> A × B -> A
+fst < a , _ > = a
+
+snd : {A B : Set} -> A × B -> B
+snd < _ , b > = b
+
+f : {A B C : Set} -> (A -> B) × (B -> C) -> (A -> C)
+f = (\p x -> snd p ((fst p) x))