Ones Inner Universe

I am 谢宇恒 (xiè yǔ héng),
an independent Chinese researcher in Foundations of Mathematics.

The area of my inquiry is beautifully formulated by Vladimir Voevodsky as the following,

> A formal deduction system together with a correspondence
> between its components and objects and actions in the world of mathematical thoughts
> which can be used to formalize all subject areas of mathematics
> is called a foundational system for mathematics or "Foundations of Mathematics".

I design programming languages
and use them as formal deduction systems
to formalize areas of mathematics which I am interested in.

I am specially interested in the formalization of Algebraic topology,
(I am trying to find an algebraic definition of infinity groupoids
that would satisfy the Grothendieck correspondence.)
and its applications in Geometric modeling.

I am also specially interested in the formalization of Category theory,
and its applications in the design of programming language's type systems.
(Which relates back to my language designs.)
This kind of applications are called Categorical semantics or Categorical logic.
(It is called "Categorical logic" because type systems
are equivalent to logic deduction systems.)

I am also interested in the formalization of Lattice theory,
and its applications in formal concept analysis.

link:README.txt
link:contents.txt
link:friends.md
link:index
link:note.md
link:quotes.md
link:spam-cn.md
link:think-twice.md
link:toc
link:lang/abc/the-abc-programmers-handbook.md
link:lang/agda/tutorial-of-agda.org
link:lang/c/pointer.org
link:lang/cicada/arrow/arrow-lang.org
link:lang/cicada/cell-complex/a-language-for-equivalence.org
link:lang/cicada/cell-complex/aeqea.org
link:lang/cicada/cell-complex/at1-note.org
link:lang/cicada/cell-complex/fibration.org
link:lang/cicada/cell-complex/holding.org
link:lang/cicada/cell-complex/index.txt
link:lang/cicada/cell-complex/main.org
link:lang/cicada/cell-complex/meaningful-distinctions.org
link:lang/cicada/cell-complex/note.org
link:lang/cicada/cell-complex/principle-of-syntax.org
link:lang/cicada/cell-complex/square.org
link:lang/cicada/cell-complex/syntax.org
link:lang/cicada/cell-complex/the-euclid-way.org
link:lang/cicada/cicada-language-note.org
link:lang/cicada/cicada-language-prose.org
link:lang/cicada/cicada-language/old/dependent-type.org
link:lang/cicada/cicada-language/old/type-check-1.org
link:lang/cicada/cicada-language/old/type-check.org
link:lang/cicada/cicada-language/open/cicada-vm-in-js.org
link:lang/cicada/cicada-language/open/constructive-and-numerical-analysis.org
link:lang/cicada/cicada-language/open/k.org
link:lang/cicada/cicada-language/open/learning-unification-from-prolog.org
link:lang/cicada/cicada-language/open/mark-language.org
link:lang/cicada/cicada-language/open/predicate.org
link:lang/cicada/cicada-language/open/tag-group-hash-table.org
link:lang/cicada/cicada-language/open/type-system-2.org
link:lang/cicada/cicada-language/open/type-system-3.org
link:lang/cicada/cicada-language/open/type-system.org
link:lang/cicada/cicada-language/open/using-dependent-type.org
link:lang/cicada/cicada-language/open/vm.org
link:lang/cicada/cicada-language/syntax-testing/functor.cl
link:lang/cicada/cicada-language/syntax-testing/list.cl
link:lang/cicada/cicada-language/syntax-testing/little-test.cl
link:lang/cicada/cicada-language/syntax-testing/misc.cl
link:lang/cicada/cicada-language/syntax-testing/natural.cl
link:lang/cicada/cicada-language/syntax-testing/red-black-tree.cl
link:lang/cicada/cicada-language/syntax-testing/vector.cl
link:lang/cicada/cicada-note.org
link:lang/cicada/cicada-nymph-note--chinese.org
link:lang/cicada/cicada-nymph-note.org
link:lang/cicada/cicada-nymph/close/local-name.org
link:lang/cicada/cicada-nymph/close/module-mechanism.org
link:lang/cicada/cicada-nymph/close/non-local-exit.org
link:lang/cicada/cicada-nymph/close/return-structured-data.org
link:lang/cicada/cicada-nymph/close/test-framework.org
link:lang/cicada/cicada-nymph/close/undo-mechanism.org
link:lang/cicada/cicada-nymph/old/code-generation.org
link:lang/cicada/cicada-nymph/old/function-as-return-value.org
link:lang/cicada/cicada-nymph/old/io.org
link:lang/cicada/cicada-nymph/old/pre-name-hash-table-period.org
link:lang/cicada/cicada-type-system.cl
link:lang/cicada/documentations-of-old-cicada.org
link:lang/cicada/early-assembly-code.org
link:lang/cicada/ten-commandments.org
link:lang/coq/about-unicode.org
link:lang/coq/coq-in-a-hurry.org
link:lang/coq/software-foundations.org
link:lang/digrap/digrap.org
link:lang/digrap/lib/basic-functions-for-graph.scm
link:lang/digrap/lib/representation-of-graph.scm
link:lang/digrap/lib/wordy-lisp.scm
link:lang/elixir/absinthe.org
link:lang/elixir/elixir-behaviors.org
link:lang/elixir/phoenix.org
link:lang/elixir/the-little-elixir-and-otp-guidebook.org
link:lang/erlang/learning-erlang.org
link:lang/forth/classical-forth.org
link:lang/forth/thinking-forth.org
link:lang/iris/iris-note.org
link:lang/joy/the-inspiration-from-joy.org
link:lang/js/tutorial-of-javascript.org
link:lang/lisp/lisp-note.org
link:lang/lisp/lisp.org
link:lang/microkanren/microkanren.org
link:lang/microkanren/microkanren.scm
link:lang/minikanren/mk.org
link:lang/minikanren/mk.scm
link:lang/minikanren/racketrc.scm
link:lang/minikanren/simple.org
link:lang/minikanren/simple.scm
link:lang/minikanren/sokuza.org
link:lang/minikanren/sokuza.scm
link:lang/minikanren/the-reasoned-schemer.org
link:lang/minikanren/the-reasoned-schemer.scm
link:lang/ml/the-little-mler--ocaml.org
link:lang/ml/the-little-mler.org
link:lang/note/7-and-7-more.org
link:lang/note/about-record-type.org
link:lang/note/aim.org
link:lang/note/implementation-of-strategy-and-technic.org
link:lang/note/programming-language-note.org
link:lang/note/sequent-and-nested-square-bracket.org
link:lang/note/stack.org
link:lang/note/the-use-of-prefix-notation.org
link:lang/pie/prelude.pie
link:lang/pie/the-little-typer.org
link:lang/planner/planner-note.md
link:lang/prolog/clause-and-effect.org
link:lang/prolog/good-prolog.md
link:lang/prolog/swi-prolog-reference-manual.org
link:lang/prolog/the-arf-of-prolog.org
link:lang/prolog/the-craft-of-prolog.org
link:lang/prolog/tutorial-of-prolog.org
link:lang/prolog/types-in-logic-programming.org
link:lang/prolog/warren-s-abstract-machine.org
link:lang/scheme/daedalus.org
link:lang/scheme/eopl.org
link:lang/scheme/learning-racket.org
link:lang/scheme/learning-scheme.org
link:lang/scheme/little-lambda.scm
link:lang/scheme/practice/little.rkt
link:lang/scheme/rnrs.org
link:lang/scheme/sicp.org
link:lang/scheme/the-little-schemer.org
link:lang/scheme/the-seasoned-schemer.org
link:lang/scheme/three-implementation-models-for-scheme.org
link:lang/shen/tutorial-of-shen.org
link:lang/smalltalk/smalltalk-note.org
link:lang/tcl/learning-tcl.org
link:lang/xml/practical-sgml.md
link:lang/xml/understanding-sgml-and-xml-tools.md
link:music/music-diary.html
link:note/biology/human-behavioral-biology.md
link:note/biology/neuroscience-note.md
link:note/category-theory/categorical-semantics.md
link:note/category-theory/categories-for-the-working-mathematician.md
link:note/category-theory/category-theory-for-programmers.md
link:note/category-theory/contextual-pre-category.md
link:note/category-theory/n-cat.org
link:note/category-theory/the-catsters.md
link:note/computer-science/algorithm/learning-algorithm.org
link:note/computer-science/architecture/architecture-with-ashi-krishnan.md
link:note/computer-science/architecture/resilient-and-enduring.org
link:note/computer-science/art-of-computer-programming/taocp.org
link:note/computer-science/automata/automata-lectures-by-jeff-ullman.org
link:note/computer-science/automata/automata-note.org
link:note/computer-science/automata/regular-algebra-and-finite-machines.org
link:note/computer-science/compiler/about-interpreter-and-compiler.org
link:note/computer-science/compiler/call-with-cc.org
link:note/computer-science/compiler/compiler.org
link:note/computer-science/compiler/understanding-and-writing-compilers.org
link:note/computer-science/computational-geometry/computational-geometry.org
link:note/computer-science/computer-graphics/computer-graphics.org
link:note/computer-science/computer-graphics/guide-to-3d-vision-computation.org
link:note/computer-science/concurrency/actor-model.org
link:note/computer-science/concurrency/concurrency.org
link:note/computer-science/concurrency/scheduling.org
link:note/computer-science/cryptography/cryptography.org
link:note/computer-science/data-mining/SPMF.org
link:note/computer-science/data-mining/anomaly-detection.org
link:note/computer-science/data-mining/root-cause-analysis.org
link:note/computer-science/database/a-relational-model-of-data-for-large-shared-data-banks.md
link:note/computer-science/database/intro-to-database-systems--course.md
link:note/computer-science/database/mysql-note.md
link:note/computer-science/database/postgresql-note.md
link:note/computer-science/database/relational-algebra.md
link:note/computer-science/database/seven-databases.md
link:note/computer-science/graph-theory/graph-grammar.org
link:note/computer-science/information-theory/entropy.org
link:note/computer-science/machine-learning/machine-learning.org
link:note/computer-science/morphogenesis/morphogenesis.org
link:note/computer-science/net/net.org
link:note/computer-science/numerical/numerical-analysis-note.org
link:note/computer-science/object-oriented/design-patterns.org
link:note/computer-science/object-oriented/object.org
link:note/computer-science/operating-system/archlinux-admin.org
link:note/computer-science/operating-system/os.org
link:note/computer-science/parsing/algorithmic-botany.md
link:note/computer-science/parsing/excerpts.md
link:note/computer-science/parsing/grammar-and-tree.md
link:note/computer-science/parsing/parsing-techniques-note.org
link:note/computer-science/protocol/network-protocol.org
link:note/computer-science/security/security.org
link:note/computer-science/semantic/semantic.org
link:note/computer-science/user-interface/learning-editor.org
link:note/computer-science/web/front-end.org
link:note/computer-science/web/graphql.org
link:note/computer-science/web/nodejs.org
link:note/computer-science/web/semantic-web.md
link:note/computer-science/web/web.org
link:note/design/editor.org
link:note/economics/finance-and-capital-markets.org
link:note/economics/financial-market.org
link:note/engineering/computational-science-and-engineering.org
link:note/engineering/engineering.org
link:note/game/combinatorial-game-theory/combinatorial-game-theory.org
link:note/game/combinatorial-game-theory/on-numbers-and-games.org
link:note/game/combinatorial-game-theory/winning-ways.org
link:note/game/game-semantics/game-semantics.org
link:note/game/game-semantics/quantification-theory.org
link:note/game/game-theory/game-theory.org
link:note/game/game-theory/theory-of-games-and-economic-behavior.org
link:note/game/topic.org
link:note/history/history-of-math.org
link:note/history/nine-chapters.org
link:note/lattice-theory/conceptual-exploration.md
link:note/lattice-theory/formal-concept-analysis/concept-in-chinese.md
link:note/lattice-theory/formal-concept-analysis/coursera-lecture--sergei-obiedkov.md
link:note/lattice-theory/formal-concept-analysis/formal-concept-analysis-in-chinese.md
link:note/lattice-theory/formal-concept-analysis/how-to-propagate-formal-concept-analysis.md
link:note/lattice-theory/formal-concept-analysis/implementation-note.md
link:note/lattice-theory/formal-concept-analysis/more-formal-notaiton-for-mathematics.md
link:note/lattice-theory/formal-concept-analysis/why-formal-concept-analysis.md
link:note/lattice-theory/introduction-to-lattices-and-order.md
link:note/leadership/how-to-speak.md
link:note/leadership/the-craft-of-writing-effectively.md
link:note/learning-to-learn/critique-of-feynman-algorithm.org
link:note/learning-to-learn/four-simple-questions-for-studying-a-subject.md
link:note/learning-to-learn/what-is-its-methodology.org
link:note/linguistic/categorial-grammar.md
link:note/linguistic/chinese/shi-ci-bi-ji/shi-ci-bi-ji.org
link:note/linguistic/classical-chinese.org
link:note/linguistic/comparative-linguistics/comparing-note.org
link:note/linguistic/construction-grammar.md
link:note/linguistic/syntax-and-semantic.org
link:note/linguistic/syntax/notation-of-calculus.org
link:note/linguistic/toki-pona.org
link:note/little-thought/computation.org
link:note/little-thought/meaning-of-type-system.org
link:note/little-thought/programming.org
link:note/little-thought/test.org
link:note/little-thought/the-meaning-is-use.org
link:note/logic/classical-logic.org
link:note/logic/hoare-logic.org
link:note/logic/how-to-mock-a-mockingbird.md
link:note/logic/language-proof-and-logic--stanford-open-course.md
link:note/logic/markov-logic.org
link:note/logic/modal-logic.md
link:note/logic/model-theory.org
link:note/logic/proof-theory.org
link:note/logic/provers.org
link:note/logic/temporal-logic.md
link:note/management/agile.org
link:note/mathematics/algebra/arith-level.org
link:note/mathematics/algebra/combinatorial-group-theory.org
link:note/mathematics/algebra/level-of-arithmetic.org
link:note/mathematics/algebraic-geometry/a-problem-solving-approach.org
link:note/mathematics/algebraic-topology/homology.org
link:note/mathematics/algebraic-topology/initiation-combinatorial-to-topology.org
link:note/mathematics/algebraic-topology/the-topology-of-cw-complexes.md
link:note/mathematics/algebraic-topology/topological-methods-in-group-theory.org
link:note/mathematics/combinatorics/combinatorics.org
link:note/mathematics/complex-system/complex-system.org
link:note/mathematics/constructivism/constructive-math.org
link:note/mathematics/constructivism/constructivism-computer-and-programming-language.org
link:note/mathematics/constructivism/learning-constructivism.org
link:note/mathematics/geometry/an-introduction-to-clifford-algebras-and-spinors.org
link:note/mathematics/geometry/continuum.org
link:note/mathematics/geometry/drawing.org
link:note/mathematics/geometry/geometry-synthsis.org
link:note/mathematics/geometry/lectures-on-polytopes.org
link:note/mathematics/geometry/mesh-generation.org
link:note/mathematics/geometry/shape-of-nature.md
link:note/mathematics/geometry/understanding-geometric-algebra.org
link:note/mathematics/mathematical-optimization/convex-optimization.org
link:note/mathematics/probability/probabilistic-systems-analysis.org.org
link:note/mathematics/statistics/fundamentals-of-statistics.org
link:note/misc/adventures-in-writing.org
link:note/misc/didactics.org
link:note/misc/work.org
link:note/music/celt/songs.org
link:note/music/seiganushiga.org
link:note/music/the-call-of-the-mountains.md
link:note/music/this-will-be-the-day.org
link:note/music/video.org
link:note/philosophy/consistency.org
link:note/philosophy/epistemology.org
link:note/philosophy/independence-awake.md
link:note/philosophy/philosophy-of-language.md
link:note/poem/chan-fu.org
link:note/psychology/positive-psychology.md
link:note/spring-and-autumn/category-theory.org
link:note/spring-and-autumn/function-and-relation.org
link:note/spring-and-autumn/life-in-hiding.org
link:note/spring-and-autumn/minikanren.org
link:note/spring-and-autumn/reading-the-reasoned-schemer.org
link:note/spring-and-autumn/sa.org
link:note/spring-and-autumn/see-and-act.org
link:note/spring-and-autumn/sequent.org
link:note/type-theory/checking-dependent-types-with-normalization-by-evaluation.org
link:note/type-theory/church-encoding.md
link:note/type-theory/church-turing-thesis.org
link:note/type-theory/function-compose-type-cut.org
link:note/type-theory/hott.org
link:note/type-theory/how-to.org
link:note/type-theory/index.txt
link:note/type-theory/inductive-type.org
link:note/type-theory/inheritance-is-not-subtyping.md
link:note/type-theory/lambda-calculus.org
link:note/type-theory/language-implementation-tricks.md
link:note/type-theory/natural-deduction.md
link:note/type-theory/normalization-by-evaluation.org
link:note/type-theory/peirce-s-law.org
link:note/type-theory/prop-as-type.org
link:note/type-theory/the-use-of-type.org
link:note/type-theory/towards-a-practical-programming-language-based-on-dependent-type-theory.md
link:note/type-theory/type-as-game.txt
link:note/type-theory/type-theory.md
link:note/type-theory/why-nominal-typing-matters-in-object-oriented-programming.md
link:paper/a-recursive-combinatorial-description-of-cell-complex.md
link:paper/a-substitution-model-for-class-definition.md
link:paper/algebraic-structure-adventure.md
link:paper/dependently-typed-jojo-calculus.md
link:paper/fulfilling-type-system.md
link:paper/fulfilling-type-system.org
link:paper/i-also-do-not-have-the-time.md
link:paper/investigations-into-cell-complex.org
link:paper/investigations-of-mathematical-deduction.org
link:paper/simply-typed-jojo-calculus.md
link:paper/some-historical-notes-about-formal-language-design.md
link:paper/substitutional-pre-category.md
link:paper/type-and-light.md
link:paper/why-pure-type-system-p.md
link:person/a-n-whitehead/a-n-whitehead.org
link:person/aaron-sloman/evolved-construction-kits-for-building-minds.md
link:person/aaron-sloman/what-s-your-main-project.md
link:person/alain-connes/alain-connes.org
link:person/alexander-grothendieck/sketch-of-a-programme.md
link:person/alonzo-church/alonzo-church.md
link:person/aristotle/aristotle.org
link:person/augustus-de-morgan/augustus-de-morgan.org
link:person/boole/boole.org
link:person/brahana/brahana.org
link:person/branko-gruenbaum/branko-gruenbaum.org
link:person/brentano/brentano.org
link:person/brouwer/brouwer.org
link:person/burnside/burnside.org
link:person/charles-bukowski/go-all-the-way.md
link:person/charles-sanders-peirce/charles-sanders-peirce.org
link:person/charles-sanders-peirce/description-of-a-notation-for-the-logic-of-relatives.md
link:person/charles-sanders-peirce/how-to-make-our-ideas-clear.md
link:person/charles-sanders-peirce/on-the-algebra-of-logic.md
link:person/charles-sanders-peirce/the-fixation-of-belief.md
link:person/charles-sanders-peirce/what-distinguishes-a-person-from-a-word-c-s-peirce-s-thought.md
link:person/chomsky/chomsky.org
link:person/clifford/clifford.org
link:person/coxeter/coxeter.org
link:person/dag-prawitz/natural-deduction-a-proof-theoretical-study.md
link:person/daniel-friedman/daniel-friedman.org
link:person/de-bruijn/a-survey-of-the-project-automath.md
link:person/de-bruijn/lambda-calculus-notation-with-nameless-dummies.md
link:person/de-bruijn/set-theory-with-type-restrictions.md
link:person/de-bruijn/telescopic-mappings-in-typed-lambda-calculus.md
link:person/de-bruijn/the-mathematical-language-automath.md
link:person/de-bruijn/verification-of-mathematical-proofs-by-a-computer.md
link:person/derrida/derrida.org
link:person/dijkstra/EWD.org
link:person/dijkstra/dijkstra.org
link:person/dijkstra/on-the-shape-of-mathematical-arguments.org
link:person/dijkstra/two-lectures.org
link:person/donella-meadows/thinking-in-systems.txt
link:person/emily-dickinson/emily-dickinson.md
link:person/errett-bishop/bishop-s-four-principles-of-constructivism.md
link:person/errett-bishop/errett-bishop.org
link:person/euclid/euclid.org
link:person/euler/euler.org
link:person/feynman/feynman.org
link:person/foucault/foucault.org
link:person/galois/我沒有時間了.md
link:person/gentzen/gentzen.org
link:person/george-boolos/logic-logic-and-logic.md
link:person/george-boolos/to-be-is-a-value-of-a-variable.md
link:person/george-pólya/how-to-solve-it.md
link:person/george-pólya/teaching-us-a-lesson.md
link:person/gottlob-frege/Begriffsschrift.md
link:person/gottlob-frege/frege-s-work-in-english.md
link:person/haskell-curry/haskell-curry.org
link:person/hatcher/hatcher.org
link:person/hegel/hegel.org
link:person/henk-barendregt/lambda-calculus-with-types.md
link:person/herbrand/herbrand.org
link:person/hermann-grassmann/hermann-grassmann.org
link:person/heyting/heyting.org
link:person/hume/hume.org
link:person/hurewicz/hurewicz.org
link:person/j-h-c-whitehead/j-h-c-whitehead.org
link:person/james-w-alexander/james-w-alexander.org
link:person/jay-wright-forrester/applications-of-system-dynamics.txt
link:person/jay-wright-forrester/principles-of-systems/chapter-1--systems.txt
link:person/jay-wright-forrester/principles-of-systems/index.txt
link:person/jay-wright-forrester/the-common-foundation-underlying-physical-and-social-systems.txt
link:person/john-cartmell/generalised-algebraic-theories-and-contextual-categories--1978-thesis.md
link:person/john-cartmell/generalised-algebraic-theories-and-contextual-categories--1985.md
link:person/john-conway/john-conway.org
link:person/john-locke/john-locke.org
link:person/john-mccarthy/john-mccarthy.org
link:person/john-milnor/john-milnor.org
link:person/jonathan-sterling/type-theory-and-its-meaning-explanations.md
link:person/joseph-goguen/a-categorical-manifesto.md
link:person/joseph-goguen/what-is-unification-p.md
link:person/lefschetz/lefschetz.org
link:person/leibniz/calculus-ratiocinator.md
link:person/leibniz/characteristica-universalis.md
link:person/leonard-susskind/leonard-susskind.org
link:person/leonardo-da-vinci/leonardo-da-vinci.org
link:person/lickorish/lickorish.org
link:person/lukasiewicz/lukasiewicz.org
link:person/marcel-berger/marcel-berger.org
link:person/marcuse/marcuse.org
link:person/martin-löf/an-intuitionistic-theory-of-types--predicative-part.org
link:person/martin-löf/an-intuitionistic-theory-of-types.org
link:person/martin-löf/constructive-mathematics-and-computer-programming.md
link:person/martin-löf/intuitionistic-type-theory.md
link:person/martin-löf/invariance-under-isomorphism-and-definability.md
link:person/martin-löf/martin-löf.org
link:person/martin-löf/on-the-meanings-of-the-logical-constants-and-the-justification-of-logical-laws.md
link:person/marvin-minsky/marvin-minsky.org
link:person/max-dehn/lectures-on-group-theory.md
link:person/max-dehn/lectures-on-surface-topology.md
link:person/max-dehn/max-dehn.org
link:person/max-dehn/on-infinite-discontinuous-groups.md
link:person/max-dehn/on-the-topology-of-three-dimensional-space.md
link:person/max-dehn/the-group-of-mapping-classes.md
link:person/max-newman/max-newman.org
link:person/n-j-wildberger/n-j-wildberger.org
link:person/newton/newton.org
link:person/nietzsche/nietzsche.org
link:person/norman-steenrod/norman-steenrod.org
link:person/oleg-kiselyov/oleg-kiselyov.org
link:person/p-j-higgins/p-j-higgins.org
link:person/patrick-winston/patrick-winston.md
link:person/pedro-domingos/pedro-domingos.org
link:person/peter-dybjer/inductive-families.md
link:person/peter-norvig/peter-norvig.org
link:person/pieter-hintjens/pieter-hintjens.org
link:person/poincaré/觀念論.md
link:person/raymond-smullyan/diagonalization-and-self-reference.org
link:person/raymond-smullyan/gödel-s-incompleteness-theorems.md
link:person/raymond-smullyan/recursion-theory-for-metamathematics.md
link:person/raymond-smullyan/set-theory-and-the-continuum-problem.md
link:person/raymond-smullyan/smullyan.org
link:person/richard-hamming/richard-hamming.org
link:person/rimbaud/煉獄.md
link:person/robin-milner/robin-milner.org
link:person/roland-backhouse/do-it-yourself-type-theory.md
link:person/ronald-brown/ronald-brown.org
link:person/rudolf-wille/restructuring-lattice-theory.md
link:person/russell/russell.org
link:person/schopenhauer/schopenhauer.org
link:person/schroeder-heister/a-natural-extension-of-natural-deduction.md
link:person/seifert/seifert.org
link:person/spinoza/spinoza.org
link:person/spivak/spivak.org
link:person/sussman/sussman.org
link:person/sze-tsen-hu/sze-tsen-hu.org
link:person/tadashi-tokieda/tadashi-tokieda.org
link:person/tarski/tarski.org
link:person/thomas-kuhn/thomas-kuhn.org
link:person/thurston/thurston.org
link:person/tibor-ganti/tibor-ganti.org
link:person/tietze/tietze.org
link:person/tony-hoare/tony-hoare.org
link:person/van-kampen/van-kampen.org
link:person/veblen/veblen.org
link:person/vladimir-voevodsky/computer-science-and-homotopy-theory.md
link:person/vladimir-voevodsky/how-i-became-interested-in-foundations-of-mathematics.md
link:person/vladimir-voevodsky/lecture-about-univalent-foundations-at-the-institut-henri-poincaré.md
link:person/vladimir-voevodsky/notes-on-type-systems.md
link:person/vladimir-voevodsky/type-systems-lecture-series.md
link:person/vladimir-voevodsky/what-is-constructive-mathematics-and-why-it-is-important.md
link:person/walter-lewin/walter-lewin.org
link:person/weil/weil.org
link:person/william-lawvere/conceptual-mathematics.md
link:person/william-lawvere/functorial-semantics-of-algebraic-theories--short.md
link:person/william-lawvere/functorial-semantics-of-algebraic-theories.md
link:person/william-lawvere/lectures.md
link:person/william-lawvere/sets-for-mathematics.md
link:person/xieyuheng/xieyuheng.org
link:person/zhaohui-luo/computation-and-reasoning.md
link:person/zhuang-zi/zhuang-zi.org
link:person/zhuang-zi/齊物論.md
link:person/ziegler/ziegler.org
link:prosa/about-implementing-arrow-and-pair-directly.md
link:prosa/architectural-styles.md
link:prosa/build-from-present-pattern.md
link:prosa/c4model.md
link:prosa/cause-and-effect.md
link:prosa/core-concepts-of-computer-science.md
link:prosa/design-syntax-for-familiarity.md
link:prosa/hypermedia.md
link:prosa/implementing-structural-typing-again.md
link:prosa/interpreter-story.md
link:prosa/json-vs-xml.md
link:prosa/module-system.md
link:prosa/mutual-recursion.md
link:prosa/object-oriented-design-patterns.md
link:prosa/programming-language-keywords.md
link:prosa/report-on-the-little-typer/1--the-more-things-change-the-more-they-stay-the-same.md
link:prosa/report-on-the-little-typer/2--doin-what-comes-naturally.md
link:prosa/report-on-the-little-typer/3--eliminate-all-natural-numbers.md
link:prosa/report-on-the-little-typer/index.md
link:prosa/report-on-the-little-typer/recess--a-forkful-of-pie.md
link:prosa/type-bound.md
link:prosa/uncoupling.md
link:prosa/use-naive-set-theory-to-intuit-type-system.md
link:review/circumscriptive-reasoning.org
link:review/elaboration-tolerance.txt
link:review/microblog.org
link:translation/a-constructivist-manifesto.md
link:translation/are-you-an-anarchist.md
link:translation/elements-of-algebra.org
link:translation/is-god-a-taoist.md
link:translation/schizophrenia-in-contemporary-mathematics.md