```
From: Thierry Coquand <Thierry.Coquand@cse.gu.se>
To: "HomotopyTypeTheory@googlegroups.com"
<HomotopyTypeTheory@googlegroups.com>
Subject: Re: [HoTT] Semantics of higher inductive types
Date: Fri, 14 Sep 2018 11:15:56 +0000 [thread overview]
Message-ID: <EA45D7F1-FC16-4653-B331-FA0218FDD5DD@chalmers.se> (raw)
In-Reply-To: <ed7ad345-85e4-4536-86d7-a57fbe3313fe@googlegroups.com>
[-- Attachment #1: Type: text/plain, Size: 9028 bytes --]
I wrote a short note<http://www.cse.chalmers.se/~coquand/hits.pdf> to confirm Andrew’s message that indeed this technique
works as well (using classical logic) for simplicial sets. This can now be presented
as a combination of various published results. (The originality is only in the presentation;
this essentially follows what is suggested in Andrew’s message.)
This provides a semantics of e.g. suspension as an operation U -> U, where U
is an univalent universe in the simplicial set model.
Thierry
On 7 Jun 2017, at 14:34, Andrew Swan <wakelin.swan@gmail.com<mailto:wakelin.swan@gmail.com>> wrote:
So suspension (or more generally pushouts/coequalisers) is what would make a really good test case for any proposed general approach — it’s the simplest HIT which as far as I know hasn’t been modelled without a size blowup in any infinite-dimensional model except cubical sets, under any of the approaches to modelling HIT’s proposed so far. (Am I right in remembering that this has been given for cubical sets? I can’t find it in any of the writeups, but I seem to recall hearing it presented at conferences.)
The technique used in cubical type theory seems fairly flexible. I'm not sure exactly how flexible, but I think I can get suspension to work in simplicial sets. In the below, throughout I use the characterisation of fibrations as maps with the rlp against the pushout product of each monomorphism with endpoint inclusion into the interval. WLOG there is also a uniformity condition - we have a choice of lift and "pulling back the monomorphism preserves the lift."
Given a fibration X -> Y, you first freely add elements N and S together with a path from N to S for each element of X (I think this is the same as what you called pre suspension). Although the pre suspension is not a fibration in general, it does have some of the properties you might expect from a fibration. Given a path in Y, and an element in the fibre of an endpoint, one can transport along the path to get something in the fibre of the other endpoint. There should also be a "flattening" operation that takes a path q in presuspension(X) over p in Y, and returns a path from q(1) to the transport along p of q(0) that lies entirely in the fibre of p(1).
You then take the "weak fibrant replacement" of the pre suspension. A map in simplicial sets is a fibration if and only if it has the rlp against each pushout product of a monomorphism with an endpoint inclusion into the interval. In fibrant replacement you freely add a diagonal lift for each such lifting problems. In weak fibrant replacement you only add fillers for some of these lifting problems. The pushout product of a monomorphism A -> B with endpoint inclusion always has codomain B x I - then only consider those lifting problems where the bottom map factors through the projection B x I -> B. I think there are two ways to ensure that the operation of weak fibrant replacement is stable under pullback - one way is carry out the operation "internally" in simplicial sets (viewed as a topos), and the other to use the algebraic small object argument, ensuring that uniformity condition above is in the definition. The intuitive reason why this should be stable is that the problem that stops the usual fibrant replacement from being stable is that e.g. when we freely add the transport of a point along a path, p we are adding a new element to the fibre of p(1) which depends on things outside of that fibre, whereas with weak fibrant replacement we only add a filler to an open box to a certain fibre if the original open box lies entirely in that fibre.
In order to show that the suspension is fibrant one has to use both the structure already present in pre suspension (transport and flattening) and the additional structure added by weak fibrant replacement. The idea is to follow the same proof as for cubical type theory. It is enough to just show composition and then derive filling. So to define the composition of an open box, first flatten it, then use the weak fibration structure to find the composition. (And I think that last part should be an instance of a general result along the lines of "if the monad of transport and flattening distributes over a monad, then the fibrant replacement monad distributes over the coproduct of that monad with weak fibrant replacement").
Best,
Andrew
On Wednesday, 7 June 2017 11:40:12 UTC+2, Peter LeFanu Lumsdaine wrote:
On Thu, Jun 1, 2017 at 6:08 PM, Peter LeFanu Lumsdaine <p.l.lu...@gmail.com> wrote:
On Thu, Jun 1, 2017 at 6:56 PM, Steve Awodey <awo...@cmu.edu> wrote:
>
> you mean the propositional truncation or suspension operations might lead to cardinals outside of a Grothendieck Universe?
Exactly, yes. There’s no reason I know of to think they *need* to, but with the construction of Mike’s and my paper, they do. And adding stronger conditions on the cardinal used won’t help. The problem is that one takes a fibrant replacement to go from the “pre-suspension” to the suspension (more precisely: a (TC,F) factorisation, to go from the universal family of pre-suspensions to the universal family of suspensions); and fibrant replacement blows up the fibers to be the size of the *base* of the family. So the pre-suspension is small, but the suspension — although essentially small — ends up as large as the universe one’s using.
I realise I was a bit unclear here: it’s only suspension that I meant to suggest is problematic, not propositional truncation. The latter seems a bit easier to do by ad hoc constructions; e.g. the construction below does it in simplicial sets, and I think a similar thing may work also in cubical sets. (I don’t claim originality for this construction; I don’t think I learned it from anywhere, but I do recall discussing it with people who were already aware of it or something similar (I think at least Mike, Thierry, and Simon Huber, at various times?), so I think multiple people may have noticed it independently.)
So suspension (or more generally pushouts/coequalisers) is what would make a really good test case for any proposed general approach — it’s the simplest HIT which as far as I know hasn’t been modelled without a size blowup in any infinite-dimensional model except cubical sets, under any of the approaches to modelling HIT’s proposed so far. (Am I right in remembering that this has been given for cubical sets? I can’t find it in any of the writeups, but I seem to recall hearing it presented at conferences.)
Construction of propositional truncation without size blowup in simplicial sets:
(1) Given a fibration Y —> X, define |Y| —> X as follows:
an element of |Y|_n consists of an n-simplex x : Δ[n] —> X, together with a “partial lift of x into Y, defined at least on all vertices”, i.e. a subpresheaf S ≤ Δ[n] containing all vertices, and a map y : S —> Y such that the evident square commutes;
reindexing acts by taking pullbacks/inverse images of the domain of the partial lift (i.e. the usual composition of a partial map with a total map).
(2) There’s an evident map Y —> |Y| over X; and the operation sending Y to Y —> |Y| —> X is (coherently) stable up to isomorphism under pullback in X. (Straightforward.)
(3) In general, a fibration is a proposition in the type-theoretic sense iff it’s orthogonal to the boundary inclusions δ[n] —> Δ[n] for all n > 0. (Non-trivial but not too hard to check.)
(4) The map |Y| —> X is a fibration, and a proposition. (Straightforward, given (3), by concretely constructing the required liftings.)
(5) The evident map Y —> |Y| over X is a cell complex constructed from boundary inclusions δ[n] —> Δ[n] with n > 0.
To see this: take the filtration of |Y| by subobjects Y_n, where the non-degenerate simplices of Y_n are those whose “missing” simplices are all of dimension ≤n. Then Y_0 = Y, and the non-degenerate simplices of Y_{n+1} that are not in Y_n are all {n+1}-cells with boundary in Y_n, so the inclusion Y_n —> Y_{n+1} may be seen as gluing on many copies of δ[n+1] —> Δ[n+1].
(6) The map Y —> |Y| is orthogonal to all propositional fibrations, stably in X. (Orthogonality is immediate from (3) and (5); stability is then by (2).)
(7) Let V be either the universe of “well-ordered α-small fibrations”, or the universe of “displayed α-small fibrations”, for α any infinite regular cardinal. Then V carries an operation representing the construction of (1), and modelling propositional truncation. (Lengthy to spell out in full, but straightforward given (2), (6).)
–p.
--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
[-- Attachment #2: Type: text/html, Size: 12412 bytes --]
```

