Takeo Imai bonotake
bonotake
/ Theme file
Created
August 29, 2011 11:58
— forked from konn/marsandvenus.als
金星人の男と火星人の女は常に本当のことだけを云い、金星人の女と火星人の男は常に嘘を吐く。一発で男か女かを見分けることのできる、「はい」か「いいえ」で答えられる質問は何か？
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| <?xml version="1.0"?> | |
| <alloy> | |
| <view> | |
| <projection> <type name="質問"/> </projection> | |
| <defaultnode/> | |
| <defaultedge/> |
bonotake
/ Allegory.v
Created
August 15, 2011 15:14
— forked from msakai/Allegory.v
Definition of Allegory
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Require Export Category. | |
| Set Implicit Arguments. | |
| Unset Strict Implicit. | |
| Section allegory. | |
| Variable C : Category. | |
| Variable Op_intersect : forall a b : Ob C, Map2 (Hom a b) (Hom a b) (Hom a b). | |
| Variable Op_converse \u00a0: forall a b : Ob C, Map (Hom a b) (Hom b a). |