41554 blogs · [ { "id": "01a087c5-3303-70a4-a868-ae0d775bda03", "title": "Subspaces Need Not Have Complement", "url": "https://bollu.github.io/articles/subspaces-need-not-have-complement.html", "published_at": "2023-04-02T00:00:00+00:00" }, { "id": "01a087c5-3303-70a4-a868-ae0d780634a1", "title": "L^\\infty Is HUGE", "url": "https://bollu.github.io/articles/linfty-is-huge.html", "published_at": "2023-04-02T00:00:00+00:00" }, { "id": "01a087c5-3304-705d-aadf-444fa705ff31", "title": "Banach Space That Does Not Admit Schrauder Basis", "url": "https://bollu.github.io/articles/banach-space-that-does-not-admit-schrauder-basis.html", "published_at": "2023-04-02T00:00:00+00:00" }, { "id": "01a087c5-3304-705d-aadf-444fa7c93831", "title": "Open Mapping Theorem", "url": "https://bollu.github.io/articles/open-mapping-theorem.html", "published_at": "2023-04-02T00:00:00+00:00" }, { "id": "01a087c5-3304-705d-aadf-444fa7fc6405", "title": "Closed Graph Theorem", "url": "https://bollu.github.io/articles/closed-graph-theorem.html", "published_at": "2023-04-02T00:00:00+00:00" }, { "id": "01a087c5-3304-705d-aadf-444fa88cb3dd", "title": "Bounded Inverse Theorem", "url": "https://bollu.github.io/articles/bounded-inverse-theorem.html", "published_at": "2023-04-02T00:00:00+00:00" }, { "id": "01a087c5-3302-72a9-816c-9613ce521210", "title": "Why NuPRL and Realisability Makes It Hard to Communicate Math", "url": "https://bollu.github.io/articles/why-nuprl-and-realisability-makes-it-hard-to-communicate-math.html", "published_at": "2023-03-28T00:00:00+00:00" }, { "id": "01a087c5-3302-72a9-816c-9613cef8f03a", "title": "Lean Does Not Allow Nested Inductive Families", "url": "https://bollu.github.io/articles/lean-does-not-allow-nested-inductive-families.html", "published_at": "2023-03-28T00:00:00+00:00" }, { "id": "01a087c5-3302-72a9-816c-9613cf4104a9", "title": "Weakly Implicit Arguments in Lean", "url": "https://bollu.github.io/articles/weakly-implicit-arguments-in-lean.html", "published_at": "2023-03-28T00:00:00+00:00" }, { "id": "01a087c5-3302-72a9-816c-9613d0285eeb", "title": "Linkers, Loaders, and ELF", "url": "https://bollu.github.io/articles/linkers-loaders-and-elf.html", "published_at": "2023-03-28T00:00:00+00:00" }, { "id": "01a087c5-3302-72a9-816c-9613d09f4e9f", "title": "Regular Epi and Regular Category", "url": "https://bollu.github.io/articles/regular-epi-and-regular-category.html", "published_at": "2023-03-28T00:00:00+00:00" }, { "id": "01a087c5-3302-72a9-816c-9613d119fc8d", "title": "Focal Point", "url": "https://bollu.github.io/articles/focal-point.html", "published_at": "2023-03-28T00:00:00+00:00" }, { "id": "01a087c5-3302-72a9-816c-9613d1ac4782", "title": "Operational Versus Denotational Semantics", "url": "https://bollu.github.io/articles/operational-versus-denotational-semantics.html", "published_at": "2023-03-28T00:00:00+00:00" }, { "id": "01a087c5-338f-71b0-ba75-f6cb642bf40e", "title": "Intuitionstic Logic as a Heyting Algebra", "url": "https://bollu.github.io/articles/intuitionstic-logic-as-a-heyting-algebra.html", "published_at": "2023-03-28T00:00:00+00:00" }, { "id": "01a087c5-3304-705d-aadf-444fa927c123", "title": "Nonexistence of Solutions for ODE and PDE", "url": "https://bollu.github.io/articles/nonexistence-of-solutions-for-ode-and-pde.html", "published_at": "2023-03-27T00:00:00+00:00" }, { "id": "01a087c5-3304-705d-aadf-444fa941c7a9", "title": "Baire Category Theorem", "url": "https://bollu.github.io/articles/baire-category-theorem.html", "published_at": "2023-03-27T00:00:00+00:00" }, { "id": "01a087c5-3304-705d-aadf-444faa3d6e41", "title": "libOpenGL, libVDSO and Nix", "url": "https://bollu.github.io/articles/libopengl-libvdso-and-nix.html", "published_at": "2023-03-27T00:00:00+00:00" }, { "id": "01a087c5-3332-73bb-9d0f-7a458483121c", "title": "There Cannot Be a Type of Size the Universe", "url": "https://bollu.github.io/articles/there-cannot-be-a-type-of-size-the-universe.html", "published_at": "2023-03-27T00:00:00+00:00" }, { "id": "01a087c5-3334-70d0-a6d5-09d7302dc71a", "title": "Full Abstraction in Semantics", "url": "https://bollu.github.io/articles/full-abstraction-in-semantics.html", "published_at": "2023-03-27T00:00:00+00:00" }, { "id": "01a087c5-3301-70cb-987f-8136117b56b7", "title": "Lax Milgram Theorem", "url": "https://bollu.github.io/articles/lax-milgram-theorem.html", "published_at": "2023-03-26T00:00:00+00:00" }, { "id": "01a087c5-3331-723a-b38a-2cbcf50e0c2d", "title": "You Don ' t Know Jack About Data Races", "url": "https://bollu.github.io/articles/you-dont-know-jack-about-data-races.html", "published_at": "2023-01-01T00:00:00+00:00" }, { "id": "01a087c5-3332-73bb-9d0f-7a457f5c44e0", "title": "Training a Custom Model for Lean4", "url": "https://bollu.github.io/articles/training-a-custom-model-for-lean4.html", "published_at": "2023-01-01T00:00:00+00:00" }, { "id": "01a087c5-3332-73bb-9d0f-7a457f8f1ac7", "title": "Stratified Synthetsis", "url": "https://bollu.github.io/articles/stratified-synthetsis.html", "published_at": "2023-01-01T00:00:00+00:00" }, { "id": "01a087c5-3332-73bb-9d0f-7a457fb29434", "title": "Mutual Recursion Elaboration in Lean", "url": "https://bollu.github.io/articles/mutual-recursion-elaboration-in-lean.html", "published_at": "2023-01-01T00:00:00+00:00" }, { "id": "01a087c5-3332-73bb-9d0f-7a4580217dc8", "title": "Subject Reduction in Lean", "url": "https://bollu.github.io/articles/subject-reduction-in-lean.html", "published_at": "2023-01-01T00:00:00+00:00" }, { "id": "01a087c5-3332-73bb-9d0f-7a4580e6b736", "title": "GNU Binutils", "url": "https://bollu.github.io/articles/gnu-binutils.html", "published_at": "2023-01-01T00:00:00+00:00" }, { "id": "01a087c5-3331-723a-b38a-2cbcf50dcee2", "title": "Stuff I Learnt in 2022", "url": "https://bollu.github.io/articles/stuff-i-learnt-in-2022.html", "published_at": "2022-11-24T00:00:00+00:00" }, { "id": "01a087c5-3332-73bb-9d0f-7a4581d91c24", "title": "Axiom K Versus UIP", "url": "https://bollu.github.io/articles/axiom-k-versus-uip.html", "published_at": "2022-11-24T00:00:00+00:00" }, { "id": "01a087c5-3332-73bb-9d0f-7a458299af68", "title": "Linear vs Uniqueness Types", "url": "https://bollu.github.io/articles/linear-vs-uniqueness-types.html", "published_at": "2022-11-24T00:00:00+00:00" }, { "id": "01a087c5-3391-73b4-b3e9-7cbe77687fb2", "title": "Tmux", "url": "https://bollu.github.io/articles/tmux.html", "published_at": "2022-11-24T00:00:00+00:00" }, { "id": "01a087c5-3332-73bb-9d0f-7a458321e34b", "title": "Any Model of Lean Must Have All Inductives", "url": "https://bollu.github.io/articles/any-model-of-lean-must-have-all-inductives.html", "published_at": "2022-11-02T00:00:00+00:00" }, { "id": "01a087c5-3332-73bb-9d0f-7a45839b3b92", "title": "Index over the Past, Fiber over the Future", "url": "https://bollu.github.io/articles/index-over-the-past-fiber-over-the-future.html", "published_at": "2022-11-02T00:00:00+00:00" }, { "id": "01a087c5-3332-73bb-9d0f-7a4583a9109f", "title": "Type Formers Need Not Be Injective", "url": "https://bollu.github.io/articles/type-formers-need-not-be-injective.html", "published_at": "2022-11-02T00:00:00+00:00" }, { "id": "01a087c5-3332-73bb-9d0f-7a4584c5b8a9", "title": "The Dependently Typed Expression Problem", "url": "https://bollu.github.io/articles/the-dependently-typed-expression-problem.html", "published_at": "2022-11-02T00:00:00+00:00" }, { "id": "01a087c5-3332-73bb-9d0f-7a45851fb2bc", "title": "Motivation for Modal Logic", "url": "https://bollu.github.io/articles/motivation-for-modal-logic.html", "published_at": "2022-10-27T00:00:00+00:00" }, { "id": "01a087c5-3332-73bb-9d0f-7a45852d1c03", "title": "Scones", "url": "https://bollu.github.io/articles/scones.html", "published_at": "2022-10-27T00:00:00+00:00" }, { "id": "01a087c5-3332-73bb-9d0f-7a45862a1eac", "title": "Presheaf Models of Type Theory", "url": "https://bollu.github.io/articles/presheaf-models-of-type-theory.html", "published_at": "2022-10-27T00:00:00+00:00" }, { "id": "01a087c5-3332-73bb-9d0f-7a4586f5a71d", "title": "Weighted Limits via Collages", "url": "https://bollu.github.io/articles/weighted-limits-via-collages.html", "published_at": "2022-10-27T00:00:00+00:00" }, { "id": "01a087c5-3332-73bb-9d0f-7a45874cd4b9", "title": "Disjoint Coproduct", "url": "https://bollu.github.io/articles/disjoint-coproduct.html", "published_at": "2022-10-27T00:00:00+00:00" }, { "id": "01a087c5-3332-73bb-9d0f-7a4588154509", "title": "Leibniz Equality in Lean4", "url": "https://bollu.github.io/articles/leibniz-equality-in-lean4.html", "published_at": "2022-10-27T00:00:00+00:00" }, { "id": "01a087c5-3332-73bb-9d0f-7a4588e58254", "title": "Strong Normalization of STLC", "url": "https://bollu.github.io/articles/strong-normalization-of-stlc.html", "published_at": "2022-10-27T00:00:00+00:00" }, { "id": "01a087c5-3332-73bb-9d0f-7a458950b01d", "title": "Subobject Classifiers of N \\to FinSet, or Precosheaf Of FinSet", "url": "https://bollu.github.io/articles/subobject-classifiers-of-n-to-finset-or-precosheaf-of-finset.html", "published_at": "2022-10-27T00:00:00+00:00" }, { "id": "01a087c5-3332-73bb-9d0f-7a458a41b7b9", "title": "Dimensions Versus Units", "url": "https://bollu.github.io/articles/dimensions-versus-units.html", "published_at": "2022-10-27T00:00:00+00:00" }, { "id": "01a087c5-3332-73bb-9d0f-7a458aa4c6d0", "title": "HoTTesT: Identity Types", "url": "https://bollu.github.io/articles/hottest-identity-types.html", "published_at": "2022-10-27T00:00:00+00:00" }, { "id": "01a087c5-3337-7214-b99e-55837b6cec67", "title": "TLDP Pages for Bash Conditionals", "url": "https://bollu.github.io/articles/tldp-pages-for-bash-conditionals.html", "published_at": "2022-10-13T00:00:00+00:00" }, { "id": "01a087c5-3337-7214-b99e-55837c3aaa0c", "title": "Remainder, Modulo", "url": "https://bollu.github.io/articles/remainder-modulo.html", "published_at": "2022-10-13T00:00:00+00:00" }, { "id": "01a087c5-3337-7214-b99e-55837cde252c", "title": "Parameters Cannot Be Changed anywhere , Not Just in Return Location", "url": "https://bollu.github.io/articles/paramete-not-just-in-return-location.html", "published_at": "2022-10-13T00:00:00+00:00" }, { "id": "01a087c5-3338-704e-845b-a56cc251cf2a", "title": "LCNF", "url": "https://bollu.github.io/articles/lcnf.html", "published_at": "2022-10-13T00:00:00+00:00" }, { "id": "01a087c5-3338-704e-845b-a56cc3335097", "title": "Predicative v/s Impredicative: On Universes in Type Theory", "url": "https://bollu.github.io/articles/predicative-vs-impredicative-on-universes-in-type-theory.html", "published_at": "2022-10-13T00:00:00+00:00" }, { "id": "01a087c5-3338-704e-845b-a56cc3ebc869", "title": "Testing Infra in Lean4", "url": "https://bollu.github.io/articles/testing-infra-in-lean4.html", "published_at": "2022-10-13T00:00:00+00:00" }, { "id": "01a087c5-3338-704e-845b-a56cc447fcec", "title": "Autocompletion in Lean4", "url": "https://bollu.github.io/articles/autocompletion-in-lean4.html", "published_at": "2022-10-13T00:00:00+00:00" }, { "id": "01a087c5-3338-704e-845b-a56cc4caf631", "title": "Inductive Types", "url": "https://bollu.github.io/articles/inductive-types.html", "published_at": "2022-10-13T00:00:00+00:00" }, { "id": "01a087c5-3338-704e-845b-a56cc5bb780a", "title": "Parameter Verus Index", "url": "https://bollu.github.io/articles/parameter-verus-index.html", "published_at": "2022-10-13T00:00:00+00:00" }, { "id": "01a087c5-3338-704e-845b-a56cc5d31069", "title": "HNF Versus WHNF", "url": "https://bollu.github.io/articles/hnf-versus-whnf.html", "published_at": "2022-10-13T00:00:00+00:00" }, { "id": "01a087c5-3332-73bb-9d0f-7a458abe760b", "title": "Left and Right Adjoints to Inverse Image", "url": "https://bollu.github.io/articles/left-and-right-adjoints-to-inverse-image.html", "published_at": "2022-09-28T00:00:00+00:00" }, { "id": "01a087c5-3332-73bb-9d0f-7a458b28cd46", "title": "Paredit via Adjoints", "url": "https://bollu.github.io/articles/paredit-via-adjoints.html", "published_at": "2022-09-28T00:00:00+00:00" }, { "id": "01a087c5-3332-73bb-9d0f-7a458bfde196", "title": "Less than Versus Less than or Equals over Z", "url": "https://bollu.github.io/articles/less-than-versus-less-than-or-equals-over-z.html", "published_at": "2022-09-28T00:00:00+00:00" }, { "id": "01a087c5-3332-73bb-9d0f-7a458c41ec1b", "title": "Allegories and Categories", "url": "https://bollu.github.io/articles/allegories-and-categories.html", "published_at": "2022-09-28T00:00:00+00:00" }, { "id": "01a087c5-3332-73bb-9d0f-7a458ca99fb3", "title": "Partial Function as Span", "url": "https://bollu.github.io/articles/partial-function-as-span.html", "published_at": "2022-09-28T00:00:00+00:00" }, { "id": "01a087c5-3332-73bb-9d0f-7a458d964230", "title": "Turing Degree", "url": "https://bollu.github.io/articles/turing-degree.html", "published_at": "2022-09-25T00:00:00+00:00" }, { "id": "01a087c5-3332-73bb-9d0f-7a458e812023", "title": "Proof That There Is a TM Whose Halting Is Independent of ZFC", "url": "https://bollu.github.io/articles/proof-that-there-is-a-tm-whose-halting-is-independent-of-zfc.html", "published_at": "2022-09-25T00:00:00+00:00" }, { "id": "01a087c5-3332-73bb-9d0f-7a458f35cd6c", "title": "Contradiction from Non-positive Occurence", "url": "https://bollu.github.io/articles/contradiction-from-non-positive-occurence.html", "published_at": "2022-09-19T00:00:00+00:00" }, { "id": "01a087c5-3333-716a-97c6-dd81d5202d0e", "title": "The Constructible Universe L", "url": "https://bollu.github.io/articles/the-constructible-universe-l.html", "published_at": "2022-09-19T00:00:00+00:00" }, { "id": "01a087c5-3333-716a-97c6-dd81d5942a30", "title": "Godel Completeness Theorem", "url": "https://bollu.github.io/articles/godel-completeness-theorem.html", "published_at": "2022-09-19T00:00:00+00:00" }, { "id": "01a087c5-3333-716a-97c6-dd81d650601d", "title": "Uniform Proofs, Focused Proofs, Polarization, Logic Programming", "url": "https://bollu.github.io/articles/uniform-proofs-focused-proofs-polarization-logic-programming.html", "published_at": "2022-09-19T00:00:00+00:00" }, { "id": "01a087c5-3391-73b4-b3e9-7cbe71f6390b", "title": "Breakdance", "url": "https://bollu.github.io/articles/breakdance.html", "published_at": "2022-09-19T00:00:00+00:00" }, { "id": "01a087c5-3391-73b4-b3e9-7cbe72ccd67b", "title": "Cardistry", "url": "https://bollu.github.io/articles/cardistry.html", "published_at": "2022-09-19T00:00:00+00:00" }, { "id": "01a087c5-3391-73b4-b3e9-7cbe750c4c81", "title": "Don ' t Try", "url": "https://bollu.github.io/articles/dont-try.html", "published_at": "2022-09-19T00:00:00+00:00" }, { "id": "01a087c5-3391-73b4-b3e9-7cbe76bf87f4", "title": "Shuffle Dancing", "url": "https://bollu.github.io/articles/shuffle-dancing.html", "published_at": "2022-09-19T00:00:00+00:00" }, { "id": "01a087c5-3333-716a-97c6-dd81d69a8e1f", "title": "Why Cut Elimination?", "url": "https://bollu.github.io/articles/why-cut-elimination.html", "published_at": "2022-09-07T00:00:00+00:00" }, { "id": "01a087c5-3333-716a-97c6-dd81d6e00e18", "title": "Forcing to Add a Function", "url": "https://bollu.github.io/articles/forcing-to-add-a-function.html", "published_at": "2022-09-07T00:00:00+00:00" }, { "id": "01a087c5-3333-716a-97c6-dd81d7540e8f", "title": "Diaconescu ' s Theorem", "url": "https://bollu.github.io/articles/diaconescus-theorem.html", "published_at": "2022-09-07T00:00:00+00:00" }, { "id": "01a087c5-3333-716a-97c6-dd81d75f7e1c", "title": "Forcing Machinery", "url": "https://bollu.github.io/articles/forcing-machinery.html", "published_at": "2022-09-07T00:00:00+00:00" }, { "id": "01a087c5-3333-716a-97c6-dd81d79b19ab", "title": "Partial Evaluation, Chapter 3", "url": "https://bollu.github.io/articles/partial-evaluation-chapter-3.html", "published_at": "2022-09-07T00:00:00+00:00" }, { "id": "01a087c5-3333-716a-97c6-dd81d84d077a", "title": "Partial Evaluation, Chapter 1", "url": "https://bollu.github.io/articles/partial-evaluation-chapter-1.html", "published_at": "2022-09-07T00:00:00+00:00" }, { "id": "01a087c5-3334-70d0-a6d5-09d72d0b1918", "title": "Diagonal Lemma for Monotone Functions", "url": "https://bollu.github.io/articles/diagonal-lemma-for-monotone-functions.html", "published_at": "2022-09-07T00:00:00+00:00" }, { "id": "01a087c5-3334-70d0-a6d5-09d72d401af1", "title": "Cantor Schroder Bernstein via Fixpoint", "url": "https://bollu.github.io/articles/cantor-schroder-bernstein-via-fixpoint.html", "published_at": "2022-09-07T00:00:00+00:00" }, { "id": "01a087c5-3334-70d0-a6d5-09d72d553129", "title": "Maximal Ideals of Boolean Algebras Are Truth Values", "url": "https://bollu.github.io/articles/maximal-ideals-of-boolean-algebras-are-truth-values.html", "published_at": "2022-09-07T00:00:00+00:00" }, { "id": "01a087c5-3334-70d0-a6d5-09d72e197f95", "title": "Resolution Algorithm for Propositional Logic", "url": "https://bollu.github.io/articles/resolution-algorithm-for-propositional-logic.html", "published_at": "2022-09-07T00:00:00+00:00" }, { "id": "01a087c5-3334-70d0-a6d5-09d72e6d7565", "title": "Completeness for First Order Logic", "url": "https://bollu.github.io/articles/completeness-for-first-order-logic.html", "published_at": "2022-09-07T00:00:00+00:00" }, { "id": "01a087c5-3334-70d0-a6d5-09d72ef1c6d4", "title": "Compactness Theorem of First Order Logic", "url": "https://bollu.github.io/articles/compactness-theorem-of-first-order-logic.html", "published_at": "2022-09-07T00:00:00+00:00" }, { "id": "01a087c5-3334-70d0-a6d5-09d72f5ff024", "title": "First Order Logic: Semantics", "url": "https://bollu.github.io/articles/first-order-logic-semantics.html", "published_at": "2022-09-07T00:00:00+00:00" }, { "id": "01a087c5-3334-70d0-a6d5-09d730a70cd2", "title": "You Could Have Invented Sequents", "url": "https://bollu.github.io/articles/you-could-have-invented-sequents.html", "published_at": "2022-08-22T00:00:00+00:00" }, { "id": "01a087c5-3334-70d0-a6d5-09d730a72615", "title": "Fibrational Category Theory, Sec 1.1, Sec 1.2", "url": "https://bollu.github.io/articles/fibrational-category-theory-sec-11-sec-12.html", "published_at": "2022-08-22T00:00:00+00:00" }, { "id": "01a087c5-3335-7263-a5c5-12c1c5652a1e", "title": "Simple Type Theory via Fibrations", "url": "https://bollu.github.io/articles/simple-type-theory-via-fibrations.html", "published_at": "2022-08-22T00:00:00+00:00" }, { "id": "01a087c5-3335-7263-a5c5-12c1c5e17eb6", "title": "Realisability Models", "url": "https://bollu.github.io/articles/realisability-models.html", "published_at": "2022-08-22T00:00:00+00:00" }, { "id": "01a087c5-3335-7263-a5c5-12c1c5e1d713", "title": "Naming Left Closed, Right Open with Start/stop", "url": "https://bollu.github.io/articles/naming-left-closed-right-open-with-startstop.html", "published_at": "2022-08-22T00:00:00+00:00" }, { "id": "01a087c5-3335-7263-a5c5-12c1c6661ccd", "title": "Nested vs Mutual Inductive Types:", "url": "https://bollu.github.io/articles/nested-vs-mutual-inductive-types.html", "published_at": "2022-08-22T00:00:00+00:00" }, { "id": "01a087c5-3335-7263-a5c5-12c1c73dc6f5", "title": "Embedding HOL in Lean", "url": "https://bollu.github.io/articles/embedding-hol-in-lean.html", "published_at": "2022-08-22T00:00:00+00:00" }, { "id": "01a087c5-3335-7263-a5c5-12c1c7ab692b", "title": "Module System for Separate Compilation", "url": "https://bollu.github.io/articles/module-system-for-separate-compilation.html", "published_at": "2022-08-22T00:00:00+00:00" }, { "id": "01a087c5-3337-7214-b99e-558376ccca30", "title": "Second Order Arithmetic", "url": "https://bollu.github.io/articles/second-order-arithmetic.html", "published_at": "2022-08-22T00:00:00+00:00" }, { "id": "01a087c5-3337-7214-b99e-558377841322", "title": "Lean4 Dev Meeting", "url": "https://bollu.github.io/articles/lean4-dev-meeting.html", "published_at": "2022-08-22T00:00:00+00:00" }, { "id": "01a087c5-3337-7214-b99e-558377ff5ed2", "title": "Categorical Model of Dependent Types", "url": "https://bollu.github.io/articles/categorical-model-of-dependent-types.html", "published_at": "2022-08-22T00:00:00+00:00" }, { "id": "01a087c5-3338-704e-845b-a56cc6a00cec", "title": "Different Types of Arguments in Lean4:", "url": "https://bollu.github.io/articles/different-types-of-arguments-in-lean4.html", "published_at": "2022-07-27T00:00:00+00:00" }, { "id": "01a087c5-3338-704e-845b-a56cc6ed20ae", "title": "Lean Tactics", "url": "https://bollu.github.io/articles/lean-tactics.html", "published_at": "2022-06-27T00:00:00+00:00" }, { "id": "01a087c5-3337-7214-b99e-558378337bf1", "title": "Coends", "url": "https://bollu.github.io/articles/coends.html", "published_at": "2022-06-26T00:00:00+00:00" }, { "id": "01a087c5-3337-7214-b99e-5583787ad435", "title": "Natural Transformations as Ends", "url": "https://bollu.github.io/articles/natural-transformations-as-ends.html", "published_at": "2022-06-26T00:00:00+00:00" }, { "id": "01a087c5-3337-7214-b99e-55837977c035", "title": "Ends and Diagonals", "url": "https://bollu.github.io/articles/ends-and-diagonals.html", "published_at": "2022-06-26T00:00:00+00:00" }, { "id": "01a087c5-3337-7214-b99e-55837a705d0a", "title": "Parabolic Dynamics and Renormalization", "url": "https://bollu.github.io/articles/parabolic-dynamics-and-renormalization.html", "published_at": "2022-06-26T00:00:00+00:00" }, { "id": "01a087c5-3337-7214-b99e-55837b1d9afb", "title": "Quantifiers as Adjoints", "url": "https://bollu.github.io/articles/quantifiers-as-adjoints.html", "published_at": "2022-06-26T00:00:00+00:00" } ] posts Claim your blog

