Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Intro and elim rules for limits and colimits #284

Closed
JasonGross opened this issue Dec 11, 2013 · 23 comments

Comments

@JasonGross
Copy link
Contributor

commented Dec 11, 2013

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

This comment has been minimized.

Copy link
Contributor

commented Dec 11, 2013

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

This comment has been minimized.

Copy link
Contributor Author

commented Dec 11, 2013

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

This comment has been minimized.

Copy link
Contributor

commented Dec 11, 2013

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

This comment has been minimized.

Copy link
Contributor Author

commented Dec 11, 2013

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

This comment has been minimized.

Copy link
Contributor

commented Dec 11, 2013

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

This comment has been minimized.

Copy link
Contributor Author

commented Dec 11, 2013

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

This comment has been minimized.

Copy link
Contributor

commented Dec 11, 2013

I don't know what that means.

@JasonGross

This comment has been minimized.

Copy link
Contributor Author

commented Dec 11, 2013

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

This comment has been minimized.

Copy link
Member

commented Dec 11, 2013

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

@spitters

This comment has been minimized.

Copy link
Member

commented Dec 11, 2013

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//issues/284#issuecomment-30293840
.

@mikeshulman

This comment has been minimized.

Copy link
Contributor

commented Dec 11, 2013

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

This comment has been minimized.

Copy link

commented Dec 11, 2013

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

This comment has been minimized.

Copy link
Contributor

commented Dec 11, 2013

"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

This comment has been minimized.

Copy link
Contributor

commented Dec 11, 2013

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

This comment has been minimized.

Copy link
Contributor

commented Dec 11, 2013

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

This comment has been minimized.

Copy link
Contributor

commented Dec 11, 2013

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

@vladimirias

This comment has been minimized.

Copy link

commented Dec 11, 2013

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

This comment has been minimized.

Copy link
Contributor

commented Dec 11, 2013

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

This comment has been minimized.

Copy link
Contributor

commented Nov 10, 2014

Can this be closed?

@JasonGross

This comment has been minimized.

Copy link
Contributor Author

commented Nov 10, 2014

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

This comment has been minimized.

Copy link
Contributor

commented Nov 10, 2014

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

This comment has been minimized.

Copy link
Contributor

commented Nov 10, 2014

@JasonGross

This comment has been minimized.

Copy link
Contributor Author

commented Nov 10, 2014

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

@JasonGross JasonGross closed this Nov 10, 2014

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
6 participants
You can’t perform that action at this time.