--#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" #-}