Intro and elim rules for limits and colimits

[JasonGross]

I'm trying to write intro and elim rules for limits and colimits. After much pain and time, I wrote intro and elim rules for colimits.* I expected that I would be able to get limits for free, because I've defined limits to be terminal morphisms, which are defined to be initial morphisms in the opposite category, and colimits are defined to be initial morphisms. However, Coq informed me that the types didn't unify, because the type (D -> C)ᵒᵖ is not the same category as Dᵒᵖ -> Cᵒᵖ, and my colimits of opposite functors talk about diagrams of the form Dᵒᵖ -> Cᵒᵖ, while my limits only know about diagrams of the form (D -> C)ᵒᵖ. If C is a category, then these categories are equal, because there's a functor ᵒᵖ : (D -> C)ᵒᵖ -> (Dᵒᵖ -> Cᵒᵖ) which has an inverse functor (it's self-inverse, but only if we have eta for records; otherwise we need to pull tricks with stripping off ᵒᵖs), and moreover (up to eta for records) these functors are judgmentally inverses. If we assume univalence, then, even without assuming that C is univalent, I think we get that these are equal precategories, because we can use univalence to prove that the types of objects, morphisms, etc, are all equal. But they're not judgmentally equal, and this makes me sad. Because it means that I'll have to either cast things across a non-computational equality, or I'll have to use the ᵒᵖ functor and the functor that it induces between comma categories and the fact that functors preserve initial and terminal objects to convert my colimits of opposite functors into limits, and it'll be a big hassle. Does anyone have ideas for how to fix this (how to classical category theorists deal with the fact that (C -> D)ᵒᵖ isn't the same as Cᵒᵖ -> Dᵒᵖ?), or am I stuck?

If this is the wrong venue for this question, where should I ask it? (The HoTT mailing list? The category theory mailing list? nCafe? mathoverflow?)

*My current work is at https://github.com/JasonGross/HoTT/blob/limit-intro-rule/theories/categories/Limits/IntroElim.v#L347 If you run Coq to the highlighted line, it will show you the difference in types I'm talking about.

[mikeshulman]

how do classical category theorists deal with the fact that (C -> D)ᵒᵖ isn't the same as Cᵒᵖ -> Dᵒᵖ?

