λC:ordered_set.λU:C squareO → Prop.
λx:C squareO. U 〈\snd x,\fst x〉.
-interpretation "relation invertion" 'invert a = (invert_os_relation _ a).
-interpretation "relation invertion" 'invert_symbol = (invert_os_relation _).
-interpretation "relation invertion" 'invert_appl a x = (invert_os_relation _ a x).
+interpretation "relation invertion" 'invert a = (invert_os_relation ? a).
+interpretation "relation invertion" 'invert_symbol = (invert_os_relation ?).
+interpretation "relation invertion" 'invert_appl a x = (invert_os_relation ? a x).
lemma hint_segment: ∀O.
segment (Type_of_ordered_set O) →
qed.
interpretation "Ordered uniform space segment" 'segset a =
- (segment_ordered_uniform_space _ a).
+ (segment_ordered_uniform_space ? a).
(* Lemma 3.2 *)
alias symbol "pi1" = "exT \fst".