(* Definition 2.13 *)
alias symbol "square" = "bishop set square".
-alias symbol "pair" = "pair".
+alias symbol "pair" = "Pair construction".
alias symbol "exists" = "exists".
alias symbol "and" = "logical and".
definition compose_bs_relations ≝
λC:bishop_set.λU,V:C square → Prop.
- λx:C square.∃y:C. U 〈fst x,y〉 ∧ V 〈y,snd x〉.
+ λx:C square.∃y:C. U 〈\fst x,y〉 ∧ V 〈y,\snd x〉.
definition compose_os_relations ≝
λC:ordered_set.λU,V:C square → Prop.
- λx:C square.∃y:C. U 〈fst x,y〉 ∧ V 〈y,snd x〉.
+ λx:C square.∃y:C. U 〈\fst x,y〉 ∧ V 〈y,\snd x〉.
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.
- λx:C square. U 〈snd x,fst x〉.
+ λx:C square. U 〈\snd x,\fst x〉.
notation < "s \sup (-1)" with precedence 70 for @{ 'invert $s }.
notation < "s \sup (-1) x" with precedence 70
us_carr:> bishop_set;
us_unifbase: (us_carr square → Prop) → CProp;
us_phi1: ∀U:us_carr square → Prop. us_unifbase U →
- (λx:us_carr square.fst x ≈ snd x) ⊆ U;
+ (λx:us_carr square.\fst x ≈ \snd x) ⊆ U;
us_phi2: ∀U,V:us_carr square → Prop. us_unifbase U → us_unifbase V →
∃W:us_carr square → Prop.us_unifbase W ∧ (W ⊆ (λx.U x ∧ V x));
us_phi3: ∀U:us_carr square → Prop. us_unifbase U →