Back to bollu.github.io

Blog · corpus.blog/blogs/bollu.github.io/posts

bollu.github.io

bollu.github.io

2023

Subspaces Need Not Have Complement original ↗

2 Apr 2023

L^\infty Is HUGE original ↗

2 Apr 2023

Banach Space That Does Not Admit Schrauder Basis original ↗

2 Apr 2023

Open Mapping Theorem original ↗

2 Apr 2023

Closed Graph Theorem original ↗

2 Apr 2023

Bounded Inverse Theorem original ↗

2 Apr 2023

Why NuPRL and Realisability Makes It Hard to Communicate Math original ↗

28 Mar 2023

Lean Does Not Allow Nested Inductive Families original ↗

28 Mar 2023

Weakly Implicit Arguments in Lean original ↗

28 Mar 2023

Linkers, Loaders, and ELF original ↗

28 Mar 2023

Regular Epi and Regular Category original ↗

28 Mar 2023

Focal Point original ↗

28 Mar 2023

Operational Versus Denotational Semantics original ↗

28 Mar 2023

Intuitionstic Logic as a Heyting Algebra original ↗

28 Mar 2023

Nonexistence of Solutions for ODE and PDE original ↗

27 Mar 2023

Baire Category Theorem original ↗

27 Mar 2023

