record relation_pair (BP1,BP2: basic_pair): Type ≝
{ concr_rel: arrows1 ? (concr BP1) (concr BP2);
form_rel: arrows1 ? (form BP1) (form BP2);
record relation_pair (BP1,BP2: basic_pair): Type ≝
{ concr_rel: arrows1 ? (concr BP1) (concr BP2);
form_rel: arrows1 ? (form BP1) (form BP2);
- | lapply (id_neutral_left1 ? (concr o) ? (⊩)) as H;
- lapply (id_neutral_right1 ?? (form o) (⊩)) as H1;
+ | lapply (id_neutral_right1 ? (concr o) ? (⊩)) as H;
+ lapply (id_neutral_left1 ?? (form o) (⊩)) as H1;
- change with (a\sub\c ∘ b\sub\c ∘ ⊩ = a'\sub\c ∘ b'\sub\c ∘ ⊩);
- change in H with (a \sub\c ∘ ⊩ = a' \sub\c ∘ ⊩);
- change in H1 with (b \sub\c ∘ ⊩ = b' \sub\c ∘ ⊩);
+ change with (⊩ ∘ (b\sub\c ∘ a\sub\c) = ⊩ ∘ (b'\sub\c ∘ a'\sub\c));
+ change in H with (⊩ ∘ a \sub\c = ⊩ ∘ a' \sub\c);
+ change in H1 with (⊩ ∘ b \sub\c = ⊩ ∘ b' \sub\c);
- change with (a12\sub\c ∘ a23\sub\c ∘ a34\sub\c ∘ ⊩ =
- (a12\sub\c ∘ (a23\sub\c ∘ a34\sub\c) ∘ ⊩));
+ change with (⊩ ∘ (a34\sub\c ∘ (a23\sub\c ∘ a12\sub\c)) =
+ ⊩ ∘ ((a34\sub\c ∘ a23\sub\c) ∘ a12\sub\c));
- change with ((id_relation_pair o1)\sub\c ∘ a\sub\c ∘ ⊩ = a\sub\c ∘ ⊩);
- apply ((id_neutral_left1 ????)‡#);
- | intros;
- change with (a\sub\c ∘ (id_relation_pair o2)\sub\c ∘ ⊩ = a\sub\c ∘ ⊩);
+ change with (⊩ ∘ (a\sub\c ∘ (id_relation_pair o1)\sub\c) = ⊩ ∘ a\sub\c);