Articles of type theory

The sections of the projection $\bigsqcup_{i:I} X_i \rightarrow I.$

I just noticed something funky. Let $X$ denote an $I$-indexed family of sets. There is a projection $$\pi_X: \bigsqcup_{i:I} X_i \rightarrow I.$$ It isn’t necessarily surjective, of course, because one or more of the $X_i$ may be empty. Anyway, I noticed that the set $\prod_{i:I} X_i$ can be identified with the set of sections of […]

Turning ZFC into a free typed algebra

The standard way of using ZFC to encode the rest of mathematics is sometimes criticized because it introduces unnecessary, strange properties such as, for example $1\in 2$ if we encode integers by ordinals. From a constructivist type theorist’s perspective, uples or functions or complex numbers should have nothing to do with the membership relation, we […]

Is there a fundamental distinction between objects and its types?

My question is related to the formal presentation of type theory as stated in the context of Homotopy Type Theory. Every formalization is grounded on typing judgements like $$ a: A $$ where mostly it is said that $a$ is an object that can be built due to several formation or term-forming rules and $A$ […]

Learning Lambda Calculus

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 Simply-typed lambda calculus Other typed lambda calculi Church’s Theory of Types (I’m not sure where this fits in). (As I understand, this should provide a solid basis for […]

Constructing a HoTT proof term of 1≠0

As an exercise in HoTT basics, I am trying to construct a term that has the type $Id_{Nat}(S(O),O)\to\bot$. If this were a Coq proof, I’d be done after a single inversion on the premise, as the impossible identity would leave zero cases to consider. I guess I could do something similar here, but I’m not […]

Is there a (foundational) type theory with the features I'm looking for?

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 the elements of $\mathbb{N}$ can be constructed using the rules: $$\frac{}{0 \in \mathbb{N}} \;\; \frac{n \in \mathbb{N}}{n+1 \in \mathbb{N}}$$ On […]

Does $A\times A\cong B\times B$ imply $A\cong B$?

This is similar to What does it take to divide by $2$? about $(A\sqcup A\cong B\sqcup B)\Rightarrow A\cong B$ which is valid in $\textsf{ZFC}$ by using cardinalities and also in $\textsf{ZF}$ by some combinatorial argument, but where it remained unclear whether constructive arguments suffice. This questions concerns products instead of disjoint union, so: Question: Does […]

Confusion about Homotopy Type Theory terminology

I’ve picked up the Homotopy Type Theory book for leisure. I’m comfortable with strongly typed languages and familiar with dependently typed languages and I enjoy topology, so I thought that the HoTT book was a good opportunity to learn some of the math underlying the type systems (and, by HoTT’s reputation, a new way of […]

Constructing dependent product (right adjoint to pullback) in a locally cartesian closed category

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 indexed by a set), or, equivalently, dependent products in models of dependent type theories). I found a proof in Awodey’s book, but […]

What good is infinity?

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 said something that shocked me a bit, because I was unable to give a rebuttal that I found satisfactory: The reason I consider [the axiom […]