next prev parent reply other threads:[~2018-09-14 11:15 UTC|newest]Thread overview:25+ messages / expand[flat|nested] mbox.gz Atom feed top 2017-05-25 18:25 Michael Shulman 2017-05-26 0:17 ` [HoTT] " Emily Riehl 2017-06-01 14:23 ` Thierry Coquand 2017-06-01 14:43 ` Michael Shulman 2017-06-01 15:30 ` Steve Awodey 2017-06-01 15:38 ` Michael Shulman 2017-06-01 15:56 ` Steve Awodey 2017-06-01 16:08 ` Peter LeFanu Lumsdaine 2017-06-06 9:19 ` Andrew Swan 2017-06-06 10:03 ` Andrew Swan 2017-06-06 13:35 ` Michael Shulman 2017-06-06 16:22 ` Andrew Swan 2017-06-06 19:36 ` Michael Shulman 2017-06-06 20:59 ` Andrew Swan 2017-06-07 9:40 ` Peter LeFanu Lumsdaine 2017-06-07 9:57 ` Thierry Coquand [not found] ` <ed7ad345-85e4-4536-86d7-a57fbe3313fe@googlegroups.com> 2017-06-07 23:06 ` Michael Shulman 2017-06-08 6:35 ` Andrew Swan2018-09-14 11:15 ` Thierry Coquand [this message]2018-09-14 14:16 ` Andrew Swan 2018-10-01 13:02 ` Thierry Coquand 2018-11-10 15:52 ` Anders Mörtberg 2018-11-10 18:21 ` Gabriel Scherer 2017-06-08 4:57 ` CARLOS MANUEL MANZUETA 2018-11-12 12:30 ` Ali Caglayan

Be sure your reply has aReply 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-toswitches of git-send-email(1): git send-email \ --in-reply-to=EA45D7F1-FC16-4653-B331-FA0218FDD5DD@chalmers.se \ --to=thierry.coquand@cse.gu.se \ --cc=HomotopyTypeTheory@googlegroups.com \ /path/to/YOUR_REPLY https://kernel.org/pub/software/scm/git/docs/git-send-email.html * If your mail client supports setting theIn-Reply-Toheader via mailto: links, try the mailto: link

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).