(* TODO: various improvements and simplifications *)
Require Import HoTT.
Require Import UnivalenceAxiom.
Section IsHProp_BiInv.
(* In this section, we show that the type BiInv(f) is a mere proposition for any function f.
Recall that BiInv(f) is one incarnation of IsEquiv(f), so this also shows that
IsEquiv(f) is a mere proposition. Our proof is different from the one of Theorem 4.3.2; it uses
the proof method of Lemma 4.1.1 relying on univalence and path induction inside the universe *)
(* Want to assume function extensionality and univalence (the latter implying the former) *)
Context `{Funext} `{Univalence}.
(* Need some general lemmas first *)
(* Contractibility is invariant under equivalence. Is this in the library, too? *)
Lemma contr_invariant {S T} : (S <~> T) -> (Contr S) -> (Contr T).
Proof.
intro equiv.
intro contr_proof.
induction contr_proof as [centerS contractionS].
(* apply the equivalence to the center of S to get the center of T *)
exists (equiv centerS).
intro y.
(* We only need the hypothesis on the point corresponding to y *)
specialize (contractionS (equiv^-1 y)).
(* Now the claim follows from path manipulation stuff *)
refine (concat _ (eisretr equiv y)).
apply ap.
assumption.
Defined.
(* Contractibility is preserved by products. Might also be in the library? *)
Lemma contr_product {S T} : (Contr S) -> (Contr T) -> (Contr (S * T)).
Proof.
intros contrS contrT.
induction contrS as [centerS contractionS].
induction contrT as [centerT contractionT].
exists (centerS, centerT).
intro y; induction y as [s t].
(* Use the characterization of paths in a product *)
apply path_prod.
- simpl; apply contractionS.
- simpl; apply contractionT.
Defined.
(* Any equivalence is equal to one coming from a path. There's probably a better way to do this *)
Lemma equiv_from_path_uncurried {S T} (e : S <~> T) : exists p : S = T, e = equiv_path _ _ p.
Proof.
exists ((equiv_path _ _)^-1 e).
refine ((eisretr (equiv_path _ _) _)^).
Defined.
(* Now the same for the underlying function of an equivalence. A bit messy... *)
Lemma equiv_from_path {S T} (f : S -> T) (w : IsEquiv f) : exists p : S = T, f = equiv_path _ _ p.
Proof.
exists ((equiv_path _ _)^-1 (BuildEquiv _ _ _ _)).
refine (@concat _ _ (equiv_fun _ _ (BuildEquiv _ _ _ _)) _ _ _).
- eauto.
- refine (ap (equiv_fun _ _) _).
refine ((eisretr (equiv_path S T) _)^).
Defined.
(* Now on towards the main theorem *)
(* The space of maps homotopic to the identity map is contractible *)
Lemma idmap_homot_contr {A} : Contr (exists g : A -> A, g == idmap).
Proof.
(* Don't like homotopy '==', so use that '==' can be replaced by '=' *)
apply (contr_invariant (S := exists g : A -> A, g = idmap)).
(* Construct the equivalence by using that if two type families are pointwise
equivalent, then the dependent pair types are equivalent. The pointwise equivalence
implicitly rely on function extensionality! *)
apply (equiv_functor_sigma idmap (fun g : A -> A => (ap10 (f := g) (g := idmap)))).
(* Now the type claimed to be contractible is the type of paths in A -> A with one fixed
endpoint. Any space of paths with only one fixed endpoint is contractible. *)
apply contr_basedpaths'.
Defined.
(* The type of all ways of showing that the identity map is an equivalence is contractible *)
Lemma idmap_equiv_contr {A} : Contr (@BiInv A A idmap).
Proof.
apply contr_product.
apply idmap_homot_contr.
apply idmap_homot_contr.
Defined.
(* Finally we can state and prove the main theorem *)
Theorem isprop_biinv {A B : Type} (f : A -> B) : IsHProp (BiInv f).
Proof.
(* Use that (T -> Contr T) implies (IsHProp T) *)
apply hprop_inhabited_contr.
(* Now we have the assumption that f is biinvertible at our disposal *)
intro biinv_witness.
(* Use the lemma that every equivalence is equal to one coming from a path in the universe *)
rewrite ((equiv_from_path f (equiv_biinv _ biinv_witness)) .2).
(* So we might as well prove the statement for all paths in the universe! *)
generalize ((equiv_from_path f (equiv_biinv f biinv_witness)) .1).
(* Now can do path induction! *)
intro p; induction p.
(* simplify a bit *)
simpl; unfold transport; simpl.
(* We've already proven this! *)
exact idmap_equiv_contr.
Defined.
End IsHProp_BiInv.