Some extensions of the fundamental theorem of identity types

[fredrik-bakke]

So my recent work on π₀-trivial types got me looking for other applications of this concept, and here's one. Essentially, this PR gives an alternative phrasing of the extended fundamental theorem of identity types such that the assumption of inhabitedness/pointedness on the base type A is not needed.

Edit: the scope of this PR has grown since the above description was written.

Summary

• Unbased version of the extended fundamental theorem of identity types
• Structured equality duality
• Strong preunivalence
• Strengthen definition of preunivalent categories
• Weaken assumptions on the type theoretic Yoneda lemma

[fredrik-bakke]

Wait a second, I'm doing a stupid

[EgbertRijke]

Do you use "structure" in the same way here as in the structure identity principle?

[fredrik-bakke]

No, here structure is used differently. Here structure is what the theorem is used to construct, not to characterize.

[EgbertRijke]

No, here structure is used differently. Here structure is what the theorem is used to construct, not to characterize.

Probably you should be very careful with terminology then. The title "fundamental theorem of identity types for structures" is suggestive of a theorem related to the structure identity principle. Could you think about phrasing your work in a less ambiguous way?

[fredrik-bakke]

No, here structure is used differently. Here structure is what the theorem is used to construct, not to characterize.

Probably you should be very careful with terminology then. The title "fundamental theorem of identity types for structures" is suggestive of a theorem related to the structure identity principle. Could you think about phrasing your work in a less ambiguous way?

Thanks, that is good to keep in mind! Sorry, this PR was originally something different, but then I realized I was thinking about things wrong so I need to think a little more before it is ready

[fredrik-bakke]

As an aside, this PR made me realize there's a canonical strengthening of preunivalence one might ought to consider, so stay tuned for that :)

[fredrik-bakke]

I figured out what the proper statement for the extended fundamental theorem should be, so we're back in business 😁

[fredrik-bakke]

Okay, now I think this PR is ready to be looked at. I renamed the previous "fundamental theorem of identity types for structures" to "structured equality duality", but that's just a name I'm making up so let me know what you feel about it. I also did some other things, see the PR main body.

[EgbertRijke]

Can you explain in this idea section what it means to "transfer along equivalences"? Is it related to transport along equivalences, for which we have a file?

[fredrik-bakke]

Yes, it's the same, just that we add it as a hypothesis to avoid univalence, since usually this property is independent of univalence

[EgbertRijke]

I meant, can you mention in the ## Idea section what you meant with transfer along equivalences. If I didn't get it, then we can be sure that others would be puzzled too.

[fredrik-bakke]

Thanks for the clarification! I thought my previous explanation would be sufficient, but realize now that it clearly wasn't. It should be fixed now.

[EgbertRijke]

I'm definitely open to using the name "equality duality", but could you explain your reasoning behind this name a bit more (in the idea section)? Why can we think of this as a duality principle? Many duality principles establish a correspondence between something covariant and something contravariant. Is that the case here too?

[fredrik-bakke]

I'll think about it!

[fredrik-bakke]

Alright, so let me try to justify the use of the word duality here. I'd like to try and formulate that in some sense both sides are straightened and unstraightened, but in opposite ways.

On the left-hand side, we have binary families of maps into B f : (x y : A) -> (x = y) -> B y, something one might view as a straightened thing, and these families of maps have P-structures on their fibers, something unstraightened. On the right-hand side, we're considering Σ A B, the literal unstraightening of B, but we are considering structures on the binary family of identity types over it, something more straightened in my mind. So we're doing a trade to have straightening in one direction for unstraightening in the other. This feels very duality-e to me.

I would like to say though, that this is also just a generalization of the Regensburg extension of the fundamental theorem, and therefore it might very well be more appropriate to give it a name closer to it. On the other hand, the fundamental theorem of identity types is about based identity types, while "structured equality duality" is not.

[fredrik-bakke]

Sorry that I'm being very loose in my arguments, I think I'll need to let the question rest for a little while until I find a good explanation or a better idea for a name.

[EgbertRijke]

Suggested change

	The main function of _preunivalence_ is to serve as a common generalization of
	The main purpose of _preunivalence_ is to serve as a common generalization of

[EgbertRijke]

In situations like this, where you want to redefine something with a different axiom, it is a question whether it is a good idea to replace the old definition, or whether to keep a version of it around while also defining the new version.

I think it could be a good idea to keep the old version around under some name, because it is clearly a condition that could come up sometimes, and under the current proposal of this PR we won't have that old definition in the library anymore.

[fredrik-bakke]

While I'd currently like to think of the previous definition as "deprecated", I don't have a good rebuttal for the proposal to keep it. However, I'd like to give it a name that makes it clear it is an inferior condition. Perhaps we can call it "quasipreunivalent" or "weakly preunivalent"?

[EgbertRijke]

Calling these categories "weakly preunivalent" creates a strange situation though, because weak preunivalent categories would then satisfy the preunivalence axiom, and preunivalent categories would satisfy the strong preunivalence axiom. This can only create confusion.

I'd propose keeping the name "Preunivalent categories" for the old concept, and indeed not changing the name "preunivalence" in foundation either. Preunivalence is a somewhat established concept, that other people like Martin Escardo, Evan Cavallo, and Peter Lumsdaine are also interested in. Then we could name the new concept "Strongly preunivalent categories", which is in line with the name for the new axiom that you came up with.

That's quite a mouthful, but it could be an advantage. If people don't like the name "strongly preunivalent category" they have an obvious alternative: Bakke categories :)

[fredrik-bakke]

Fiiiiine, we'll call them strongly preunivalent. Is it okay if we remove most mentions of preunivalent categories over strongly preunivalent categories though? The preunivalence axiom (for all types) has the advantage over preunivalence for categories, AFAIK, that one can metatheoretically prove that id-equiv : {l : Level} {X : UU l} -> X ≃ X is the only type-polymorphic function of this signature, while for categories it is possible that one indeed has multiple families of morphisms of type (x : obj C) -> iso C x x.

[EgbertRijke]

Yes, that's fine. Thank you so much for doing that.

Could you also include some discussion of why you think the stronger version has advantages? You've clearly thought deeply about these conditions and I could definitely learn from it if you'd write it down carefully.