General scheme for inductive types about book

[mikeshulman]

The definition of accessibility in section 9.8 is an inductive family.

[txa]

Yes, but it is of a simple form in that the signature functor doesn't need to refer to equality.

Peter Hancock calls these families protestant while the others are catholic (because they are based on the belief in transsubstantiation :-)

From: Mike Shulman <[email protected]mailto:[email protected]>
Reply-To: HoTT/book <[email protected]mailto:[email protected]>
To: HoTT/book <[email protected]mailto:[email protected]>
Cc: Thorsten Altenkirch <[email protected]mailto:[email protected]>
Subject: Re: [book] General scheme for inductive types (#34)

The definition of accessibility in section 9.8 is an inductive family.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/34#issuecomment-15527500.

This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment

may still contain software viruses which could damage your computer system:

you are advised to perform your own checks. Email communications with the

University of Nottingham may be monitored as permitted by UK legislation.

[mikeshulman]

What you just said is incomprehensible to me. (-:

On Wed, Mar 27, 2013 at 2:54 PM, Thorsten Altenkirch <
[email protected]> wrote:

Yes, but it is of a simple form in that the signature functor doesn't need
to refer to equality.

Peter Hancock calls these families protestant while the others are
catholic (because they are based on the belief in transsubstantiation :-)

From: Mike Shulman <[email protected]<mailto:
[email protected]>>
Reply-To: HoTT/book <[email protected]mailto:[email protected]>

To: HoTT/book <[email protected]mailto:[email protected]>
Cc: Thorsten Altenkirch <[email protected]mailto:[email protected]>
Subject: Re: [book] General scheme for inductive types (#34)

The definition of accessibility in section 9.8 is an inductive family.

—
Reply to this email directly or view it on GitHub<
https://github.com/HoTT/book/issues/34#issuecomment-15527500>.

This message and any attachment are intended solely for the addressee and
may contain confidential information. If you have received this message in
error, please send it back to me, and immediately delete it. Please do not
use, copy or disclose the information contained in this message or in any
attachment. Any views or opinions expressed by the author of this email do
not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an
attachment

may still contain software viruses which could damage your computer
system:

you are advised to perform your own checks. Email communications with the

University of Nottingham may be monitored as permitted by UK legislation.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/34#issuecomment-15545753
.

[txa]

Sorry. I general if all constructs of an inductive family X : I -> U are of the form,

c : (i : I) ? -> X i

then it is "protestant". E.g.

acc : (x : I)((y : I) y < x -> Acc < y) -> Acc < x

is of the form. A non-protestant example is the family of finite types e.g.

fsucc : (n : Nat) Fin n -> Fin (suc n)

The point is that non-protestant inductive families rely on equality. In the fsuc case the signature functor is

F : (Nat -> Set) -> Nat -> Set
F X m = Sigma n : Nat, suc m = n x X m

Thorsten

From: Mike Shulman <[email protected]mailto:[email protected]>
Reply-To: HoTT/book <[email protected]mailto:[email protected]>
Date: Wednesday, 27 March 2013 13:59
To: HoTT/book <[email protected]mailto:[email protected]>
Cc: Thorsten Altenkirch <[email protected]mailto:[email protected]>
Subject: Re: [book] General scheme for inductive types (#34)

What you just said is incomprehensible to me. (-:

On Wed, Mar 27, 2013 at 2:54 PM, Thorsten Altenkirch <
[email protected]:[email protected]> wrote:

Yes, but it is of a simple form in that the signature functor doesn't need
to refer to equality.

Peter Hancock calls these families protestant while the others are
catholic (because they are based on the belief in transsubstantiation :-)

From: Mike Shulman <[email protected]mailto:[email protected]<mailto:
[email protected]mailto:[email protected]>>
Reply-To: HoTT/book <[email protected]mailto:[email protected]mailto:[email protected]>

To: HoTT/book <[email protected]mailto:[email protected]mailto:[email protected]>
Cc: Thorsten Altenkirch <[email protected]mailto:[email protected]mailto:[email protected]>
Subject: Re: [book] General scheme for inductive types (#34)

The definition of accessibility in section 9.8 is an inductive family.

?
Reply to this email directly or view it on GitHub<
https://github.com/HoTT/book/issues/34#issuecomment-15527500>.

This message and any attachment are intended solely for the addressee and
may contain confidential information. If you have received this message in
error, please send it back to me, and immediately delete it. Please do not
use, copy or disclose the information contained in this message or in any
attachment. Any views or opinions expressed by the author of this email do
not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an
attachment

may still contain software viruses which could damage your computer
system:

you are advised to perform your own checks. Email communications with the

University of Nottingham may be monitored as permitted by UK legislation.

?
Reply to this email directly or view it on GitHubhttps://github.com//issues/34#issuecomment-15545753
.

?
Reply to this email directly or view it on GitHubhttps://github.com//issues/34#issuecomment-15546135.

This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment

may still contain software viruses which could damage your computer system:

you are advised to perform your own checks. Email communications with the

University of Nottingham may be monitored as permitted by UK legislation.

[mikeshulman]

Ah, right. I've seen that distinction, but not the terminology you used.
Are the "protestant" ones any simpler to describe for the informal reader,
though? The signature functor belongs to the semantics, not the syntax
(right?).

On Wed, Mar 27, 2013 at 10:51 PM, Thorsten Altenkirch <
[email protected]> wrote:

Sorry. I general if all constructs of an inductive family X : I -> U are
of the form,

c : (i : I) ? -> X i

then it is "protestant". E.g.

acc : (x : I)((y : I) y < x -> Acc < y) -> Acc < x

is of the form. A non-protestant example is the family of finite types
e.g.

fsucc : (n : Nat) Fin n -> Fin (suc n)

The point is that non-protestant inductive families rely on equality. In
the fsuc case the signature functor is

F : (Nat -> Set) -> Nat -> Set
F X m = Sigma n : Nat, suc m = n x X m

Thorsten

From: Mike Shulman <[email protected]<mailto:
[email protected]>>
Reply-To: HoTT/book <[email protected]mailto:[email protected]>

Date: Wednesday, 27 March 2013 13:59
To: HoTT/book <[email protected]mailto:[email protected]>
Cc: Thorsten Altenkirch <[email protected]mailto:[email protected]>
Subject: Re: [book] General scheme for inductive types (#34)

What you just said is incomprehensible to me. (-:

On Wed, Mar 27, 2013 at 2:54 PM, Thorsten Altenkirch <
[email protected]:[email protected]> wrote:

Yes, but it is of a simple form in that the signature functor doesn't
need
to refer to equality.

Peter Hancock calls these families protestant while the others are
catholic (because they are based on the belief in transsubstantiation
:-)

From: Mike Shulman <[email protected]<mailto:
[email protected]><mailto:
[email protected]mailto:[email protected]>>
Reply-To: HoTT/book <[email protected]<mailto:
[email protected]>mailto:[email protected]>

To: HoTT/book <[email protected]<mailto:[email protected]
mailto:[email protected]>
Cc: Thorsten Altenkirch <[email protected]<mailto:[email protected]
mailto:[email protected]>
Subject: Re: [book] General scheme for inductive types (#34)

The definition of accessibility in section 9.8 is an inductive family.

?
Reply to this email directly or view it on GitHub<
https://github.com/HoTT/book/issues/34#issuecomment-15527500>.

This message and any attachment are intended solely for the addressee
and
may contain confidential information. If you have received this message
in
error, please send it back to me, and immediately delete it. Please do
not
use, copy or disclose the information contained in this message or in
any
attachment. Any views or opinions expressed by the author of this email
do
not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an
attachment

may still contain software viruses which could damage your computer
system:

you are advised to perform your own checks. Email communications with
the

University of Nottingham may be monitored as permitted by UK
legislation.

?
Reply to this email directly or view it on GitHub<
https://github.com/HoTT/book/issues/34#issuecomment-15545753>
.

?
Reply to this email directly or view it on GitHub<
https://github.com/HoTT/book/issues/34#issuecomment-15546135>.

This message and any attachment are intended solely for the addressee and
may contain confidential information. If you have received this message in
error, please send it back to me, and immediately delete it. Please do not
use, copy or disclose the information contained in this message or in any
attachment. Any views or opinions expressed by the author of this email do
not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an
attachment

may still contain software viruses which could damage your computer
system:

you are advised to perform your own checks. Email communications with the

University of Nottingham may be monitored as permitted by UK legislation.

—

Reply to this email directly or view it on GitHubhttps://github.com//issues/34#issuecomment-15565562
.

[txa]

The non-protestant types implicitly refer to equality. Could this be an issue if the index type is not a set?

Thorsten

From: Mike Shulman <[email protected]mailto:[email protected]>
Reply-To: HoTT/book <[email protected]mailto:[email protected]>
Date: Wednesday, 27 March 2013 21:56
To: HoTT/book <[email protected]mailto:[email protected]>
Cc: Thorsten Altenkirch <[email protected]mailto:[email protected]>
Subject: Re: [book] General scheme for inductive types (#34)

Ah, right. I've seen that distinction, but not the terminology you used.
Are the "protestant" ones any simpler to describe for the informal reader,
though? The signature functor belongs to the semantics, not the syntax
(right?).

On Wed, Mar 27, 2013 at 10:51 PM, Thorsten Altenkirch <
[email protected]:[email protected]> wrote:

Sorry. I general if all constructs of an inductive family X : I -> U are
of the form,

c : (i : I) ? -> X i

then it is "protestant". E.g.

acc : (x : I)((y : I) y < x -> Acc < y) -> Acc < x

is of the form. A non-protestant example is the family of finite types
e.g.

fsucc : (n : Nat) Fin n -> Fin (suc n)

The point is that non-protestant inductive families rely on equality. In
the fsuc case the signature functor is

F : (Nat -> Set) -> Nat -> Set
F X m = Sigma n : Nat, suc m = n x X m

Thorsten

From: Mike Shulman <[email protected]mailto:[email protected]<mailto:
[email protected]mailto:[email protected]>>
Reply-To: HoTT/book <[email protected]mailto:[email protected]mailto:[email protected]>

Date: Wednesday, 27 March 2013 13:59
To: HoTT/book <[email protected]mailto:[email protected]mailto:[email protected]>
Cc: Thorsten Altenkirch <[email protected]mailto:[email protected]mailto:[email protected]>
Subject: Re: [book] General scheme for inductive types (#34)

What you just said is incomprehensible to me. (-:

On Wed, Mar 27, 2013 at 2:54 PM, Thorsten Altenkirch <
[email protected]:[email protected]:[email protected]> wrote:

Yes, but it is of a simple form in that the signature functor doesn't
need
to refer to equality.

Peter Hancock calls these families protestant while the others are
catholic (because they are based on the belief in transsubstantiation
:-)

From: Mike Shulman <[email protected]mailto:[email protected]<mailto:
[email protected]mailto:[email protected]><mailto:
[email protected]mailto:[email protected]mailto:[email protected]>>
Reply-To: HoTT/book <[email protected]mailto:[email protected]<mailto:
[email protected]mailto:[email protected]>mailto:[email protected]>

To: HoTT/book <[email protected]mailto:[email protected]<mailto:[email protected]
mailto:[email protected]>
Cc: Thorsten Altenkirch <[email protected]mailto:[email protected]<mailto:[email protected]
mailto:[email protected]>
Subject: Re: [book] General scheme for inductive types (#34)

The definition of accessibility in section 9.8 is an inductive family.

?
Reply to this email directly or view it on GitHub<
https://github.com/HoTT/book/issues/34#issuecomment-15527500>.

This message and any attachment are intended solely for the addressee
and
may contain confidential information. If you have received this message
in
error, please send it back to me, and immediately delete it. Please do
not
use, copy or disclose the information contained in this message or in
any
attachment. Any views or opinions expressed by the author of this email
do
not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an
attachment

may still contain software viruses which could damage your computer
system:

you are advised to perform your own checks. Email communications with
the

University of Nottingham may be monitored as permitted by UK
legislation.

?
Reply to this email directly or view it on GitHub<
https://github.com/HoTT/book/issues/34#issuecomment-15545753>
.

?
Reply to this email directly or view it on GitHub<
https://github.com/HoTT/book/issues/34#issuecomment-15546135>.

This message and any attachment are intended solely for the addressee and
may contain confidential information. If you have received this message in
error, please send it back to me, and immediately delete it. Please do not
use, copy or disclose the information contained in this message or in any
attachment. Any views or opinions expressed by the author of this email do
not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an
attachment

may still contain software viruses which could damage your computer
system:

you are advised to perform your own checks. Email communications with the

University of Nottingham may be monitored as permitted by UK legislation.

—

Reply to this email directly or view it on GitHubhttps://github.com//issues/34#issuecomment-15565562
.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/34#issuecomment-15565653.

This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment

may still contain software viruses which could damage your computer system:

you are advised to perform your own checks. Email communications with the

University of Nottingham may be monitored as permitted by UK legislation.

[mikeshulman]

I don't see why it would.
On Mar 27, 2013 11:25 PM, "Thorsten Altenkirch" [email protected]
wrote:

The non-protestant types implicitly refer to equality. Could this be an
issue if the index type is not a set?

Thorsten

From: Mike Shulman <[email protected]<mailto:
[email protected]>>
Reply-To: HoTT/book <[email protected]mailto:[email protected]>

Date: Wednesday, 27 March 2013 21:56
To: HoTT/book <[email protected]mailto:[email protected]>
Cc: Thorsten Altenkirch <[email protected]mailto:[email protected]>
Subject: Re: [book] General scheme for inductive types (#34)

Ah, right. I've seen that distinction, but not the terminology you used.
Are the "protestant" ones any simpler to describe for the informal reader,
though? The signature functor belongs to the semantics, not the syntax
(right?).

On Wed, Mar 27, 2013 at 10:51 PM, Thorsten Altenkirch <
[email protected]:[email protected]> wrote:

Sorry. I general if all constructs of an inductive family X : I -> U are
of the form,

c : (i : I) ? -> X i

then it is "protestant". E.g.

acc : (x : I)((y : I) y < x -> Acc < y) -> Acc < x

is of the form. A non-protestant example is the family of finite types
e.g.

fsucc : (n : Nat) Fin n -> Fin (suc n)

The point is that non-protestant inductive families rely on equality. In
the fsuc case the signature functor is

F : (Nat -> Set) -> Nat -> Set
F X m = Sigma n : Nat, suc m = n x X m

Thorsten

From: Mike Shulman <[email protected]<mailto:
[email protected]><mailto:
[email protected]mailto:[email protected]>>
Reply-To: HoTT/book <[email protected]<mailto:
[email protected]>mailto:[email protected]>

Date: Wednesday, 27 March 2013 13:59
To: HoTT/book <[email protected]<mailto:[email protected]
mailto:[email protected]>
Cc: Thorsten Altenkirch <[email protected]<mailto:[email protected]
mailto:[email protected]>
Subject: Re: [book] General scheme for inductive types (#34)

What you just said is incomprehensible to me. (-:

On Wed, Mar 27, 2013 at 2:54 PM, Thorsten Altenkirch <
[email protected]:[email protected]<mailto:
[email protected]>> wrote:

Yes, but it is of a simple form in that the signature functor doesn't
need
to refer to equality.

Peter Hancock calls these families protestant while the others are
catholic (because they are based on the belief in transsubstantiation
:-)

From: Mike Shulman <[email protected]<mailto:
[email protected]><mailto:
[email protected]mailto:[email protected]><mailto:
[email protected]mailto:[email protected]<mailto:
[email protected]>>>
Reply-To: HoTT/book <[email protected]<mailto:
[email protected]><mailto:
[email protected]mailto:[email protected]><mailto:
[email protected]>>

To: HoTT/book <[email protected]<mailto:[email protected]
<mailto:[email protected]
mailto:[email protected]>
Cc: Thorsten Altenkirch <[email protected]<mailto:[email protected]
<mailto:[email protected]
mailto:[email protected]>
Subject: Re: [book] General scheme for inductive types (#34)

The definition of accessibility in section 9.8 is an inductive family.

?
Reply to this email directly or view it on GitHub<
https://github.com/HoTT/book/issues/34#issuecomment-15527500>.

This message and any attachment are intended solely for the addressee
and
may contain confidential information. If you have received this
message
in
error, please send it back to me, and immediately delete it. Please do
not
use, copy or disclose the information contained in this message or in
any
attachment. Any views or opinions expressed by the author of this
email
do
not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an
attachment

may still contain software viruses which could damage your computer
system:

you are advised to perform your own checks. Email communications with
the

University of Nottingham may be monitored as permitted by UK
legislation.

?
Reply to this email directly or view it on GitHub<
https://github.com/HoTT/book/issues/34#issuecomment-15545753>
.

?
Reply to this email directly or view it on GitHub<
https://github.com/HoTT/book/issues/34#issuecomment-15546135>.

This message and any attachment are intended solely for the addressee
and
may contain confidential information. If you have received this message
in
error, please send it back to me, and immediately delete it. Please do
not
use, copy or disclose the information contained in this message or in
any
attachment. Any views or opinions expressed by the author of this email
do
not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an
attachment

may still contain software viruses which could damage your computer
system:

you are advised to perform your own checks. Email communications with
the

University of Nottingham may be monitored as permitted by UK
legislation.

—

Reply to this email directly or view it on GitHub<
https://github.com/HoTT/book/issues/34#issuecomment-15565562>
.

—
Reply to this email directly or view it on GitHub<
https://github.com/HoTT/book/issues/34#issuecomment-15565653>.

This message and any attachment are intended solely for the addressee and
may contain confidential information. If you have received this message in
error, please send it back to me, and immediately delete it. Please do not
use, copy or disclose the information contained in this message or in any
attachment. Any views or opinions expressed by the author of this email do
not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an
attachment

may still contain software viruses which could damage your computer
system:

you are advised to perform your own checks. Email communications with the

University of Nottingham may be monitored as permitted by UK legislation.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/34#issuecomment-15566273
.