Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: Thorsten Altenkirch <Thorsten....@nottingham.ac.uk>
To: Michael Shulman <shu...@sandiego.edu>,
	nicolai.kraus <nicola...@gmail.com>
Cc: Jon Sterling <j...@jonmsterling.com>,
	"'Martin Escardo' via Homotopy Type Theory"
	<homotopyt...@googlegroups.com>,
	nicolai.kraus <nicola...@gmail.com>
Subject: Re: [HoTT] Identity versus equality
Date: Sun, 10 May 2020 19:15:11 +0000	[thread overview]
Message-ID: <1B7C6C2A-CE2D-4A0D-BEF4-5A36C34EAAF2@nottingham.ac.uk> (raw)
In-Reply-To: <CAOvivQxLJtTuWW-HJRqOjR_J1dw9U_xrrV=xpqLqG37f=r4Osw@mail.gmail.com>

I thought so but now Nicolai says it is not?

From a type-theoretic point of view it seems more natural to say that indexed M-types are fibrant even if the index is not. Saying that natural numbers are cofibrant assigns a special role to one particular inductive type.

Thorsten

On 10/05/2020, 15:35, "Michael Shulman" <shu...@sandiego.edu> wrote:

    Many or all coinductive types can be constructed, at least up to
    equivalence, using Pi-types and (some kind of) Nat.  Is there any
    chance that "exo-Nat is cofibrant" could be used to justify the
    existence/fibrancy of the coinductive types you want?

    On Sun, May 10, 2020 at 7:20 AM Nicolai Kraus <nicola...@gmail.com> wrote:
    >
    > On 10/05/2020 15:01, Michael Shulman wrote:
    > > On Sun, May 10, 2020 at 4:46 AM Thorsten Altenkirch
    > > <Thorsten....@nottingham.ac.uk> wrote:
    > >> Defining simplicial types isn't entirely straightforward (as you know I suppose), because Delta is not directed. We can do semi-simplicial types as a Reedy limit, i.e. an infinite Sigma type
    > > We can certainly *talk* about simplicial types in 2LTT as exofunctors
    > > from the exocategory Delta to the exocategory Type.  I assume the
    > > point you're making is that we don't have a (fibrant) *type of*
    > > simplicial types, whereas we do have a fibrant type of semisimplicial
    > > types (under appropriate axioms)?
    >
    > Judging from the rest of his message, I believe that Thorsten was
    > talking about the direct replacement construction in Christian's and my
    > abstract arXiv:1704.04543. With the assumption "exo-Nat is cofibrant",
    > this gives us a fibrant type that one could call "simplicial types" (and
    > Thorsten does). But of course it's an encoding. If we decide to use such
    > encodings, I fear we may lose the main advantage that the "axiomatic"
    > representations in HoTT have, namely avoiding encodings. (I mean the
    > "main advantage" of HoTT compared to traditional approaches, e.g. taking
    > bisimplicial sets.)
    >
    > >> You need some extra principles, e.g. that strict Nat is fibrant or maybe better that certain coinductive types exist.
    > > Personally, I think the best axiom to use here is that exo-Nat is
    > > *cofibrant*, i.e. Pi-types with domain exo-Nat preserve fibrancy.  We
    > > don't know how to model "exo-Nat is fibrant" in all higher toposes,
    > > but it's easy to interpret "exo-Nat is cofibrant" in such models,
    > > since Pi-types with domain exo-Nat are just externally-infinite
    > > products.
    >
    > I completely agree with your preference for this axiom :-)
    > But Thorsten does has a point if we consider the "engineering level"
    > that was discussed earlier in this thread. Allowing coinductive types
    > with exo-Nat as an index makes it possible to use your paper (Higher
    > Stucture Identity Principle, arXiv:2004.06572) and get a construction of
    > semi-simplicial types which is more convenient to use in a proof assistant.
    >
    > -- Nicolai




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 contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.





  parent reply	other threads:[~2020-05-10 19:15 UTC|newest]

