(* -*- mode: coq; mode: visual-line -*- *)
Require Import HoTT.Basics HoTT.Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Local Open Scope nat_scope.
Local Open Scope path_scope.

(** * Cantor space 2^N *)

Definition Cantor : Type := nat -> Bool.

Definition cantor_fold : Cantor + Cantor -> Cantor.
Cantor + Cantor -> Cantor
Proof.
Cantor + Cantor -> Cantor
  intros [c|c]; intros n.
c: Cantor
n: nat
Bool
c: Cantor
n: nat
Bool
  -
c: Cantor
n: nat
Bool destruct n as [|n].
c: Cantor
Bool
c: Cantor
n: nat
Bool
    +
c: Cantor
Bool exact true.
    +
c: Cantor
n: nat
Bool exact (c n).
  -
c: Cantor
n: nat
Bool destruct n as [|n].
c: Cantor
Bool
c: Cantor
n: nat
Bool
    +
c: Cantor
Bool exact false.
    +
c: Cantor
n: nat
Bool exact (c n).
Defined.

Definition cantor_unfold : Cantor -> Cantor + Cantor.
Cantor -> Cantor + Cantor
Proof.
Cantor -> Cantor + Cantor
  intros c.
c: Cantor
Cantor + Cantor
  case (c 0).
c: Cantor
Cantor + Cantor
c: Cantor
Cantor + Cantor
  -
c: Cantor
Cantor + Cantor exact (inl (fun n => c n.+1)).
  -
c: Cantor
Cantor + Cantor exact (inr (fun n => c n.+1)).
Defined.

Global Instance isequiv_cantor_fold `{Funext} : IsEquiv cantor_fold.
H: Funext
IsEquiv cantor_fold
Proof.
H: Funext
IsEquiv cantor_fold
  refine (isequiv_adjointify _ cantor_unfold _ _).
H: Funext
(fun x : Cantor => cantor_fold (cantor_unfold x)) ==
idmap
H: Funext
(fun x : Cantor + Cantor =>
 cantor_unfold (cantor_fold x)) == idmap
  -
H: Funext
(fun x : Cantor => cantor_fold (cantor_unfold x)) ==
idmap intros c; apply path_arrow; intros n.
H: Funext
c: Cantor
n: nat
cantor_fold (cantor_unfold c) n = c n
    induction n as [|n IH].
H: Funext
c: Cantor
cantor_fold (cantor_unfold c) 0 = c 0
H: Funext
c: Cantor
n: nat
IH: cantor_fold (cantor_unfold c) n = c n
cantor_fold (cantor_unfold c) n.+1 = c n.+1
    +
H: Funext
c: Cantor
cantor_fold (cantor_unfold c) 0 = c 0 unfold cantor_unfold.
H: Funext
c: Cantor
cantor_fold
  (if c 0
   then inl (fun n : nat => c n.+1)
   else inr (fun n : nat => c n.+1)) 0 = c 0
      case (c 0); reflexivity.
    +
H: Funext
c: Cantor
n: nat
IH: cantor_fold (cantor_unfold c) n = c n
cantor_fold (cantor_unfold c) n.+1 = c n.+1 unfold cantor_unfold.
H: Funext
c: Cantor
n: nat
IH: cantor_fold (cantor_unfold c) n = c n
cantor_fold
  (if c 0
   then inl (fun n : nat => c n.+1)
   else inr (fun n : nat => c n.+1)) n.+1 = c n.+1
      case (c 0); reflexivity.
  -
H: Funext
(fun x : Cantor + Cantor =>
 cantor_unfold (cantor_fold x)) == idmap intros [c|c]; apply path_sum; reflexivity.
Defined.

Definition equiv_cantor_fold `{Funext} : Cantor + Cantor <~> Cantor
  := Build_Equiv _ _ cantor_fold _.

Definition equiv_cantor_unfold `{Funext} : Cantor <~> Cantor + Cantor
  := Build_Equiv _ _ cantor_unfold (isequiv_inverse equiv_cantor_fold).