Theory Axioms_Complement

section Axioms of complements

theory Axioms_Complement
  imports Laws
begin

typedecl ('a, 'b) complement_domain
instance complement_domain :: (domain, domain) domain..

― ‹We need that there is at least one object in our category. We call is termsome_domain.
typedecl some_domain
instance some_domain :: domain..

axiomatization where 
  complement_exists: register F  G :: ('a, 'b) complement_domain update  'b update. compatible F G  iso_register (F;G) for F :: 'a::domain update  'b::domain update

axiomatization where complement_unique: compatible F G  iso_register (F;G)  compatible F H  iso_register (F;H)
           equivalent_registers G H 
    for F :: 'a::domain update  'b::domain update and G :: 'g::domain update  'b update and H :: 'h::domain update  'b update

end