Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [HoTT] A unifying cartesian cubical type theory
@ 2019-02-14 19:04 Anders Mortberg
  2019-02-14 20:06 ` Andrew Pitts
                   ` (2 more replies)
  0 siblings, 3 replies; 18+ messages in thread
From: Anders Mortberg @ 2019-02-14 19:04 UTC (permalink / raw)
  To: Homotopy Type Theory

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.

^ permalink raw reply	[flat|nested] 18+ messages in thread

* Re: [HoTT] A unifying cartesian cubical type theory
  2019-02-14 19:04 [HoTT] A unifying cartesian cubical type theory 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-18 14:05 ` [HoTT] " Andrew Swan
  2 siblings, 1 reply; 18+ messages in thread
From: Andrew Pitts @ 2019-02-14 20:06 UTC (permalink / raw)
  To: Homotopy Type Theory; +Cc: Anders Mortberg, Prof. Andrew M Pitts

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.

^ permalink raw reply	[flat|nested] 18+ messages in thread

* Re: [HoTT] A unifying cartesian cubical type theory
  2019-02-14 19:04 [HoTT] A unifying cartesian cubical type theory Anders Mortberg
  2019-02-14 20:06 ` Andrew Pitts
@ 2019-02-15  8:16 ` Bas Spitters
  2019-02-15 16:32   ` Anders Mörtberg
  2019-02-18 14:05 ` [HoTT] " Andrew Swan
  2 siblings, 1 reply; 18+ messages in thread
From: Bas Spitters @ 2019-02-15  8:16 UTC (permalink / raw)
  To: Anders Mortberg; +Cc: Homotopy Type Theory

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.

^ permalink raw reply	[flat|nested] 18+ messages in thread

* Re: [HoTT] A unifying cartesian cubical type theory
  2019-02-14 20:06 ` Andrew Pitts
@ 2019-02-15 15:38   ` Anders Mörtberg
  0 siblings, 0 replies; 18+ messages in thread
From: Anders Mörtberg @ 2019-02-15 15:38 UTC (permalink / raw)
  To: Homotopy Type Theory


[-- 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 --]

^ permalink raw reply	[flat|nested] 18+ messages in thread

* Re: [HoTT] A unifying cartesian cubical type theory
  2019-02-15  8:16 ` Bas Spitters
@ 2019-02-15 16:32   ` Anders Mörtberg
  2019-02-16  0:01     ` Michael Shulman
  0 siblings, 1 reply; 18+ messages in thread
From: Anders Mörtberg @ 2019-02-15 16:32 UTC (permalink / raw)
  To: Homotopy Type Theory


[-- 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 --]

^ permalink raw reply	[flat|nested] 18+ messages in thread

* Re: [HoTT] A unifying cartesian cubical type theory
  2019-02-15 16:32   ` Anders Mörtberg
@ 2019-02-16  0:01     ` Michael Shulman
  2019-02-16  0:14       ` Steve Awodey
  0 siblings, 1 reply; 18+ messages in thread
From: Michael Shulman @ 2019-02-16  0:01 UTC (permalink / raw)
  To: Anders Mörtberg; +Cc: Homotopy Type Theory

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.

^ permalink raw reply	[flat|nested] 18+ messages in thread

* Re: [HoTT] A unifying cartesian cubical type theory
  2019-02-16  0:01     ` Michael Shulman
@ 2019-02-16  0:14       ` Steve Awodey
  2019-02-16 12:30         ` streicher
  0 siblings, 1 reply; 18+ messages in thread
From: Steve Awodey @ 2019-02-16  0:14 UTC (permalink / raw)
  To: Michael Shulman; +Cc: Anders Mörtberg, Homotopy Type Theory

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.

^ permalink raw reply	[flat|nested] 18+ messages in thread

* Re: [HoTT] A unifying cartesian cubical type theory
  2019-02-16  0:14       ` Steve Awodey
@ 2019-02-16 12:30         ` streicher
  2019-02-16 19:51           ` Thomas Streicher
  2019-02-16 21:58           ` Richard Williamson
  0 siblings, 2 replies; 18+ messages in thread
From: streicher @ 2019-02-16 12:30 UTC (permalink / raw)
  To: Steve Awodey
  Cc: Michael Shulman, "Anders Mörtberg",
	Homotopy Type Theory

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

^ permalink raw reply	[flat|nested] 18+ messages in thread

* Re: [HoTT] A unifying cartesian cubical type theory
  2019-02-16 12:30         ` streicher
@ 2019-02-16 19:51           ` Thomas Streicher
  2019-02-16 22:27             ` Steve Awodey
  2019-02-16 21:58           ` Richard Williamson
  1 sibling, 1 reply; 18+ messages in thread
From: Thomas Streicher @ 2019-02-16 19:51 UTC (permalink / raw)
  To: Steve Awodey
  Cc: Michael Shulman, "Anders Mörtberg",
	Homotopy Type Theory

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

^ permalink raw reply	[flat|nested] 18+ messages in thread

* Re: [HoTT] A unifying cartesian cubical type theory
  2019-02-16 12:30         ` streicher
  2019-02-16 19:51           ` Thomas Streicher
