Agda-2.3.2.2: examples/outdated-and-incorrect/Subset.agda

-- Proof irrelevance is nice when you want to work with subsets.
module Subset where

data True : Prop where
  tt : True

data False : Prop where

data (|) (A:Set)(P:A -> Prop) : Set where
  sub : (x:A) -> P x -> A | P

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

mutual
  IsEven : Nat -> Prop
  IsEven  zero   = True
  IsEven (suc n) = IsOdd n

  IsOdd : Nat -> Prop
  IsOdd  zero   = False
  IsOdd (suc n) = IsEven n

Even : Set
Even = Nat | IsEven

Odd : Set
Odd = Nat | IsOdd

(+) : Nat -> Nat -> Nat
zero  + m = m
suc n + m = suc (n + m)