Transport-split and preunivalent type families

[fredrik-bakke]

This is the follow-up PR to #1009.

Summary

• Transport-split type families are type families B such that equiv-tr B admits fiberwise sections
  • This notion is equivalent to univalent type families by a corollary of the fundamental theorem of identity types
• Some infrastructure and basic lemmas for univalent type families
• Preunivalent type families are type families B such that equiv-tr B is a fiberwise embedding
  • 3-for-2 for preunivalent type families using the preunivalence axiom
  • Some other infrastructure
• Fin is preunivalent

Future work

• Closure properties for univalent and preunivalent type families

Co-authored-by: Egbert Rijke [email protected]

[fredrik-bakke]

The terminology "equivalence injective type family" is still a bit subobtimal, because it is so close to suggesting the definition of injective type family that I'm not really fond of. So I've been thinking about whether there could be more interesting concepts lurking under here.

The family of maps in equivalence injective type families are converse to the transport maps tr B : (x = y) -> (B x <~> B y). The main example of equivalence injective type families is the family Fin, but for Fin something more holds: this map has a section. So how about abolishing any suggestion of "injective type family" altogether, and call these type families transport-split?

In other words, a type family B would be called transport-split if the map tr B : (x = y) -> (B x <~> B y) has a section for each x y : A. In particular, if a type family is transport split, we have a family of maps (B x <~> B y) -> (x = y) indexed by x y : A, and moreover, this family of maps sends id-equiv (B x) to refl.

Originally posted by @EgbertRijke in #1009 (comment)

What you're saying here seems to suggest that Fin is a univalent type family, i.e. that (n ＝ m) ≃ (Fin n ≃ Fin m), since every transport-split type family is univalent. However, this cannot be true as (n ＝ m) is a proposition while (Fin n ≃ Fin m) is not for n = m > 1. Instead, is-equivalence-injective-Fin is only a retraction of equiv-tr, and not a section.

[EgbertRijke]

The terminology "equivalence injective type family" is still a bit subobtimal, because it is so close to suggesting the definition of injective type family that I'm not really fond of. So I've been thinking about whether there could be more interesting concepts lurking under here.
The family of maps in equivalence injective type families are converse to the transport maps tr B : (x = y) -> (B x <~> B y). The main example of equivalence injective type families is the family Fin, but for Fin something more holds: this map has a section. So how about abolishing any suggestion of "injective type family" altogether, and call these type families transport-split?
In other words, a type family B would be called transport-split if the map tr B : (x = y) -> (B x <~> B y) has a section for each x y : A. In particular, if a type family is transport split, we have a family of maps (B x <~> B y) -> (x = y) indexed by x y : A, and moreover, this family of maps sends id-equiv (B x) to refl.

Originally posted by @EgbertRijke in #1009 (comment)

What you're saying here seems to suggest that Fin is a univalent type family, i.e. that (n ＝ m) ≃ (Fin n ≃ Fin m), since every transport-split type family is univalent. However, this cannot be true as (n ＝ m) is a proposition while (Fin n ≃ Fin m) is not for n = m > 1. Instead, is-equivalence-injective-Fin is only a retraction of equiv-tr, and not a section.

Oh! fundamental-theorem-id-section worked? I deleted that comment because I made it late at night and thought I was making a mistake. That's nice!

I certainly did not intend to suggest that Fin is a univalent type family.

[fredrik-bakke]

Oh! fundamental-theorem-id-section worked? I deleted that comment because I made it late at night and thought I was making a mistake. That's nice!

Yes :) Luckily you couldn't hide the comment from me

[fredrik-bakke]

Sorry for the accusatory tone of my message. I just wanted to clarify as I was confused for a bit. This begs the question if we should care about type families such that equiv-tr B admits retractions however, which is equivalent to your observation that is-equivalence-injective-Fin refl = id-equiv I believe

[EgbertRijke]

Sorry for the accusatory tone of my message. I just wanted to clarify as I was confused for a bit. This begs the question if we should care about type families such that equiv-tr B admits retractions however, which is equivalent to your observation that is-equivalence-injective-Fin refl = id-equiv I believe

I see, yes I must have misspoken when I said section/retraction and perhaps I meant the other. I'm glad you were able to sort it out, and the proof that transport-split families are univalent is certainly worthy of being recorded in the library.

[fredrik-bakke]

Here's something I think may be possible to prove using preunivalence without using univalence: type-Set is a preunivalent type family.

[fredrik-bakke]

Here's something I think may be possible to prove using preunivalence without using univalence: type-Set is a preunivalent type family.

Okay, that was too easy. I bet it can be done without univalence or preunivalence. Anyway, I'll leave that for another time.

[fredrik-bakke]

Alright, I'm opening this PR up for review now. I believe you should have co-authorship over this PR, Egbert, given the ideas you contributed to it. Thank you for that!

[EgbertRijke]

This is a PR of the highest quality! Thank you Fredrik!

[fredrik-bakke]

Thank you for the generous words! I believe I've resolved all of your comments now.

[EgbertRijke]

Thank you for including me as a coauthor btw!