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]

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]

Looks good to me!

[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 <[email protected]>

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 [email protected].