--#include "Lib/SET.alfa"

--#include "Lib/Op/Nat.alfa"

--#include "Lib/Op/Bool.alfa"

--#include "Sigma.alfa"
--#include "And.alfa"

open SET
 use  Unit,  Bool,  Absurd,  Nat,  True,  Pow,  Rel,  rel,  Reflexive,
      Symmetrical,  Transitive,  Substitutive,  Deq,  Equality,
      Datoid,  Setoid, cmp,  id, Times, pair

open OpNat  use  one,  two,  (+)

open OpBool  use  and

{-
liftRel (A::Set)(r::rel A) :: Rel A
  = \(h::A) -> \(h'::A) -> True (r h h')

substitutive (A::Set)(r::rel A) :: Type
  = Substitutive A (liftRel A r)
-}

package Datoids where
  eqBool (a::Bool)(b::Bool) :: Bool
    = case a of {
        (false) ->
          case b of {
            (false) -> true@_;
            (true) -> false@_;};
        (true) ->
          case b of {
            (false) -> false@_;
            (true) -> true@_;};}
  DBool :: Datoid
    = struct {
        Elem = Bool;
        eq = eqBool;
        ref =
          \(x::Elem) ->
          case x of {
            (false) -> tt@_;
            (true) -> tt@_;};
        subst =
          \(P::Pow Elem) ->
          \(a1::Elem) ->
          \(a2::Elem) ->
          \(h::True (eq a1 a2)) ->
          \(h'::P a1) ->
          case a1 of {
            (false) ->
              case a2 of {
                (false) -> h';
                (true) -> case h of { };};
            (true) ->
              case a2 of {
                (false) -> case h of { };
                (true) -> h';};};}
  eqNat (m::Nat)(n::Nat) :: Bool
    = case m of {
        (zer) ->
          case n of {
            (zer) -> true@_;
            (suc n') -> false@_;};
        (suc n') ->
          case n of {
            (zer) -> false@_;
            (suc n0) -> eqNat n' n0;};}
  DNat :: Datoid
    = struct {
        Elem = Nat;
        eq = eqNat;
        ref =
          \(x::Elem) ->
          case x of {
            (zer) -> tt@_;
            (suc n) -> ref n;};
        subst =
          \(P::Pow Elem) ->
          \(a1::Elem) ->
          \(a2::Elem) ->
          \(h::True (eq a1 a2)) ->
          \(h'::P a1) ->
          case a1 of {
            (zer) ->
              case a2 of {
                (zer) -> h';
                (suc n) -> case h of { };};
            (suc n) ->
              case a2 of {
                (zer) -> case h of { };
                (suc n') ->
                  let mutual P1 :: Pow Elem
                               = \(x::Elem) -> P (suc@_ x)
                             h1 :: P1 n
                               = h'
                  in  subst P1 n n' h h1;};};}
{-# Alfa unfoldgoals off
brief on
hidetypeannots off
wide
typesignatures
nd
hiding on
var "eqNat" infix as "=="
var "Unit" as "()"
con "tt" as "*"
var "Sigma" quantifier domain on as "S" with symbolfont
var "And" infix rightassoc as "´" with symbolfont
con "Pair" tuple
con "si" tuple
con "Zero" as "0"
var "one" as "1"
var "two" as "2"
var "cmp" hide 3
var "id" hide 1
 #-}