libOpenGL, libVDSO and Nix original ↗

27 Mar 2023

There Cannot Be a Type of Size the Universe original ↗

27 Mar 2023

Full Abstraction in Semantics original ↗

27 Mar 2023

Lax Milgram Theorem original ↗

26 Mar 2023

You Don ' t Know Jack About Data Races original ↗

1 Jan 2023

Training a Custom Model for Lean4 original ↗

1 Jan 2023

Stratified Synthetsis original ↗

1 Jan 2023

Mutual Recursion Elaboration in Lean original ↗

1 Jan 2023

Subject Reduction in Lean original ↗

1 Jan 2023

GNU Binutils original ↗

1 Jan 2023

2022

Stuff I Learnt in 2022 original ↗

24 Nov 2022

Axiom K Versus UIP original ↗

24 Nov 2022

Linear vs Uniqueness Types original ↗

24 Nov 2022

Tmux original ↗

24 Nov 2022

Any Model of Lean Must Have All Inductives original ↗

2 Nov 2022

Index over the Past, Fiber over the Future original ↗

2 Nov 2022

Type Formers Need Not Be Injective original ↗

2 Nov 2022

The Dependently Typed Expression Problem original ↗

2 Nov 2022

Motivation for Modal Logic original ↗

27 Oct 2022

