---

Definition: p_subset
A ⊆{T} B ==  ∀x:T. ((A x) ⇒ (B x))

Lemma: p_subset_wf
∀[T:Type]. ∀[A,B:T ⟶ ℙ].  (A ⊆{T} B ∈ ℙ)

Definition: p_equiv
A ≡{T} B ==  A ⊆{T} B ∧ B ⊆{T} A

Lemma: p_equiv_wf
∀[T:Type]. ∀[A,B:T ⟶ ℙ].  (A ≡{T} B ∈ ℙ)

Definition: detach
T-Detach(A) ==  ∀x:T. Dec(A x)

Lemma: detach_wf
∀[T:Type]. ∀[A:T ⟶ ℙ].  (T-Detach(A) ∈ ℙ)

Definition: detach_fun
detach_fun(T;A) ==  {d:T ⟶ 𝔹| ∀x:T. (A x ⇐⇒ ↑(d x))} 

Lemma: detach_fun_wf
∀[T:Type]. ∀[A:T ⟶ ℙ].  (detach_fun(T;A) ∈ Type)

Lemma: detach_fun_properties
∀[T:Type]. ∀[A:T ⟶ ℙ].  ((∀x:T. SqStable(A x)) ⇒ (∀d:detach_fun(T;A). {∀x:T. (A x ⇐⇒ ↑(d x))}))

Lemma: exists_det_fun
∀[T:Type]. ∀[A:T ⟶ ℙ].  ((∀x:T. SqStable(A x)) ⇒ (detach_fun(T;A) ⇐⇒ ∀x:T. Dec(A x)))

Lemma: exists_det_fun_a
∀[T:Type]. ∀[A:T ⟶ ℙ].  ((∀x:T. SqStable(A x)) ⇒ (detach_fun(T;A) ⇐⇒ {∀x:T. Dec(A x)}))

Lemma: dec_alt_char
∀[T:Type]. ∀[A:T ⟶ ℙ].  (∀x:T. Dec(A x) ⇐⇒ (∀x:T. SqStable(A x)) ∧ detach_fun(T;A))

Lemma: dec_alt_char_a
∀[T:Type]. ∀[A:T ⟶ ℙ].  (∀x:T. Dec(A x) ⇐⇒ (∀x:T. SqStable(A x)) ∧ detach_fun(T;A))

Definition: ab_binrel
x,y:T. E[x; y] ==  λx,y. E[x; y]

Lemma: ab_binrel_wf
∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (x,y:T. E[x;y] ∈ T ⟶ T ⟶ ℙ)

