Mercurial > hg > Members > atton > agda-proofs
view sandbox/InferenceTypeComposition.agda @ 77:a2e6f61d5f2b default tip
Add modus-ponens
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 09 Feb 2017 06:32:03 +0000 |
parents | 723532aa0592 |
children |
line wrap: on
line source
module InferenceTypeComposition where open import Relation.Binary.PropositionalEquality infixl 30 _+++_ -- _+++_ : {A B C : Set} {equiv : B ≡ B} -> (A -> B) -> (B -> C) -> (A -> C) _+++_ : {A B C : Set} -> (A -> B) -> (B -> C) -> (A -> C) _+++_ f g = \x -> g (f x) comp-sample : {A B C D : Set} -> (A -> B) -> (B -> C) -> (C -> D) -> (A -> D) comp-sample f g h = f +++ g +++ h