--#include "../Prelude.alfa"

--#include "Base.alfa"

--#include "DatoidBase.alfa"

open DatoidBase  use  deqUnit,  deqTimes,  deqSum

-- One Datoid utility specialized to DAlgebraic:

-- If one of two isomorphic sets is a datoid, then both are.

-- As Intro is an isomorphism we can define this special case (needed below).

liftDeq (fi::Sig)(d::Deq (F fi (T fi))) :: Deq (T fi)
  = struct {
      eq =
        \(t1::T fi) ->
        \(t2::T fi) ->
        case t1 of { (Intro x1) -> case t2 of { (Intro x2) -> d.eq x1 x2;};};
      ref = \(t::T fi) -> case t of { (Intro x) -> d.ref x;};
      subst =
        \(C::T fi -> Set) ->
        \(t1::T fi) ->
        \(t2::T fi) ->
        case t1 of {
          (Intro x1) ->
            case t2 of {
              (Intro x2) -> d.subst (\(x::F fi (T fi)) -> C (Intro@_ x)) x1 x2;};};}

-- The recursive step / induction step

deqstep (fi::Sig)(Y::Set)(d::Deq Y) :: Deq (F fi Y)
  = case fi of {
      (nil) -> deqUnit;
      (nonrec D g) ->
        deqSum D.Elem (\(d'::D.Elem) -> F (g d') Y) (deqD D)
          (\(a::D.Elem) -> deqstep (g a) Y d);
      (rec fi') -> deqTimes Y (F fi' Y) d (deqstep fi' Y d);}

-- Tie the knot: we get datoids from all DAlgebraic codes 

deq (fi::Sig) :: Deq (T fi)
  = liftDeq fi (deqstep fi (T fi) (deq fi))

{-# Alfa unfoldgoals off
brief on
hidetypeannots off
wide

nd
hiding on
var "deqSum" hide 2
var "deqTimes" hide 2
var "Eq" distfix3 as "Eq"
 #-}