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.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.PathGroupoids Require Import Types.Empty Types.Sigma Types.Sum Types.Prod Types.Equiv. Require Import Spaces.Nat.Core. Require Import Finite.Fin.