Idris code for the problem posed in Joseph Abrahamson's type theory talk http://jspha.com/posts/papers_we_love_BOS_2/

DecideParity.idr

-- Axioms
rec_N :
  (P : Nat -> Type) ->
  (ind : (n : Nat) -> P n -> P (S n)) ->
  (base : P Z) ->
  (m : Nat) ->
  P m
Even : (n : Nat) -> Type
Odd : (n : Nat) -> Type
zeroIsEven : Even Z
succEven : Even n -> Odd (S n)
succOdd : Odd n -> Even (S n)

-- Proof
decideParity : (n : Nat) -> Either (Even n) (Odd n)
decideParity = rec_N P ind base
  where
    P : (n : Nat) -> Type
    P n = Either (Even n) (Odd n)

    ind : (n : Nat) -> P n -> P (S n)
    ind n (Left p) = Right (succEven p)
    ind n (Right p) = Left (succOdd p)

    base : P Z
    base = Left zeroIsEven

DecideParity2.idr

-- Same as above, but replacing Either with (\/) and giving it introduction
-- and elimination axioms similar to the other types being used

-- Axioms
ind_N :
  (P : Nat -> Type) ->
  (ind : (n : Nat) -> P n -> P (S n)) ->
  (base : P Z) ->
  (m : Nat) ->
  P m

infixl 9 \/
(\/) : {A, B : Type} -> A -> B -> Type
inl : {A, B : Type} -> A -> A \/ B
inr : {A, B : Type} -> B -> A \/ B
rec_or : {A, B, C : Type} -> (A -> C) -> (B -> C) -> (A \/ B) -> C

Even : (n : Nat) -> Type
Odd : (n : Nat) -> Type
zeroIsEven : Even Z
succEven : Even n -> Odd (S n)
succOdd : Odd n -> Even (S n)

-- Proof
decideParity : (n : Nat) -> Even n \/ Odd n
decideParity = ind_N P ind base
  where
    P : (n : Nat) -> Type
    P n = Even n \/ Odd n

    ind : (n : Nat) -> P n -> P (S n)
    ind n = rec_or (inr . succEven) (inl . succOdd)

    base : P Z
    base = inl zeroIsEven