I've been trying to find a proof that the pullback functors in a locally cartesian closed category have right adjoints (used to model the notion of indexed product inside a category (rather than ...
I like to distinguish between sets and subsets. We imagine that sets are floating free in the universe, and that the elements of a set are constructed according to some kind of recursive rules. Like ...
What are some good online/free resources (tutorials, guides, exercises, and the like) for learning Lambda Calculus? Specifically, I am interested in the following areas: Untyped lambda calculus ...
I am becoming increasingly convinced that Wildberger's views are, if a little bizarre, at least not hopelessly inconsistent. When I was reading the comments in the video following (MF17), somebody ...
My question is which functions can not be allowed in a statically typed programming language, so that the "canonical" category is less coarse than what you get if you define it's arrows to be ...
I'm slowly grasping this, though the different formulations of type theory make it difficult. In http://imps.mcmaster.ca/doc/seven-virtues.pdf types can only be formed from *, i, and a->b when a and ...
The problem was encountered when learning Computability Notes by Roberto Zunino (link), page 9 and 11. It seems as if it is a well-known issue and I don't need to specify the "canonical" meaning of ...