fact: 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.
imports: HoTT.Basics HoTT.Types HoTT.HSet HoTT.Spaces.Nat.Core HoTT.Spaces.Finite.Fin