(* 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.