<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 CREATED="1385597681199" ID="ID_1206471263" MODIFIED="1385597687519" TEXT="executable like Haskell"/>
</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 CREATED="1385597624397" ID="ID_995313728" MODIFIED="1385597661388" TEXT="how fun non executable program?"/>
</node>
<node CREATED="1385597979683" ID="ID_1830603554" MODIFIED="1385597984087" TEXT="How popular?">
<node CREATED="1385597984088" ID="ID_1047860825" MODIFIED="1385597987107" TEXT="Coq"/>
<node CREATED="1385597987723" ID="ID_1005518327" MODIFIED="1385598007540" TEXT="Every students use Coq"/>
</node>
</node>
<node CREATED="1384158575905" ID="ID_1857200497" MODIFIED="1384158578202" POSITION="right" TEXT="Proof">
<node CREATED="1385597911855" ID="ID_226453773" MODIFIED="1385597918132" TEXT="Hayting Algebra"/>
<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="1385597309971" ID="ID_1759517864" MODIFIED="1385597312786" TEXT="emacs"/>
<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="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="1385552532612" ID="ID_40469366" MODIFIED="1385597757862" 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="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 CREATED="1385597581793" ID="ID_560374" MODIFIED="1385597584096" TEXT="all manual">
<node CREATED="1385597584881" ID="ID_1563058814" MODIFIED="1385597593100" TEXT="no haskell support"/>
</node>
</node>
<node CREATED="1385553423068" ID="ID_1167992721" MODIFIED="1385553433515" POSITION="right" TEXT="Comparing Haskell">
<node CREATED="1385597515449" ID="ID_148577390" MODIFIED="1385597522642" TEXT="strongness of types"/>
<node CREATED="1385597771461" ID="ID_1284279754" MODIFIED="1385597775740" TEXT="similar syntax"/>
</node>
<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="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="1385598120000" TEXT="selecting input arguments"/>
<node CREATED="1385598122577" ID="ID_1512810213" MODIFIED="1385598134539" TEXT="assumption as input arguments"/>
</node>
<node CREATED="1385598147877" ID="ID_1767619024" MODIFIED="1385598171099" TEXT="handling not-yet-proved part">
<node CREATED="1385598184783" ID="ID_1082183331" MODIFIED="1385598190881" TEXT="as inpput arguments"/>
<node CREATED="1385598192184" ID="ID_14552462" MODIFIED="1385598216243" TEXT="postulate"/>
</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="1385597285233" ID="ID_1903486565" MODIFIED="1385597287428" TEXT="eval">
<node CREATED="1385597287429" ID="ID_1235285760" MODIFIED="1385597292767" TEXT="environment of eval"/>
</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="1385597890324" ID="ID_1847853272" MODIFIED="1385597941292" TEXT="by types"/>
<node CREATED="1385597893765" ID="ID_1389031272" MODIFIED="1385597945129" TEXT="by models">
<node CREATED="1385597950001" ID="ID_151641398" MODIFIED="1385597956505" TEXT="not given by Agda"/>
</node>
</node>
<node CREATED="1385552451013" ID="ID_831968301" MODIFIED="1385552457147" TEXT="pattern matching">
<node CREATED="1385597962784" ID="ID_87138651" MODIFIED="1385597972049" TEXT="is this understandings?"/>
</node>
<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="1385597697480" ID="ID_895791945" MODIFIED="1385597703669" TEXT="Haskell like syntax">
<node CREATED="1385597717172" ID="ID_1406282220" MODIFIED="1385597721238" TEXT="strange symbols"/>
<node CREATED="1385597723709" ID="ID_1501399885" MODIFIED="1385597727477" TEXT="emacs support"/>
</node>
<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 CREATED="1385552342991" ID="ID_1939991054" MODIFIED="1385552354178" POSITION="right" TEXT="Proof by human">
<node CREATED="1385552354669" ID="ID_154501585" MODIFIED="1385552370256" TEXT="wrote at book space">
<node CREATED="1385597411306" ID="ID_41605107" MODIFIED="1385597416033" TEXT="3 lines of proof">
<node CREATED="1385597422045" ID="ID_1465170514" MODIFIED="1385597433982" TEXT="many missing parts"/>
<node CREATED="1385597436540" ID="ID_1855719075" MODIFIED="1385597452864" TEXT="exercise"/>
</node>
<node CREATED="1385597804760" ID="ID_552514819" MODIFIED="1385597842300" TEXT="write necessary keywords to recall only"/>
</node>
<node CREATED="1385552371251" ID="ID_836715929" MODIFIED="1385552382002" TEXT="typed text">
<node CREATED="1385597464732" ID="ID_664600436" MODIFIED="1385597469501" TEXT="missing parts"/>
<node CREATED="1385597848856" ID="ID_1150238160" MODIFIED="1385597852328" TEXT="formatting problem">
<node CREATED="1385597852600" ID="ID_1735973674" MODIFIED="1385597854304" TEXT="TeX"/>
<node CREATED="1385597854832" ID="ID_526772293" MODIFIED="1385597862164" TEXT="Commutive diagram"/>
</node>
</node>
<node CREATED="1385552385336" ID="ID_1562417181" MODIFIED="1385552400070" TEXT="Written in Proof System">
<node CREATED="1385597474149" ID="ID_1437200348" MODIFIED="1385597476509" TEXT="checked"/>
<node CREATED="1385597477565" ID="ID_1553409639" MODIFIED="1385597481238" TEXT="have to be complete"/>
</node>
</node>
</node>
</map>