help links subscribe changes refresh edit

	Limits and Colimits	SubDomain
SandBoxAldorInductiveTypes ←	↑		→ SandBoxProduct

SandBoxEqualizerInOpenAxiom

Edit detail for SandBoxEqualizerInOpenAxiom revision 1 of 2

	1 2
Editor: page Time: 2009/01/08 11:29:59 GMT-8
Note:

changed:
-
In FriCAS 'Equalizer' (See: LimitsAndColimits) can be defined as a
'SubDomain' as follows, but this does not work in the most recent
version of OpenAxiom which produces the error message::

  predicate =f(#1)g(#1) is not simple enough

\begin{spad}
)abbrev domain EQLZR Equalizer
Equalizer(X:SetCategory,Y:SetCategory,f:X->Y, g:X->Y): SetCategory with
    eq: % -> X
  == SubDomain(X,f #1 = g #1) add
    --
    eq(x:%):X == x pretend X

)abbrev package EQLZF EqualizerFunctions
EqualizerFunctions(X:SetCategory,Y:SetCategory,f:X->Y,g:X->Y, M:SetCategory,m:M->X): with
    u: M->Equalizer(X,Y,f,g)
  == add
    --
    u(x:M):Equalizer(X,Y,f,g) == m(x) pretend Equalizer(X,Y,f,g)
\end{spad}

\begin{axiom}
)show Equalizer(Float,Float,sin,cos)
\end{axiom}

In FriCAS? Equalizer (See: LimitsAndColimits?) can be defined as a SubDomain as follows, but this does not work in the most recent version of OpenAxiom? which produces the error message:

  predicate =f(#1)g(#1) is not simple enough

spad

)abbrev domain EQLZR Equalizer
Equalizer(X:SetCategory,Y:SetCategory,f:X->Y, g:X->Y): SetCategory with
    eq: % -> X
  == SubDomain(X,f #1 = g #1) add
    --
    eq(x:%):X == x pretend X

)abbrev package EQLZF EqualizerFunctions
EqualizerFunctions(X:SetCategory,Y:SetCategory,f:X->Y,g:X->Y, M:SetCategory,m:M->X): with
    u: M->Equalizer(X,Y,f,g)
  == add
    --
    u(x:M):Equalizer(X,Y,f,g) == m(x) pretend Equalizer(X,Y,f,g)

spad

   Compiling OpenAxiom source code from file 
      /var/zope2/var/LatexWiki/3871883559109604243-25px001.spad using 
      Spad compiler.
   EQLZR abbreviates domain Equalizer 
------------------------------------------------------------------------
   initializing NRLIB EQLZR for Equalizer 
   compiling into NRLIB EQLZR 
   Adding $ modemaps
   Adding X modemaps
   Adding Y modemaps
   Adding Boolean modemaps
****** comp fails at level 1 with expression: ******
((|add| (|SubDomain| X (= (|f| |#1|) (|g| |#1|)))
        (CAPSULE (DEF (|eq| |x|) (X $) (NIL NIL) (|pretend| |x| X)))))
****** level 1  ******
$x:= (add (SubDomain X (= (f #1) (g #1))) (CAPSULE (DEF (eq x) (X $) (NIL NIL) (pretend x X))))
$m:= (Join (SetCategory) (CATEGORY domain (SIGNATURE eq (X $))))
$f:=
((((~= # . #2=(# #)) (= # . #5=(# #)) (|coerce| # . #8=(# #))
   (|hash| # . #11=(# #)) ...)))

   >> Apparent user error:
   predicate =f(#1)g(#1) is not simple enough

axiom

)show Equalizer(Float,Float,sin,cos)

   Equalizer is an unknown constructor and so is unavailable. Did you
      mean to use -> but type something different instead?