Structural Rules and Inductive Types
90 views
Skip to first unread message
Brandon Harrington
Feb 17, 2019, 3:46:07 PM2/17/19
to HoTT Cafe
Hi everyone! I'm on here because I have been working through the HoTT book for a couple years. I have come across something about formal inductive types that I am not certain about. Looking at the appendix for the formal presentation, inductive types are introduced as rules in the theory. My questions are thus:
- Shouldn't this mean that type theories with different inductive types are different since there are different rules in each?
- Is there some finite collection of formal rules that allows for the introduction of all inductive types into the theory?
- W-Types capture recursion principles, but is there an internal family of types similar to the W-Types that encapsulates all inductive types? (For example, how would one generally represent sum types and product types internally?)
Michael Shulman
Feb 19, 2019, 7:46:05 PM2/19/19
to Brandon Harrington, HoTT Cafe
Yes, type theories with rules for different collections of inductive
types are technically different type theories. It is a theorem that
all inductive types are "reducible" to W-types along with sums and
products, but I don't remember the precise statement. It is possible
to formulate precisely what it means for a type theory to have "all
inductive types", although this is not really a *finite* collection of
rules unless you do something fancy like internalizing the inductive
specification of an inductive type. (And there are multiple different
meanings of "all inductive types" too, e.g. you could include or not
inductive-inductive types or indexed inductive types, and for higher
inductive types giving such a specification is a current research
question (though some proposed solutions exist I believe).)
Unfortunately I don't have time to track down all the references right
now, but maybe someone else has them closer to hand or memory.
> --
> You received this message because you are subscribed to the Google Groups "HoTT Cafe" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to hott-cafe+...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
types are technically different type theories. It is a theorem that
all inductive types are "reducible" to W-types along with sums and
products, but I don't remember the precise statement. It is possible
to formulate precisely what it means for a type theory to have "all
inductive types", although this is not really a *finite* collection of
rules unless you do something fancy like internalizing the inductive
specification of an inductive type. (And there are multiple different
meanings of "all inductive types" too, e.g. you could include or not
inductive-inductive types or indexed inductive types, and for higher
inductive types giving such a specification is a current research
question (though some proposed solutions exist I believe).)
Unfortunately I don't have time to track down all the references right
now, but maybe someone else has them closer to hand or memory.
> You received this message because you are subscribed to the Google Groups "HoTT Cafe" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to hott-cafe+...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
Hendrik Boom
Feb 19, 2019, 8:04:59 PM2/19/19
to Michael Shulman, Brandon Harrington, HoTT Cafe
On Tue, Feb 19, 2019 at 04:45:52PM -0800, Michael Shulman wrote:
> Yes, type theories with rules for different collections of inductive
> types are technically different type theories. It is a theorem that
> all inductive types are "reducible" to W-types along with sums and
> products, but I don't remember the precise statement. It is possible
> to formulate precisely what it means for a type theory to have "all
> inductive types", although this is not really a *finite* collection of
> rules unless you do something fancy like internalizing the inductive
> specification of an inductive type. (And there are multiple different
> meanings of "all inductive types" too, e.g. you could include or not
> inductive-inductive types or indexed inductive types, and for higher
> inductive types giving such a specification is a current research
> question (though some proposed solutions exist I believe).)
The question of "all inductive types" would seem to be equivalent to
> Yes, type theories with rules for different collections of inductive
> types are technically different type theories. It is a theorem that
> all inductive types are "reducible" to W-types along with sums and
> products, but I don't remember the precise statement. It is possible
> to formulate precisely what it means for a type theory to have "all
> inductive types", although this is not really a *finite* collection of
> rules unless you do something fancy like internalizing the inductive
> specification of an inductive type. (And there are multiple different
> meanings of "all inductive types" too, e.g. you could include or not
> inductive-inductive types or indexed inductive types, and for higher
> inductive types giving such a specification is a current research
> question (though some proposed solutions exist I believe).)
the question of "all ordinals", which verges on paradox.
-- hendrik
Michael Shulman
Feb 19, 2019, 8:55:34 PM2/19/19
to Hendrik Boom, Brandon Harrington, HoTT Cafe
Well, there's nothing paradoxical about the statement that all
ordinals exist. (-: But it's true that stronger meanings of "all
inductive types" do correspond in some sense to stronger principles of
well-founded induction in set theory, e.g. some versions of
induction-recursion correspond in some way to Mahlo cardinals.
ordinals exist. (-: But it's true that stronger meanings of "all
inductive types" do correspond in some sense to stronger principles of
well-founded induction in set theory, e.g. some versions of
induction-recursion correspond in some way to Mahlo cardinals.
Peter Hancock
Feb 20, 2019, 6:32:09 AM2/20/19
to HoTT Cafe
On Wednesday, 20 February 2019 01:55:34 UTC, Michael Shulman wrote:
Well, there's nothing paradoxical about the statement that all
ordinals exist. (-: But it's true that stronger meanings of "all
inductive types" do correspond in some sense to stronger principles of
well-founded induction in set theory, e.g. some versions of
induction-recursion correspond in some way to Mahlo cardinals.
The situation with "inductive types" (typified by "W-types", and their indexed
variant, the Petersson-Synek general tree types) is complicated in the
presence of universes. A universe gives you a "carrier" in which to
iterate W-types. (The PS trees are no "stronger" than the W-types.)
The "W" construction corresponds to the step to the next regular.
Without a universe, one can say, very roughly, that
inductive definitions correspond to the first singular uncountable cardinal
aleph_\omega.
With one universe, the corresponding thing is an inaccessible cardinal.
In some respects, having a universe is a little like having the replacement
axiom in set-theory. You can then iterate the power-set operator.
(Otherwise you just get to V_{\omega.2}, as in Zermelo set-theory.)
an (externally indexed) omega-hierarchy of higher-order universe operators.
As you say, the corresponding thing here is a Mahlo cardinal.
(Anton Setzer has worked extensively on such things.)
As far as I know, proof-theorists would be very surprised if the
new-fangled variants of induction coming from HTT contributed
proof-theoretic strength. Of course they may bring great expressive
power.
Michael Shulman
Feb 20, 2019, 6:44:28 AM2/20/19
to Peter Hancock, HoTT Cafe
Thanks for explaining that! Can you say a bit more about in what
sense W corresponds to "the next regular"? In particular, I was under
the impression that type theory (with LEM, say, but not AC, in the
propositionally-truncated senses of the HoTT book, and without
univalence for simplicity) could not prove that any uncountable
regular cardinals exist, because it should have models in ZF set
theory, and ZF doesn't prove that any uncountable regular cardinals
exist (at least, assuming the consistency of some large cardinal
hypotheses). This is one way in which higher inductive types are
known to increase expressivity at least, because they can prove that
uncountable regular cardinals exist (see section 9 of
https://arxiv.org/abs/1705.07088).
sense W corresponds to "the next regular"? In particular, I was under
the impression that type theory (with LEM, say, but not AC, in the
propositionally-truncated senses of the HoTT book, and without
univalence for simplicity) could not prove that any uncountable
regular cardinals exist, because it should have models in ZF set
theory, and ZF doesn't prove that any uncountable regular cardinals
exist (at least, assuming the consistency of some large cardinal
hypotheses). This is one way in which higher inductive types are
known to increase expressivity at least, because they can prove that
uncountable regular cardinals exist (see section 9 of
https://arxiv.org/abs/1705.07088).
Peter Hancock
Feb 20, 2019, 8:09:47 AM2/20/19
to HoTT Cafe
On 20/02/2019 11:44, Michael Shulman wrote:
> Thanks for explaining that! Can you say a bit more about in what
> sense W corresponds to "the next regular"? In particular, I was under> the impression that type theory (with LEM, say, but not AC, in the
> propositionally-truncated senses of the HoTT book, and without
> univalence for simplicity) could not prove that any uncountable
> regular cardinals exist, because it should have models in ZF set
> theory, and ZF doesn't prove that any uncountable regular cardinals
> exist (at least, assuming the consistency of some large cardinal
> hypotheses). This is one way in which higher inductive types are
> known to increase expressivity at least, because they can prove that
> uncountable regular cardinals exist (see section 9 of
> https://arxiv.org/abs/1705.07088).
On 20/02/2019 11:44, Michael Shulman wrote:
> Thanks for explaining that! Can you say a bit more about in what
> sense W corresponds to "the next regular"? In particular, I was under
> the impression that type theory (with LEM, say, but not AC, in the
> propositionally-truncated senses of the HoTT book, and without
> univalence for simplicity) could not prove that any uncountable
> regular cardinals exist, because it should have models in ZF set
> theory, and ZF doesn't prove that any uncountable regular cardinals
> exist (at least, assuming the consistency of some large cardinal
> hypotheses). This is one way in which higher inductive types are
> known to increase expressivity at least, because they can prove that
> uncountable regular cardinals exist (see section 9 of
> https://arxiv.org/abs/1705.07088).
> Thanks for explaining that! Can you say a bit more about in what
> sense W corresponds to "the next regular"? In particular, I was under
> the impression that type theory (with LEM, say, but not AC, in the
> propositionally-truncated senses of the HoTT book, and without
> univalence for simplicity) could not prove that any uncountable
> regular cardinals exist, because it should have models in ZF set
> theory, and ZF doesn't prove that any uncountable regular cardinals
> exist (at least, assuming the consistency of some large cardinal
> hypotheses). This is one way in which higher inductive types are
> known to increase expressivity at least, because they can prove that
> uncountable regular cardinals exist (see section 9 of
> https://arxiv.org/abs/1705.07088).
Well, I'll have a look at the arxiv paper, but I'm a bit puzzled that
you say ZF doesn't prove uncountable regulars exist!
The first one is aleph_1, or perhaps I should say beth_1, or rather
I should say ZF + GCH. Sorry for any such sloppiness. (I'm not a set-theorist...)
Or could I just define a cardinal to be an ordinal not 1-1 with any smaller ordinal?
(Another sloppiness I am prone to is saying, eg, "inaccessible" when I
should say "weakly inaccessible".)
As for "W" encoding "the step to the next regular", let's suppose that
the family { B a | a : A } consists of all the regulars we have defined
so far. Then the tree's inhabiting W A B are closed under all suprema
of sequences indexed by any (B a). So W A B is "regular" and above B a,
and the least such. Form now {B' a' | a' : A + 1} by adjoining W A B to B.
If our starting family was { 0, 1, Nat } , we are now stepping through
the regular cardinals/ordinals w_1, w_2, w_3, ... .
To iterate the process, we have to internalise it in type-theory, and for that
we need some kind of universe, to do the iteration "in". (But in fact, the
most elegant was to proceed is to use induction-recursion directly.)
I suppose I should say more precisely how I am thinking about regularity,
or at least indicate how I deal with ordinals in type-theory.
In set theory (possibly without the foundation axiom), one can define an
ordinal to be a well founded transitive set, all of whose elements are
transitive.
In type-theory, we can emulate such a structure using a type A, and
a function pd : A -> Fam A, where Fam A is (Sigma B : Set) B -> A.
(That's large, but one can replace "Set" by some suitable universe, if it matters.)
Think of the inhabitants of A as ordinal notations, and pd as assigning
to a notation the family of it's immediate predecessors.
We can pass to the transitive closure of such a structure. (This can be done in many ways.)
Then we can define an *accessible* element of A, by an inductive definition.
Finally we can say that the structure is an ordinal if all elements are accessible.
We define equality on A essentially as bisimulation. (More or less as
Peter Aczel did in his paper on modelling CZF in type-theory. Formal coinduction
is unnecessary, provided everything is well-founded.)
We can then define a : A to be regular, with a little handwaving, as follows:
for all b < a, and f : b -> a,
exists c < a, s.t. f : b -> c
With less handwaving, that means
(Pi t : B a)(Pi f : B (pd a t) -> B a)
(Sigma t' : B a)(Sigma g : B (pd a t) -> B (pd a t'))
(Pi b : B (pd a t)) f b = pd (pd a t') (g b)
No doubt there are some errors there, but I hope it gives an idea of
how the "pseudo-set-theory" might be translated into "machine-code".
Other definitions are possible, that may be easier to work with.
I apologise for the length of this, and that it is still rather sloppy;
quite some work is necessary to make everything plain and above-board.
you say ZF doesn't prove uncountable regulars exist!
The first one is aleph_1, or perhaps I should say beth_1, or rather
I should say ZF + GCH. Sorry for any such sloppiness. (I'm not a set-theorist...)
Or could I just define a cardinal to be an ordinal not 1-1 with any smaller ordinal?
(Another sloppiness I am prone to is saying, eg, "inaccessible" when I
should say "weakly inaccessible".)
As for "W" encoding "the step to the next regular", let's suppose that
the family { B a | a : A } consists of all the regulars we have defined
so far. Then the tree's inhabiting W A B are closed under all suprema
of sequences indexed by any (B a). So W A B is "regular" and above B a,
and the least such. Form now {B' a' | a' : A + 1} by adjoining W A B to B.
If our starting family was { 0, 1, Nat } , we are now stepping through
the regular cardinals/ordinals w_1, w_2, w_3, ... .
To iterate the process, we have to internalise it in type-theory, and for that
we need some kind of universe, to do the iteration "in". (But in fact, the
most elegant was to proceed is to use induction-recursion directly.)
I suppose I should say more precisely how I am thinking about regularity,
or at least indicate how I deal with ordinals in type-theory.
In set theory (possibly without the foundation axiom), one can define an
ordinal to be a well founded transitive set, all of whose elements are
transitive.
In type-theory, we can emulate such a structure using a type A, and
a function pd : A -> Fam A, where Fam A is (Sigma B : Set) B -> A.
(That's large, but one can replace "Set" by some suitable universe, if it matters.)
Think of the inhabitants of A as ordinal notations, and pd as assigning
to a notation the family of it's immediate predecessors.
We can pass to the transitive closure of such a structure. (This can be done in many ways.)
Then we can define an *accessible* element of A, by an inductive definition.
Finally we can say that the structure is an ordinal if all elements are accessible.
We define equality on A essentially as bisimulation. (More or less as
Peter Aczel did in his paper on modelling CZF in type-theory. Formal coinduction
is unnecessary, provided everything is well-founded.)
We can then define a : A to be regular, with a little handwaving, as follows:
for all b < a, and f : b -> a,
exists c < a, s.t. f : b -> c
With less handwaving, that means
(Pi t : B a)(Pi f : B (pd a t) -> B a)
(Sigma t' : B a)(Sigma g : B (pd a t) -> B (pd a t'))
(Pi b : B (pd a t)) f b = pd (pd a t') (g b)
No doubt there are some errors there, but I hope it gives an idea of
how the "pseudo-set-theory" might be translated into "machine-code".
Other definitions are possible, that may be easier to work with.
I apologise for the length of this, and that it is still rather sloppy;
quite some work is necessary to make everything plain and above-board.
Michael Shulman
Feb 20, 2019, 8:12:42 AM2/20/19
to Peter Hancock, Peter Hancock, HoTT Cafe
On Wed, Feb 20, 2019 at 4:59 AM Peter Hancock <postm...@hbb98.plus.com> wrote:
> Well, I'll have a look at the arxiv paper, but I'm a bit puzzled that
> you say ZF doesn't prove uncountable regulars exist!
> The first one is aleph_1, or perhaps I should say beth_1, or rather
> I should say ZF + GCH. Sorry for any such sloppiness. (I'm not a set-theorist...)
The statement that aleph_1 is regular is the statement that a
> Well, I'll have a look at the arxiv paper, but I'm a bit puzzled that
> you say ZF doesn't prove uncountable regulars exist!
> The first one is aleph_1, or perhaps I should say beth_1, or rather
> I should say ZF + GCH. Sorry for any such sloppiness. (I'm not a set-theorist...)
countable union of countable sets is countable, which is unprovable in
ZF. The standard proof uses countable choice (though the statement
itself is, I believe, weaker than full countable choice).
More generally, in "All uncountable cardinals can be singular" (Israel
J. Math. (1980) 35: 61), Gitik constructed a model of ZF in which
aleph_0 is the only infinite regular cardinal, under the assumption
that ZFC is consistent with the existence of arbitrarily large
strongly compact cardinals.
Of course a countable *disjoint* union of countable sets is always
countable. That seems to be the notion of "regularity" that you're
capturing with W, but it's not the set-theoretic one.
> Or could I just define a cardinal to be an ordinal not 1-1 with any smaller ordinal?
>
> (Another sloppiness I am prone to is saying, eg, "inaccessible" when I
> should say "weakly inaccessible".)
>
> As for "W" encoding "the step to the next regular", let's suppose that
> the family { B a | a : A } consists of all the regulars we have defined
> so far. Then the tree's inhabiting W A B are closed under all suprema
> of sequences indexed by any (B a). So W A B is "regular" and above B a,
> and the least such. Form now {B' a' | a' : A + 1} by adjoining W A B to B.
> If our starting family was { 0, 1, Nat } , we are now stepping through
Andrej Bauer
Feb 20, 2019, 4:14:21 PM2/20/19
to Michael Shulman, HoTT Cafe
> Of course a countable *disjoint* union of countable sets is always
> countable.
Always? If every countable disjoint union of countable sets is
> countable.
countable, then every countable union of countable sets is countable,
since such unions are images of disjoint unions, yes?
With kind regards,
Andrej
Michael Shulman
Feb 20, 2019, 6:59:42 PM2/20/19
to Andrej Bauer, HoTT Cafe
Sorry, maybe I was mixing up "countable" and "denumerable"? And/or
conflating mere existence of bijections with distinguished structure
of bijections? There are a bunch of intricacies in definitions here
to sort out in the absence of choice. But the main point is that
whatever kind of "regular cardinal" you get by applying W to the
natural numbers, it's not "regular" in the same sense as the
set-theoretic aleph_1.
conflating mere existence of bijections with distinguished structure
of bijections? There are a bunch of intricacies in definitions here
to sort out in the absence of choice. But the main point is that
whatever kind of "regular cardinal" you get by applying W to the
natural numbers, it's not "regular" in the same sense as the
set-theoretic aleph_1.
Hendrik Boom
Feb 21, 2019, 7:11:06 AM2/21/19
to Michael Shulman, Andrej Bauer, HoTT Cafe
On Wed, Feb 20, 2019 at 03:59:29PM -0800, Michael Shulman wrote:
> Sorry, maybe I was mixing up "countable" and "denumerable"? And/or
And there's also subcountable.
> Sorry, maybe I was mixing up "countable" and "denumerable"? And/or
What are these subte distinction? Is one an image of a countable set
and the other something that's injected into a countable set? And
which is which?
Hendrik Boom
Feb 21, 2019, 7:15:12 AM2/21/19
to Michael Shulman, Andrej Bauer, HoTT Cafe
When I tried to use list-reply to this message, my mailer reported "No
mailing lists found."
Now ages ago I thought this was just a problem with Google Groups,
but I've discovered that other Google Groups do have their mailing list
headers set, and don't have this problem.
But there are mailing list headers on the message I was trying to
reply-to-list to. And to a casual look, they seem OK.
So something seems to be very subtly wrong with the way this list is
set up.
-- hendrik
On Wed, Feb 20, 2019 at 03:59:29PM -0800, Michael Shulman wrote:
mailing lists found."
Now ages ago I thought this was just a problem with Google Groups,
but I've discovered that other Google Groups do have their mailing list
headers set, and don't have this problem.
But there are mailing list headers on the message I was trying to
reply-to-list to. And to a casual look, they seem OK.
So something seems to be very subtly wrong with the way this list is
set up.
-- hendrik
On Wed, Feb 20, 2019 at 03:59:29PM -0800, Michael Shulman wrote:
Hendrik Boom
Feb 21, 2019, 7:33:47 AM2/21/19
to Michael Shulman, Andrej Bauer, HoTT Cafe
And I forgot to change the subject line on the previous message.
Michael Shulman
Feb 21, 2019, 8:56:06 AM2/21/19
to Hendrik Boom, Andrej Bauer, HoTT Cafe
Maybe you can just use ordinary reply.
Michael Shulman
Feb 21, 2019, 9:00:49 AM2/21/19
to Hendrik Boom, Andrej Bauer, HoTT Cafe
I am not sure that the terminology is uniform across all authors, in
fact I am pretty sure it's not.
fact I am pretty sure it's not.
Reply all
Reply to author
Forward
0 new messages