Require Export UniMath.Foundations.All.
Require Export UniMath.MoreFoundations.All.
(** Start of the emulated S1. Don't touch!!! *)
Module Export S1.
Private Inductive S1 : UU := base : S1.
Axiom loop : base = base.
Definition S1_ind (P : S1 -> UU) (b : P base) (l : PathOver loop b b) (x : S1) : P x :=
match x with base => b end.
Definition S1_rec (A : UU) (b : A) (l : b = b) : S1 -> A :=
S1_ind (λ _, A) b (PathOverConstant_map1 loop l).
Axiom S1_ind_beta_loop : forall (P : S1 -> UU) (b : P base) (l : PathOver loop b b), apd (S1_ind P b l) loop = l.
Axiom S1_rec_beta_loop : forall (A : UU) (b : A) (l : b = b), maponpaths (S1_rec A b l) loop = l.
End S1.
(** End of the emulated S1. Don't touch!!! *)
(** The definition of Z we will use. It is essentially `coprod nat nat`, but
* with more memorable names `Pos` and `NegS` instead of `inl` and `inr`.
* `NegS 1` means -2. *)
Inductive Z : UU :=
| Pos : nat -> Z
| NegS : nat -> Z.
(** We define the `succ` function that increment integers by 1. *)
Definition succ (i : Z) : Z :=
match i with
| Pos n => Pos (S n)
| NegS 0 => Pos 0
| NegS (S n) => NegS n
end.
(** [Exercise] We then define the `pred` function that decrement
* integers by 1. *)
Definition pred (i : Z) : Z :=
match i with
| Pos (S n) => Pos n
| Pos 0 => NegS 0
| NegS n => NegS (S n)
end.
(** [Exercise] `pred` is a left inverse of `succ` *)
Lemma pred_succ (i : Z) : pred (succ i) = i.
Proof.
induction i.
- reflexivity.
- induction n.
+ reflexivity.
+ reflexivity.
Defined.
(** [Exercise] `pred` is a right inverse of `succ` *)
Lemma succ_pred (i : Z) : succ (pred i) = i.
Proof.
induction i.
- induction n.
+ reflexivity.
+ reflexivity.
- reflexivity.
Defined.
(** Therefore, `succ` is an equivalence! *)
Definition succ_equiv : Z ≃ Z :=
make_weq succ (isweq_iso succ pred pred_succ succ_pred).
(** Decoding: from numbers to paths *)
(** The definition for non-negative numbers `Pos n`. *)
Fixpoint loopexpPos (n : nat) : base = base :=
match n with
| 0 => idpath base
| S n => loopexpPos n @ loop
end.
(** The definition for negative numbers `NegS n`. *)
Fixpoint loopexpNegS (n : nat) : base = base :=
match n with
| 0 => ! loop
| S n => loopexpNegS n @ ! loop
end.
(** The conversion from loops to numbers. Think about the numbers as
* an "encoding" of loops. In the case of the circle, this is also
* called "winding numbers". *)
Definition loopexp (x : Z) : base = base :=
match x with
| Pos n => loopexpPos n
| NegS n => loopexpNegS n
end.
(** Encoding: from paths to numbers. This is not trivial at all,
* as it seems we have no way to recover the number from seemingly
* "unstructured" paths. We summon covering spaces to help us. *)
(** The (universal) covering space of the circle. *)
Definition Cover : S1 -> UU :=
S1_rec UU Z (weqtopaths succ_equiv).
(** Transporting along `loop` is the same as applying `succ`.
* (We will not use this lemma in the final theorems.) *)
Lemma loop_transport (x : Z) : transportf Cover loop x = succ x.
Proof.
etrans.
- exact (functtransportf Cover (idfun UU) loop x).
- unfold Cover. rewrite S1_rec_beta_loop.
refine (toforallpaths _ _ _ _ x).
apply weqpath_transport.
Defined.
(** A very useful lemma that mimics the existing lemma `weqpath_transport` *)
Lemma invweqpath_transport {A B : UU} (e : A ≃ B)
: transportf (λ A, A) (! (weqtopaths e)) = pr1 (invweq e).
Proof.
etrans.
- symmetry. refine (pr1_eqweqmap2 _).
- rewrite eqweqmap_pathsinv0.
rewrite eqweqmap_weqtopaths.
reflexivity.
Defined.
(** [Exercise] prove that transporting along the inverse of
* `loop` is the same as applying `pred`. *)
Lemma invloop_transport (x : Z) : transportf Cover (! loop) x = pred x.
Proof.
etrans.
- exact (functtransportf Cover (idfun UU) (! loop) x).
- rewrite maponpathsinv0.
unfold Cover. rewrite S1_rec_beta_loop.
refine (toforallpaths _ _ _ _ x).
apply invweqpath_transport.
Defined.
(** Now we are ready to define the encoding function.*)
Definition encode' {x : S1} (p : base = x) (start : Z) : Cover x :=
transportf Cover p start.
Definition encode {x : S1} (p : base = x) : Cover x :=
encode' p (Pos 0).
(** This section proves that `encode` is the right inverse of `loopexp`.
* That is, we can encode a loop back to its representing number. *)
(** [Exercise] A useful lemma.
*
* Hint: `Search (transportf _ _ (transportf _ _ _)).` *)
Lemma encode'_encode (p : base = base) (q : base = base)
: encode' q (encode p) = encode (p @ q).
Proof.
unfold encode. unfold encode'.
apply transport_f_f.
Defined.
(** [Exercise] Another lemma. *)
Lemma encode'_loop (i : Z) : encode' loop i = succ i.
Proof.
unfold encode'.
rewrite (transport_idfun Cover loop i).
unfold Cover. rewrite S1_rec_beta_loop.
refine (toforallpaths _ _ _ _ i).
apply weqpath_transport.
Defined.
(** [Exercise] Yet another lemma. *)
Lemma encode'_invloop (i : Z) : encode' (! loop) i = pred i.
Proof.
unfold encode'.
rewrite (transport_idfun Cover (! loop) i).
rewrite maponpathsinv0.
unfold Cover. rewrite S1_rec_beta_loop.
refine (toforallpaths _ _ _ _ i).
apply invweqpath_transport.
Defined.
(** [Exercise, difficult] Putting all these lemmas together... *)
Lemma encode_loopexp (i : Z) : encode (loopexp i) = i.
Proof.
induction i.
- induction n.
+ reflexivity.
+ simpl in *. etrans.
* symmetry. exact (encode'_encode (loopexpPos n) loop).
* rewrite IHn. apply encode'_loop.
- induction n.
+ apply (encode'_invloop (Pos 0)).
+ simpl in *. etrans.
* symmetry. exact (encode'_encode (loopexpNegS n) (! loop)).
* rewrite IHn. apply encode'_invloop.
Defined.
(** Now, we wish to prove that `encode` is also the right inverse of
`loopexp` as follows: *)
Lemma loopexp_encode (p : base = base): (loopexp (encode p)) = p.
(** However, this is incredibly hard because we cannot do induction
* on `p` (why?). To overcome the difficulty, we have to loose at least
* one end point of `p` to an arbitrary point in `S1`. While `encode`
* can handle arbitrary path from `base` to an arbitrary point, `loopexp`
* needs to be generalized to handle such a free end point. We will call
* the generalized `loopexp` as `decode`, and revisit the lemma later. *)
Abort. (* We will prove this lemma after a long journey. *)
(** [Exercise] prove how `loopexp` and `succ` work with each other.
*
* Hint: `Search (_ @ _ @ _ = _).` *)
Lemma loopexp_succ (i : Z) : loopexp (succ i) = loopexp i @ loop.
Proof.
induction i.
- reflexivity.
- induction n.
+ simpl. symmetry. apply pathsinv0l.
+ simpl. rewrite <- (path_assoc _ (! loop) loop).
rewrite (pathsinv0l loop).
rewrite pathscomp0rid.
reflexivity.
Defined.
(** [Exercise, optional] You can also prove the opposite case,
* though we will not use this lemma. *)
Lemma loopexp_pred (i : Z) : loopexp (pred i) = loopexp i @ ! loop.
Proof.
induction i.
- induction n.
+ reflexivity.
+ simpl. rewrite <- (path_assoc _ loop (! loop)).
rewrite (pathsinv0r loop).
rewrite pathscomp0rid.
reflexivity.
- reflexivity.
Defined.
(** [Exercise] A very useful lemma that can be proved in 2 tactics. *)
Lemma transportf_arrow {A : Type} {B C : A -> Type}
{x y : A} (p : x = y) (f : B x -> C x) (b' : B y)
: (transportf (λ x, B x -> C x) p f) b'
= transportf C p (f (transportf B (! p) b')).
Proof.
induction p. reflexivity.
Defined.
(** [Exercise, very difficult] This is the generalized `loopexp` that
* works for all elements of type `Cover x`, not just `Cover base`
* which is `Z`. *)
Definition decode {x : S1} : Cover x -> base = x.
Proof.
refine (S1_ind (λ x, Cover x -> base = x) loopexp _ x).
apply transportf_to_pathover.
apply funextsec. intro i.
(** [Exercise] Finish the rest of the definition. *)
rewrite transportf_arrow.
rewrite transportf_id1.
etrans.
- apply maponpaths_2, maponpaths, invloop_transport.
- rewrite <- (loopexp_succ (pred i)).
apply maponpaths.
exact (succ_pred i).
Defined.
(** [Exercise] After all the preparation, this is a one-liner. *)
Lemma decode_encode {x : S1} (p : base = x): (decode (encode p)) = p.
Proof.
induction p. reflexivity.
Defined.
(** [Exercise] Finally... *)
Lemma loopexp_encode (p : base = base): (loopexp (encode p)) = p.
Proof.
use decode_encode.
Defined.
(** [Exercise] We proved it! *)
Theorem Omega1S1 : (base = base) ≃ Z.
Proof.
refine (make_weq encode (isweq_iso _ _ _ _)).
- exact loopexp_encode.
- exact encode_loopexp.
Defined.
(** BONUS: We can prove that S1 has h-level 3 but not 2, thanks
* to the constructions and the theorem we just established. *)
Lemma invmaponpathsPos {n m : nat} : Pos n = Pos m -> n = m.
Proof.
intro p.
set (f := λ n, match n with Pos n => n | _ => 0 end).
exact (maponpaths f p).
Defined.
Lemma invmaponpathsNegS {n m : nat} : NegS n = NegS m -> n = m.
Proof.
intro p.
set (f := λ n, match n with NegS n => n | _ => 0 end).
exact (maponpaths f p).
Defined.
Lemma negpathPosNegS {n m : nat} : ¬ (Pos n = NegS m).
Proof.
intro p.
set (f := λ i, match i with Pos _ => true | NegS _ => false end).
exact (nopathstruetofalse (maponpaths f p)).
Defined.
(** [Exercise, difficult] Prove that `Z` has decidable equality. *)
Theorem isdeceqZ : isdeceq Z.
Proof.
intros i j.
induction i as [n1 | n1].
- induction j as [n2 | n2].
+ assert (natdeceq := isdeceqnat n1 n2).
induction natdeceq as [eq | neq].
* left. rewrite eq. reflexivity.
* right. intro eq. apply neq. exact (invmaponpathsPos eq).
+ right. apply negpathPosNegS.
- induction j as [n2 | n2].
+ right. intro eq. apply (negpathPosNegS (! eq)).
+ assert (natdeceq := isdeceqnat n1 n2).
induction natdeceq as [eq | neq].
* left. rewrite eq. reflexivity.
* right. intro eq. apply neq. exact (invmaponpathsNegS eq).
Defined.
(** Okay, `Z` is a set. *)
Theorem isasetZ : isaset Z.
Proof. exact (isasetifdeceq _ isdeceqZ). Defined.
(** Therefore, `base = base` is also a set. *)
Lemma isasetOmega1S1 : isaset (base = base).
Proof. exact (isofhlevelweqb 2 Omega1S1 isasetZ). Defined.
(** [Exercise, extremely difficult] Prove that S1 has h-level 3. *)
Theorem isagroupoidS1 : isofhlevel 3 S1.
Proof.
simple refine (S1_ind (λ x, forall y, isaset (x = y)) _ _).
+ simpl. simple refine (S1_ind (λ y, isaset (base = y)) _ _).
* exact isasetOmega1S1.
* apply transportf_to_pathover, proofirrelevance.
refine (isapropisofhlevel 2 (base = base)).
+ apply transportf_to_pathover, proofirrelevance.
apply impred_isaprop. intro y.
refine (isapropisofhlevel 2 (base = y)).
Defined.
(** [Exercise] Prove that `loop` is not the constant path. *)
Lemma negpathsloopidpath : ¬ (loop = idpath base).
Proof.
intro eq.
assert (p : Pos 1 = Pos 0).
- etrans.
+ symmetry. apply (encode'_loop (Pos 0)).
+ rewrite eq. reflexivity.
- apply (negpathssx0 0), invmaponpathsPos. exact p.
Defined.
(** [Exercise] Prove that `S1` is not a set. *)
Theorem negisasetS1 : ¬ isaset S1.
Proof.
intro isasetS1.
apply negpathsloopidpath, isasetS1.
Defined.