(* *)
(**************************************************************************)
-include "ground/notation/relations/doteq_4.ma".
+include "ground/notation/relations/circled_eq_4.ma".
include "ground/lib/relations.ma".
(* EXTENSIONAL EQUIVALENCE FOR FUNCTIONS ************************************)
interpretation
"extensional equivalence"
- 'DotEq A B f1 f2 = (exteq A B f1 f2).
+ 'CircledEq A B f1 f2 = (exteq A B f1 f2).
(* Basic constructions ******************************************************)
(* Constructions with compose ***********************************************)
lemma compose_repl_fwd_dx (A) (B) (C) (g) (f1) (f2):
- f1 â\89\90{A,B} f2 â\86\92 g â\88\98 f1 â\89\90{A,C} g ∘ f2.
+ f1 â\8a\9c{A,B} f2 â\86\92 g â\88\98 f1 â\8a\9c{A,C} g ∘ f2.
#A #B #C #g #f1 #f2 #Hf12 #a
whd in ⊢ (??%%); //
qed.
lemma compose_repl_bak_dx (A) (B) (C) (g) (f1) (f2):
- f1 â\89\90{A,B} f2 â\86\92 g â\88\98 f2 â\89\90{A,C} g ∘ f1.
+ f1 â\8a\9c{A,B} f2 â\86\92 g â\88\98 f2 â\8a\9c{A,C} g ∘ f1.
/3 width=1 by compose_repl_fwd_dx, exteq_sym/
qed.
lemma compose_repl_fwd_sn (A) (B) (C) (g1) (g2) (f):
- g1 â\89\90{B,C} g2 â\86\92 g1 â\88\98 f â\89\90{A,C} g2 ∘ f.
+ g1 â\8a\9c{B,C} g2 â\86\92 g1 â\88\98 f â\8a\9c{A,C} g2 ∘ f.
#A #B #C #g1 #g2 #f #Hg12 #a
whd in ⊢ (??%%); //
qed.
lemma compose_repl_bak_sn (A) (B) (C) (g1) (g2) (f):
- g1 â\89\90{B,C} g2 â\86\92 g2 â\88\98 f â\89\90{A,C} g1 ∘ f.
+ g1 â\8a\9c{B,C} g2 â\86\92 g2 â\88\98 f â\8a\9c{A,C} g1 ∘ f.
/3 width=1 by compose_repl_fwd_sn, exteq_sym/
qed.
lemma compose_assoc (A1) (A2) (A3) (A4) (f3:A3→A4) (f2:A2→A3) (f1:A1→A2):
- f3 â\88\98 (f2 â\88\98 f1) â\89\90 f3 ∘ f2 ∘ f1.
+ f3 â\88\98 (f2 â\88\98 f1) â\8a\9c f3 ∘ f2 ∘ f1.
// qed.