@ 2019-02-16 21:58           ` Richard Williamson
  2019-02-17  9:15             ` Thomas Streicher
  1 sibling, 1 reply; 18+ messages in thread
From: Richard Williamson @ 2019-02-16 21:58 UTC (permalink / raw)
  To: streicher
  Cc: Steve Awodey, Michael Shulman,
	"Anders Mörtberg",
	Homotopy Type Theory

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

^ permalink raw reply	[flat|nested] 18+ messages in thread

* Re: [HoTT] A unifying cartesian cubical type theory
  2019-02-16 19:51           ` Thomas Streicher
@ 2019-02-16 22:27             ` Steve Awodey
  2019-02-17  9:43               ` Thomas Streicher
  0 siblings, 1 reply; 18+ messages in thread
From: Steve Awodey @ 2019-02-16 22:27 UTC (permalink / raw)
  To: Thomas Streicher
  Cc: Michael Shulman, Anders Mörtberg, Homotopy Type Theory


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

^ permalink raw reply	[flat|nested] 18+ messages in thread

* Re: [HoTT] A unifying cartesian cubical type theory
  2019-02-16 21:58           ` Richard Williamson
@ 2019-02-17  9:15             ` Thomas Streicher
  2019-02-17 13:49               ` Richard Williamson
  0 siblings, 1 reply; 18+ messages in thread
From: Thomas Streicher @ 2019-02-17  9:15 UTC (permalink / raw)
  To: Richard Williamson
  Cc: Steve Awodey, Michael Shulman,
	"Anders Mörtberg",
	Homotopy Type Theory

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

^ permalink raw reply	[flat|nested] 18+ messages in thread

* Re: [HoTT] A unifying cartesian cubical type theory
  2019-02-16 22:27             ` Steve Awodey
@ 2019-02-17  9:43               ` Thomas Streicher
  2019-02-17 14:14                 ` Licata, Dan
  0 siblings, 1 reply; 18+ messages in thread
From: Thomas Streicher @ 2019-02-17  9:43 UTC (permalink / raw)
  To: Steve Awodey
  Cc: Michael Shulman, Anders Mörtberg, Homotopy Type Theory

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

^ permalink raw reply	[flat|nested] 18+ messages in thread

* Re: [HoTT] A unifying cartesian cubical type theory
  2019-02-17  9:15             ` Thomas Streicher
@ 2019-02-17 13:49               ` Richard Williamson
  0 siblings, 0 replies; 18+ messages in thread
From: Richard Williamson @ 2019-02-17 13:49 UTC (permalink / raw)
  To: Thomas Streicher
  Cc: Steve Awodey, Michael Shulman,
	"Anders Mörtberg",
	Homotopy Type Theory

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.

^ permalink raw reply	[flat|nested] 18+ messages in thread

* Re: [HoTT] A unifying cartesian cubical type theory
  2019-02-17  9:43               ` Thomas Streicher
@ 2019-02-17 14:14                 ` Licata, Dan
  0 siblings, 0 replies; 18+ messages in thread
From: Licata, Dan @ 2019-02-17 14:14 UTC (permalink / raw)
  To: Homotopy Type Theory

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.

^ permalink raw reply	[flat|nested] 18+ messages in thread

* [HoTT] Re: A unifying cartesian cubical type theory
  2019-02-14 19:04 [HoTT] A unifying cartesian cubical type theory Anders Mortberg
  2019-02-14 20:06 ` Andrew Pitts
  2019-02-15  8:16 ` Bas Spitters
@ 2019-02-18 14:05 ` Andrew Swan
  2019-02-18 15:31   ` Anders Mörtberg
  2 siblings, 1 reply; 18+ messages in thread
From: Andrew Swan @ 2019-02-18 14:05 UTC (permalink / raw)
  To: Homotopy Type Theory


[-- 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 --]

^ permalink raw reply	[flat|nested] 18+ messages in thread

* [HoTT] Re: A unifying cartesian cubical type theory
  2019-02-18 14:05 ` [HoTT] " Andrew Swan
@ 2019-02-18 15:31   ` Anders Mörtberg
  2019-06-16 16:04     ` Anders Mörtberg
  0 siblings, 1 reply; 18+ messages in thread
From: Anders Mörtberg @ 2019-02-18 15:31 UTC (permalink / raw)
  To: Homotopy Type Theory


[-- 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 --]

^ permalink raw reply	[flat|nested] 18+ messages in thread

* [HoTT] Re: A unifying cartesian cubical type theory
  2019-02-18 15:31   ` Anders Mörtberg
@ 2019-06-16 16:04     ` Anders Mörtberg
  0 siblings, 0 replies; 18+ messages in thread
From: Anders Mörtberg @ 2019-06-16 16:04 UTC (permalink / raw)
  To: Homotopy Type Theory


[-- 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 --]

^ permalink raw reply	[flat|nested] 18+ messages in thread

end of thread, other threads:[~2019-06-16 16:04 UTC | newest]

Thread overview: 18+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2019-02-14 19:04 [HoTT] A unifying cartesian cubical type theory 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 ` [HoTT] " Andrew Swan
2019-02-18 15:31   ` Anders Mörtberg
2019-06-16 16:04     ` Anders Mörtberg

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