--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Agda.mm	Thu Nov 28 09:27:34 2013 +0900
@@ -0,0 +1,135 @@
+<map version="0.9.0">
+<!-- To view this file, download free mind mapping software FreeMind from http://freemind.sourceforge.net -->
+<node CREATED="1384158495265" ID="ID_1057489819" MODIFIED="1384158505062" TEXT="Agda">
+<node CREATED="1384158505773" ID="ID_375459405" MODIFIED="1384158511281" POSITION="right" TEXT="Programming in Agda">
+<node CREATED="1384158511282" ID="ID_173554271" MODIFIED="1384158517612" TEXT="Programming?">
+<node CREATED="1384158518929" ID="ID_132864750" MODIFIED="1384158520292" TEXT="append"/>
+<node CREATED="1385553167504" ID="ID_655374031" MODIFIED="1385553174525" TEXT="normalzation as eval"/>
+</node>
+<node CREATED="1385553140807" ID="ID_1697810219" MODIFIED="1385553143740" TEXT="Proof">
+<node CREATED="1385553144895" ID="ID_5020353" MODIFIED="1385553161258" TEXT="complain nothing is the goal"/>
+</node>
+</node>
+<node CREATED="1384158575905" ID="ID_1857200497" MODIFIED="1384158578202" POSITION="right" TEXT="Proof">
+<node CREATED="1384158578203" ID="ID_1658338767" MODIFIED="1384158586181" TEXT="Curry Howard"/>
+<node CREATED="1384158587810" ID="ID_1975721703" MODIFIED="1384158597800" TEXT="Lambda as proof"/>
+<node CREATED="1385554013320" ID="ID_1356905670" MODIFIED="1385554017783" TEXT="Martin Lof">
+<node CREATED="1385554020817" ID="ID_356163234" MODIFIED="1385554031250" TEXT="Intutionistic Logic"/>
+</node>
+</node>
+<node CREATED="1385552512024" ID="ID_147799666" MODIFIED="1385552516341" POSITION="right" TEXT="Agda Proof System">
+<node CREATED="1385552516856" ID="ID_1464159621" MODIFIED="1385552528505" TEXT="expression"/>
+<node CREATED="1385552559432" ID="ID_133092931" MODIFIED="1385552561277" TEXT="binding"/>
+<node CREATED="1385553356789" ID="ID_1762984421" MODIFIED="1385553364891" TEXT="implicit parameters"/>
+<node CREATED="1385552549038" ID="ID_1258388375" MODIFIED="1385552552692" TEXT="lambda expression"/>
+<node CREATED="1385552529036" ID="ID_1881312508" MODIFIED="1385552530633" TEXT="type"/>
+<node CREATED="1385552532612" ID="ID_40469366" MODIFIED="1385552535010" TEXT="equality">
+<node CREATED="1385597173078" ID="ID_503695732" MODIFIED="1385597179382" TEXT="relation"/>
+<node CREATED="1385597180159" ID="ID_366226932" MODIFIED="1385597182662" TEXT="identity"/>
+</node>
+<node CREATED="1385552538773" ID="ID_594724672" MODIFIED="1385552539866" TEXT="data">
+<node CREATED="1385552575615" ID="ID_1970582835" MODIFIED="1385552578092" TEXT="equality"/>
+</node>
+<node CREATED="1385552540357" ID="ID_27933366" MODIFIED="1385552542986" TEXT="record"/>
+<node CREATED="1385553086985" ID="ID_1287863407" MODIFIED="1385553091444" TEXT="level of Set">
+<node CREATED="1385553107280" ID="ID_1726309329" MODIFIED="1385553114125" TEXT="especialy in set"/>
+</node>
+<node CREATED="1385554049111" ID="ID_1268043793" MODIFIED="1385554060412" TEXT="Qunatifiers">
+<node CREATED="1385554060934" ID="ID_98595305" MODIFIED="1385554062564" TEXT="for all"/>
+<node CREATED="1385554063438" ID="ID_938488241" MODIFIED="1385554066022" TEXT="exisits"/>
+</node>
+</node>
+<node CREATED="1385553423068" ID="ID_1167992721" MODIFIED="1385553433515" POSITION="right" TEXT="Comparing Haskell"/>
+<node CREATED="1384158640697" ID="ID_1899173298" MODIFIED="1384158643661" POSITION="right" TEXT="Category">
+<node CREATED="1385552494294" ID="ID_1015253891" MODIFIED="1385552505083" TEXT="definition of Category">
+<node CREATED="1385597141136" ID="ID_193939883" MODIFIED="1385597144786" TEXT="Monoid"/>
+</node>
+<node CREATED="1384158643993" ID="ID_1820912347" MODIFIED="1384158649133" TEXT="natural transformation">
+<node CREATED="1385553771910" ID="ID_179921992" MODIFIED="1385553774629" TEXT="nkf example"/>
+</node>
+<node CREATED="1385552884093" ID="ID_1465613770" MODIFIED="1385552886994" TEXT="What for?"/>
+</node>
+<node CREATED="1385552342991" ID="ID_1939991054" MODIFIED="1385552354178" POSITION="left" TEXT="Proof by human">
+<node CREATED="1385552354669" ID="ID_154501585" MODIFIED="1385552370256" TEXT="wrote at book space"/>
+<node CREATED="1385552371251" ID="ID_836715929" MODIFIED="1385552382002" TEXT="typed text"/>
+<node CREATED="1385552385336" ID="ID_1562417181" MODIFIED="1385552400070" TEXT="Written in Proof System"/>
+</node>
+<node CREATED="1384158653521" ID="ID_666651656" MODIFIED="1384158659565" POSITION="left" TEXT="technique">
+<node CREATED="1384158660337" ID="ID_1951403393" MODIFIED="1384158666022" TEXT="?">
+<node CREATED="1385553875993" ID="ID_1969521083" MODIFIED="1385553887280" TEXT="show type of this place"/>
+</node>
+<node CREATED="1384158666649" ID="ID_1339522289" MODIFIED="1385552771364" TEXT="equaltion transformation">
+<node CREATED="1385552998803" ID="ID_406773110" MODIFIED="1385553004592" TEXT="using ? in transformation"/>
+<node CREATED="1385553932043" ID="ID_115305994" MODIFIED="1385553943751" TEXT="determine the result"/>
+<node CREATED="1385553955708" ID="ID_105082961" MODIFIED="1385553960578" TEXT="try and error">
+<node CREATED="1385553963308" ID="ID_454085934" MODIFIED="1385553966355" TEXT="automatic?"/>
+<node CREATED="1385553972519" ID="ID_1468748078" MODIFIED="1385553979196" TEXT="unspeficed example"/>
+</node>
+</node>
+<node CREATED="1385553312419" ID="ID_570137281" MODIFIED="1385553316034" TEXT="record">
+<node CREATED="1385553316404" ID="ID_1584846061" MODIFIED="1385553329979" TEXT="descipbing mathematical construct"/>
+<node CREATED="1385554082422" ID="ID_1122297353" MODIFIED="1385554088641" TEXT="sntandard procedure">
+<node CREATED="1385554130413" ID="ID_170791825" MODIFIED="1385554140797" TEXT="to show the existence of the record"/>
+<node CREATED="1385554092447" ID="ID_1172230634" MODIFIED="1385554100198" TEXT="define record"/>
+<node CREATED="1385554100656" ID="ID_1463057859" MODIFIED="1385554109327" TEXT="describe field"/>
+<node CREATED="1385554109800" ID="ID_1363129826" MODIFIED="1385554115073" TEXT="proof filed"/>
+</node>
+<node CREATED="1385552973397" ID="ID_975113480" MODIFIED="1385554244732" TEXT="where to put variables?">
+<node CREATED="1385552981158" ID="ID_271531253" MODIFIED="1385552985460" TEXT="equalizer"/>
+</node>
+</node>
+<node CREATED="1385553337511" ID="ID_375830623" MODIFIED="1385553340044" TEXT="lemma">
+<node CREATED="1385553340598" ID="ID_1472759359" MODIFIED="1385553342884" TEXT="theorem"/>
+<node CREATED="1385553343847" ID="ID_1243315508" MODIFIED="1385553350226" TEXT="input"/>
+</node>
+<node CREATED="1385552588272" ID="ID_102481863" MODIFIED="1385552600054" TEXT="unproofbable theorem">
+<node CREATED="1385552600714" ID="ID_310970637" MODIFIED="1385552682204" TEXT="functional extensionarity "/>
+<node CREATED="1385552710574" ID="ID_1830254576" MODIFIED="1385552716716" TEXT="congulurence"/>
+</node>
+<node CREATED="1385552778933" ID="ID_111669053" MODIFIED="1385552786125" TEXT="type inconsistency">
+<node CREATED="1385552786679" ID="ID_463662714" MODIFIED="1385552788556" TEXT="red"/>
+</node>
+<node CREATED="1385552790550" ID="ID_1875122156" MODIFIED="1385552814210" TEXT="insufficent instanciation">
+<node CREATED="1385552814757" ID="ID_1350447565" MODIFIED="1385552817194" TEXT="yellow"/>
+</node>
+<node CREATED="1385553372431" ID="ID_922931873" MODIFIED="1385553392411" TEXT="make implict variable explicit">
+<node CREATED="1385553402940" ID="ID_1458630954" MODIFIED="1385553409689" TEXT="in lambda parameter"/>
+</node>
+<node CREATED="1385553033119" ID="ID_848845946" MODIFIED="1385553036165" TEXT="module">
+<node CREATED="1385553037809" ID="ID_1708974052" MODIFIED="1385553041116" TEXT="module parameter"/>
+<node CREATED="1385553043977" ID="ID_106475876" MODIFIED="1385553054929" TEXT="mono-morphism">
+<node CREATED="1385553057444" ID="ID_548012657" MODIFIED="1385553064202" TEXT="strange symbols"/>
+</node>
+</node>
+</node>
+<node CREATED="1384158677282" ID="ID_174231957" MODIFIED="1385552419537" POSITION="left" TEXT="mathematical thinking">
+<node CREATED="1384158684403" ID="ID_1399570192" MODIFIED="1384158689741" TEXT="understanding"/>
+<node CREATED="1385552451013" ID="ID_831968301" MODIFIED="1385552457147" TEXT="pattern matching"/>
+<node CREATED="1385552461182" ID="ID_220420516" MODIFIED="1385552466866" TEXT="problem solving">
+<node CREATED="1385552466866" ID="ID_781175552" MODIFIED="1385552473172" TEXT="proof finding"/>
+</node>
+<node CREATED="1385552477803" ID="ID_1460716599" MODIFIED="1385552482511" TEXT="problem finding"/>
+</node>
+<node CREATED="1385552909317" ID="ID_1707994061" MODIFIED="1385552914641" POSITION="left" TEXT="usefulness of Agda">
+<node CREATED="1385552915662" ID="ID_643691875" MODIFIED="1385552927413" TEXT="to complete understandings"/>
+<node CREATED="1385552934325" ID="ID_133712397" MODIFIED="1385552943388" TEXT="see the proof symmetrry"/>
+<node CREATED="1385552951917" ID="ID_1111590064" MODIFIED="1385552962300" TEXT="find proof"/>
+<node CREATED="1385553232568" ID="ID_468716239" MODIFIED="1385553237087" TEXT="all manual">
+<node CREATED="1385553237769" ID="ID_1111001659" MODIFIED="1385553241551" TEXT="no tactics"/>
+<node CREATED="1385553247808" ID="ID_1663360868" MODIFIED="1385553251590" TEXT="visible proof"/>
+</node>
+<node CREATED="1385553266033" ID="ID_1734836012" MODIFIED="1385553271207" TEXT="proof is very personal">
+<node CREATED="1385553272594" ID="ID_1133435953" MODIFIED="1385553275976" TEXT="special symbols"/>
+<node CREATED="1385553278491" ID="ID_1356974254" MODIFIED="1385553295237" TEXT="customaization of equations and transformation"/>
+<node CREATED="1385553706422" ID="ID_364674985" MODIFIED="1385553716075" TEXT="module parameter selection"/>
+</node>
+</node>
+<node CREATED="1385553189860" ID="ID_867277383" MODIFIED="1385553192010" POSITION="left" TEXT="How to use">
+<node CREATED="1385553195958" ID="ID_286425960" MODIFIED="1385553205471" TEXT="to understand Cateogory theory">
+<node CREATED="1385553734186" ID="ID_1768850276" MODIFIED="1385553736159" TEXT="Monad"/>
+<node CREATED="1385553737601" ID="ID_1237992091" MODIFIED="1385553742471" TEXT="Kan extension"/>
+</node>
+<node CREATED="1385553208022" ID="ID_1238219050" MODIFIED="1385553225357" TEXT="Hoare logic like proof of practical programming"/>
+</node>
+</node>
+</map>