The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

It's proved. HoTT is the only place I know to get lemmas about equality from 
so that's what I used, but this is axiom less so can be done without HoTT too.

Thought process:
- eq_rect is complicated, let's turn it into transport to simplify the goal
  this worked but is not actually useful in the end
- maybe there's a fancy destruct which will work (simple proofs about 
equality are all about the well chosen destruct)
  this went nowhere fast
- maybe I can construct a counterexample using univalence on boolean negation
  obviously this couldn't work
- this looks like the incomplete IsEquiv from HoTT where we can construct 
some fancy equality proofs to get the full IsEquiv stuff
  let's look at the construction to see if I get any ideas
  a bit of messing about then leads to the solution

Gaëtan Gilbert

On 10/10/2020 08:11, Talia Ringer wrote:
> Hello friends,
>
> I got nerd sniped this morning on a proof task I've been at for like 11 
> hours. Most of the proof obligations are done now, but I ended up stuck at 
> one particular proof obligation that I'm not sure how to solve, or if it is 
> solvable in general. But also I need to work on job applications and normal 
> last year of grad school things, and I haven't eaten dinner. So if you help 
> me out with this one proof obligation, I'll give you appropriate credit and 
> also get you a beer or dessert.
>
> For real. I don't have technical mentors or local expertise to consult.
>
> Essentially, I have two types:
>
>     A : Type
>
>     B : Type
>
> that are equivalent:
>
>     f : A -> B
>
>     g : B -> A
>     section : forall a, g (f a) = a.
>     retraction : forall b, f (g b) = b.
>
>
> I know literally nothing else about my types or my equivalence. *I want to 
> know if it is possible to solve this proof obligation:*
>
>     *P : B -> Type
>     a : A
>     f0 : forall a : A, P (f a)
>     ______________________________________(1/1)
>     eq_rect (f (g (f a))) P (f0 (g (f a))) (f a) (retraction (f a)) = f0 a*
>
>
> (I have already solved this proof obligation:
>
>     a : A
>     ______________________________________(1/1)
>     eq_rect (f (g (f a))) (fun _ : B => A) (g (f a)) (f a) (retraction (f a)) 
> = a
>
> Literally just "rewrite retraction. apply section." works. But that didn't 
> help me, and I also couldn't get Coq to use the same tactics.)
>
> I can't figure out whether this is me being really bad at equalities of 
> equalities and dependent rewrites, or whether there is something we must know 
> about A, B, or our equivalence for this to hold, or whether there is an 
> additional axiom we must assume for this to hold in general. And it's 11:00 
> PM and I haven't eaten dinner, so time to ask you all:
>
>   * Is this provable? If so, how? (And why am I so bad at equalities of 
> equalities?)
>   * If it is not, can you explain why?
>   * Is there anything I could assume about A and B to make it provable?
>   * Is there anything I could assume about f, g, section, or retraction to 
> make it provable?
>
> Hopefully someone else finds this fun, too. Or really likes beer.
>
> Talia
From HoTT Require Import Basics.Overture Basics.PathGroupoids.

Section S.
  Context
    (A : Type)
    (B : Type)
    (f : A -> B)
    (g : B -> A)
    (section : forall a, g (f a) = a)
    (retraction : forall b, f (g b) = b).

  (* Taken from https://github.com/HoTT/HoTT/blob/1977b2be2ff7d8eaee8ffc2687c94acfe0d498d1/theories/Basics/Equivalences.v#L130
     They're Let in a section so we have to redefine them. *)
  Definition section' x :=
    ap g (ap f (section x)^)  @  ap g (retraction (f x))  @  section x.

  Lemma is_adjoint' (a : A) : retraction (f a) = ap f (section' a).
  Proof.
    unfold section'.
    apply moveR_M1.
    repeat rewrite ap_pp, concat_p_pp; rewrite <- ap_compose.
    rewrite (concat_pA1 (fun b => (retraction b)^) (ap f (section a)^)).
    repeat rewrite concat_pp_p; rewrite ap_V; apply moveL_Vp; rewrite concat_p1.
    rewrite concat_p_pp, <- ap_compose.
    rewrite (concat_pA1 (fun b => (retraction b)^) (retraction (f a))).
    rewrite concat_pV, concat_1p; reflexivity.
  Qed.

  Lemma bla (P : B -> Type) (a : A) (F : forall a, P (f a))
    : paths_rect _ (f (g (f a))) (fun a _ => P a) (F (g (f a))) (f a) (retraction (f a)) = F a.
  Proof.
    change (transport P (retraction (f a)) (F (g (f a))) = F a).
    rewrite is_adjoint'.
    destruct (section' a).
    reflexivity.
  Qed.
End S.
Print Assumptions bla.
(* Closed under the global context: not dependent on funext / univalence *)