Thinking about the semantics of OCaml... Given type t = T of t you can define cyclic values like
val x : t = T
but you can also define a fixed point combinator in the usual way and then fix (fun x -> T x) is another inhabitant of t (that loops and never yields a value).
I thought OCaml had semantics in pointed sets and its data types were interpreted coinductively or something, but that can't be right since the terminal coalgebra for the identity endofunctor on pointed sets is the singleton... @jonmsterling what do you make of this?
=> More informations about this toot | View the thread
Has anyone ever used "without loss of generality" when constructing an inhabitant of something that is not a proposition?
=> More informations about this toot | View the thread
Wait, Kőnig's lemma is (classically) equivalent to Brouwer's fan theorem (Cantor space is compact)? That explains why you can prove it using Tychonoff's theorem!
(So many names...)
=> More informations about this toot | View the thread
What's the simplest model of MLTT that refutes propext? cc @AndrasKovacs
=> More informations about this toot | View the thread
Hayao Miyazaki after being shown some AI animation: “I strongly feel that this is an insult to life itself”
https://www.youtube.com/watch?v=ngZ0K3lWKRc
=> More informations about this toot | View the thread
Is there a simple enough condition on a category C for PSh(C) to have split supports (every subterminal object is projective), assuming choice in the metatheory? I think it's enough to ask for the terminal object to be projective, so the question is the same as "which shapes of diagrams have all limits in the category of nonempty sets"?
=> More informations about this toot | View the thread
Could someone who actually knows topos theory check my answer here?
=> More informations about this toot | View the thread
cute game https://nozomu57.itch.io/clockwork-island
=> More informations about this toot | View the thread
@jcreed I mentioned your blog here.
=> More informations about this toot | View the thread
snow :)
=> More informations about this toot | View the thread
=> More informations about this toot | View the thread
This is the funniest pair of posts I have ever seen on Reddit: https://old.reddit.com/r/bicycling/comments/l5k40/i_have_a_bib_problempuzzle/
=> More informations about this toot | View the thread
Damn it, how does inline math work on this instance again?
=> More informations about this toot | View the thread
@trebor can I interest you in a Haskell question? As I understand it, the problem is to solve the word problem for free groups using their universal property.
=> More informations about this toot | View the thread
I answered a question on CS.SE about the "other" dependent generalisations of sum types and function types.
=> More informations about this toot | View the thread
Theorem 3.9.7
Corollary 4.2.1
Awooooo 5.6.7.0.9
=> More informations about this toot | View the thread
("Original" animation by Alex Bombelli.)
=> More informations about this toot | View the thread
=> More informations about this toot | View the thread
How do we stop teaching to people that ∀ implies ∃, or that anything exists, or that ∃ x. ⊤ is a theorem of "classical first-order logic"? Should we stop teaching LK/LJ sequent calculus? Are there any textbooks on first-order logic that use type theoretic syntax? @jonmsterling do you have any thoughts on this?
=> More informations about this toot | View the thread
PHILIPPICAE IN STUDENTES LITTERARUM (PRIMA, SECUNDA, TERTIA, QUARTA, QUINTA)
=> More informations about this toot | View the thread
=> This profile with reblog | Go to ncf@types.pl account This content has been proxied by September (3851b).Proxy Information
text/gemini