Require Import HoTT.Basics HoTT.Types.Require Import HoTT.Basics HoTT.Types.

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.

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
  match c 0 with
  | true => inl (fun n : nat => c n.+1)
  | false => inr (fun n : nat => c n.+1)
  end 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
  match c 0 with
  | true => inl (fun n0 : nat => c n0.+1)
  | false => inr (fun n0 : nat => c n0.+1)
  end 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).