1312 

  1312 

  1313   (FIXME: We did not do anything with morphisms. Anything interesting

  1313   (FIXME: We did not do anything with morphisms. Anything interesting

  1314   one can say about them?)

  1314   one can say about them?)

  1315 *}

  1315 *}

  1316 

  1316 

  1318 

  1318 

  1319 text {*

  1319 text {*

  1320 Conversions are meta-equalities depending on some input term. There type is

  1320 Conversions are meta-equalities depending on some input term. There type is

  1321 as follows:

  1321 as follows:

  1322 *}

  1322 *}