Lemma: ab_binrel_functionality
∀[T:Type]. ∀[E,E':T ⟶ T ⟶ ℙ].  ((∀x,y:T.  (E[x;y] ⇐⇒ E'[x;y])) ⇒ ((x,y:T. E[x;y]) <≡>{T} (x,y:T. E'[x;y])))

Definition: binrel_ap
a [r] b ==  r a b

Lemma: binrel_ap_wf
∀[T:Type]. ∀[r:T ⟶ T ⟶ ℙ]. ∀[a,b:T].  (a [r] b ∈ ℙ)

Lemma: binrel_ap_functionality_wrt_breqv
∀[T:Type]. ∀[r,r':T ⟶ T ⟶ ℙ].  ∀a,b:T.  ((r <≡>{T} r') ⇒ (a [r] b ⇐⇒ a [r'] b))

Definition: dec_binrel
dec_binrel(T;r) ==  ∀x,y:T.  Dec(r x y)

Lemma: dec_binrel_wf
∀[T:Type]. ∀[r:T ⟶ T ⟶ ℙ].  (dec_binrel(T;r) ∈ ℙ)

Definition: xxrefl
(!cond_cons(xxbasic; basic)):: refl(T;E) ==  Refl(T;x,y.E x y)

Lemma: xxrefl_wf
∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (refl(T;E) ∈ ℙ)

Lemma: xxrefl_functionality_wrt_breqv
∀[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].  ((R <≡>{T} R') ⇒ (refl(T;R) ⇐⇒ refl(T;R')))

Definition: xxsym
sym(T;E) ==  Sym(T;x,y.E x y)

Lemma: xxsym_wf
∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (sym(T;E) ∈ ℙ)

Lemma: xxsym_functionality_wrt_breqv
∀[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].  ((R <≡>{T} R') ⇒ (sym(T;R) ⇐⇒ sym(T;R')))

Definition: xxtrans
(!cond_cons(xxbasic; basic)):: trans(T;E) ==  Trans(T;x,y.E x y)

Lemma: xxtrans_wf
∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (trans(T;E) ∈ ℙ)

Lemma: xxtrans_functionality_wrt_breqv
∀[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].  ((R <≡>{T} R') ⇒ (trans(T;R) ⇐⇒ trans(T;R')))

Definition: xxsymmetrize
xxsymmetrize(E) ==  λx,y. ((E x y) ∧ (E y x))

Lemma: xxsymmetrize_wf
∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (xxsymmetrize(E) ∈ T ⟶ T ⟶ ℙ)

Definition: xxirrefl
(basic):: irrefl(T;R) ==  Irrefl(T;x,y.R x y)

Lemma: xxirrefl_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (irrefl(T;R) ∈ ℙ)

Definition: xxanti_sym
(!cond_cons(xxbasic; basic)):: anti_sym(T;R) ==  AntiSym(T;x,y.R x y)

Lemma: xxanti_sym_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (anti_sym(T;R) ∈ ℙ)

Lemma: xxanti_sym_functionality_wrt_breqv
∀[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].  uiff(anti_sym(T;R);anti_sym(T;R')) supposing R <≡>{T} R'

Definition: xxst_anti_sym
(basic):: st_anti_sym(T;R) ==  StAntiSym(T;x,y.R x y)

Lemma: xxst_anti_sym_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (st_anti_sym(T;R) ∈ ℙ)

Definition: xxconnex
(basic):: connex(T;R) ==  Connex(T;x,y.R x y)

Lemma: xxconnex_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (connex(T;R) ∈ ℙ)

Lemma: xxconnex_functionality_wrt_breqv
∀[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].  ((R <≡>{T} R') ⇒ (connex(T;R) ⇐⇒ connex(T;R')))

Definition: xxorder
(compound):: order(T;R) ==  refl(T;R) ∧ trans(T;R) ∧ anti_sym(T;R)

Lemma: xxorder_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (order(T;R) ∈ ℙ)

Definition: xxequiv_rel
(compound):: EquivRel(T;R) ==  refl(T;R) ∧ trans(T;R) ∧ sym(T;R)

Lemma: xxequiv_rel_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (EquivRel(T;R) ∈ ℙ)

Lemma: xxorder_functionality_wrt_breqv
∀[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].  ((R <≡>{T} R') ⇒ (order(T;R) ⇐⇒ order(T;R')))

Lemma: xxorder_eq_order
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (order(T;R) = Order(T;x,y.R x y) ∈ ℙ)

Definition: xxlinorder
xxlinorder(T;R) ==  Linorder(T;x,y.R x y)

Lemma: xxlinorder_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (xxlinorder(T;R) ∈ ℙ)

Definition: refl_cl
Eo ==  λx,y. ((x = y ∈ T) ∨ (E x y))

Lemma: refl_cl_wf
∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (Eo ∈ T ⟶ T ⟶ ℙ)

Definition: sym_cl
E↔ ==  λx,y. ((E x y) ∧ (E y x))

Lemma: sym_cl_wf
∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (E↔ ∈ T ⟶ T ⟶ ℙ)

Definition: s_part
E\ ==  λx,y. ((E x y) ∧ (¬(E y x)))

Lemma: s_part_wf
∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (E\ ∈ T ⟶ T ⟶ ℙ)

Lemma: s_part_functionality_wrt_breqv
∀[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].  ((R <≡>{T} R') ⇒ ((R\) <≡>{T} (R'\)))

Lemma: s_part_char
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[a,b:T].  (((R\) a b) = ((R a b) ∧ (¬(R b a))) ∈ ℙ)

Lemma: xxorder_split
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  (order(T;R) ⇒ (∀x,y:T.  Dec(x = y ∈ T)) ⇒ (∀a,b:T.  (R a b ⇐⇒ ((R\) a b) ∨ (a = b ∈ T))))

