(* Some results about the circle in HoTT. Since this file is meant to be read by humans and not compiled, it makes
sense to include some 'Check' commands for better understanding *)
Require Import HoTT.
(* Want to assume the univalence axiom and function extensionality (the former implying the latter) *)
Context `{Univalence} `{Funext}.
(* Main results in this section: loop is not equal to the constant path; but the circle is connected *)
Section CircleProperties.
(* Define the type family from Exercise 8.8, i.e. the 'junior Hopf fibration' or 'twisted double cover of S1' *)
Definition twstd_dbl_cvr
: S1 -> Type
:= S1_rectnd Type Bool (path_universe negb).
(* The following result from the library can be used to characterize transport along loop *)
Check (transport_idmap_ap _ twstd_dbl_cvr _ _ loop).
(* The characterization is that transport along loop is precisely negb, i.e. the 'flip' map on Bool *)
Lemma transport_loop_eq_negb : transport twstd_dbl_cvr loop = negb.
Proof.
apply path_forall. (* function extensionality *)
intro b.
rewrite (transport_idmap_ap _ twstd_dbl_cvr _ _ loop).
unfold twstd_dbl_cvr.
(* At this point we can use the propositional computation rule for S1 with respect to the inductive definition
of twisted_double_cover *)
rewrite (S1_rectnd_beta_loop _ _ _).
apply transport_path_universe.
Defined.
(* We can use this to show that transport along loop is not equal to transport along the constant path *)
Lemma trans_loop_ne_trans_idpath : (transport twstd_dbl_cvr loop = transport twstd_dbl_cvr idpath) -> Empty.
Proof.
intro eq_transports.
apply false_ne_true.
rewrite transport_loop_eq_negb in eq_transports.
unfold transport in eq_transports; simpl in eq_transports.
exact (ap (fun f : Bool -> Bool => f true) eq_transports).
Defined.
(* Now it follows that loop is not equal to the constant path *)
Theorem loop_not_idpath : (loop = 1) -> Empty.
Proof.
intro loop_eq_idpath.
apply trans_loop_ne_trans_idpath.
rewrite loop_eq_idpath.
trivial.
Defined.
(* Hence the circle is not a set *)
Corollary S1_not_hset : (IsHSet S1) -> Empty.
Proof.
intro S1_hset_proof.
apply axiomK_hset in S1_hset_proof.
specialize (S1_hset_proof base loop).
exact (loop_not_idpath S1_hset_proof).
Defined.
(* Therefore the circle is not a mere proposition either *)
Corollary S1_not_hprop : (IsHProp S1) -> Empty.
Proof.
intro S1_hprop_proof.
apply S1_not_hset.
apply trunc_succ.
Defined.
(* Therefore the cicle is not contractible either *)
Corollary S1_not_contr : (Contr S1) -> Empty.
Proof.
intro S1_contr_proof.
apply S1_not_hprop.
apply trunc_succ.
Defined.
Require Import Connectedness.
(* But the circle is connected! *)
Theorem circle_connected : IsConnected 0 S1.
Proof.
(* The definition of connectedness in the library is such that we have to reduce it first to
showing that the hset truncation is contractible *)
apply @isconnected_from_iscontr_truncation.
(* Can take base as the center of contraction *)
exists (truncation_incl base).
(* We can now use the elimination rule for the set truncation *)
apply Truncation_rect.
- apply trunc_succ.
(* Now use circle elimination *)
- refine (S1_rect _ idpath _).
(* This equality follows from Axiom K, which holds by virtue of the set truncation being a set *)
apply axiomK_hset.
(* The set truncation is indeed a set *)
apply istrunc_truncation.
Defined.