Scones original ↗

27 Oct 2022

Presheaf Models of Type Theory original ↗

27 Oct 2022

Weighted Limits via Collages original ↗

27 Oct 2022

Disjoint Coproduct original ↗

27 Oct 2022

Leibniz Equality in Lean4 original ↗

27 Oct 2022

Strong Normalization of STLC original ↗

27 Oct 2022

Subobject Classifiers of N \to FinSet, or Precosheaf Of FinSet original ↗

27 Oct 2022

Dimensions Versus Units original ↗

27 Oct 2022

HoTTesT: Identity Types original ↗

27 Oct 2022

TLDP Pages for Bash Conditionals original ↗

13 Oct 2022

Remainder, Modulo original ↗

13 Oct 2022

Parameters Cannot Be Changed anywhere , Not Just in Return Location original ↗

13 Oct 2022

LCNF original ↗

13 Oct 2022

Predicative v/s Impredicative: On Universes in Type Theory original ↗

13 Oct 2022

Testing Infra in Lean4 original ↗

13 Oct 2022

Autocompletion in Lean4 original ↗

13 Oct 2022

Inductive Types original ↗

13 Oct 2022

Parameter Verus Index original ↗

13 Oct 2022

HNF Versus WHNF original ↗

13 Oct 2022

Left and Right Adjoints to Inverse Image original ↗