Lemma: xxtrans_imp_sp_trans
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (trans(T;R) ⇒ trans(T;R\))

Lemma: refl_cl_is_order
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  trans(T;R) ⇒ order(T;Ro) supposing irrefl(T;R)

Lemma: irrefl_trans_imp_sasym
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (st_anti_sym(T;R)) supposing (trans(T;R) and irrefl(T;R))

Lemma: xxconnex_iff_trichot
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ((∀a,b:T.  Dec(R a b)) ⇒ (connex(T;R) ⇐⇒ {∀a,b:T.  (((R\) a b) ∨ ((R↔) a b) ∨ ((R\) b a))}))

Lemma: xxconnex_iff_trichot_a
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (connex(T;Ro) ⇐⇒ ∀a,b:T.  ((R a b) ∨ (a = b ∈ T) ∨ (R b a)))

Lemma: rel_le_refl_cl_sp
∀[T:Type]. ∀[r:T ⟶ T ⟶ ℙ].  (dec_binrel(T;x,y:T. x = y ∈ T) ⇒ r ≡>{T} (r\\00B8) supposing anti_sym(T;r))

Lemma: refl_cl_sp_le_rel
∀[T:Type]. ∀[r:T ⟶ T ⟶ ℙ].  (refl(T;r) ⇒ ((r\\00B8) ≡>{T} r))

Lemma: refl_cl_sp_cancel
∀[T:Type]. ∀[r:T ⟶ T ⟶ ℙ].  (dec_binrel(T;x,y:T. x = y ∈ T) ⇒ refl(T;r) ⇒ (r\\00B8) <≡>{T} r supposing anti_sym(T;r))

Lemma: rel_le_sp_refl_cl
∀[T:Type]. ∀[r:T ⟶ T ⟶ ℙ].  (r ≡>{T} (ro\)) supposing (st_anti_sym(T;r) and irrefl(T;r))

Lemma: sp_refl_cl_le_rel
∀[T:Type]. ∀[r:T ⟶ T ⟶ ℙ].  ((ro\) ≡>{T} r)

Lemma: sp_refl_cl_cancel
∀[T:Type]. ∀[r:T ⟶ T ⟶ ℙ].  ((ro\) <≡>{T} r) supposing (st_anti_sym(T;r) and irrefl(T;r))

Definition: ident
(basic):: Ident(T;op;id) ==  ∀[x:T]. (((x op id) = x ∈ T) ∧ ((id op x) = x ∈ T))

Lemma: ident_wf
∀[T:Type]. ∀[op:T ⟶ T ⟶ T]. ∀[id:T].  (Ident(T;op;id) ∈ ℙ)

Lemma: sq_stable__ident
∀[T:Type]. ∀[op:T ⟶ T ⟶ T]. ∀[id:T].  SqStable(Ident(T;op;id))

Definition: bilinear
(basic):: 
BiLinear(T;pl;tm) ==
  ∀[a,x,y:T].  (((a tm (x pl y)) = ((a tm x) pl (a tm y)) ∈ T) ∧ (((x pl y) tm a) = ((x tm a) pl (y tm a)) ∈ T))

Lemma: bilinear_wf
∀[T:Type]. ∀[pl,tm:T ⟶ T ⟶ T].  (BiLinear(T;pl;tm) ∈ ℙ)

Lemma: sq_stable__bilinear
∀[T:Type]. ∀[pl,tm:T ⟶ T ⟶ T].  SqStable(BiLinear(T;pl;tm))

Lemma: bilinear_comm_elim
∀[T:Type]. ∀[pl,tm:T ⟶ T ⟶ T].
  (BiLinear(T;pl;tm)) supposing ((∀a,x,y:T.  ((a tm (x pl y)) = ((a tm x) pl (a tm y)) ∈ T)) and Comm(T;tm))

Definition: bilinear_p
(basic):: 
IsBilinear(A;B;C;+a;+b;+c;f) ==
  (∀[a1,a2:A]. ∀[b:B].  (((a1 +a a2) f b) = ((a1 f b) +c (a2 f b)) ∈ C))
  ∧ (∀[a:A]. ∀[b1,b2:B].  ((a f (b1 +b b2)) = ((a f b1) +c (a f b2)) ∈ C))

