Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: type theory

Topic: how was Martin-Löf's 'Type in Type' theory supposed to work?

Oscar Cunningham (Apr 11 2021 at 08:19):

My understanding is that this is the 'most permissive pure type system' as described at https://ncatlab.org/nlab/show/pure+type+system#inconsistent_systems. I realise that this was proved inconsistent by Girard. But before that it was intended to function a foundation for mathematics. My question is how would that have worked?

Dependent product types are given to us by the deduction rules. But how can we use these to define other types? Can we define dependent sum types purely in terms of products? How would we get the natural numbers, booleans, etc?

James Wood (Apr 11 2021 at 08:55):

We don't know about the 1971 paper, but in his 1975 paper there is separate provision for Π, Σ, and ℕ in the rules of the system. I've always assumed that the 1971 system is similar.

Kenji Maillard (Apr 11 2021 at 08:58):

I guess you could use the same techniques as in System F, Church encodings: booleans would then be encoded by $\texttt{Bool} := \forall \alpha : \ast, \alpha \to \alpha \to \alpha$ with $\texttt{true} := \lambda (\alpha : \ast)(x~y : \alpha). x$, $\texttt{false} := \lambda (\alpha : \ast)(x~y : \alpha). y$ and $\texttt{indBool} := \lambda (P : \texttt{Bool} \to \ast)(p_t : P~\texttt{true})(p_f : P~\texttt{false})(b : \texttt{Bool}). b~(b~\ast~(P~\texttt{true})~(P~\texttt{false}))~p_t~p_f$ where I use that $\ast : \ast$ in the second application to $b : \texttt{Bool}$.
Edit: Not sure the eliminator returns the right type though (you would need $P~b \equiv b~\ast~(P~\texttt{true})~(P~\texttt{false})$)

James Wood (Apr 11 2021 at 09:06):

Though, with the intensional Martin-Löf identity type, equality of Church encoded types is going to be quite bad.

Oscar Cunningham (Apr 11 2021 at 09:46):

My guess had been that the relation between the 1971 and 1975 papers was analogous to the relation between Frege's set theory and ZF. For example with unrestricted comprehension you can easily prove that every set has a powerset. You just directly have the set whose elements are precisely the subsets of your original set. But in ZFC you have to explicitly put in an axiom to allow you to construct powersets.

I'd assumed that Martin-Löf's 1975 paper was similar. After weakening the type system to avoid Girard's paradox he then had to add in a bunch of constructors to get back what had been lost.

Kenji Maillard (Apr 11 2021 at 09:46):

@James Wood if you add primitive identity types, they won't fare well with church encoded datatypes.
But you can also (try to) church encode the identity types themselves, that seems to be the most straightforward solution from a PTS pov. Anyway, I'm not really sure what to expect from the resulting theory: it is logically inconsistent, and from a computational pov there isn't much to observe

Verity Scheel (Apr 11 2021 at 14:06):

The trick seems to be that you need some kind of parametricity or naturality to ensure that the functions encode only the constructors you expect.

Verity Scheel (Apr 11 2021 at 14:07):

(e.g. if you have LEM you can construct non-parametric functions)

Verity Scheel (Apr 11 2021 at 14:10):

@Mike Shulman wrote a post about adding coherence conditions to functions to obtain non-truncated coproducts, but he mentioned that it required a pre-existing type of natural numbers: https://homotopytypetheory.org/2018/11/26/impredicative-encodings-part-3/ (I don't know if there's been more progress here since then)

Verity Scheel (Apr 11 2021 at 14:12):

In general I'm optimistic that functions actually provide most of the structure needed for type theories, and inductive types are “merely” conveniences to obtain better computation rules and prevent universe explosions (especially without impredicativity), but it's far from obvious because of the risk of logical contradictions …

Verity Scheel (Apr 11 2021 at 14:13):

Funext becomes a much bigger issue, though …

Cody Roux (Apr 11 2021 at 16:48):

It's worth noting that people had been working with simple type theory and higher-order predicate logic for decades at this point. The inadequacy of the church encodings can be "fixed" by restricting to the well formed naturals, i.e. the ones obeying $\mathrm{Nat}(n) := \forall X, 0\in X \rightarrow (\forall x, x\in X \rightarrow S\ x\in X) \rightarrow n\in X$.

Then every statement about naturals needs to be relativized, e.g. $\forall n m : N, n+m = m+n$ becomes $\forall n m : N, \mathrm{Nat}(n)\rightarrow \mathrm{Nat}(m)\rightarrow n + m = m + n$.

Again, people had been doing things this way for a while.

Mike Shulman (Apr 11 2021 at 18:08):

Nick Scheel said:

Mike Shulman wrote a post about adding coherence conditions to functions to obtain non-truncated coproducts, but he mentioned that it required a pre-existing type of natural numbers

FWIW, instead of the natural numbers, I believe you can use coinductive types as long as they satisfy "coinductive extensionality" (equality is bisimulation). You also don't need the natural numbers if you have UIP; then the Awodey-Frey-Speight construction works directly. So you could restrict to the types that are h-sets and use that construction. Or you could use setoids.

Mike Shulman (Apr 11 2021 at 18:09):

Cody Roux said:

The inadequacy of the church encodings can be "fixed" by restricting to the well formed naturals

What's the meaning of "fixed" in quotes? Does the resulting type $\mathbb{N} \coloneqq \sum_{n:N} \mathrm{Nat}(n)$ satisfy the correct induction principle?

Verity Scheel (Apr 11 2021 at 19:55):

I think you need that $\mathrm{Nat}(n)$ is a subsingleton, which is not the case assuming $X : N \to \ast$. You could have $X : N \to \mathrm{Prop}$, but then you can only eliminate into mere propositions. So I suspect there needs to also be a condition on $\mathrm{Nat}(n)$ to say it is the canonical induction principle … maybe there's some nice trick like in the blog post, before we get an infinite tower of well-formednesses.

Cody Roux (Apr 12 2021 at 01:01):

Mike Shulman said:

Cody Roux said:

The inadequacy of the church encodings can be "fixed" by restricting to the well formed naturals

What's the meaning of "fixed" in quotes? Does the resulting type $\mathbb{N} \coloneqq \sum_{n:N} \mathrm{Nat}(n)$ satisfy the correct induction principle?

It does not, sadly (at least in the 2nd order predicate calculus). Indeed there is no type which satisfies the induction principle, so you have to add the extra qualification/relativization for each proposition about natural numbers.

It's also consistent to assume it as an axiom, of course, but that's pretty unsatisfying.

Mike Shulman (Apr 12 2021 at 09:50):

Thanks. It does seem plausible that that's what Martin-Lof originally had in mind, although nowadays we can imagine better ways to do things. (-:

Oscar Cunningham (Apr 05 2022 at 17:26):

James Wood said:

We don't know about the 1971 paper, but in his 1975 paper there is separate provision for Π, Σ, and ℕ in the rules of the system. I've always assumed that the 1971 system is similar.

The 1971 paper is now online here: https://raw.githubusercontent.com/michaelt/martin-lof/master/pdfs/martin-loef1971%20-%20A%20Theory%20of%20Types.pdf
And it turns out I was right! His original system uses only $\prod$ s. He defines $\sum$ via:

$\sum_{x:A}B(x) := \prod_{X:V}\left(\prod_{x:A}(B\to X)\right) \to X$