Ask @ice1000 anything about higher inductive types. Currently he's studying it in-depth. He'll be interested in explaining things to you.
Category Theory for Programmers
https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/
https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/
Bartosz Milewski's Programming Cafe
Category Theory for Programmers: The Preface
Table of Contents Part One Category: The Essence of Composition Types and Functions Categories Great and Small Kleisli Categories Products and Coproducts Simple Algebraic Data Types Functors Functo…
Easy.pdf
187.6 KB
Simple Easy! An implementation of dependent type lambda calculus
Summary of Truth about Types, a talk by Bartosz Milewski
https://rakhim.org/summary-of-truth-about-types-a-talk-by-bartosz-milewski/
https://rakhim.org/summary-of-truth-about-types-a-talk-by-bartosz-milewski/
Graph Representations for Higher-Order Logic and Theorem Proving
https://arxiv.org/abs/1905.10006
https://arxiv.org/abs/1905.10006
Generative Language Modeling for Automated Theorem Proving
https://arxiv.org/pdf/2009.03393.pdf
https://arxiv.org/pdf/2009.03393.pdf
Towards Finding Longer Proofs
https://arxiv.org/pdf/1905.13100.pdf
https://arxiv.org/pdf/1905.13100.pdf
HoTT-I, the underlying type theory of Arend
https://arxiv.org/abs/2004.14195
https://arxiv.org/abs/2004.14195
An illustration of Hopf fibration
https://twitter.com/vi_ne_te/status/1302273506055516161
https://twitter.com/vi_ne_te/status/1302273506055516161
Twitter
Vignette
https://t.co/6XnX9C6xRr
Codependent types
https://twitter.com/shlevy/status/1302668614353539074
https://twitter.com/shlevy/status/1302668614353539074
Twitter
Shea Levy
@tizusa233 @cronokirby No full example I can convey in a tweet yet. One intuition: With a dependent function, the codomain varies based on elements of (i.e. functions into) the domain. With a codependent function, the domain varies based on destructors of…
Pure & constructive mathematics in theory and use
Codependent types https://twitter.com/shlevy/status/1302668614353539074
There's also cosigma types that we can explore
Kreisel's "Unwinding" Program
https://math.stanford.edu/~feferman/papers/unwind.pdf
https://math.stanford.edu/~feferman/papers/unwind.pdf
Intutionistic Sets and Ordinals
http://www.paultaylor.eu/ordinals/intso.pdf
http://www.paultaylor.eu/ordinals/intso.pdf
Practical Foundations of Mathematics
http://www.paultaylor.eu/prafm/
http://www.paultaylor.eu/prafm/
Relating first-order set theories, toposes and categories of classes
http://www.phil.cmu.edu/projects/ast/Papers/Awodey-Butz-Simpson-Streicher-APAL-2013.pdf
http://www.phil.cmu.edu/projects/ast/Papers/Awodey-Butz-Simpson-Streicher-APAL-2013.pdf
Infinite Time Turing Machines
https://arxiv.org/pdf/math/9808093.pdf
https://arxiv.org/pdf/math/9808093.pdf
An introduction to locally finitely presentable categories
https://pi.math.cornell.edu/~maru/documents/locally_finitely_presentable_cats.pdf
https://pi.math.cornell.edu/~maru/documents/locally_finitely_presentable_cats.pdf
1460059215690.pdf
3.7 MB
Conceptual Mathematics
A new pass at the NF consistency proof
https://randall-holmes.github.io/Nfproof/newattempt.pdf
https://randall-holmes.github.io/Nfproof/newattempt.pdf