Lemma: bilinear_p_wf
∀[A,B,C:Type]. ∀[+a:A ⟶ A ⟶ A]. ∀[+b:B ⟶ B ⟶ B]. ∀[+c:C ⟶ C ⟶ C]. ∀[f:A ⟶ B ⟶ C].
  (IsBilinear(A;B;C;+a;+b;+c;f) ∈ ℙ)

Lemma: sq_stable__bilinear_p
∀[A,B,C:Type]. ∀[+a:A ⟶ A ⟶ A]. ∀[+b:B ⟶ B ⟶ B]. ∀[+c:C ⟶ C ⟶ C]. ∀[f:A ⟶ B ⟶ C].
  SqStable(IsBilinear(A;B;C;+a;+b;+c;f))

Definition: action_p
(basic):: IsAction(A;x;e;S;f) ==  (∀[a,b:A].  ∀u:S. (((a x b) f u) = (a f (b f u)) ∈ S)) ∧ (∀[u:S]. ((e f u) = u ∈ S))

Lemma: action_p_wf
∀[A:Type]. ∀[x:A ⟶ A ⟶ A]. ∀[e:A]. ∀[S:Type]. ∀[f:A ⟶ S ⟶ S].  (IsAction(A;x;e;S;f) ∈ ℙ)

Lemma: sq_stable__action_p
∀[A:Type]. ∀[x:A ⟶ A ⟶ A]. ∀[e:A]. ∀[S:Type]. ∀[f:A ⟶ S ⟶ S].  SqStable(IsAction(A;x;e;S;f))

Definition: dist_1op_2op_lr
(basic):: 
Dist1op2opLR(A;1op;2op) ==
  ∀[u,v:A].  (((1op (u 2op v)) = ((1op u) 2op v) ∈ A) ∧ ((1op (u 2op v)) = (u 2op (1op v)) ∈ A))

Lemma: dist_1op_2op_lr_wf
∀[A:Type]. ∀[f:A ⟶ A]. ∀[x:A ⟶ A ⟶ A].  (Dist1op2opLR(A;f;x) ∈ ℙ)

Lemma: sq_stable__dist_1op_2op_lr
∀[A:Type]. ∀[f:A ⟶ A]. ∀[x:A ⟶ A ⟶ A].  SqStable(Dist1op2opLR(A;f;x))

Definition: fun_thru_1op
(basic):: fun_thru_1op(A;B;opa;opb;f) ==  ∀[a:A]. ((f (opa a)) = (opb (f a)) ∈ B)

Lemma: fun_thru_1op_wf
∀[A,B:Type]. ∀[opa:A ⟶ A]. ∀[opb:B ⟶ B]. ∀[f:A ⟶ B].  (fun_thru_1op(A;B;opa;opb;f) ∈ ℙ)

Lemma: sq_stable__fun_thru_1op
∀[A,B:Type]. ∀[opa:A ⟶ A]. ∀[opb:B ⟶ B]. ∀[f:A ⟶ B].  SqStable(fun_thru_1op(A;B;opa;opb;f))

Definition: fun_thru_2op
(basic):: FunThru2op(A;B;opa;opb;f) ==  ∀[a1,a2:A].  ((f (a1 opa a2)) = ((f a1) opb (f a2)) ∈ B)

Lemma: fun_thru_2op_wf
∀[A,B:Type]. ∀[opa:A ⟶ A ⟶ A]. ∀[opb:B ⟶ B ⟶ B]. ∀[f:A ⟶ B].  (FunThru2op(A;B;opa;opb;f) ∈ ℙ)

Lemma: sq_stable__fun_thru_2op
∀[A,B:Type]. ∀[opa:A ⟶ A ⟶ A]. ∀[opb:B ⟶ B ⟶ B]. ∀[f:A ⟶ B].  SqStable(FunThru2op(A;B;opa;opb;f))

Definition: cancel
(basic):: Cancel(T;S;op) ==  ∀[u,v:T]. ∀[w:S].  u = v ∈ T supposing (w op u) = (w op v) ∈ T

