chap3.txt

  
  3 Morphisms
  
  Any  GAP  object satisfying IsCapCategoryMorphism can be added to a category
  and then becomes a morphism in this category. Any morphism can belong to one
  or  no category. After a GAP object is added to the category, it knows which
  things  can be computed in its category and to which category it belongs. It
  knows   categorical   properties  and  attributes,  and  the  functions  for
  existential quantifiers can be applied to the morphism.
  
  
  3.1 Attributes for the Type of Morphisms
  
  3.1-1 CapCategory
  
  CapCategory( alpha )  attribute
  Returns:  a category
  
  The  argument is a morphism \alpha. The output is the category \mathbf{C} to
  which \alpha was added.
  
  3.1-2 Source
  
  Source( alpha )  attribute
  Returns:  an object
  
  The argument is a morphism \alpha: a \rightarrow b. The output is its source
  a.
  
  3.1-3 Range
  
  Range( alpha )  attribute
  Returns:  an object
  
  The  argument is a morphism \alpha: a \rightarrow b. The output is its range
  b.
  
  
  3.2 Categorical Properties of Morphisms
  
  3.2-1 AddIsMonomorphism
  
  AddIsMonomorphism( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given  function F to the category for the basic operation IsMonomorphism. F:
  \alpha \mapsto \mathtt{IsMonomorphism}(\alpha).
  
  3.2-2 AddIsEpimorphism
  
  AddIsEpimorphism( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given  function  F to the category for the basic operation IsEpimorphism. F:
  \alpha \mapsto \mathtt{IsEpimorphism}(\alpha).
  
  3.2-3 AddIsIsomorphism
  
  AddIsIsomorphism( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given  function  F to the category for the basic operation IsIsomorphism. F:
  \alpha \mapsto \mathtt{IsIsomorphism}(\alpha).
  
  3.2-4 AddIsSplitMonomorphism
  
  AddIsSplitMonomorphism( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  IsSplitMonomorphism. F: \alpha \mapsto \mathtt{IsSplitMonomorphism}(\alpha).
  
  3.2-5 AddIsSplitEpimorphism
  
  AddIsSplitEpimorphism( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given function F to the category for the basic operation IsSplitEpimorphism.
  F: \alpha \mapsto \mathtt{IsSplitEpimorphism}(\alpha).
  
  3.2-6 AddIsOne
  
  AddIsOne( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given  function  F  to the category for the basic operation IsOne. F: \alpha
  \mapsto \mathtt{IsOne}(\alpha).
  
  3.2-7 AddIsIdempotent
  
  AddIsIdempotent( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given  function  F  to the category for the basic operation IsIdempotent. F:
  \alpha \mapsto \mathtt{IsIdempotent}(\alpha).
  
  
  3.3 Non-Categorical Properties of Morphisms
  
  Non-categorical properties are not stable under equivalences of categories.
  
  3.3-1 IsIdenticalToIdentityMorphism
  
  IsIdenticalToIdentityMorphism( alpha )  property
  Returns:  a boolean
  
  The  argument  is  a morphism \alpha: a \rightarrow b. The output is true if
  \alpha = \mathrm{id}_a, otherwise the output is false.
  
  3.3-2 AddIsIdenticalToIdentityMorphism
  
  AddIsIdenticalToIdentityMorphism( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  IsIdenticalToIdentityMorphism.           F:          \alpha          \mapsto
  \mathtt{IsIdenticalToIdentityMorphism}(\alpha).
  
  3.3-3 IsIdenticalToZeroMorphism
  
  IsIdenticalToZeroMorphism( alpha )  property
  Returns:  a boolean
  
  The  argument  is  a morphism \alpha: a \rightarrow b. The output is true if
  \alpha = 0, otherwise the output is false.
  
  3.3-4 AddIsIdenticalToZeroMorphism
  
  AddIsIdenticalToZeroMorphism( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  IsIdenticalToZeroMorphism.            F:            \alpha           \mapsto
  \mathtt{IsIdenticalToZeroMorphism }(\alpha).
  
  3.3-5 AddIsEndomorphism
  
  AddIsEndomorphism( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given  function F to the category for the basic operation IsEndomorphism. F:
  \alpha \mapsto \mathtt{IsEndomorphism}(\alpha).
  
  3.3-6 AddIsAutomorphism
  
  AddIsAutomorphism( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given  function F to the category for the basic operation IsAutomorphism. F:
  \alpha \mapsto \mathtt{IsAutomorphism}(\alpha).
  
  
  3.4 Equality and Congruence for Morphisms
  
  3.4-1 IsCongruentForMorphisms
  
  IsCongruentForMorphisms( alpha, beta )  operation
  Returns:  a boolean
  
  The  arguments  are two morphisms \alpha, \beta: a \rightarrow b. The output
  is true if \alpha \sim_{a,b} \beta, otherwise the output is false.
  
  3.4-2 AddIsCongruentForMorphisms
  
  AddIsCongruentForMorphisms( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  IsCongruentForMorphisms.        F:       (\alpha,       \beta)       \mapsto
  \mathtt{IsCongruentForMorphisms}(\alpha, \beta).
  
  3.4-3 IsEqualForMorphisms
  
  IsEqualForMorphisms( alpha, beta )  operation
  Returns:  a boolean
  
  The  arguments  are two morphisms \alpha, \beta: a \rightarrow b. The output
  is true if \alpha = \beta, otherwise the output is false.
  
  3.4-4 AddIsEqualForMorphisms
  
  AddIsEqualForMorphisms( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  IsEqualForMorphisms.         F:        (\alpha,        \beta)        \mapsto
  \mathtt{IsEqualForMorphisms}(\alpha, \beta).
  
  3.4-5 IsEqualForMorphismsOnMor
  
  IsEqualForMorphismsOnMor( alpha, beta )  operation
  Returns:  a boolean
  
  The   arguments  are  two  morphisms  \alpha:  a  \rightarrow  b,  \beta:  c
  \rightarrow d. The output is true if \alpha = \beta, otherwise the output is
  false.
  
  3.4-6 AddIsEqualForMorphismsOnMor
  
  AddIsEqualForMorphismsOnMor( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  IsEqualForMorphismsOnMor.       F:       (\alpha,       \beta)       \mapsto
  \mathtt{IsEqualForMorphismsOnMor}(\alpha, \beta).
  
  
  3.5 Basic Operations for Morphisms in Ab-Categories
  
  3.5-1 IsZeroForMorphisms
  
  IsZeroForMorphisms( alpha )  operation
  Returns:  a boolean
  
  The  argument  is  a morphism \alpha: a \rightarrow b. The output is true if
  \alpha \sim_{a,b} 0, otherwise the output is false.
  
  3.5-2 AddIsZeroForMorphisms
  
  AddIsZeroForMorphisms( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given function F to the category for the basic operation IsZeroForMorphisms.
  F: \alpha \mapsto \mathtt{IsZeroForMorphisms}(\alpha).
  
  3.5-3 AdditionForMorphisms
  
  AdditionForMorphisms( alpha, beta )  operation
  Returns:  a morphism in \mathrm{Hom}(a,b)
  
  The  arguments  are two morphisms \alpha, \beta: a \rightarrow b. The output
  is the addition \alpha + \beta.
  
  3.5-4 AddAdditionForMorphisms
  
  AddAdditionForMorphisms( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  AdditionForMorphisms. F: (\alpha, \beta) \mapsto \alpha + \beta.
  
  3.5-5 SubtractionForMorphisms
  
  SubtractionForMorphisms( alpha, beta )  operation
  Returns:  a morphism in \mathrm{Hom}(a,b)
  
  The  arguments  are two morphisms \alpha, \beta: a \rightarrow b. The output
  is the addition \alpha - \beta.
  
  3.5-6 AddSubtractionForMorphisms
  
  AddSubtractionForMorphisms( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  SubtractionForMorphisms. F: (\alpha, \beta) \mapsto \alpha - \beta.
  
  3.5-7 AdditiveInverseForMorphisms
  
  AdditiveInverseForMorphisms( alpha )  operation
  Returns:  a morphism in \mathrm{Hom}(a,b)
  
  The  argument  is  a  morphism  \alpha:  a  \rightarrow b. The output is its
  additive inverse -\alpha.
  
  3.5-8 AddAdditiveInverseForMorphisms
  
  AddAdditiveInverseForMorphisms( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  AdditiveInverseForMorphisms. F: \alpha \mapsto -\alpha.
  
  3.5-9 ZeroMorphism
  
  ZeroMorphism( a, b )  operation
  Returns:  a morphism in \mathrm{Hom}(a,b)
  
  The  arguments are two objects a and b. The output is the zero morphism 0: a
  \rightarrow b.
  
  3.5-10 AddZeroMorphism
  
  AddZeroMorphism( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given  function  F  to the category for the basic operation ZeroMorphism. F:
  (a,b) \mapsto (0: a \rightarrow b).
  
  
  3.6 Subobject and Factorobject Operations
  
  Subobjects  of  an  object  c  are  monomorphisms with range c and a special
  function  for  comparision.  Similarly,  factorobjects  of  an  object c are
  epimorphisms with source c and a special function for comparision.
  
  3.6-1 IsEqualAsSubobjects
  
  IsEqualAsSubobjects( alpha, beta )  operation
  Returns:  a boolean
  
  The  arguments  are  two  subobjects  \alpha:  a  \rightarrow  c,  \beta:  b
  \rightarrow  c.  The  output is true if there exists an isomorphism \iota: a
  \rightarrow  b  such that \beta \circ \iota \sim_{a,c} \alpha, otherwise the
  output is false.
  
  3.6-2 AddIsEqualAsSubobjects
  
  AddIsEqualAsSubobjects( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  IsEqualAsSubobjects.         F:        (\alpha,        \beta)        \mapsto
  \mathtt{IsEqualAsSubobjects}(\alpha,\beta).
  
  3.6-3 IsEqualAsFactorobjects
  
  IsEqualAsFactorobjects( alpha, beta )  operation
  Returns:  a boolean
  
  The  arguments  are  two  factorobjects  \alpha:  c  \rightarrow a, \beta: c
  \rightarrow  b.  The  output is true if there exists an isomorphism \iota: b
  \rightarrow  a  such that \iota \circ \beta \sim_{c,a} \alpha, otherwise the
  output is false.
  
  3.6-4 AddIsEqualAsFactorobjects
  
  AddIsEqualAsFactorobjects( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  IsEqualAsFactorobjects.        F:        (\alpha,       \beta)       \mapsto
  \mathtt{IsEqualAsFactorobjects}(\alpha,\beta).
  
  3.6-5 IsDominating
  
  IsDominating( alpha, beta )  operation
  Returns:  a boolean
  
  In  short:  Returns  true  iff  \alpha  is  smaller  than  \beta.  \\   Full
  description:  The  arguments  are  two  subobjects  \alpha: a \rightarrow c,
  \beta: b \rightarrow c. The output is true if there exists a morphism \iota:
  a \rightarrow b such that \beta \circ \iota \sim_{a,c} \alpha, otherwise the
  output is false.
  
  3.6-6 AddIsDominating
  
  AddIsDominating( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given  function  F  to the category for the basic operation IsDominating. F:
  (\alpha, \beta) \mapsto \mathtt{IsDominating}(\alpha,\beta).
  
  3.6-7 IsCodominating
  
  IsCodominating( alpha, beta )  operation
  Returns:  a boolean
  
  In  short:  Returns  true  iff  \alpha  is  smaller  than  \beta.  \\   Full
  description:  The  arguments  are two factorobjects \alpha: c \rightarrow a,
  \beta: c \rightarrow b. The output is true if there exists a morphism \iota:
  b \rightarrow a such that \iota \circ \beta \sim_{c,a} \alpha, otherwise the
  output is false.
  
  3.6-8 AddIsCodominating
  
  AddIsCodominating( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given  function F to the category for the basic operation IsCodominating. F:
  (\alpha, \beta) \mapsto \mathtt{IsCodominating}(\alpha,\beta).
  
  
  3.7 Identity Morphism and Composition of Morphisms
  
  3.7-1 IdentityMorphism
  
  IdentityMorphism( a )  attribute
  Returns:  a morphism in \mathrm{Hom}(a,a)
  
  The   argument  is  an  object  a.  The  output  is  its  identity  morphism
  \mathrm{id}_a.
  
  3.7-2 AddIdentityMorphism
  
  AddIdentityMorphism( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given  function  F to the category for the basic operation IdentityMorphism.
  F: a \mapsto \mathrm{id}_a.
  
  3.7-3 PreCompose
  
  PreCompose( alpha, beta )  operation
  Returns:  a morphism in \mathrm{Hom}( a, c )
  
  The   arguments  are  two  morphisms  \alpha:  a  \rightarrow  b,  \beta:  b
  \rightarrow  c.  The  output  is  the  composition  \beta  \circ  \alpha:  a
  \rightarrow c.
  
  3.7-4 PreCompose
  
  PreCompose( L )  operation
  Returns:  a morphism in \mathrm{Hom}(a_1, a_{n+1})
  
  This  is  a  convenience  method.  The argument is a list of morphisms L = (
  \alpha_1:  a_1  \rightarrow  a_2,  \alpha_2:  a_2  \rightarrow  a_3,  \dots,
  \alpha_n:   a_n  \rightarrow  a_{n+1}  ).  The  output  is  the  composition
  \alpha_{n}  \circ ( \alpha_{n-1} \circ ( \dots ( \alpha_2 \circ \alpha_1 ) )
  ).
  
  3.7-5 AddPreCompose
  
  AddPreCompose( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given  function  F  to  the  category for the basic operation PreCompose. F:
  (\alpha, \beta) \mapsto \beta \circ \alpha.
  
  3.7-6 PostCompose
  
  PostCompose( beta, alpha )  operation
  Returns:  a morphism in \mathrm{Hom}( a, c )
  
  The   arguments  are  two  morphisms  \beta:  b  \rightarrow  c,  \alpha:  a
  \rightarrow  b.  The  output  is  the  composition  \beta  \circ  \alpha:  a
  \rightarrow c.
  
  3.7-7 PostCompose
  
  PostCompose( L )  operation
  Returns:  a morphism in \mathrm{Hom}(a_1, a_{n+1})
  
  This  is  a  convenience  method.  The argument is a list of morphisms L = (
  \alpha_n:  a_n  \rightarrow  a_{n+1}, \alpha_{n-1}: a_{n-1} \rightarrow a_n,
  \dots,  \alpha_1:  a_1  \rightarrow  a_2  ).  The  output is the composition
  ((\alpha_{n} \circ \alpha_{n-1}) \circ \dots \alpha_2) \circ \alpha_1.
  
  3.7-8 AddPostCompose
  
  AddPostCompose( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given  function  F  to  the category for the basic operation PostCompose. F:
  (\alpha, \beta) \mapsto \alpha \circ \beta.
  
  
  3.8 Well-Definedness of Morphisms
  
  3.8-1 IsWellDefinedForMorphisms
  
  IsWellDefinedForMorphisms( alpha )  operation
  Returns:  a boolean
  
  The  argument  is  a  morphism  \alpha.  The  output  is  true  if \alpha is
  well-defined, otherwise the output is false.
  
  3.8-2 AddIsWellDefinedForMorphisms
  
  AddIsWellDefinedForMorphisms( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  IsWellDefinedForMorphisms.            F:            \alpha           \mapsto
  \mathtt{IsWellDefinedForMorphisms}( \alpha ).
  
  
  3.9 Basic Operations for Morphisms in Abelian Categories
  
  3.9-1 LiftAlongMonomorphism
  
  LiftAlongMonomorphism( iota, tau )  operation
  Returns:  a morphism in \mathrm{Hom}(t,k)
  
  The  arguments  are a monomorphism \iota: k \hookrightarrow a and a morphism
  \tau:  t \rightarrow a such that there is a morphism u: t \rightarrow k with
  \iota \circ u \sim_{t,a} \tau. The output is such a u.
  
  3.9-2 AddLiftAlongMonomorphism
  
  AddLiftAlongMonomorphism( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  LiftAlongMonomorphism.  The function F maps a pair (\iota, \tau) to a lift u
  if it exists, and to fail otherwise.
  
  3.9-3 ColiftAlongEpimorphism
  
  ColiftAlongEpimorphism( epsilon, tau )  operation
  Returns:  a morphism in \mathrm{Hom}(c,t)
  
  The  arguments  are  an epimorphism \epsilon: a \rightarrow c and a morphism
  \tau:  a \rightarrow t such that there is a morphism u: c \rightarrow t with
  u \circ \epsilon \sim_{a,t} \tau. The output is such a u.
  
  3.9-4 AddColiftAlongEpimorphism
  
  AddColiftAlongEpimorphism( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  ColiftAlongEpimorphism.  The  function  F  maps a pair (\epsilon, \tau) to a
  lift u if it exists, and to fail otherwise.
  
  
  3.10 Lift/ Colift
  
      For   any  pair  of  morphisms  \alpha:  a  \rightarrow  c,  \beta:  b
        \rightarrow  c,  we call each morphism \alpha / \beta: a \rightarrow b
        such  that  \beta  \circ  (\alpha / \beta) \sim_{a,c} \alpha a lift of
        \alpha along \beta.
  
      For   any  pair  of  morphisms  \alpha:  a  \rightarrow  c,  \beta:  a
        \rightarrow  b,  we  call  each  morphism  \alpha  \backslash \beta: c
        \rightarrow  b  such  that  (\alpha  \backslash  \beta)  \circ  \alpha
        \sim_{a,b} \beta a  colift of \beta along \alpha.
  
  Note  that  such lifts (or colifts) do not have to be unique. So in general,
  we  do  not expect that algorithms computing lifts (or colifts) do this in a
  functorial  way.  Thus  the operations \mathtt{Lift} and \mathtt{Colift} are
  not   regarded   as   categorical  operations,  but  only  as  set-theoretic
  operations.
  
  3.10-1 Lift
  
  Lift( alpha, beta )  operation
  Returns:  a morphism in \mathrm{Hom}(a,b) + \{ \mathtt{fail} \}
  
  The   arguments  are  two  morphisms  \alpha:  a  \rightarrow  c,  \beta:  b
  \rightarrow  c  such that there is a lift \alpha / \beta: a \rightarrow b of
  \alpha  along \beta, i.e., a morphism such that \beta \circ (\alpha / \beta)
  \sim_{a,c}  \alpha. The output is such a lift or \mathtt{fail} if it doesn't
  exist.
  
  3.10-2 AddLift
  
  AddLift( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given  function F to the category for the basic operation Lift. The function
  F  maps a pair (\alpha, \beta) to a lift \alpha / \beta if it exists, and to
  fail otherwise.
  
  3.10-3 Colift
  
  Colift( alpha, beta )  operation
  Returns:  a morphism in \mathrm{Hom}(c,b) + \{ \mathtt{fail} \}
  
  The   arguments  are  two  morphisms  \alpha:  a  \rightarrow  c,  \beta:  a
  \rightarrow  b  such  that  there  is  a  colift  \alpha \backslash \beta: c
  \rightarrow  b  of  \beta  along \alpha., i.e., a morphism such that (\alpha
  \backslash \beta) \circ \alpha \sim_{a,b} \beta. The output is such a colift
  or \mathtt{fail} if it doesn't exist.
  
  3.10-4 AddColift
  
  AddColift( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given  function  F  to  the  category  for  the  basic operation Colift. The
  function  F  maps a pair (\alpha, \beta) to a colift \alpha \backslash \beta
  if it exists, and to fail otherwise.
  
  
  3.11 Inverses
  
  Let  \alpha:  a  \rightarrow  b  be  a  morphism.  An inverse of \alpha is a
  morphism  \alpha^{-1}:  b  \rightarrow  a such that \alpha \circ \alpha^{-1}
  \sim_{b,b}   \mathrm{id}_b   and   \alpha^{-1}   \circ   \alpha   \sim_{a,a}
  \mathrm{id}_a.
  
  3.11-1 AddInverse
  
  AddInverse( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given  function F to the category for the basic operation Inverse. F: \alpha
  \mapsto \alpha^{-1}.
  
  
  3.12 Tool functions for caches
  
  3.12-1 IsEqualForCacheForMorphisms
  
  IsEqualForCacheForMorphisms( phi, psi )  operation
  Returns:  true or false
  
  Compares two objects in the cache
  
  3.12-2 AddIsEqualForCacheForMorphisms
  
  AddIsEqualForCacheForMorphisms( c, F )  operation
  Returns:  northing
  
  By  default,  CAP uses caches to store the values of Categorical operations.
  To  get  a value out of the cache, one needs to compare the input of a basic
  operation  with  its  previous  input. To compare morphisms in the category,
  IsEqualForCacheForMorphism  is  used.  By  default  this  is  an  alias  for
  IsEqualForMorphismsOnMor,  where  fail is substituted by false. If you add a
  function,  this  function  used  instead.  A function F: a,b \mapsto bool is
  expected  here.  The  output has to be true or false. Fail is not allowed in
  this context.