Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: Nicolai Kraus <nicola...@gmail.com>
To: Michael Shulman <shu...@sandiego.edu>,
	Thorsten Altenkirch <Thorsten....@nottingham.ac.uk>
Cc: Jon Sterling <j...@jonmsterling.com>,
	'Martin Escardo' via Homotopy Type Theory
	<homotopyt...@googlegroups.com>
Subject: Re: [HoTT] Identity versus equality
Date: Sun, 10 May 2020 15:20:33 +0100	[thread overview]
Message-ID: <3ec2f134-cbd4-7bfd-0a69-efb734a4a231@gmail.com> (raw)
In-Reply-To: <CAOvivQxD-gJgp=Az0b=ysOygQryp695uNQjKbrOr-cEQTU-aeA@mail.gmail.com>

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

  reply	other threads:[~2020-05-10 14:20 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 [this message]
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
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=3ec2f134-cbd4-7bfd-0a69-efb734a4a231@gmail.com \
    --to="nicola..."@gmail.com \
    --cc="Thorsten...."@nottingham.ac.uk \
    --cc="homotopyt..."@googlegroups.com \
    --cc="j..."@jonmsterling.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).