Thread overview: 61+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2020-05-05  8:47 Ansten Mørch Klev
2020-05-06 16:02 ` [HoTT] " Joyal, André
2020-05-06 19:01   ` Steve Awodey
2020-05-06 19:18     ` Michael Shulman
2020-05-06 19:31       ` Steve Awodey
2020-05-06 20:30         ` Joyal, André
2020-05-06 22:52         ` Thorsten Altenkirch
2020-05-06 22:54       ` Thorsten Altenkirch
2020-05-06 23:29         ` Joyal, André
2020-05-07  6:11           ` Egbert Rijke
2020-05-07  6:58           ` Thorsten Altenkirch
2020-05-07  9:04             ` Ansten Mørch Klev
2020-05-07 10:09             ` Thomas Streicher
2020-05-07 16:13               ` Joyal, André
2020-05-07 21:41                 ` David Roberts
2020-05-07 23:43                   ` Joyal, André
2020-05-07 23:56                     ` David Roberts
2020-05-08  6:40                       ` Thomas Streicher
2020-05-08 21:06                         ` Joyal, André
2020-05-08 23:44                           ` Steve Awodey
2020-05-09  2:46                             ` Joyal, André
2020-05-09  3:09                               ` Jon Sterling
     [not found]                             ` <CADZEZBY+3z6nrRwsx9p-HqYuTxAnwMUHv7JasHy8aoy1oaGPcw@mail.gmail.com>
2020-05-09  2:50                               ` Steve Awodey
2020-05-09  8:28                           ` Thomas Streicher
2020-05-09 15:53                             ` Joyal, André
2020-05-09 18:43                               ` Thomas Streicher
2020-05-09 20:18                                 ` Joyal, André
2020-05-09 21:27                                   ` Jon Sterling
2020-05-10  2:19                                     ` Joyal, André
2020-05-10  3:04                                       ` Jon Sterling
2020-05-10  9:09                                         ` Thomas Streicher
2020-05-10 11:59                                           ` Thorsten Altenkirch
2020-05-10 11:46                                     ` Thorsten Altenkirch
2020-05-10 14:01                                       ` Michael Shulman
2020-05-10 14:20                                         ` Nicolai Kraus
2020-05-10 14:34                                           ` Michael Shulman
2020-05-10 14:52                                             ` Nicolai Kraus
2020-05-10 15:16                                               ` Michael Shulman
2020-05-10 15:23                                                 ` Nicolai Kraus
2020-05-10 16:13                                                   ` Nicolai Kraus
2020-05-10 16:28                                                     ` Michael Shulman
2020-05-10 18:18                                                       ` Nicolai Kraus
2020-05-10 19:15                                             ` Thorsten Altenkirch [this message]
2020-05-10 19:20                                         ` Thorsten Altenkirch
2020-05-10 12:53                                   ` Ulrik Buchholtz
2020-05-10 14:01                                     ` Michael Shulman
2020-05-10 14:27                                       ` Nicolai Kraus
2020-05-10 15:35                                         ` Ulrik Buchholtz
2020-05-10 16:30                                           ` Michael Shulman
2020-05-10 18:56                                           ` Nicolai Kraus
2020-05-10 18:04                                     ` Joyal, André
2020-05-11  7:33                                       ` Thomas Streicher
2020-05-11 14:54                                         ` Joyal, André
2020-05-11 16:37                                           ` stre...
2020-05-11 16:42                                             ` Michael Shulman
2020-05-11 17:27                                               ` Thomas Streicher
2020-05-10 16:51                                   ` Nicolai Kraus
2020-05-10 18:57                                     ` Michael Shulman
2020-05-10 19:18                                     ` Nicolai Kraus
2020-05-10 20:22                                       ` Michael Shulman
2020-05-10 22:08                                         ` Joyal, André

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=1B7C6C2A-CE2D-4A0D-BEF4-5A36C34EAAF2@nottingham.ac.uk \
    --to="thorsten...."@nottingham.ac.uk \
    --cc="homotopyt..."@googlegroups.com \
    --cc="j..."@jonmsterling.com \
    --cc="nicola..."@gmail.com \
    --cc="shu..."@sandiego.edu \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).