Int_ind. Global Instance decidable_paths_int@{} : DecidablePaths Int. Proof. intros x y. destruct x as [x | | x], y as [y | | y]. 2-4,6-8: right; intros; discriminate. 2: by left. 1,2: nrapply decidable_iff. 1,3: split. 1,3: nrapply ap. 1,2: intros H; by injection H. 1,2: exact _. Defined.
Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe. Require Import Spaces.Nat.Core.