28 Sept 2022

Paredit via Adjoints original ↗

28 Sept 2022

Less than Versus Less than or Equals over Z original ↗

28 Sept 2022

Allegories and Categories original ↗

28 Sept 2022

Partial Function as Span original ↗

28 Sept 2022

Turing Degree original ↗

25 Sept 2022

Proof That There Is a TM Whose Halting Is Independent of ZFC original ↗

25 Sept 2022

Contradiction from Non-positive Occurence original ↗

19 Sept 2022

The Constructible Universe L original ↗

19 Sept 2022

Godel Completeness Theorem original ↗

19 Sept 2022

Uniform Proofs, Focused Proofs, Polarization, Logic Programming original ↗

19 Sept 2022

Breakdance original ↗

19 Sept 2022

Cardistry original ↗

19 Sept 2022

Don ' t Try original ↗

19 Sept 2022

Shuffle Dancing original ↗

19 Sept 2022

Why Cut Elimination?original ↗

7 Sept 2022

Forcing to Add a Function original ↗

7 Sept 2022

Diaconescu ' s Theorem original ↗

7 Sept 2022

Forcing Machinery original ↗

7 Sept 2022

Partial Evaluation, Chapter 3 original ↗

7 Sept 2022

Partial Evaluation, Chapter 1 original ↗

