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.
On Thu, 14 Feb 2019 at 19:05, Anders Mortberg <andersmortberg@gmail.com> wrote: > 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. I was interested to read this, because I too use that weakened form of fibration in some work attempting to get a model of univalence based only on composition of paths rather than more general Kan filling operations — so far unpublished, because I can't quite see how to get univalent universes to work (but seem frustratingly close to it). Anyway, what I wanted to say is that perhaps one should call these things "Dold fibrations" by analogy with the classic notion of Dold fibration in topological spaces <https://ncatlab.org/nlab/show/Dold+fibration>? Andy -- 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.
Thanks. This looks very interesting. Did you think about the corresponding model structure? https://ncatlab.org/nlab/show/type-theoretic+model+structure Because, we know that Cartesian cubical sets are not equivalent to simplicial sets, but as far as I know, this is still unclear for the DeMorgan cubical sets. https://ncatlab.org/nlab/show/cubical+type+theory#models On Thu, Feb 14, 2019 at 8:05 PM Anders Mortberg <andersmortberg@gmail.com> 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. -- 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.1: Type: text/plain, Size: 2556 bytes --] On Thursday, February 14, 2019 at 3:06:29 PM UTC-5, Andrew Pitts wrote: > > On Thu, 14 Feb 2019 at 19:05, Anders Mortberg <andersm...@gmail.com > <javascript:>> wrote: > > 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. > > I was interested to read this, because I too use that weakened form > of fibration in some work attempting to get a model of univalence > based only on composition of paths rather than more general Kan > filling operations — so far unpublished, because I can't quite see how > to get univalent universes to work (but seem frustratingly close to > it). > > Very interesting that you also considered this form of weakened fibrations! I also thought a bit about basing things on a binary composition operation, but I never could get it to work. I managed to convince myself some year ago that in the presence of connections and reversals (potentially with Boolean structure) homogeneous composition (hcomp^0->1) is equivalent to binary composition, but without this structure on the interval I don't really see what to do. But on the other hand, if you don't have connections then I don't think you need the fibrations to lift against arbitrary subtubes but rather only open boxes in the sense of BCH... Anyway, the univalent universes (in particular fibrancy of Glue types) is by far the hardest thing in our note (as seems to always be the case). The way we do it is an adaptation of what we did back in CCHM, but because of the weakness we have to do additional corrections in the construction which makes it quite a bit longer. Anyway, what I wanted to say is that perhaps one should call these > things "Dold fibrations" by analogy with the classic notion of Dold > fibration in topological spaces > <https://ncatlab.org/nlab/show/Dold+fibration>? > > Andy > Thanks for the pointer! I didn't know about them and will have to think a bit whether what we have could be seen as a cubical variation of them. -- Anders -- 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: 3894 bytes --]
[-- Attachment #1.1: Type: text/plain, Size: 3365 bytes --] No, we didn't think about model structures yet. First of all one has to figure out how to write our Kan operations as a lifting condition (this is not entirely obvious because of the additional weakness). The observation that the type theoretic model structure on De Morgan cubical sets is not equivalent to the one on spaces is simpler than for Cartesian cubical sets as we have reversals. The case that is not known AFAIK is for the one based on distributive lattices (so only with connections, but no reversals), i.e. the "Dedekind" cubes. -- Anders On Friday, February 15, 2019 at 3:16:56 AM UTC-5, Bas Spitters wrote: > > Thanks. This looks very interesting. > > Did you think about the corresponding model structure? > https://ncatlab.org/nlab/show/type-theoretic+model+structure > > Because, we know that Cartesian cubical sets are not equivalent to > simplicial sets, but as far as I know, this is still unclear for the > DeMorgan cubical sets. > https://ncatlab.org/nlab/show/cubical+type+theory#models > > On Thu, Feb 14, 2019 at 8:05 PM Anders Mortberg > <andersm...@gmail.com <javascript:>> 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 <javascript:>. > > > For more options, visit https://groups.google.com/d/optout. > -- 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: 6293 bytes --]
Please don't call these "type-theoretic model structures". There are many other model categories that model type theories in ways unrelated to cubes, notably the classical simplicial model categories that model Book HoTT. Maybe something like "cubical-type model structures"? On Fri, Feb 15, 2019 at 8:32 AM Anders Mörtberg <andersmortberg@gmail.com> wrote: > > No, we didn't think about model structures yet. First of all one has to figure out how to write our Kan operations as a lifting condition (this is not entirely obvious because of the additional weakness). > > The observation that the type theoretic model structure on De Morgan cubical sets is not equivalent to the one on spaces is simpler than for Cartesian cubical sets as we have reversals. The case that is not known AFAIK is for the one based on distributive lattices (so only with connections, but no reversals), i.e. the "Dedekind" cubes. > > -- > Anders > > On Friday, February 15, 2019 at 3:16:56 AM UTC-5, Bas Spitters wrote: >> >> Thanks. This looks very interesting. >> >> Did you think about the corresponding model structure? >> https://ncatlab.org/nlab/show/type-theoretic+model+structure >> >> Because, we know that Cartesian cubical sets are not equivalent to >> simplicial sets, but as far as I know, this is still unclear for the >> DeMorgan cubical sets. >> https://ncatlab.org/nlab/show/cubical+type+theory#models >> >> On Thu, Feb 14, 2019 at 8:05 PM Anders Mortberg >> <andersm...@gmail.com> 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. > > -- > 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. -- 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.
I think the idea is that the model structure is constructed / proved using ideas from type theory (like univalence), rather than that it is a model of type theory. But I agree that the terminology is confusing. The methodology is, I think, due to Christian Sattler — so maybe Sattler model structure is more appropriate? Steve > On Feb 15, 2019, at 7:01 PM, Michael Shulman <shulman@sandiego.edu> wrote: > > Please don't call these "type-theoretic model structures". There are > many other model categories that model type theories in ways unrelated > to cubes, notably the classical simplicial model categories that model > Book HoTT. Maybe something like "cubical-type model structures"? > > On Fri, Feb 15, 2019 at 8:32 AM Anders Mörtberg > <andersmortberg@gmail.com> wrote: >> >> No, we didn't think about model structures yet. First of all one has to figure out how to write our Kan operations as a lifting condition (this is not entirely obvious because of the additional weakness). >> >> The observation that the type theoretic model structure on De Morgan cubical sets is not equivalent to the one on spaces is simpler than for Cartesian cubical sets as we have reversals. The case that is not known AFAIK is for the one based on distributive lattices (so only with connections, but no reversals), i.e. the "Dedekind" cubes. >> >> -- >> Anders >> >> On Friday, February 15, 2019 at 3:16:56 AM UTC-5, Bas Spitters wrote: >>> >>> Thanks. This looks very interesting. >>> >>> Did you think about the corresponding model structure? >>> https://ncatlab.org/nlab/show/type-theoretic+model+structure >>> >>> Because, we know that Cartesian cubical sets are not equivalent to >>> simplicial sets, but as far as I know, this is still unclear for the >>> DeMorgan cubical sets. >>> https://ncatlab.org/nlab/show/cubical+type+theory#models >>> >>> On Thu, Feb 14, 2019 at 8:05 PM Anders Mortberg >>> <andersm...@gmail.com> 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. >> >> -- >> 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. > > -- > 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. -- 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.
> I think the idea is that the model structure is constructed / proved using > ideas from type theory (like univalence), rather than that it is a model > of type theory. But I agree that the terminology is confusing. > The methodology is, I think, due to Christian Sattler — so maybe Sattler > model structure is more appropriate? When the interval is fixed one might speak of minimal Cisinski model structure since it is the one with the fewest weak equivalences. Of course, Sattler studied them a lot so it's good name either. Unfortunately, we don't know when minimal and test model structure concide. Thomas -- 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.
> > I think the idea is that the model structure is constructed / proved using > > ideas from type theory (like univalence), rather than that it is a model > > of type theory. But I agree that the terminology is confusing. > > The methodology is, I think, due to Christian Sattler ??? so maybe Sattler > > model structure is more appropriate? > > When the interval is fixed one might speak of minimal Cisinski model > structure since it is the one with the fewest weak equivalences. > Of course, Sattler studied them a lot so it's good name either. Well, Coquand-Sattler might be better because it was first used in the [CCHM] paper. From the many anodyne monos of the test model structure one took just those which were syntactically convenient. But, as far as I know the test model structure also gives rise to a model of cubical TT because its more restrictive class off fibrations suffices for interpreting sytax. > Unfortunately, we don't know when minimal and test model structure concide. Thomas -- 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.
> Unfortunately, we don't know when minimal and test model structure concide. Maybe one can expect them never to coincide, by the following loose reasoning: in between the minimal model structure and the test model structure should lie something like an (infinity,1)-model structure, i.e. something like a cubical version (in the chosen flavour) of a quasi-categorical model structure, and one does not of course expect the (infinity,1)-model structure to coincide with the test one. For simplicial sets it is known of course that one has the quasi-categorical model structure strictly lying in between the minimal one and the test one. Best wishes, Richard -- 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.
> On Feb 16, 2019, at 2:51 PM, Thomas Streicher <streicher@mathematik.tu-darmstadt.de> wrote: > >>> I think the idea is that the model structure is constructed / proved using >>> ideas from type theory (like univalence), rather than that it is a model >>> of type theory. But I agree that the terminology is confusing. >>> The methodology is, I think, due to Christian Sattler ??? so maybe Sattler >>> model structure is more appropriate? >> >> When the interval is fixed one might speak of minimal Cisinski model >> structure since it is the one with the fewest weak equivalences. >> Of course, Sattler studied them a lot so it's good name either. > > Well, Coquand-Sattler might be better because it was first used in the > [CCHM] paper. From the many anodyne monos of the test model structure > one took just those which were syntactically convenient. I don’t want to minimize the importance of the work on cubical type theory — which I believe is very great — but it has focussed on building models of type theory directly, often within other type theories, rather than on building Quillen model categories. To be sure, many ideas, and some terminology, from model category theory are used, but without showing or even claiming that there is a Quillen model structure. > But, as far as I know the test model structure also gives rise to a > model of cubical TT because its more restrictive class off fibrations > suffices for interpreting sytax. has it been shown that the test model structure interprets Pi types, universes, and univalence? Steve > >> Unfortunately, we don't know when minimal and test model structure concide. > > Thomas > > -- > 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. -- 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.
> Maybe one can expect them never to coincide, by the following loose > reasoning: in between the minimal model structure and the test model > structure should lie something like an (infinity,1)-model structure, > i.e. something like a cubical version (in the chosen flavour) of a > quasi-categorical model structure, and one does not of course expect > the (infinity,1)-model structure to coincide with the test one. For > simplicial sets it is known of course that one has the > quasi-categorical model structure strictly lying in between the > minimal one and the test one. but in simplicial sets the minimal and the test model structure do coincide (since filling open boxes is tantamount to filling horns as shown at the beginning of Goerss and Jardine) Thomas -- 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.
> I don???t want to minimize the importance of the work on cubical type theory > ??? which I believe is very great ??? but it has focussed on building models of type theory > directly, often within other type theories, rather than on building Quillen model categories. > To be sure, many ideas, and some terminology, from model category theory are used, > but without showing or even claiming that there is a Quillen model structure. They didn't emphasize model structures but they are around and more explicitly in Sattler's work. Admittedly, there are sometimes distinctions which only make sense if the meta theory is constructive. But if one ignores that then they are interpreting syntax in minimal Cisinski model structures defined by open box filling conditions. One does know that minimal and test model structure fall apart when taking as site free finitely generated de Morgan algebras as shown by Sattler. It is unknown when taking the "cartesian site" of finite lattices and monotone maps between them (opposite to free finitely generated distributive lattices and homomorphisms). I agree that in the published papers on cubical TT the model category aspect is not shown bluntly but Thierry is aware of it and it shows up in Christian's work quite explicitly. Moreover, I think it is not important to choose the minimal Cisinski model structures as one can interpret Cubical TT also in the test model structure on cubical sets. There are fewer fibrations since there are more anodyne cofibrations but when interpreting syntax one stays within this more restricted collection of fibrations. The only problem with simplical sets is that finite powers of the interval are not representable. That's overcome by choosing the cubical site. But one may still restrict fibrations to those of the test model structure and one gets the simplical set model when restricting the fibration to simplicial sets. Thomas PS Thierry insists on constructing models in constructive meta theories like CZF with universes or extensional type theory with universes. This has the benefit of obtaining conservation results but is not necessary for the interpreted theories having computational meaning. The theories have their computational meaning independently from the models they are interpreted in. -- 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.
Dear Thomas, > but in simplicial sets the minimal and the test model structure > do coincide I don't think this is correct if by 'minimal' one means choosing the set S of monomorphisms in the donnée homotopique to be the empty set. Every Cisinski model structure is a Bousfield localisation of the minimal one in this sense. In particular, the quasi-categorical is, and the usual one whose fibrant objects are Kan complexes is a Bousfield localisation of that again. None of them are Quillen equivalent. One reference where this is touched on slightly is towards the beginning of Joyal's notes on quasi-categories. http://mat.uab.cat/~kock/crm/hocat/advanced-course/Quadern45-2.pdf I expect the same pattern for all cube-like test categories. Best wishes, Richard -- 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.
This is very cool! It's great to know that we can do without the diagonal cofibrations if we weaken the notion of fibration. Here's a reformulation of this Kan operation that I find intriguing: in the internal language, I think Evan and Anders' definition is equivalent to saying that A : I → Set has Kan composition iff Π r:I, the map (λ f → f r) : (Π (x : I) → A x) → (A r) is an equivalence where equivalence is defined to be hfiber contractible, and contractible is defined to be "any partial element extends to a total one" (i.e. "trivial fibration") In contrast, the stricter notion, where com^r->r is strictly the identity is A : I → Set has Kan composition means Π r:I, b : A(r), the strict fiber (i.e. SFiber (f : A → B) b = Σ a:A. f(a) =strictly b) of the map (λ f → f r) : (Π (x : I) → A x) → (A r) is contractible Here's why: (1) The definition in Evan and Anders' note, in pseudo-internal-language notation (ignoring the boundary constraint proofs) is: hasWCom : (I → Set) → Set hasWCom A = (r r' : I) → (α : Set) {{cα : Cofib α}} (t : (x : I) → α → A x) (b : A r [ α ↦ t rα) ] ) → A r' [ α ↦ t r' ] hasWPath :(I → Set) → (wcomA : hasWCom A) → Set hasWPath A wcomA = (r : I) → (α : Set) {{cα : Cofib α}} (t : (x : I) → α → A x) (b : A r [ α ↦ t r) ] ) → (Path (A r) (wcomA r r' α t b) (fst b)) [ α ↦ \ _ → t r' ] (i.e. the path is constantly t r' on α) (2) If you move the r' binding inward and fuse the two functions into one, you get hasWCom : (I → Set) → Set hasWCom A = (r : I) → (α : Set) {{cα : Cofib α}} (t : (x : I) → α → A x) (b : A r [ α ↦ t r) ] ) → (Σ f:((r' : I) → A r'). Path (A r) (f r) b) [ α ↦ (\ r' → t r' , \ _ → t r) ] (i.e. on α, f is t - , and the path is constant.) If we ignore the partial element stuff for a bit, that's hasWCom : (I → Set) → Set hasWCom A = (r : I) → (b : A r ) → (Σ f : ((r' : I) → A r'). Path (A r) (f r) b) which is apply : (r : I) → ((x : I) → A x) → A r hasWCom : (I → Set l) → Set hasWCom A = (r : I) → (b : A r ) → HFiber (apply r) b (3) Restoring and rearranging the partial element constraint to t instead of b gives hasWCom : (I → Set) → Set hasWCom A = (r : I) → (α : Set) {{cα : Cofib α}} (b : A r ) (t : α → (x : I) → (A x [x = r ↦ b]) ) → (HFiber (apply r) b) [ α ↦ (\ r' → t r' pα , \ _ → t r) ] which is, strangely enough, exactly the weird definition of equivalence that a group came up with at Dagstuhl while trying to optmize cubicaltt. (4) Assuming using that weird definition of equivalence is not essential, we could rephrase using the hfiber-contractible definition, where contractible is defined to mean that any partial element extends to a total one: -- trivial fibration: any partial element can be extended ContractibleFill : (A : Set) → Set ContractibleFill A = (α : Set) {{cα : Cofib α}} → (t : α → A) → A [α ↦ t ] isEquivFill : (A : Set) (B : Set) (f : A → B) → Set isEquivFill A B f = (b : B) → ContractibleFill (HFiber f b) isKan : (I → Set) → Set isKan A = (r : I) → isEquivFill ((x : I) → A x) (A r) (apply A r) This unwinds to almost the operation you have, except that this definition has a partial element of the whole HFiber (apply A r) b on α, i.e. t r has a path to b, rather than being required to be strictly equal to it. For the strict one, we have hasCom : (I → Set l) → Set hasCom A = (r r' : I) (α : Set) {{_ : Cofib α}} → (t : (z : I) → α → A z) → (b : A r [ α ↦ t r ]) → A r' [ α ↦ t r' , (r = r') ↦ ⇒ (fst b) ] i.e. (r : I) (α : Set) {{_ : Cofib α}} → (t : (z : I) → α → A z) → (b : A r [ α ↦ t r ]) → Σ (f : (r' : I) → A r')[α ↦ t]. f r = b) i.e. (r : I) (b : A r) → (α : Set) {{_ : Cofib α}} → (t : α → Σ f:((z : I) → A z). f r = b) → Σ (f : (r' : I) → A r')[α ↦ t]. f r = b i.e. (r : I) (b : A r) → (α : Set) {{_ : Cofib α}} → (t : α → SFiber f b) → SFiber f b [ α ↦ t ] (using uniqueness for =) i.e. (r : I) (b : A r) → Contractible(SFiber f b) -- 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.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. Best, Andrew 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 --]
[-- Attachment #1.1: Type: text/plain, Size: 8329 bytes --] Thanks Dan and Andrew for analyzing our work further! I find Dan's reformulation of our Kan condition quite illuminating: A : I → Set has Kan composition iff Π r:I, the map (λ f → f r) : (Π (x : I) → A x) → (A r) is an equivalence My intuition is that this says that A is fibrant iff for any r : I the type A r can be extended to all of I in a uniform way. I believe that we can reformulate the Kan condition we had in CCHM as: A : I → Set has Kan composition iff the map (λ f → f 0) : (Π (x : I) → A x) → (A 0) is an equivalence In the presence of a meet connection these two formulations are path-equal by moving along "i /\ r" (this is what motivates the use of connections in CCHM). What our note shows is that this natural generalization of CCHM is closed under all of the cubical type formers and hence form a model of univalent type theory even in the absence of connections. In particular it is not necessary to further require the strict fibers as in AFH/ABCFHL when generalizing CCHM. This is what lets us drop the assumption that the diagonal I -> I x I is a cofibration (what we referred to as "diagonal cofibrations" above) in order to construct univalent fibrant universes. I haven't yet had time to analyze Andrew's definition, but if it works then I would be very interested in knowing if the Sattler model structure construction works. If I understand Christian's work correctly the construction of the WFS's require very few assumptions and the 2-out-of-3 property relies on the equivalence extension property which follows from the existence of fibrant Glue types (which is in our note). -- Anders On Monday, February 18, 2019 at 9:05:54 AM UTC-5, Andrew Swan wrote: > > 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. > > > Best, > Andrew > > > > 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: 9721 bytes --]
[-- Attachment #1.1: Type: text/plain, Size: 2373 bytes --] With Andrew Swan we have now worked out a categorical presentation of our generalized notion of fibrations for cartesian cubical sets. We have also proved that Sattler's model structure theorem applies. For details see: https://github.com/mortberg/gen-cart/blob/master/modelstructure.pdf A special case of our result is a model structure on cartesian cubical sets that does not require that the diagonal map on the interval is a cofibration (i.e. "diagonal cofibrations"). We hence obtain the Sattler model structure on De Morgan and distributive lattice cubical sets as a special case when the cube category has connections. Furthermore, we also obtain the model structure on cartesian cubical sets sketched by Coquand ( https://groups.google.com/forum/#!msg/homotopytypetheory/RQkLWZ_83kQ/tAyb3zYTBQAJ) and more recently spelled out in detail by Awodey ( https://github.com/awodey/math/blob/master/QMS/qms.pdf) when we add the assumption of diagonal cofibrations. We have also formalized the cubical model based on generalized fibrations in the Orton-Pitts style using Agda: https://github.com/mortberg/gen-cart/tree/master/agda The formalization contains the standard type formers of cubical type theory (Pi, Sigma, Path, Id, Glue and univalence). We have not yet formalized the LOPS universe construction as this requires a special branch of Agda that we're waiting for to get merged into master, but we don't expect any problems with this as LOPS applies to cartesian cubical sets as exponentiating by the interval has a right adjoint. Furthermore, the LOPS construction has already been formalized for cartesian cubical sets in ABCFHL (https://github.com/dlicata335/cart-cube). We have also formalized the construction of both of the two factorization systems using Andrew's W-types with reductions (https://arxiv.org/abs/1802.07588). Comments are very welcome! -- Anders, Evan and Andrew -- 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. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/2b7b0d66-4787-4fad-9ee4-7a0bd29faab8%40googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 4867 bytes --]