Surely you can guess the answer to that: we identify them by abuse of notation. (-:

[JasonGross]

Is there any hope of having them be judgmentally equal in a proof assistant? (Perhaps by some special handling of univalence for isomorphisms which are guaranteed to be unique by parametricity? But then I might be worried about whether x = y and y = x are going to get identified, and if this would force all paths to be their own inverses.)

[mikeshulman]

I am somewhat dubious; currently my inclination is towards fewer judgmental equalities rather than more. But that sort of question is an important research direction to pursue.

[JasonGross]

Why fewer rather than more? I see that it makes it less likely for you to run in to inconsistencies, and easier to analyze metatheoretically, but I feel like it's nice to have as many judgmental equalities as you possibly can, because explicitly transporting over paths is painful, especially when you have to iterate it to get higher coherences (and especially especially when not having an equality be judgmental means you have to introduce applications of funext, and then figure out how to make them go away when you want to prove higher coherences).

[mikeshulman]

Well, it makes it less likely for you to run in to inconsistencies, and easier to analyze metatheoretically. (-: It also may make it easier (or, perhaps, possible) to construct sheaf and realizability models. It's true that explicitly transporting over paths is currently painful, but one might hope that advances in automation could assist with that in other ways than by making more equalities judgmental.

[JasonGross]

I'm attracted to the view that any decidable equivalence relation should be a candidate for judgmental equality (possibly subject to a few restrictions), as suggested at the bottom of page 9 of http://coq.inria.fr/files/coq5-slides-herbelin.pdf. Is there any work on finding frameworks for constructing models for arbitrary decidable equivalence relations used as judgmental equality?

[mikeshulman]

I don't know what that means.

[JasonGross]

If you mean my first sentence, I think http://hal.archives-ouvertes.fr/docs/00/49/77/94/PDF/lics-2010.pdf might be a good relevant paper. (Unless there's something more specific about it that's confusing.) If you mean my second sentence, I guess I was wondering if there's any hope of having a recipe for constructing sheaf or realizability (or other kinds of) models for things like CoqMT or other theories in that direction.

[andrejbauer]

Jeremy Avigad, Chris Kapulkin and @peterlefanulumsdaine have implemented limits on top of the HoTT library. Maybe there can be some code resuse?

[spitters]

Vladimir is trying to do something similar. http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/HTS_slides.pdf

On Wed, Dec 11, 2013 at 5:54 AM, Jason Gross notifications@github.comwrote:

I'm attracted to the view that any decidable equivalence relation should be a candidate for judgmental equality (possibly subject to a few restrictions), as suggested at the bottom of page 9 of http://coq.inria.fr/files/coq5-slides-herbelin.pdf. Is there any work on finding frameworks for constructing models for arbitrary decidable equivalence relations used as judgmental equality?

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/HoTT/issues/284#issuecomment-30293840 .

[mikeshulman]

I think AKL implemented homotopy limits of types, whereas here we are talking about limits in an arbitrary 1-category. The only overlap is if the types are sets, then their homotopy limits are limits in the 1-category Set.

[vladimirias]

On Dec 11, 2013, at 7:41 AM, Bas Spitters notifications@github.com wrote:

Vladimir is trying to do something similar. http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/HTS_slides.pdf

On Wed, Dec 11, 2013 at 5:54 AM, Jason Gross notifications@github.comwrote:

I'm attracted to the view that any decidable equivalence relation should be a candidate for judgmental equality (possibly subject to a few restrictions), as suggested at the bottom of page 9 of http://coq.inria.fr/files/coq5-slides-herbelin.pdf. Is there any work on finding frameworks for constructing models for arbitrary decidable equivalence relations used as judgmental equality?

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/HoTT/issues/284#issuecomment-30293840 .

— Reply to this email directly or view it on GitHub.

Actually what we are trying to do with two equalities is different. The idea of making any (context dependent) decidable equivalence relation into definitional equality is semantically strange.

For example in the context X : Type, is : iscontr X the usual path-equality on X is decidable (since any two objects of type X are path-equal). However, the univalent model of X is quite likely to be a large simplicial set with many points and taking all of those to be strictly equal should I think lead to a contradiction.

V.

[mikeshulman]

"semantically strange, and probably contradictory" was my reaction as well. Perhaps, though, the "decidable equivalence relations" under consideration are not actually internal to the theory, but rather implemented in some ML or tactic language outside of Coq? I wasn't able to figure this out from Jason's link. That would be semantically even stranger, but would require some other sort of argument to yield a contradiction. Or maybe I'm misunderstanding entirely.

[peterlefanulumsdaine]

On Wed, Dec 11, 2013 at 9:34 AM, Mike Shulman notifications@github.comwrote:

I think AKL implemented homotopy limits of types, whereas here we are talking about limits in an arbitrary 1-category. The only overlap is if the types are sets, then their homotopy limits are limits in the 1-category Set.

Just to confirm: yep, this is an accurate description of what we did, plus the fact that in order to work with arbitrary types without coherence issues, we restricted to limits over graphs. It can be found at https://github.com/peterlefanulumsdaine/hott-limits.

–p.

[peterlefanulumsdaine]

On Wed, Dec 11, 2013 at 10:30 AM, Vladimir Voevodsky < notifications@github.com> wrote:

On Dec 11, 2013, at 7:41 AM, Bas Spitters notifications@github.com wrote:

Actually what we are trying to do with two equalities is different. The idea of making any (context dependent) decidable equivalence relation into definitional equality is semantically strange.

For example in the context X : Type, is : iscontr X the usual path-equality on X is decidable (since any two objects of type X are path-equal). However, the univalent model of X is quite likely to be a large simplicial set with many points and taking all of those to be strictly equal should I think lead to a contradiction.

Yes, it does. As has been discussed here before, if any contractible type is definitionally contractible, then by applying this to types of the form { x : X & x = x0 }, you can recover the reflection rule that propositional implies definitional equality. This implies that all types are hsets, and so is inconsistent with Univalence.

–p.

[mikeshulman]

@peterlefanulumsdaine - maybe that contradiction would be a good exercise to put in the book, since it seems to come up again and again.

[vladimirias]

On Dec 11, 2013, at 11:19 AM, Peter LeFanu Lumsdaine wrote:

On Wed, Dec 11, 2013 at 10:30 AM, Vladimir Voevodsky < notifications@github.com> wrote:

On Dec 11, 2013, at 7:41 AM, Bas Spitters notifications@github.com wrote:

Actually what we are trying to do with two equalities is different. The idea of making any (context dependent) decidable equivalence relation into definitional equality is semantically strange.

For example in the context X : Type, is : iscontr X the usual path-equality on X is decidable (since any two objects of type X are path-equal). However, the univalent model of X is quite likely to be a large simplicial set with many points and taking all of those to be strictly equal should I think lead to a contradiction.

Yes, it does. As has been discussed here before, if any contractible type is definitionally contractible, then by applying this to types of the form { x : X & x = x0 }, you can recover the reflection rule that propositional implies definitional equality. This implies that all types are hsets, and so is inconsistent with Univalence.

–p. — Reply to this email directly or view it on GitHub.

Cool! V.

[mikeshulman]

The contradiction doesn't even require allowing context-dependent equivalence relations. We can give a specific type in the empty context, namely { X : Type & X = 2 }, and a specific equivalence relation on that type, namely the full one, such that if that equivalence relation entails judgmental equality then univalence is false.

[mikeshulman]

Can this be closed?

[JasonGross]

My initial question is still open, but it's more likely that this is an open research question, or a far-out hope, and perhaps not appropriate as an open issue here.

[mikeshulman]

Yeah, it's a bit unclear, but it might be better to reserve the open issues on this project for software-type issues rather than math research questions.

[mikeshulman]

For open math problems there is http://ncatlab.org/homotopytypetheory/show/open+problems

[JasonGross]

I've added a bullet point there under "Higher algebra and higher category theory", with a link to this issue.