Equivalences

We now give many ways to construct equivalences. In each case, we define an instance of the typeclass IsEquiv named isequiv_X, followed by an element of the record type Equiv named equiv_X. Whenever we need to assume, as a hypothesis, that a certain function is an equivalence, we do it by assuming separately a function and a proof of IsEquiv. This is more general than assuming an inhabitant of Equiv, since the latter has an implicit coercion and an existing instance to give us the former automatically. Moreover, implicit generalization makes it easy to assume a function and a proof of IsEquiv. A word on naming: some of the lemmas about equivalences are analogues of those for paths in PathGroupoids. We name them in an analogous way but adding _equiv in an appropriate place, e.g. instead of moveR_M we have moveR_equiv_M.

The identity map is an equivalence.

The composition of equivalences is an equivalence.

We put g and f in equiv_scope explicitly. This is a partial work-around for https://github.com/coq/coq/issues/3990, which is that implicitly bound scopes don't nest well.

A tactic to simplify "oE". See ev_equiv below for a more extensive tactic.

Transporting is an equivalence.

In all the above cases, we were able to directly construct all the structure of an equivalence. However, as is evident, sometimes it is quite difficult to prove the adjoint law. The following adjointification theorem allows us to be lazy about this if we wish. It says that if we have all the data of an (adjoint) equivalence except the triangle identity, then we can always obtain the triangle identity by modifying the datum equiv_is_section (or equiv_is_retraction). The proof is the same as the standard categorical argument that any equivalence can be improved to an adjoint equivalence. As a stylistic matter, we try to avoid using adjointification in the library whenever possible, to preserve the homotopies specified by the user.

We don't make this a typeclass instance, because we want to control when we are applying it.

Anything homotopic to an equivalence is an equivalence. This should not be an instance; it can cause the unifier to spin forever searching for functions to be homotopic to.

If e is an equivalence, f is homotopic to e, and g is homotopic to e^-1, then there is an equivalence whose underlying map is f and whose inverse is g, definitionally.

An involution is an endomap that is its own inverse.

Several lemmas useful for rewriting.

Equivalence preserves contractibility (which of course is trivial under univalence).

Any two contractible types are equivalent.

The projection from the sum of a family of contractible types is an equivalence.

Equivalences between path spaces If f is an equivalence, then so is ap f. We are lazy and use adjointify.

Assuming function extensionality, composing with an equivalence is itself an equivalence

Conversely, if pre- or post-composing with a function is always an equivalence, then that function is also an equivalence. This is a form of the Yoneda lemma. It's convenient to know that we only need to assume the equivalence when the other type is the domain or the codomain.

The inverse of an equivalence is an equivalence.

If the goal is IsEquiv _^-1, then use isequiv_inverse; otherwise, don't pretend worry about if the goal is an evar and we want to add a ^-1.

Equiv A B is a symmetric relation.

Inversion respects composition

Inversion respects homotopies

If g \o f and f are equivalences, so is g. This is not an Instance because it would require Coq to guess f.

If g \o f and g are equivalences, so is f.

Combining these with isequiv_compose, we see that equivalences can be transported across commutative squares.

Based homotopy spaces

The function equiv_ind says that given an equivalence f : A <~> B, and a hypothesis from B, one may always assume that the hypothesis is in the image of e. In fibrational terms, if we have a fibration over B which has a section once pulled back along an equivalence f : A <~> B, then it has a section over all of B.

Using equiv_ind, we define a handy little tactic which introduces a variable and simultaneously substitutes it along an equivalence.

The same, but for several variables.

A lemma that combines equivalence induction with path induction. If e is an equivalence from a = b to X, then to prove ∀ x, P x it is enough to prove ∀ p : a = b, P (e p), and so by path induction it suffices to prove P (e 1). The idiom for using this is to first revert b X, which allows Coq to determine the family P. After using this, b will be replaced by a in the goal.

equiv_composeR', a flipped version of equiv_compose', is (like concatR) most often useful partially applied, to give the “first half” of an equivalence one is constructing and leave the rest as a subgoal. One could similarly define equiv_composeR as a flip of equiv_compose, but it doesn’t seem so useful since it doesn’t leave the remaining equivalence as a subgoal.

It's often convenient when constructing a chain of equivalences to use equiv_compose', etc. But when we treat an Equiv object constructed in that way as a function, via the coercion equiv_fun, Coq sometimes needs a little help to realize that the result is the same as ordinary composition. This tactic provides that help.

