--#include "DAlgebraic.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@_ (si@_ Z@_ tt@_)

Isucc (n::IN) :: IN
  = Intro@_ (si@_ S@_ (Pair@_ n tt@_))

Ione :: IN
  = Isucc Izero

eqKnot (fi::Sig)(a::T fi)(b::T fi) :: Bool
  = d_eq (T fi) (eqKnot fi) fi (out fi a) (out fi b)

eqIN (a::IN)(b::IN) :: Bool
  = eqKnot spN a b

eqIN2 (a::IN)(b::IN) :: Bool
  = It2 spN Bool d_eq a b
{-# Alfa unfoldgoals off
brief on
hidetypeannots off
wide
typesignatures
nd
hiding on
 #-}