2
module QualifiedConstructors where
13
one₂ = Nat₂.suc Nat₂.zero
15
record Suc : Set where
25
conv Nat₂.zero = Nat₁.zero
26
conv (Nat₂.suc n) = Nat₁.suc (conv n)
28
data _≡_ {A : Set}(x : A) : A → Set where
31
inj : (n m : Nat₁) → Nat₁.suc n ≡ suc m → n ≡ m