Lemma: cancel_wf
∀[T,S:Type]. ∀[op:S ⟶ T ⟶ T].  (Cancel(T;S;op) ∈ ℙ)

Lemma: sq_stable__cancel
∀[T,S:Type]. ∀[op:S ⟶ T ⟶ T].  SqStable(Cancel(T;S;op))

Definition: monot
(basic):: monot(T;x,y.R[x; y];f) ==  ∀x,y:T.  (R[x; y] ⇒ R[f x; f y])

Lemma: monot_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[f:T ⟶ T].  (monot(T;x,y.R[x;y];f) ∈ ℙ)

Lemma: sq_stable__monot
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀f:T ⟶ T. ((∀x,y:T.  SqStable(R[x;y])) ⇒ SqStable(monot(T;x,y.R[x;y];f)))

Lemma: monot_functionality
∀[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].
  ∀f:T ⟶ T. ((∀x,y:T.  (R[x;y] ⇐⇒ R'[x;y])) ⇒ (monot(T;x,y.R[x;y];f) ⇐⇒ monot(T;x,y.R'[x;y];f)))

Definition: monotone
monotone(T;T';x,y.R[x; y];x,y.R'[x; y];f) ==  ∀x,y:T.  (R[x; y] ⇒ R'[f x; f y])

Lemma: monotone_wf
∀[T,T':Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[R':T' ⟶ T' ⟶ ℙ]. ∀[f:T ⟶ T'].  (monotone(T;T';x,y.R[x;y];x,y.R'[x;y];f) ∈ ℙ)

Definition: rels_iso
(basic):: RelsIso(T;T';x,y.R[x; y];x,y.R'[x; y];f) ==  ∀x,y:T.  (R[x; y] ⇐⇒ R'[f x; f y])

Lemma: rels_iso_wf
∀[T,T':Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[R':T' ⟶ T' ⟶ ℙ]. ∀[f:T ⟶ T'].  (RelsIso(T;T';x,y.R[x;y];x,y.R'[x;y];f) ∈ ℙ)

Lemma: assoc_shift
∀[A,B:Type]. ∀[opa:A ⟶ A ⟶ A]. ∀[opb:B ⟶ B ⟶ B]. ∀[f:A ⟶ B].
  (Assoc(A;opa)) supposing (Assoc(B;opb) and FunThru2op(A;B;opa;opb;f) and Inj(A;B;f))

Lemma: comm_shift
∀[A,B:Type]. ∀[opa:A ⟶ A ⟶ A]. ∀[opb:B ⟶ B ⟶ B]. ∀[f:A ⟶ B].
  (Comm(A;opa)) supposing (Comm(B;opb) and FunThru2op(A;B;opa;opb;f) and Inj(A;B;f))

Lemma: cancel_shift
∀[A,B:Type]. ∀[opa:A ⟶ A ⟶ A]. ∀[opb:B ⟶ B ⟶ B]. ∀[f:A ⟶ B].
  (Cancel(A;A;opa)) supposing (Cancel(B;B;opb) and FunThru2op(A;B;opa;opb;f) and Inj(A;B;f))

Lemma: eqfun_p_shift
∀[A,B:Type]. ∀[eqa:A ⟶ A ⟶ 𝔹]. ∀[eqb:B ⟶ B ⟶ 𝔹]. ∀[f:A ⟶ B].
  (IsEqFun(A;eqa)) supposing (IsEqFun(B;eqb) and RelsIso(A;B;x,y.↑(x eqa y);x,y.↑(x eqb y);f) and Inj(A;B;f))

Lemma: sym_shift
∀[A,B:Type]. ∀[R:A ⟶ A ⟶ ℙ]. ∀[S:B ⟶ B ⟶ ℙ].
  ∀f:A ⟶ B. (RelsIso(A;B;x,y.R[x;y];x,y.S[x;y];f) ⇒ Sym(B;x,y.S[x;y]) ⇒ Sym(A;x,y.R[x;y]))

Lemma: usym_shift
∀[A,B:Type]. ∀[R:A ⟶ A ⟶ ℙ]. ∀[S:B ⟶ B ⟶ ℙ].
  ∀f:A ⟶ B
    ((∀[x,y:A].  R[x;y] supposing R[x;y])
    ⇒ RelsIso(A;B;x,y.R[x;y];x,y.S[x;y];f)
    ⇒ UniformlySym(B;x,y.S[x;y])
    ⇒ UniformlySym(A;x,y.R[x;y]))

Lemma: trans_shift
∀[A,B:Type]. ∀[R:A ⟶ A ⟶ ℙ]. ∀[S:B ⟶ B ⟶ ℙ].
  ∀f:A ⟶ B. (RelsIso(A;B;x,y.R[x;y];x,y.S[x;y];f) ⇒ Trans(B;x,y.S[x;y]) ⇒ Trans(A;x,y.R[x;y]))

Lemma: utrans_shift
∀[A,B:Type]. ∀[R:A ⟶ A ⟶ ℙ]. ∀[S:B ⟶ B ⟶ ℙ].
  ∀f:A ⟶ B
    ((∀[x,y:A].  R[x;y] supposing R[x;y])
    ⇒ RelsIso(A;B;x,y.R[x;y];x,y.S[x;y];f)
    ⇒ UniformlyTrans(B;x,y.S[x;y])
    ⇒ UniformlyTrans(A;x,y.R[x;y]))

Lemma: connex_shift
∀[A,B:Type]. ∀[R:A ⟶ A ⟶ ℙ]. ∀[S:B ⟶ B ⟶ ℙ].
  ∀f:A ⟶ B. (RelsIso(A;B;x,y.R[x;y];x,y.S[x;y];f) ⇒ Connex(B;x,y.S[x;y]) ⇒ Connex(A;x,y.R[x;y]))

Lemma: anti_sym_shift
∀[A,B:Type]. ∀[R:A ⟶ A ⟶ ℙ]. ∀[S:B ⟶ B ⟶ ℙ]. ∀[f:A ⟶ B].
  (AntiSym(A;x,y.R[x;y])) supposing (AntiSym(B;x,y.S[x;y]) and RelsIso(A;B;x,y.R[x;y];x,y.S[x;y];f) and Inj(A;B;f))

Lemma: uanti_sym_shift
∀[A,B:Type]. ∀[R:A ⟶ A ⟶ ℙ]. ∀[S:B ⟶ B ⟶ ℙ]. ∀[f:A ⟶ B].
  (UniformlyAntiSym(A;x,y.R[x;y])) supposing 
     (UniformlyAntiSym(B;x,y.S[x;y]) and 
     RelsIso(A;B;x,y.R[x;y];x,y.S[x;y];f) and 
     Inj(A;B;f))

Lemma: refl_shift
∀[A,B:Type]. ∀[R:A ⟶ A ⟶ ℙ]. ∀[S:B ⟶ B ⟶ ℙ].
  ∀f:A ⟶ B. (RelsIso(A;B;x,y.R[x;y];x,y.S[x;y];f) ⇒ Refl(B;x,y.S[x;y]) ⇒ Refl(A;x,y.R[x;y]))

Lemma: urefl_shift
∀[A,B:Type]. ∀[R:A ⟶ A ⟶ ℙ]. ∀[S:B ⟶ B ⟶ ℙ].
  ∀f:A ⟶ B
    ((∀[x,y:A].  R[x;y] supposing R[x;y])
    ⇒ RelsIso(A;B;x,y.R[x;y];x,y.S[x;y];f)
    ⇒ UniformlyRefl(B;x,y.S[x;y])
    ⇒ UniformlyRefl(A;x,y.R[x;y]))

Lemma: monot_shift
∀[A,B:Type]. ∀[R:A ⟶ A ⟶ ℙ]. ∀[S:B ⟶ B ⟶ ℙ].
  ∀opa:A ⟶ A. ∀opb:B ⟶ B. ∀f:A ⟶ B.
    RelsIso(A;B;x,y.R[x;y];x,y.S[x;y];f) ⇒ monot(B;x,y.S[x;y];opb) ⇒ monot(A;x,y.R[x;y];opa) 
    supposing fun_thru_1op(A;B;opa;opb;f)



Home Index