Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.PathGroupoidsRequire Import Basics.Overture Basics.Tactics Basics.Trunc Basics.PathGroupoids
  Basics.Equivalences Basics.Decidable Basics.Classes.
Require Import Types.Empty Types.Sigma Types.Sum Types.Prod Types.Equiv.
Require Import Spaces.Nat.Core.
Require Import Finite.Fin.

Local Open Scope nat_scope.

Set Universe Minimization ToSet.

Definition FinNat@{} (n : nat) : Type0 := {x : nat | x < n}.

Definition zero_finnat@{} (n : nat) : FinNat n.+1
  := (0; _ : 0 < n.+1).

Definition succ_finnat@{} {n : nat} (u : FinNat n) : FinNat n.+1
  := (u.1.+1; leq_succ u.2).

Definition path_succ_finnat {n : nat} (x : nat) (h : x.+1 < n.+1)
  : succ_finnat (x; leq_pred' h) = (x.+1; h).
n, x: nat
h: x.+1 < n.+1
succ_finnat (x; leq_pred' h) = (x.+1; h)
Proof.
n, x: nat
h: x.+1 < n.+1
succ_finnat (x; leq_pred' h) = (x.+1; h)
  by apply path_sigma_hprop.
Defined.

Definition last_finnat@{} (n : nat) : FinNat n.+1
  := exist (fun x => x < n.+1) n (leq_refl n.+1).

Definition incl_finnat@{} {n : nat} (u : FinNat n) : FinNat n.+1
  := (u.1; leq_trans u.2 (leq_succ_r (leq_refl n))).

Definition finnat_ind@{u} (P : forall n : nat, FinNat n -> Type@{u})
  (z : forall n : nat, P n.+1 (zero_finnat n))
  (s : forall (n : nat) (u : FinNat n), P n u -> P n.+1 (succ_finnat u))
  {n : nat} (u : FinNat n)
  : P n u.
P: forall n0 : nat, FinNat n0 -> Type
z: forall n0 : nat, P n0.+1 (zero_finnat n0)
s: forall (n0 : nat) (u0 : FinNat n0), P n0 u0 -> P n0.+1 (succ_finnat u0)
n: nat
u: FinNat n
P n u
Proof.
P: forall n0 : nat, FinNat n0 -> Type
z: forall n0 : nat, P n0.+1 (zero_finnat n0)
s: forall (n0 : nat) (u0 : FinNat n0), P n0 u0 -> P n0.+1 (succ_finnat u0)
n: nat
u: FinNat n
P n u
  simple_induction n n IHn; intro u.
P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u0 : FinNat n), P n u0 -> P n.+1 (succ_finnat u0)
u: FinNat 0
P 0 u
P: forall n0 : nat, FinNat n0 -> Type
z: forall n0 : nat, P n0.+1 (zero_finnat n0)
s: forall (n0 : nat) (u0 : FinNat n0), P n0 u0 -> P n0.+1 (succ_finnat u0)
n: nat
IHn: forall u0 : FinNat n, P n u0
u: FinNat n.+1
P n.+1 u
  -
P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u0 : FinNat n), P n u0 -> P n.+1 (succ_finnat u0)
u: FinNat 0
P 0 u elim (not_lt_zero_r u.1 u.2).
  -
P: forall n0 : nat, FinNat n0 -> Type
z: forall n0 : nat, P n0.+1 (zero_finnat n0)
s: forall (n0 : nat) (u0 : FinNat n0), P n0 u0 -> P n0.+1 (succ_finnat u0)
n: nat
IHn: forall u0 : FinNat n, P n u0
u: FinNat n.+1
P n.+1 u destruct u as [x h].
P: forall n0 : nat, FinNat n0 -> Type
z: forall n0 : nat, P n0.+1 (zero_finnat n0)
s: forall (n0 : nat) (u : FinNat n0), P n0 u -> P n0.+1 (succ_finnat u)
n: nat
IHn: forall u : FinNat n, P n u
x: nat
h: x < n.+1
P n.+1 (x; h)
    destruct x as [| x].
P: forall n0 : nat, FinNat n0 -> Type
z: forall n0 : nat, P n0.+1 (zero_finnat n0)
s: forall (n0 : nat) (u : FinNat n0), P n0 u -> P n0.+1 (succ_finnat u)
n: nat
IHn: forall u : FinNat n, P n u
h: 0 < n.+1
P n.+1 (0; h)
P: forall n0 : nat, FinNat n0 -> Type
z: forall n0 : nat, P n0.+1 (zero_finnat n0)
s: forall (n0 : nat) (u : FinNat n0), P n0 u -> P n0.+1 (succ_finnat u)
n: nat
IHn: forall u : FinNat n, P n u
x: nat
h: x.+1 < n.+1
P n.+1 (x.+1; h)
    +
P: forall n0 : nat, FinNat n0 -> Type
z: forall n0 : nat, P n0.+1 (zero_finnat n0)
s: forall (n0 : nat) (u : FinNat n0), P n0 u -> P n0.+1 (succ_finnat u)
n: nat
IHn: forall u : FinNat n, P n u
h: 0 < n.+1
P n.+1 (0; h) nrefine (transport (P n.+1) _ (z _)).
P: forall n0 : nat, FinNat n0 -> Type
z: forall n0 : nat, P n0.+1 (zero_finnat n0)
s: forall (n0 : nat) (u : FinNat n0), P n0 u -> P n0.+1 (succ_finnat u)
n: nat
IHn: forall u : FinNat n, P n u
h: 0 < n.+1
zero_finnat n = (0; h)
      by apply path_sigma_hprop.
    +
P: forall n0 : nat, FinNat n0 -> Type
z: forall n0 : nat, P n0.+1 (zero_finnat n0)
s: forall (n0 : nat) (u : FinNat n0), P n0 u -> P n0.+1 (succ_finnat u)
n: nat
IHn: forall u : FinNat n, P n u
x: nat
h: x.+1 < n.+1
P n.+1 (x.+1; h) refine (transport (P n.+1) (path_succ_finnat _ _) _).
P: forall n0 : nat, FinNat n0 -> Type
z: forall n0 : nat, P n0.+1 (zero_finnat n0)
s: forall (n0 : nat) (u : FinNat n0), P n0 u -> P n0.+1 (succ_finnat u)
n: nat
IHn: forall u : FinNat n, P n u
x: nat
h: x.+1 < n.+1
P n.+1 (succ_finnat (x; leq_pred' h))
      apply s.
P: forall n0 : nat, FinNat n0 -> Type
z: forall n0 : nat, P n0.+1 (zero_finnat n0)
s: forall (n0 : nat) (u : FinNat n0), P n0 u -> P n0.+1 (succ_finnat u)
n: nat
IHn: forall u : FinNat n, P n u
x: nat
h: x.+1 < n.+1
P n (x; leq_pred' h) apply IHn.
Defined.

Definition finnat_ind_beta_zero@{u} (P : forall n : nat, FinNat n -> Type@{u})
  (z : forall n : nat, P n.+1 (zero_finnat n))
  (s : forall (n : nat) (u : FinNat n), P n u -> P n.+1 (succ_finnat u))
  (n : nat)
  : finnat_ind P z s (zero_finnat n) = z n.
P: forall n0 : nat, FinNat n0 -> Type
z: forall n0 : nat, P n0.+1 (zero_finnat n0)
s: forall (n0 : nat) (u : FinNat n0), P n0 u -> P n0.+1 (succ_finnat u)
n: nat
finnat_ind P z s (zero_finnat n) = z n
Proof.
P: forall n0 : nat, FinNat n0 -> Type
z: forall n0 : nat, P n0.+1 (zero_finnat n0)
s: forall (n0 : nat) (u : FinNat n0), P n0 u -> P n0.+1 (succ_finnat u)
n: nat
finnat_ind P z s (zero_finnat n) = z n
  snapply (transport2 _ (q:=idpath@{Set})).
P: forall n0 : nat, FinNat n0 -> Type
z: forall n0 : nat, P n0.+1 (zero_finnat n0)
s: forall (n0 : nat) (u : FinNat n0), P n0 u -> P n0.+1 (succ_finnat u)
n: nat
path_sigma_hprop (zero_finnat n) (0; (zero_finnat n).2) 1 = 1
  rapply path_ishprop.
Defined.

Definition finnat_ind_beta_succ@{u} (P : forall n : nat, FinNat n -> Type@{u})
  (z : forall n : nat, P n.+1 (zero_finnat n))
  (s : forall (n : nat) (u : FinNat n),
       P n u -> P n.+1 (succ_finnat u))
  {n : nat} (u : FinNat n)
  : finnat_ind P z s (succ_finnat u) = s n u (finnat_ind P z s u).
P: forall n0 : nat, FinNat n0 -> Type
z: forall n0 : nat, P n0.+1 (zero_finnat n0)
s: forall (n0 : nat) (u0 : FinNat n0), P n0 u0 -> P n0.+1 (succ_finnat u0)
n: nat
u: FinNat n
finnat_ind P z s (succ_finnat u) = s n u (finnat_ind P z s u)
Proof.
P: forall n0 : nat, FinNat n0 -> Type
z: forall n0 : nat, P n0.+1 (zero_finnat n0)
s: forall (n0 : nat) (u0 : FinNat n0), P n0 u0 -> P n0.+1 (succ_finnat u0)
n: nat
u: FinNat n
finnat_ind P z s (succ_finnat u) = s n u (finnat_ind P z s u)
  destruct u as [u1 u2]; simpl; unfold path_succ_finnat.
P: forall n0 : nat, FinNat n0 -> Type
z: forall n0 : nat, P n0.+1 (zero_finnat n0)
s: forall (n0 : nat) (u : FinNat n0), P n0 u -> P n0.+1 (succ_finnat u)
n, u1: nat
u2: u1 < n
transport (P n.+1)
  (path_sigma_hprop (succ_finnat (u1; leq_pred' (leq_succ u2)))
     (u1.+1; leq_succ u2) 1)
  (s n (u1; leq_pred' (leq_succ u2))
     (finnat_ind P z s (u1; leq_pred' (leq_succ u2)))) =
s n (u1; u2) (finnat_ind P z s (u1; u2))
  destruct (path_ishprop u2 (leq_pred' (leq_succ u2))).
P: forall n0 : nat, FinNat n0 -> Type
z: forall n0 : nat, P n0.+1 (zero_finnat n0)
s: forall (n0 : nat) (u : FinNat n0), P n0 u -> P n0.+1 (succ_finnat u)
n, u1: nat
u2: u1 < n
transport (P n.+1)
  (path_sigma_hprop (succ_finnat (u1; u2)) (u1.+1; leq_succ u2) 1)
  (s n (u1; u2) (finnat_ind P z s (u1; u2))) =
s n (u1; u2) (finnat_ind P z s (u1; u2))
  refine (transport2 _ (q:=idpath@{Set}) _ _).
P: forall n0 : nat, FinNat n0 -> Type
z: forall n0 : nat, P n0.+1 (zero_finnat n0)
s: forall (n0 : nat) (u : FinNat n0), P n0 u -> P n0.+1 (succ_finnat u)
n, u1: nat
u2: u1 < n
path_sigma_hprop (succ_finnat (u1; u2)) (u1.+1; leq_succ u2) 1 = 1
  rapply path_ishprop.
Defined.

Definition is_bounded_fin_to_nat@{} {n} (k : Fin n)
  : fin_to_nat k < n.
n: nat
k: Fin n
fin_to_nat k < n
Proof.
n: nat
k: Fin n
fin_to_nat k < n
  induction n as [| n IHn].
k: Fin 0
fin_to_nat k < 0
n: nat
k: Fin n.+1
IHn: forall k0 : Fin n, fin_to_nat k0 < n
fin_to_nat k < n.+1
  -
k: Fin 0
fin_to_nat k < 0 elim k.
  -
n: nat
k: Fin n.+1
IHn: forall k0 : Fin n, fin_to_nat k0 < n
fin_to_nat k < n.+1 destruct k as [k | []].
n: nat
k: Fin n
IHn: forall k0 : Fin n, fin_to_nat k0 < n
fin_to_nat (inl k) < n.+1
n: nat
IHn: forall k : Fin n, fin_to_nat k < n
fin_to_nat (inr tt) < n.+1
    +
n: nat
k: Fin n
IHn: forall k0 : Fin n, fin_to_nat k0 < n
fin_to_nat (inl k) < n.+1 rapply lt_succ_r. (* Typeclass search finds a different solution, but we want this one. *)
    +
n: nat
IHn: forall k : Fin n, fin_to_nat k < n
fin_to_nat (inr tt) < n.+1 exact _.
Defined.

Definition fin_to_finnat {n} (k : Fin n) : FinNat n
  := (fin_to_nat k; is_bounded_fin_to_nat k).

(** Because the proof of [is_bounded_fin_to_nat] was chosen carefully, we have the following definitional equality. *)
Definition path_fin_to_finnat_fin_incl_incl_finnat_fin_to_finnat {n} (k : Fin n)
  : fin_to_finnat (fin_incl k) = incl_finnat (fin_to_finnat k)
  := idpath.

Fixpoint finnat_to_fin@{} {n : nat} : FinNat n -> Fin n
  := match n with
     | 0 => fun u => Empty_rec (not_lt_zero_r _ u.2)
     | n.+1 => fun u =>
        match u with
        | (0; _) => fin_zero
        | (x.+1; h) => fsucc (finnat_to_fin (x; leq_pred' h))
        end
     end.

Definition path_fin_to_finnat_fsucc@{} {n : nat} (k : Fin n)
  : fin_to_finnat (fsucc k) = succ_finnat (fin_to_finnat k).
n: nat
k: Fin n
fin_to_finnat (fsucc k) = succ_finnat (fin_to_finnat k)
Proof.
n: nat
k: Fin n
fin_to_finnat (fsucc k) = succ_finnat (fin_to_finnat k)
  apply path_sigma_hprop.
n: nat
k: Fin n
(fin_to_finnat (fsucc k)).1 = (succ_finnat (fin_to_finnat k)).1
  apply path_nat_fsucc.
Defined.

Definition path_fin_to_finnat_fin_zero@{} (n : nat)
  : fin_to_finnat (@fin_zero n) = zero_finnat n.
n: nat
fin_to_finnat fin_zero = zero_finnat n
Proof.
n: nat
fin_to_finnat fin_zero = zero_finnat n
  apply path_sigma_hprop.
n: nat
(fin_to_finnat fin_zero).1 = (zero_finnat n).1
  exact path_nat_fin_zero.
Defined.

Definition path_finnat_to_fin_succ@{} {n : nat} (u : FinNat n)
  : finnat_to_fin (succ_finnat u) = fsucc (finnat_to_fin u).
n: nat
u: FinNat n
finnat_to_fin (succ_finnat u) = fsucc (finnat_to_fin u)
Proof.
n: nat
u: FinNat n
finnat_to_fin (succ_finnat u) = fsucc (finnat_to_fin u)
  cbn.
n: nat
u: FinNat n
fsucc
  (finnat_to_fin
     (u.1;
     leq_rec u.1.+2 (fun (m : nat) (_ : u.1.+2 <= m) => u.1.+1 <= nat_pred m)
       (leq_refl u.1.+1)
       (fun (m : nat) (_ : u.1.+2 <= m) (IHleq : u.1.+1 <= nat_pred m) =>
        leq_trans IHleq pred_leq)
       n.+1 (leq_succ u.2))) =
fsucc (finnat_to_fin u) do 2 f_ap.
n: nat
u: FinNat n
(u.1;
leq_rec u.1.+2 (fun (m : nat) (_ : u.1.+2 <= m) => u.1.+1 <= nat_pred m)
  (leq_refl u.1.+1)
  (fun (m : nat) (_ : u.1.+2 <= m) (IHleq : u.1.+1 <= nat_pred m) =>
   leq_trans IHleq pred_leq)
  n.+1 (leq_succ u.2)) =
u by apply path_sigma_hprop.
Defined.

Definition path_finnat_to_fin_incl@{} {n : nat} (u : FinNat n)
  : finnat_to_fin (incl_finnat u) = fin_incl (finnat_to_fin u).
n: nat
u: FinNat n
finnat_to_fin (incl_finnat u) = fin_incl (finnat_to_fin u)
Proof.
n: nat
u: FinNat n
finnat_to_fin (incl_finnat u) = fin_incl (finnat_to_fin u)
  revert n u.
forall (n : nat) (u : FinNat n),
finnat_to_fin (incl_finnat u) = fin_incl (finnat_to_fin u)
  snapply finnat_ind.
forall n : nat,
(fun (n0 : nat) (u : FinNat n0) =>
 finnat_to_fin (incl_finnat u) = fin_incl (finnat_to_fin u)) n.+1
  (zero_finnat n)
forall (n : nat) (u : FinNat n),
(fun (n0 : nat) (u0 : FinNat n0) =>
 finnat_to_fin (incl_finnat u0) = fin_incl (finnat_to_fin u0)) n u ->
(fun (n0 : nat) (u0 : FinNat n0) =>
 finnat_to_fin (incl_finnat u0) = fin_incl (finnat_to_fin u0)) n.+1
  (succ_finnat u)
  1: reflexivity.
forall (n : nat) (u : FinNat n),
(fun (n0 : nat) (u0 : FinNat n0) =>
 finnat_to_fin (incl_finnat u0) = fin_incl (finnat_to_fin u0)) n u ->
(fun (n0 : nat) (u0 : FinNat n0) =>
 finnat_to_fin (incl_finnat u0) = fin_incl (finnat_to_fin u0)) n.+1
  (succ_finnat u)
  intros n u; cbn beta; intros p.
n: nat
u: FinNat n
p: finnat_to_fin (incl_finnat u) = fin_incl (finnat_to_fin u)
finnat_to_fin (incl_finnat (succ_finnat u)) =
fin_incl (finnat_to_fin (succ_finnat u))
  lhs exact (path_finnat_to_fin_succ (incl_finnat u)).
n: nat
u: FinNat n
p: finnat_to_fin (incl_finnat u) = fin_incl (finnat_to_fin u)
fsucc (finnat_to_fin (incl_finnat u)) =
fin_incl (finnat_to_fin (succ_finnat u))
  lhs exact (ap fsucc p).
n: nat
u: FinNat n
p: finnat_to_fin (incl_finnat u) = fin_incl (finnat_to_fin u)
fsucc (fin_incl (finnat_to_fin u)) = fin_incl (finnat_to_fin (succ_finnat u))
  exact (ap fin_incl (path_finnat_to_fin_succ _))^.
Defined.

Definition path_finnat_to_fin_last@{} (n : nat)
  : finnat_to_fin (last_finnat n) = fin_last.
n: nat
finnat_to_fin (last_finnat n) = fin_last
Proof.
n: nat
finnat_to_fin (last_finnat n) = fin_last
  induction n as [| n IHn].
finnat_to_fin (last_finnat 0) = fin_last
n: nat
IHn: finnat_to_fin (last_finnat n) = fin_last
finnat_to_fin (last_finnat n.+1) = fin_last
  -
finnat_to_fin (last_finnat 0) = fin_last reflexivity.
  -
n: nat
IHn: finnat_to_fin (last_finnat n) = fin_last
finnat_to_fin (last_finnat n.+1) = fin_last exact (ap fsucc IHn).
Defined.

Definition path_finnat_to_fin_to_finnat@{} {n : nat} (u : FinNat n)
  : fin_to_finnat (finnat_to_fin u) = u.
n: nat
u: FinNat n
fin_to_finnat (finnat_to_fin u) = u
Proof.
n: nat
u: FinNat n
fin_to_finnat (finnat_to_fin u) = u
  induction n as [| n IHn].
u: FinNat 0
fin_to_finnat (finnat_to_fin u) = u
n: nat
u: FinNat n.+1
IHn: forall u0 : FinNat n, fin_to_finnat (finnat_to_fin u0) = u0
fin_to_finnat (finnat_to_fin u) = u
  -
u: FinNat 0
fin_to_finnat (finnat_to_fin u) = u elim (not_lt_zero_r _ u.2).
  -
n: nat
u: FinNat n.+1
IHn: forall u0 : FinNat n, fin_to_finnat (finnat_to_fin u0) = u0
fin_to_finnat (finnat_to_fin u) = u destruct u as [x h].
n, x: nat
h: x < n.+1
IHn: forall u : FinNat n, fin_to_finnat (finnat_to_fin u) = u
fin_to_finnat (finnat_to_fin (x; h)) = (x; h)
    apply path_sigma_hprop.
n, x: nat
h: x < n.+1
IHn: forall u : FinNat n, fin_to_finnat (finnat_to_fin u) = u
(fin_to_finnat (finnat_to_fin (x; h))).1 = (x; h).1
    destruct x as [| x].
n: nat
h: 0 < n.+1
IHn: forall u : FinNat n, fin_to_finnat (finnat_to_fin u) = u
(fin_to_finnat (finnat_to_fin (0; h))).1 = (0; h).1
n, x: nat
h: x.+1 < n.+1
IHn: forall u : FinNat n, fin_to_finnat (finnat_to_fin u) = u
(fin_to_finnat (finnat_to_fin (x.+1; h))).1 = (x.+1; h).1
    +
n: nat
h: 0 < n.+1
IHn: forall u : FinNat n, fin_to_finnat (finnat_to_fin u) = u
(fin_to_finnat (finnat_to_fin (0; h))).1 = (0; h).1 exact (ap pr1 (path_fin_to_finnat_fin_zero n)).
    +
n, x: nat
h: x.+1 < n.+1
IHn: forall u : FinNat n, fin_to_finnat (finnat_to_fin u) = u
(fin_to_finnat (finnat_to_fin (x.+1; h))).1 = (x.+1; h).1 refine ((path_fin_to_finnat_fsucc _)..1 @ _).
n, x: nat
h: x.+1 < n.+1
IHn: forall u : FinNat n, fin_to_finnat (finnat_to_fin u) = u
(succ_finnat
   (fin_to_finnat
      ((fix finnat_to_fin (n0 : nat) : FinNat n0 -> Fin n0 :=
          match n0 as n1 return (FinNat n1 -> Fin n1) with
          | 0 => fun u : FinNat 0 => Empty_rec (not_lt_zero_r u.1 u.2)
          | n1.+1 =>
              fun u : FinNat n1.+1 =>
              let u0 := u in
              let proj1 := u0.1 in
              let h0 := u0.2 in
              match proj1 as proj0 return (proj0 < n1.+1 -> Fin n1.+1) with
              | 0 => fun _ : 0 < n1.+1 => fin_zero
              | x0.+1 =>
                  fun h1 : x0.+1 < n1.+1 =>
                  fsucc (finnat_to_fin n1 (x0; leq_pred' h1))
              end h0
          end)
         n (x; leq_pred' h)))).1 =
(x.+1; h).1
      exact (ap S (IHn (x; leq_pred' h))..1).
Defined.

Definition path_fin_to_finnat_to_fin@{} {n : nat} (k : Fin n)
  : finnat_to_fin (fin_to_finnat k) = k.
n: nat
k: Fin n
finnat_to_fin (fin_to_finnat k) = k
Proof.
n: nat
k: Fin n
finnat_to_fin (fin_to_finnat k) = k
  induction n as [| n IHn].
k: Fin 0
finnat_to_fin (fin_to_finnat k) = k
n: nat
k: Fin n.+1
IHn: forall k0 : Fin n, finnat_to_fin (fin_to_finnat k0) = k0
finnat_to_fin (fin_to_finnat k) = k
  -
k: Fin 0
finnat_to_fin (fin_to_finnat k) = k elim k.
  -
n: nat
k: Fin n.+1
IHn: forall k0 : Fin n, finnat_to_fin (fin_to_finnat k0) = k0
finnat_to_fin (fin_to_finnat k) = k destruct k as [k | []].
n: nat
k: Fin n
IHn: forall k0 : Fin n, finnat_to_fin (fin_to_finnat k0) = k0
finnat_to_fin (fin_to_finnat (inl k)) = inl k
n: nat
IHn: forall k : Fin n, finnat_to_fin (fin_to_finnat k) = k
finnat_to_fin (fin_to_finnat (inr tt)) = inr tt
    +
n: nat
k: Fin n
IHn: forall k0 : Fin n, finnat_to_fin (fin_to_finnat k0) = k0
finnat_to_fin (fin_to_finnat (inl k)) = inl k specialize (IHn k).
n: nat
k: Fin n
IHn: finnat_to_fin (fin_to_finnat k) = k
finnat_to_fin (fin_to_finnat (inl k)) = inl k
      refine (path_finnat_to_fin_incl (fin_to_finnat k) @ _).
n: nat
k: Fin n
IHn: finnat_to_fin (fin_to_finnat k) = k
fin_incl (finnat_to_fin (fin_to_finnat k)) = inl k
      exact (ap fin_incl IHn).
    +
n: nat
IHn: forall k : Fin n, finnat_to_fin (fin_to_finnat k) = k
finnat_to_fin (fin_to_finnat (inr tt)) = inr tt apply path_finnat_to_fin_last.
Defined.

Definition equiv_fin_finnat@{} (n : nat) : Fin n <~> FinNat n
  := equiv_adjointify fin_to_finnat finnat_to_fin
      path_finnat_to_fin_to_finnat
      path_fin_to_finnat_to_fin.