Infinitely and finitely coherent equivalences and infinitely and finitely coherently invertible maps

[EgbertRijke]

This PR is part of the diploma project of @maybemabeline.

We add some new definitions to the library, and we found some ways to express infinite coherence.

[fredrik-bakke]

This is super cool! I will review it when I have a little more energy. Did you consider the definition of ∞-path-split maps also?

[EgbertRijke]

Sure, it is very unfinished at the moment, so there is absolutely no rush with a review.

[fredrik-bakke]

Ah, okay. I will hold off on a review then 🙂

[EgbertRijke]

I'm gonna need limits of inverse sequential diagrams to make progress, but I don't want to do that now. So I declare this PR ready for review.

[fredrik-bakke]

...we do have them

[fredrik-bakke]

but maybe there's something more you had in mind?

[EgbertRijke]

I know that we have them, but this PR is becoming a serious amount of work if I want to formalize everything that I am ready to claim informally. It will be a longer project, and it is better keep this PR short. I should work on spans too.

[fredrik-bakke]

Okey dokey.

[fredrik-bakke]

Here are some things one can prove about the transpose-eq hypothesis. Indeed, it is equivalent to having a retraction. Maybe one can prove this without funext?

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (g : B → A)
  where

  transpose-eq-is-retraction :
    g ∘ f ~ id → {x : B} {y : A} → x ＝ f y → g x ＝ y
  transpose-eq-is-retraction H {.(f y)} {y} refl = H y

  transpose-eq-is-retraction' :
    g ∘ f ~ id → {x : A} {y : B} → f x ＝ y → x ＝ g y
  transpose-eq-is-retraction' H {x} {.(f x)} refl = inv (H x)

  is-retraction-transpose-eq :
    ({x : B} {y : A} → x ＝ f y → g x ＝ y) → g ∘ f ~ id
  is-retraction-transpose-eq H x = H refl

  is-retraction-transpose-eq' :
    ({x : A} {y : B} → f x ＝ y → x ＝ g y) → g ∘ f ~ id
  is-retraction-transpose-eq' H x = inv (H refl)

  is-injective-has-transpose-eq :
    ({x : B} {y : A} → x ＝ f y → g x ＝ y) → is-injective f
  is-injective-has-transpose-eq H =
    is-injective-retraction f (g , is-retraction-transpose-eq H)

  is-retraction-is-retraction-transpose-eq :
    is-retraction-transpose-eq ∘ transpose-eq-is-retraction ~ id
  is-retraction-is-retraction-transpose-eq H = refl

  is-section-is-retraction-transpose-eq :
    transpose-eq-is-retraction ∘ is-retraction-transpose-eq ~ id
  is-section-is-retraction-transpose-eq H =
    eq-multivariable-htpy-implicit 2 (λ x y → eq-htpy (λ where refl → refl))

[EgbertRijke]

Here are some things one can prove about the transpose-eq hypothesis. Indeed, it is equivalent to having a retraction. Maybe one can prove this without funext?

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (g : B → A)
  where

  transpose-eq-is-retraction :
    g ∘ f ~ id → {x : B} {y : A} → x ＝ f y → g x ＝ y
  transpose-eq-is-retraction H {.(f y)} {y} refl = H y

  transpose-eq-is-retraction' :
    g ∘ f ~ id → {x : A} {y : B} → f x ＝ y → x ＝ g y
  transpose-eq-is-retraction' H {x} {.(f x)} refl = inv (H x)

  is-retraction-transpose-eq :
    ({x : B} {y : A} → x ＝ f y → g x ＝ y) → g ∘ f ~ id
  is-retraction-transpose-eq H x = H refl

  is-retraction-transpose-eq' :
    ({x : A} {y : B} → f x ＝ y → x ＝ g y) → g ∘ f ~ id
  is-retraction-transpose-eq' H x = inv (H refl)

  is-injective-has-transpose-eq :
    ({x : B} {y : A} → x ＝ f y → g x ＝ y) → is-injective f
  is-injective-has-transpose-eq H =
    is-injective-retraction f (g , is-retraction-transpose-eq H)

  is-retraction-is-retraction-transpose-eq :
    is-retraction-transpose-eq ∘ transpose-eq-is-retraction ~ id
  is-retraction-is-retraction-transpose-eq H = refl

  is-section-is-retraction-transpose-eq :
    transpose-eq-is-retraction ∘ is-retraction-transpose-eq ~ id
  is-section-is-retraction-transpose-eq H =
    eq-multivariable-htpy-implicit 2 (λ x y → eq-htpy (λ where refl → refl))

Nice! We already have transpose-eq-retraction and transpose-eq-section in the library. The entries you mention here naturally belong to retractions and to sections (for the duals that you didn't write out).

[fredrik-bakke]

Nice! We already have transpose-eq-retraction and transpose-eq-section in the library. The entries you mention here naturally belong to retractions and to sections (for the duals that you didn't write out).

Feel free to add them to this PR without crediting me. 😄

[fredrik-bakke]

Feel free to add them to this PR without crediting me. 😄

Never mind. I'll add them in #1024

[EgbertRijke]

I am factoring out transpositions of identifications along retractions and sections in this pull request. I don't quite understand why it was considered a nontrivial task, because I'm just moving some entries to new files.

[fredrik-bakke]

I am factoring out transpositions of identifications along retractions and sections in this pull request. I don't quite understand why it was considered a nontrivial task, because I'm just moving some entries to new files.

I think the contents of transposing-identifications-along-equivalences should depend on the contents of transposing-identifications-along-sections and transposing-identifications-along-retractions, as it canonically makes a case analysis between the two.

[EgbertRijke]

That's a separate good idea, but it was not what I was asking for when I suggested to simply put the entries you already formalised in files analogous to transposition-identifications-along-equivalences.

[EgbertRijke]

But yes, I like that idea :)

[EgbertRijke]

I addressed all the comments. Thank you for the thorough review @fredrik-bakke!

[fredrik-bakke]

Since this is part of @maybemabeline's diploma project, do you intend to add her as a co-author on this PR?

[EgbertRijke]

Sure! Could you do that?:)

[EgbertRijke]

Thanks for thinking about that!

[fredrik-bakke]

Usually, it requires the co-author's e-mail I think. We can see if it works by using the GitHub handle, e.g.

Co-authored-by: maybemabeline <maybemabeline>

Or, if you have the e-mail she uses with her GitHub account, simply add

Co-authored-by: maybemabeline <the@email.com>

to the commit message.

[maybemabeline]

Thank you for thinking of me :) I didn't have anything to do with this specific PR, but this hierarchy of coherence conditions was something that me and Egbert were thinking about a few months ago. The email I use with this account is mabeltree2@gmail.com.