Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: Andrew Swan <wakelin.swan@gmail.com>
To: Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>
Subject: [HoTT] Re: A unifying cartesian cubical type theory
Date: Mon, 18 Feb 2019 06:05:54 -0800 (PST)	[thread overview]
Message-ID: <31a5586c-c66a-4d66-a384-199d9d453a3b@googlegroups.com> (raw)
In-Reply-To: <CAMWCppkw1yGyey0rDGnUawyiVN7TQ2cL6GKNfSXV__zuJvvONA@mail.gmail.com>

[-- Attachment #1.1: Type: text/plain, Size: 6355 bytes --]

I decided to have a go at translating the ideas over to lifting problems 
and model structures. Dan's remarks were quite helpful and possibly some of 
this is a rephrasing of those ideas.

We have an interval object I, and write d0 and d1 for the endpoint 
inclusions 1 -> I. We want to ensure in any case that for i = 0,1 di has 
the enriched/fibred/internal left lifting property against every fibration. 
That is, for every object B, we want that the maps (1, di) : B -> B x I are 
trivial cofibrations. Now if the (trivial) (co)fibrations we defined are 
going to form part of a model structure, we will need that for any map r : 
B -> I, the map (1, r) : B -> B x I is a weak equivalence. This is because 
the projection B x I -> B is a weak equivalence by applying 3-for-2 and 
using that (1, d0) is a trivial cofibration, and then applying 3-for-2 
again the other way, it follows that (1, r) is a weak equivalence.

Therefore when we define fibrations, we want to ensure that we do so in a 
way that guarantees (1, r) : B -> B x I is a weak equivalence. If I has 
connections, then it would be easier, but they are not present in cartesian 
cubical sets, so we look for some other way.

One way to do this is to choose the generating trivial cofibrations so that 
every map (1, r) is a trivial cofibration. For some other arguments to 
work, we include not just these maps, but close under pushout product with 
cofibrations. Therefore we take the generating trivial cofibrations to be 
every map generated as follows: Given a map r : B -> I, and a cofibration m 
: A -> B, we note that m and (1, r) can both be viewed as maps in the slice 
category C/B. We construct the pushout product of (1, r) and m in the slice 
category, and take this to be a generating trivial cofibration. This gives 
the ABCFHL definition of fibration.

However, this has the disadvantage that as a special case we have made the 
map I -> I x I a trivial cofibration, so if we want this to be part of a 
model structure we also need it to be a cofibration. This means we can't 
take the face lattice to be the (generating) cofibrations.

Therefore we need a way to choose the trivial cofibrations that makes every 
map (1, r) : B -> B x I a weak equivalence without adding any new 
cofibrations. We again work in the slice category over B. Since we are now 
working in the slice category, the terminal object 1, is the identity on B, 
and we have a cofibrant subobject A of 1, and a map r : 1 -> I. We take the 
mapping cylinder factorisation of r to get 1 -> T -> I. One can show that 
the map 1 -> T is a cofibration (assuming endpoint inclusions are disjoint 
and both cofibrations, and cofibrations are closed under pullback). Hence 
if we make 1 -> T a trivial cofibration, it won't add any new cofibrations. 
Moreover making 1 -> T a weak equivalence promises to be a reasonable 
substitute for making r a weak equivalence, because the map T -> I should 
also be weak equivalence in any case. Now, as before we also close under 
pushout product with m, again computed in the slice category over B.

Unfolding the definition of mapping cylinder, we get a concrete description 
of T. It is the pushout of two copies of I, along the maps d0 : 1 -> I and 
r : 1 -> I, making a "T" shape where the end of one interval is joined to 
the other at point r. We can also illustrate what the pushout product with 
a cofibration looks like, using the boundary inclusion 2 -> I as an 
example: The codomain is the product T x I and the domain is the subobject 
consisting of two copies of T on each end of the cylinder together with a 
line connecting the bases of the Ts. It's a little tricky to show the 
resulting definition of fibration follows from Anders and Evan's 
definition, but I think it works, by using their observation that they do 
have Kan composition in the usual sense for open boxes (pushout products of 
cofibrations and endpoint inclusions).

It seems reasonable to conjecture then that the Mortberg-Cavallo definition 
of fibration and trivial fibration form part of a model structure, and 
moreover we might also conjecture that if we define fibration to be "right 
lifting property against open box inclusion" and cofibration to be given by 
the face lattice it does not extend to a model structure on cartesian 
cubical sets.


On Thursday, 14 February 2019 20:05:07 UTC+1, Anders Mörtberg wrote:
> Evan Cavallo and I have worked out a new cartesian cubical type theory 
> that generalizes the existing work on cubical type theories and models 
> based on a structural interval: 
> http://www.cs.cmu.edu/~ecavallo/works/unifying-cartesian.pdf 
> The main difference from earlier work on similar models is that it 
> depends neither on diagonal cofibrations nor on connections or 
> reversals. In the presence of these additional structures, our notion 
> of fibration coincides with that of the existing cartesian and De 
> Morgan cubical set models. This work can therefore be seen as a 
> generalization of the existing models of univalent type theory which 
> also clarifies the connection between them. 
> The key idea is to weaken the notion of fibration from the cartesian 
> Kan operations com^r->s so that they are not strictly the identity 
> when r=s. Instead we introduce weak cartesian Kan operations that are 
> only the identity function up to a path when r=s. Semantically this 
> should correspond to a weaker form of a lifting condition where the 
> lifting only satisfies some of the eqations up to homotopy. We verify 
> in the note that this weaker notion of fibration is closed under the 
> type formers of cubical type theory (nat, Sigma, Pi, Path, Id, Glue, 
> U) so that we get a model of univalent type theory. We also verify 
> that the circle works and we don't expect any substantial problems 
> with extending it to more complicated HITs (like pushouts). 
> -- 
> Anders and Evan 

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 #1.2: Type: text/html, Size: 7458 bytes --]

  parent reply	other threads:[~2019-02-18 14:05 UTC|newest]

Thread overview: 18+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2019-02-14 19:04 [HoTT] " Anders Mortberg
2019-02-14 20:06 ` Andrew Pitts
2019-02-15 15:38   ` Anders Mörtberg
2019-02-15  8:16 ` Bas Spitters
2019-02-15 16:32   ` Anders Mörtberg
2019-02-16  0:01     ` Michael Shulman
2019-02-16  0:14       ` Steve Awodey
2019-02-16 12:30         ` streicher
2019-02-16 19:51           ` Thomas Streicher
2019-02-16 22:27             ` Steve Awodey
2019-02-17  9:43               ` Thomas Streicher
2019-02-17 14:14                 ` Licata, Dan
2019-02-16 21:58           ` Richard Williamson
2019-02-17  9:15             ` Thomas Streicher
2019-02-17 13:49               ` Richard Williamson
2019-02-18 14:05 ` Andrew Swan [this message]
2019-02-18 15:31   ` [HoTT] " Anders Mörtberg
2019-06-16 16:04     ` Anders Mörtberg

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:

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

  git send-email \
    --in-reply-to=31a5586c-c66a-4d66-a384-199d9d453a3b@googlegroups.com \
    --to=wakelin.swan@gmail.com \
    --cc=HomotopyTypeTheory@googlegroups.com \


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