--#include "Datoid.alfa"

--#include "New/Datoid/Unit.alfa"

Ncons :: Set
  = data Z | S

DNcons :: Datoid
  = struct {
      Elem = Ncons;
      eq =
        {-#H#-}\(c1::Elem) ->
               \(c2::Elem) ->
               case c1 of {
                 (Z) ->
                   case c2 of {
                     (Z) -> true@_;
                     (S) -> false@_;};
                 (S) ->
                   case c2 of {
                     (Z) -> false@_;
                     (S) -> true@_;};};
      ref =
        {-#H#-}\(x::Elem) ->
               case x of {
                 (Z) -> tt@_;
                 (S) -> tt@_;};
      subst =
        {-#H#-}\(P::Pow Elem) ->
               \(a1::Elem) ->
               \(a2::Elem) ->
               \(h::True (eq a1 a2)) ->
               \(h'::P a1) ->
               case a1 of {
                 (Z) ->
                   case a2 of {
                     (Z) -> h';
                     (S) -> case h of { };};
                 (S) ->
                   case a2 of {
                     (Z) -> case h of { };
                     (S) -> h';};};}

sigmaN (i::Ncons) :: Sig
  = case i of {
      (Z) -> nil@_;
      (S) -> rec@_ nil@_;}

spN :: Sig
  = nonrec@_ DNcons sigmaN

FN (X::Set) :: Set
  = F spN X

IN :: Set
  = T spN

Izero :: IN
  = Intro@_
      (dep_pair DNcons.Elem (\(d::DNcons.Elem) -> F (sigmaN d) (T spN)) Z@_
         tt@_)

Isucc (n::IN) :: IN
  = Intro@_
      (dep_pair DNcons.Elem (\(d::DNcons.Elem) -> F (sigmaN d) (T spN)) S@_
         (pair (T spN) (F nil@_ (T spN)) n tt@_))

Ione :: IN
  = Isucc Izero

eqIN :: IN -> IN -> Bool
  = (deq spN).eq

test1 :: Bool
  = eqIN Ione Ione

test2 :: Bool
  = eqIN Izero Ione
{-# Alfa unfoldgoals off
brief on
hidetypeannots off
wide

nd
hiding on
 #-}