Building equivalences between nested sigma and record types

The following tactic make_equiv builds an equivalence between two types built out of arbitrarily nested sigma and record types, not necessarily right-associated, as long as they have all the same underyling components. This is more general than issig in that it doesn't just prove equivalences between a single record type and a single right-nested tower of sigma types, but less powerful in that it can't deduce the latter nested tower of sigmas automatically: you have to have both sides of the equivalence known.

Don't destruct paths

Don't apply functions

In case anyone ever needs it, here's the version that doesn't adjointify. It's not the default, because it can be slow.

Here are some examples of the use of this tactic that you can uncomment and explore.

Goal forall (A : Type) (B : A -> Type) (C : forall a:A, B a -> Type) (D : forall (a:A) (b:B a), C a b -> Type),
     { ab : {a : A & B a } & { c : C ab.1 ab.2 & D ab.1 ab.2 c } }
     <~> { a : A & { bc : { b : B a & C a b } & D a bc.1 bc.2 } }.
  intros A B C D.
  make_equiv.
  Undo.
  (** Here's the eventually successful proof script produced by [make_equiv], extracted from [Info 0 make_equiv] and prettified, so you can step through it and see how the tactic works. *)
  snrefine (equiv_adjointify _ _ _ _).
  - (** Here begins [decomposing_intros] *)
    intros x; cbn in x.
    elim x; clear x.
    intros x; cbn in x.
    elim x; clear x.
    intros a; cbn in a.
    intros b; cbn in b.
    intros x; cbn in x.
    elim x; clear x.
    intros c; cbn in c. 
    intros d; cbn in d.
    (** Here begins [build_record] *)
    cbn; unshelve econstructor.
    { cbn; exact a. }
    { cbn; unshelve econstructor.
      { cbn; unshelve econstructor.
        { cbn; exact b. }
        { cbn; exact c. } }
      { cbn; exact d. } }
  - intros x; cbn in x.
    elim x; clear x.
    intros a; cbn in a.
    intros x; cbn in x.
    elim x; clear x.
    intros x; cbn in x.
    elim x; clear x. 
    intros b; cbn in b.
    intros c; cbn in c.
    intros d; cbn in d.
    cbn; unshelve econstructor.
    { cbn; unshelve econstructor.
      { cbn; exact a. }
      { cbn; exact b. } }
    { cbn; unshelve econstructor.
      { cbn; exact c. }
      { cbn; exact d. } }
  - intros x; cbn in x.
    elim x; clear x.
    intros a; cbn in a.
    intros x; cbn in x.
    elim x; clear x.
    intros x; cbn in x.
    elim x; clear x. 
    intros b; cbn in b.
    intros c; cbn in c.
    intros d; cbn in d.
    cbn; exact idpath.
  - intros x; cbn in x.
    elim x; clear x.
    intros x; cbn in x.
    elim x; clear x.
    intros a; cbn in a.
    intros b; cbn in b.
    intros x; cbn in x.
    elim x; clear x.
    intros c; cbn in c. 
    intros d; cbn in d.
    cbn; exact idpath.
Defined.

Here is an example illustrating the need for multi_assumption instead of just assumption.

Goal forall (A:Type) (R:A->A->Type),
    { x : A & { y : A & R x y } } <~> { xy : A * A & R (fst xy) (snd xy) }.
  intros A R.
  make_equiv.
  Undo.
  snrefine (equiv_adjointify _ _ _ _).
  - intros x; cbn in x.
    elim x; clear x.
    intros a1; cbn in a1.
    intros x; cbn in x.
    elim x; clear x.
    intros a2; cbn in a2.
    intros r; cbn in r.
    cbn; unshelve econstructor.
    { cbn; unshelve econstructor. 
      { (** [build_record] can't guess at this point that it needs to use [a1] instead of [a2], and in fact it tries [a2] first; but later on, [exact r] fails in that case, causing backtracking to this point and a re-try with [a1].  *)
        cbn; exact a1. }
      { cbn; exact a2. } }
    cbn; exact r.
  - intros x; cbn in x.
    elim x; clear x.
    intros x; cbn in x.
    elim x; clear x.
    intros a1; cbn in a1.
    intros a2; cbn in a2.
    intros r; cbn in r.
    cbn; unshelve econstructor.
    { cbn; exact a1. }
    { cbn; unshelve econstructor.
      { cbn; exact a2. }
      { cbn; exact r. } }
  - intros x; cbn in x.
    elim x; clear x.
    intros x; cbn in x.
    elim x; clear x.
    intros a1; cbn in a1.
    intros a2; cbn in a2.
    intros r; cbn in r.
    cbn; exact idpath.
  - intros x; cbn in x.
    elim x; clear x.
    intros a1; cbn in a1.
    intros x; cbn in x.
    elim x; clear x.
    intros a2; cbn in a2.
    intros r; cbn in r.
    cbn; exact idpath.
Defined.

Some "real-world" examples where make_equiv simplifies things a lot include the associativity/symmetry proofs in Types/Sigma.v, issig_pequiv' in Pointed/pEquiv.v, and loop_susp_adjoint in Pointed/pSusp.v. Now we give a version of make_equiv that can also prove equivalences of nested sigma- and record types that involve contracting based path-spaces on either or both sides. The basepoint and the path don't have to appear together, but can be in arbitrarily separated parts of the nested structure. It does this by selectively applying path-induction to based paths appearing on both sides, if needed. We start with a version of decomposing_intros that is willing to destruct paths, though as a second choice.

Don't destruct paths at first

Don't apply functions at first

Destruct paths as a second choice. But sometimes destruct isn't smart enough to generalize the other hypotheses that use the free endpoint, so we manually apply paths_ind, or its right-handed version, instead.

Ensure that b and x come first in the ∀ goal resulting from generalize dependent, so that paths_ind can apply to it.

Check that b was actually reverted. (If it's a section variable that the goal depends on, generalize dependent b will "succeed", but actually fail to generalize the goal over b (since that can't be done within the section) and not clear b from the context.)

Try the other endpoint too.

Going the other direction, we have to be willing to insert identity paths to fill in the based path-spaces that got destructed. In fact econstructor is already willing to do that, since idpath is the constructor of paths. However, our previous build_record won't manage to get to the point of being able to apply econstructor to the necessary paths, since it'll get stuck earlier on trying to find the basepoint. Thus, we give a version of build_record that is willing to create existential variables ("evars") for goals that it can't solve, in hopes that a later idpath (produced by econstructor) will determine them by unification. Note that if there are other fields that depend on the basepoint that occur before the idpath, the evar will -- and, indeed, must -- get instantiated by them instead. This is why multi_assumption, above, must be willing to instantiate evars.

Create a fresh evar to solve this goal

Now here's the improved version of make_equiv.

solve [ unshelve TAC ] ensures that TAC succeeds without leaving any leftover evars.

As before, we give some examples.

Section Examples.
  Context (A : Type) (B : A -> Type) (a0 : A).
  Goal { a : A & { b : B a & a = a0 } } <~> B a0.
  Proof.
    make_equiv_contr_basedpaths.
    Undo.
    snrefine (equiv_adjointify _ _ _ _).
    - (** Here begins [decomposing_intros_with_paths] *)
      intros x; cbn in x.
      elim x; clear x.
      intros a; cbn in a.
      intros x; cbn in x. 
      elim x; clear x.
      intros b; cbn in b.
      intros p; cbn in p.
      (** [decomposing_intros] wouldn't be willing to destruct [p] here, because it's a path.  But [decomposing_intros_with_paths] will try it when all else fails. *)
      move p before a.
      generalize dependent a.
      not (move a at top).
      refine (paths_ind_r _ _ _).
      intros b; cbn in b.
      (** Here begins [build_record_with_evars] *)
      exact b.
    - (** Here begins [decomposing_intros_with_paths] *)
      intros b; cbn in b.
      (** Here begins [build_record_with_evars] *)
      cbn; unshelve econstructor.
      { let x := fresh in evar (x : A); exact x. }
      cbn; unshelve econstructor.
      { (** This instantiates the evar. *)
        exact b. }
      { cbn; unshelve econstructor. }
    - intros b; cbn in b.
      exact idpath.
    - intros x; cbn in x.
      elim x; clear x.
      intros a; cbn in a.
      intros x; cbn in x. 
      elim x; clear x.
      intros b; cbn in b.
      intros p; cbn in p.
      move p before a.
      generalize dependent a.
      not (move a at top).
      refine (paths_ind_r _ _ _).
      intros b; cbn in b.
      exact idpath.
  Defined.
End Examples.

Some "real-world" examples where make_equiv_contr_basedpaths simplifies things a lot include hfiber_compose in HFiber.v, hfiber_pullback_along in Limits/Pullback.v, and equiv_Ocodeleft2plus in BlakersMassey.v.