Require Import HoTT.

Notation "x ⟿ y" := (@paths _ x y) (at level 20) : new_scope.
Open Scope new_scope.

(** Here we define the Circle S1 *)

Module Export Circle.

  Private Inductive C : Type
    := base : C.

  Axiom loop : base ⟿ base.

  Definition C_ind (P : C -> Type) (b : P base) (l : transport P loop b ⟿ b)
    : forall (x:C), P x
    := fun x => match x with
             | base => fun _ => b
             end l.

  Axiom C_ind_beta_loop : forall (P : C -> Type) (b : P base) (l : transport P loop b ⟿ b),
      apD (C_ind P b l) loop ⟿ l.

End Circle.

Definition C_rec (P : Type) (b : P) (l : b ⟿ b)
  : C -> P
  := C_ind (fun _ => P) b (transport_const _ _ @ l).

Definition C_rec_beta_loop (P : Type) (b : P) (l : b ⟿ b)
  : ap (C_rec P b l) loop ⟿ l.
Proof.
  unfold C_rec.
  refine (cancelL (transport_const loop b) _ _ _).
  refine ((apD_const (C_ind (fun _ => P) b _) loop)^ @ _).
  refine (C_ind_beta_loop (fun _ => P) _ _).
Defined.

(** Here we define the integers *)
Inductive Pos : Type1 :=
| one : Pos
| succ_pos : Pos -> Pos.

Inductive Int : Type1 :=
| neg : Pos -> Int
| zero : Int
| pos : Pos -> Int.

Definition succ_int (z : Int) : Int
  := match z with
       | neg (succ_pos n) => neg n
       | neg one => zero
       | zero => pos one
       | pos n => pos (succ_pos n)
     end.

Definition pred_int (z : Int) : Int
  := match z with
       | neg n => neg (succ_pos n)
       | zero => neg one
       | pos one => zero
       | pos (succ_pos n) => pos n
     end.

Instance isequiv_succ_int : IsEquiv succ_int.
Proof.
  refine (isequiv_adjointify succ_int pred_int _ _).
  intros [[|n] | | [|n]]; reflexivity.
  intros [[|n] | | [|n]]; reflexivity.
Defined.

Instance ishset_Pos : IsHSet Pos.
Proof.
  refine (trunc_equiv nat _).
  refine (nat_rec Pos one (fun n => succ_pos)). 
  refine (isequiv_adjointify _ _ _ _).
  - exact (Pos_rect (fun _ => nat) 0 (fun _ => S)).
  - intro p; induction p.
    reflexivity. cbn. apply ap. exact IHp.
  - intro n; induction n.
    reflexivity.
    simpl. apply ap. exact IHn.
Qed.

Instance ishset_Int : IsHSet Int.
Proof.
  refine (trunc_equiv (Pos + Unit + Pos) _).
  intros [[p | t] | q].
  exact (neg p). exact zero. exact (pos q).
  refine (isequiv_adjointify _ _ _ _).
  - intro p; destruct p.
    left. left. exact p.
    left; right. exact tt.
    right; exact p.
  - intro p; destruct p; reflexivity.
  - intros [[p | t] | q]; [ reflexivity | destruct t; reflexivity | reflexivity ].
Qed.
    
(** We define the composition of loops *)

Definition loop_n (n:Int)
  : base ⟿ base.
Proof.
  induction n.
  - induction p.
    + exact loop^.
    + exact (IHp @ loop^).
  - exact idpath.
  - induction p.
    + exact loop.
    + exact (IHp @ loop).
Defined.
     

(** We want to show some functoriality property of [loop] *)

Lemma loop_n_loop (n:Int)
  : (loop_n n @ loop) ⟿ (loop @ loop_n n).
(** Do a loop, then n loops. Now, do n loops, then a loop. Tadaa! *)
Proof.
  induction n; simpl.
  - induction p; simpl.
    exact (concat_Vp loop @ (concat_pV loop)^).
    rewrite concat_pV_p.
    rewrite concat_p_pp. apply moveL_pV.
    exact IHp.
  - exact (concat_1p loop @ (concat_p1 loop)^).
  - induction p; simpl.
    reflexivity.
    rewrite !concat_p_pp. apply whiskerR. exact IHp.
Qed.
    
Lemma loop_n_pred (n:Int)
  : (loop_n (pred_int n)) ⟿ (loop^ @ loop_n n).
(** Do n-1 loops. Now, do a backward loop, then n loops. *)
Proof.
  induction n.
  - induction p.
    + simpl. reflexivity.
    + simpl in *.
      rewrite concat_p_pp.
      apply (ap (fun x => x @ loop^)).
      exact IHp.
  - simpl. symmetry; apply concat_p1.
  - induction p.
    + simpl. symmetry; apply concat_Vp.
    + apply moveL_Vp.
      rewrite <- loop_n_loop. reflexivity.
Qed.

(** The universal cover of the circle *)

Context `{ua : Univalence}.

Definition Cover : C -> Type.
Proof.
  refine (C_rec _ _ _).
  - exact Int.
  - refine (path_universe succ_int).
Defined.

Definition transport_Cover_loop (z : Int)
  : transport Cover loop z ⟿ succ_int z.
Proof.
  refine (transport_compose idmap Cover loop z @ _).
  unfold Cover; rewrite C_rec_beta_loop.
  apply transport_path_universe.
Defined.

Definition transport_Cover_loopV (z : Int)
  : transport Cover loop^ z ⟿ pred_int z.
Proof.
  refine (transport_compose idmap Cover loop^ z @ _).
  rewrite ap_V.
  unfold Cover; rewrite C_rec_beta_loop.
  rewrite <- (path_universe_V succ_int).
  apply transport_path_universe.
Defined.


Definition encode (x:C) : (base ⟿ x) -> Cover x
  := fun p => transport Cover p zero.

Definition decode (x:C) : Cover x -> base ⟿ x.
Proof.
  revert x.
  refine (C_ind _ _ _).
  - simpl. intro n. exact (loop_n n).
  - apply path_forall; intro n.
    refine (transport_arrow _ _ _ @ _).
    refine (transport_paths_r _ _ @ _).
    simpl.
    rewrite transport_Cover_loopV.
    rewrite loop_n_pred. rewrite concat_pp_p.
    apply moveR_Vp.
    apply loop_n_loop.
Defined.

Lemma decode_encode (x:C) : forall p, decode x (encode x p) ⟿ p.
Proof.
     
  intro p. destruct p.
  simpl. reflexivity.
Qed.

Lemma encode_decode (x:C) : forall c, encode x (decode x c) ⟿ c.
Proof.
  revert x.
  refine (C_ind _ _ _).
  - simpl. unfold encode. simpl.
    destruct c.
    + induction p.
      simpl.
      rewrite transport_Cover_loopV. simpl. reflexivity.
      
      simpl.
      rewrite transport_pp.
      rewrite IHp.
      rewrite transport_Cover_loopV.
      reflexivity.
    + simpl. reflexivity.

    + induction p.
      simpl. apply transport_Cover_loop.
      simpl. rewrite transport_pp.
      rewrite IHp.
      apply transport_Cover_loop.

  - simpl.
    apply path_forall; intro z.
    apply set_path2.
Defined.

Theorem π1S1 : (base ⟿ base) ⟿ Int.
Proof.
  apply path_universe_uncurried.
  exists (encode base).
  refine (isequiv_adjointify _ _ _ _).
  apply decode.
  intro x. apply encode_decode.
  intro x. apply decode_encode.
Qed.