Re: making a cone universal in a faithful way

[Lutz Schroeder <Lutz.Schroeder@dfki.de>, <categories@mta.ca>]

Dear Dimitri,

> You are right. I didn't checked very carefully the local confluence of my
> rewriting system. To get confluence, I need to add the fact that the
> bimorphism f satisfies "fu = vf implies u = 1 and v = 1". So this is enough
> for f to be a potential isomorphism.

Yes, that does the trick, and is also the best sufficient condition that
I have been able to come up with in my thesis. I would guess something
similar might work for the general case, but the condition is actually
so strong as to be somewhat unsatisfactory. Note in particular that it
fails for actual (nontrivial) isomorphisms. I poked around this problem
for quite a bit back then but haven't been able to isolate a
satisfactory criterion (other than the obvious one that talks explicitly
about equality in a non-confluent axiom system).

Good luck,

Lutz



-- 
--------------------------------------
PD Dr. Lutz Schröder
Senior Researcher
DFKI Bremen	
Safe and Secure Cognitive Systems
Cartesium, Enrique-Schmidt-Str. 5
D-28359 Bremen

phone: (+49) 421-218-64216
Fax:   (+49) 421-218-9864216
mail: Lutz.Schroeder@dfki.de
www.dfki.de/sks/staff/lschrode
--------------------------------------


-------------------------------------------------------------
Deutsches Forschungszentrum für Künstliche Intelligenz GmbH
Firmensitz: Trippstadter Strasse 122, D-67663 Kaiserslautern

Geschäftsführung:
Prof. Dr. Dr. h.c. mult. Wolfgang Wahlster (Vorsitzender)
Dr. Walter Olthoff

Vorsitzender des Aufsichtsrats:
Prof. Dr. h.c. Hans A. Aukes

Amtsgericht Kaiserslautern, HRB 2313
-------------------------------------------------------------




[For admin and other information see: http://www.mta.ca/~cat-dist/ ]