(n : nat) : nat -> nat := fun i => if dec (i < n)%nat then i else i.+1%nat. Global Instance isinjective_skip n : IsInjective ( n). Proof. hnf. intros x y p. unfold in p. destruct (dec (x < n)%nat) as [H|H], (dec (y < n)%nat) as [H'|H']. - exact p. - destruct p^. contradiction (H' (leq_trans _ H)). - destruct p. contradiction (H (leq_trans _ H')). - by apply path_nat_succ. Defined.
Require Import Basics.Overture Basics.Trunc Basics.Tactics Basics.Decidable. Require Import Types.Sigma. Require Import Spaces.List.Core Spaces.List.Theory Spaces.List.Paths. Require Import Algebra.Rings.Ring Algebra.Rings.Module Algebra.Rings.CRing Require Import abstract_algebra. Require Import WildCat.Core WildCat.Paths. Require Import Modalities.ReflectiveSubuniverse.