Skip to content

Add notion of isomorphism between OFEs

Robbert Krebbers requested to merge robbert/iso into master

Add ofe_iso A B that states that OFEs A and B` are isomorphic. Some features:

  • Proved that ofe_iso is reflexive, symmetric, and transitive. Note that I don't use the Equivalence class, since ofe_iso is a Type, not a Prop.
  • Proved that ofe_iso A B itself is a OFE, and if A and B are COFEs, it's a COFE.
  • Refactored the COFE solver to make use of ofe_iso.

I don't think it's extraordinarily useful that ofe_iso A B itself is a (C)OFE, but it holds, so why not have it :)

Edited by Robbert Krebbers

Merge request reports