A unifying cartesian cubical type theory

[Anders Mortberg]

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

[Andrew Pitts]

On Thu, 14 Feb 2019 at 19:05, Anders Mortberg <andersm...@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

[Bas Spitters]

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

> --
> 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 HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Anders Mörtberg]

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

 

[Anders Mörtberg]

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

> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsub...@googlegroups.com.

[Michael Shulman]

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"?

>> > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@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 HomotopyTypeThe...@googlegroups.com.

[Steve Awodey]

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

[stre...@mathematik.tu-darmstadt.de]

> 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

[Thomas Streicher]

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

[Richard Williamson]

> 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

[Steve Awodey]

> On Feb 16, 2019, at 2:51 PM, Thomas Streicher <stre...@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
>

[Thomas Streicher]

> 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

[Thomas Streicher]

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

[Richard Williamson]

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

[Licata, Dan]

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)

[Andrew Swan]

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

[Anders Mörtberg]

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

[Anders Mörtberg]

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