I started an article about [[Martin-Lof+dependent+type+theory|Martin-Löf dependent type theory]]. I hope there aren't any major mistakes!

One minor point: I overloaded $\mathrm{cases}$ by using it for both finite sum types and dependent sum types. Can anyone think of a better name for the operation for finite sum types?

]]>As explained in the well-order article, any well-order (i.e. extensional, transitive well-founded relation) is a linear order in classical mathematics. The proof given is rather complicated. Happily, within constructive mathematics, there’s a stronger result with a simple proof, as I’ll explain.

Given an irreflexive, transitive relation $\prec$ on a set $X$, say that elements $a, b \in X$ are *trichotomously related* when either $a \prec b$ or $a=b$ or $b \prec a$. (Clearly no more than one of these can be true.) Say that $\prec$ is *trichotomous* when any $a,b \in X$ are trichotomously related.

Theorem: a transitive well-founded relation $\prec$ on a set $X$ is trichotomous iff it is both extensional and decidable.

Proof: ($\Rightarrow$) is trivial. For ($\Leftarrow$), we claim that, for any $a,b \in X$, if $a$ is trichotomously related with every $y \prec b$, and every $x \prec a$ with $b$, then $a$ and $b$ are trichotomously related. Therefore any $a,b \in X$ are trichotomously related, by induction.

The claim is proved as follows. Decidability of the propositions $a \prec b$ and $b \prec a$ gives either $a \prec b$ or $b \prec a$ or both $a \nprec b$ and $b \nprec a$. In the last case, $x \prec a$ implies $x \prec b$, since $x$ is trichotomously related with $b$ but $x \neq b$ and $b \nprec x$, and likewise $y \prec b$ implies $y \prec a$, so extensionality gives $a=b$. Thus $a$ and $b$ are trichotomously related.

Martín Escardó has pointed out to me that this proof lies within intensional Martin-Löf dependent type theory.

]]>This is basically a reference request: It was recently pointed out to me that the construction and correctness of the sheafification functor (in the context of 1-topos theory) depends on either the axiom of choice (using Grothendieck’s ++-construction or variations thereof) or impredicativity (using Lawvere’s construction).

Do any of you know a place where sheafification is discussed relative to a constructive, predicative metatheory without any choice?

I’m aware of Moerdijk and Palmgren’s: Type theories, toposes and constructive set theory: predicative aspects of AST. There sheafification is constructed for “collection sites”, but I don’t think there are many infinitary collection sites without assuming AMC. Maybe I’m wrong?

For coherent sites, there’s no problem, as only finite choice is needed. I’m interested primarily in the case of sites with countable covers.

A big hammer (if we have it?) might be to say that in the internal logic of the presheaf topos, sheafification is a localization and could presumably be done with an internal localization HIT (which we have if we have inductive types in the meta-theory?) Or perhaps there’s directly a fancy HIT in the metatheory that builds sheafification?

]]>At this old blog post, I found the following statement:

This sentence is false and it has a well-defined truth-value.

In the comments, we find this statement

$\neg\square P \wedge (\square P \vee \square\neg P).$

where $\square P$ is ’$P$ is provable in PA’ (insert other system here if desired).

Clearly the first version is not the same as the second, constructively (aside from other issues like translating ’has a well-defined truth value). The author (Michael O’Connor) goes on to say:

It occurred to me that the fact that $\neg\square P \wedge (\square P \vee \square\neg P)$ is a sentence whose decidability is undecidable in PA is actually not at all remarkable: every sentence which is undecidable in PA is such that its decidability is undecidable in PA, since for PA to prove a sentence is undecidable in PA, it would have to prove that it can’t prove something, which is equivalent to it proving its consistency. So I will have to work a little harder to find a provability model of this.

However, what can we say if we drop LEM?

]]>The following interesting question(s) have been raised by Martin Escardó on the Agda mailing list and the constructive-news list.

Is there a constructive proof that there is no injection $\mathbb{N}^\mathbb{N} \to \mathbb{N}$?

Is there a constructive proof that given any function $H\colon \mathbb{N}^\mathbb{N} \to \mathbb{N}$, there exist functions $f,g\colon \mathbb{N}\to\mathbb{N}$ and $k\in \mathbb{N}$ such that $H(f)=H(g)$ but $f(k)\neq g(k)$?

Both are obviously true assuming classical logic, and the latter can apparently also be proven if one assumes “continuity principles”. As far as counterexamples go, in the effective topos, $\mathbb{N}^\mathbb{N}$ is a sub*quotient* of $\mathbb{N}$, but not a subobject of it. In D4.1.9 of the Elephant there is a Grothendieck topos in which $\mathbb{N}^\mathbb{N}$ is a subquotient of $\mathbb{N}$, namely the classifying topos of the theory of a partial surjection from $\mathbb{N}$ to $\mathbb{N}^\mathbb{N}$ – but afterwards he explains why that approach wouldn’t work for an injection $\mathbb{N}^\mathbb{N} \to \mathbb{N}$, and how one *can* prove constructively that there is no surjection $\mathbb{N}\to \mathbb{N}^\mathbb{N}$.

It seems like surely the answer to (1), at least, should be known… but I don’t know it.

]]>Should the predicate $\Diamond$ on a formal topology be regarded as making it into an overt space?

]]>