interpretation "bishop set relations composition" 'compose a b = (compose_bs_relations _ a b).
interpretation "ordered set relations composition" 'compose a b = (compose_os_relations _ a b).
definition invert_bs_relation ≝
λC:bishop_set.λU:C square → Prop.
interpretation "bishop set relations composition" 'compose a b = (compose_bs_relations _ a b).
interpretation "ordered set relations composition" 'compose a b = (compose_os_relations _ a b).
definition invert_bs_relation ≝
λC:bishop_set.λU:C square → Prop.