id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. comp ??? a (id o1) = a
}.
-notation "hvbox(A break ⇒ B)" right associative with precedence 50 for @{ 'arrows $A $B }.
-interpretation "arrows1" 'arrows A B = (unary_morphism1 A B).
-interpretation "arrows" 'arrows A B = (unary_morphism A B).
-
notation > "𝐈𝐝 term 90 A" non associative with precedence 90 for @{ 'id $A }.
notation < "mpadded width -90% (𝐈) 𝐝 \sub term 90 A" non associative with precedence 90 for @{ 'id $A }.
@ setoid; @;
##[ #T1; #T2;
alias symbol "eq" = "setoid eq".
- napply (∃f:T1 ⇒ T2.∃g:T2 ⇒ T1. (∀x.f (g x) = x) ∧ (∀y.g (f y) = y));
+ napply (∃f:T1 ⇒_0 T2.∃g:T2 ⇒_0 T1. (∀x.f (g x) = x) ∧ (∀y.g (f y) = y));
##| #A; @ (𝐈𝐝 A); @ (𝐈𝐝 A); @; #x; napply #;
##| #A; #B; *; #f; *; #g; *; #Hfg; #Hgf; @g; @f; @; nassumption;
##| #A; #B; #C; *; #f; *; #f'; *; #Hf; #Hf'; *; #g; *; #g'; *; #Hg; #Hg';
nrecord unary_morphism01 (A : setoid) (B: setoid1) : Type[1] ≝
{ fun01:1> A → B;
- prop01: ∀a,a'. eq ? a a' → eq1 ? (fun01 a) (fun01 a')
+ prop01: ∀a,a'. eq0 ? a a' → eq1 ? (fun01 a) (fun01 a')
}.
interpretation "prop01" 'prop1 c = (prop01 ????? c).