7 Sept 2022

Diagonal Lemma for Monotone Functions original ↗

7 Sept 2022

Cantor Schroder Bernstein via Fixpoint original ↗

7 Sept 2022

Maximal Ideals of Boolean Algebras Are Truth Values original ↗

7 Sept 2022

Resolution Algorithm for Propositional Logic original ↗

7 Sept 2022

Completeness for First Order Logic original ↗

7 Sept 2022

Compactness Theorem of First Order Logic original ↗

7 Sept 2022

First Order Logic: Semantics original ↗

7 Sept 2022

You Could Have Invented Sequents original ↗

22 Aug 2022

Fibrational Category Theory, Sec 1.1, Sec 1.2 original ↗

22 Aug 2022

Simple Type Theory via Fibrations original ↗

22 Aug 2022

Realisability Models original ↗

22 Aug 2022

Naming Left Closed, Right Open with Start/stop original ↗

22 Aug 2022

Nested vs Mutual Inductive Types:original ↗

22 Aug 2022

Embedding HOL in Lean original ↗

22 Aug 2022

Module System for Separate Compilation original ↗

22 Aug 2022

Second Order Arithmetic original ↗

22 Aug 2022

Lean4 Dev Meeting original ↗

22 Aug 2022

Categorical Model of Dependent Types original ↗

22 Aug 2022

Different Types of Arguments in Lean4:original ↗

27 Jul 2022

Lean Tactics original ↗

27 Jun 2022

Coends original ↗

26 Jun 2022

Natural Transformations as Ends original ↗

26 Jun 2022

Ends and Diagonals original ↗

26 Jun 2022

Parabolic Dynamics and Renormalization original ↗

26 Jun 2022

Quantifiers as Adjoints original ↗

26 Jun 2022