pi_eq: {A,Aˈ,B,Bˈ} A≡Aˈ ⟶ ({x} x%A ⟶ B x ≡ Bˈ x) ⟶ (Π A [x] B x) ≡ (Π Aˈ [x] Bˈ x) ❘
= [A,Aˈ,B,Bˈ,P,Q] sub_antisym (pi_sub_lr (eqtp_subtp (eqtp_sym P)) (eqtp_subtp_map Aˈ B Bˈ (eqtp_param A Aˈ B Bˈ P Q))) (pi_sub_lr A Aˈ Bˈ B (eqtp_subtp P) (eqtp_subtp_map A Bˈ B (eqtp_sym_map A B Bˈ Q))) ❙
= [A,Aˈ,B,Bˈ,P,Q] subtp_antisym (pi_sub_lr (eqtp_subtp (eqtp_sym P)) (eqtp_subtp_map Aˈ B Bˈ (eqtp_param A Aˈ B Bˈ P Q))) (pi_sub_lr A Aˈ Bˈ B (eqtp_subtp P) (eqtp_subtp_map A Bˈ B (eqtp_sym_map A B Bˈ Q))) ❙
refine: tp ⟶ (tm ⟶ tm) ⟶ tp❘# 1 | 2 prec 5❙
refine_tp: {A,p} $A ⟶ ({x} x%A ⟶ p x % bool) ⟶ $A|p❙
= [A,Aˈ,p,pˈ,P,Q] sub_antisym (refine_sub_lr (eqtp_subtp P) ((eq_impl A p pˈ) Q)) (refine_sub_lr (eqtp_subtp eqtp_sym P) ((eq_impl_back_eq A Aˈ p pˈ) P Q)) ❙
= [A,Aˈ,p,pˈ,P,Q] subtp_antisym (refine_sub_lr (eqtp_subtp P) ((eq_impl A p pˈ) Q)) (refine_sub_lr (eqtp_subtp eqtp_sym P) ((eq_impl_back_eq A Aˈ p pˈ) P Q)) ❙
= [A,B,f,t,tˈ,P,Q,R,S] eq_trans (S t P) (app_tp (lam_tp eqtp_refl S) Q) (S tˈ Q) (app_sub_eq_help P Q R S) (eq_sym (app_sub_eq_help2 P Q R S))❙
EqRel_subs: {A,r,x,y,z,w} ({s,t} s%A ⟶ t%A ⟶ (r s t)%bool) ⟶ x%A ⟶ y%A ⟶ z%A ⟶ w%A ⟶ ⊦x =A z ⟶ ⊦y =A w ⟶ ⊦(r x y) =bool (r z w) ❘
= [A,r,x,y,z,w,P,Q,R,S,T,U,V] (eq_trans bool (r x y) (r x w) (r z w) (P x y Q R) (P x w Q T) (P z w S T) (app_sub_eq A ([m] bool) ([m] r x m) y w R T V ([t,k:t%A] P x t Q k)) (app_sub_eq A ([m] bool) ([m] r m w) x z Q S U ([t,k:t%A] P t w k T)))❙
t_sat_pred: {A,p,s,t} s%A ⟶ t%A ⟶ ⊦s =A t ⟶ ({x} x%A ⟶ p x % bool) ⟶ ⊦p s ⟶ t%(A|p)❘
= [A,p,s,t,P,Q,R,S,T] refine_I Q valid_eq_flip T (app_sub_eq A ([x] bool) p s t P Q R S)❙
singleton_sub: {A,p,s} s%A ⟶ ({x} x%A ⟶ p x % bool) ⟶ ⊦p s ⟶ (A|([x] x =A s)) < (A|p)❘
= [A,p,s,P,Q,R] [t:tm, k:t%(A|([x] x =A s))] refine_I (refine_E1 k) (refine_eq_pres_help4 P (refine_E1 k) (eq_sym (refine_E2 k)) Q R)❙
dep_pred_s: {A,s,p} s%A ⟶ ({x} x%A ⟶ p x % bool) ⟶ ⊦p s ⟶ ({t} t%A ⟶ ((p t ∧ (t =(A|([x] p x)) s))) %bool) ❘
= [A,s,p,P,Q,R] [t,k:t%A] and_tp (Q t k) ([l:⊦p t] eq_tp (refine_I A ([x] p x) t k l) (refine_I A ([x] p x) s P R)) ❙
dep_pred_s_sat_s: {A,s,p} s%A ⟶ ({x} x%A ⟶ p x % bool) ⟶ ⊦p s ⟶ ⊦ ((p s ∧ (s =(A|([x] p x)) s))) ❘
= [A,s,p,P,Q,R] and_I R (eq_refl (refine_I A ([x] p x) s P R)) ❙
dep_pred_s_sat_t: {A,s,t,p} s%A ⟶ t%A ⟶ ({x} x%A ⟶ p x % bool) ⟶ ⊦p s ⟶ ⊦s =A t ⟶ ⊦ (((p t) ∧ (t =(A|([x] p x)) s))) ❘
= [A,s,t,p,P,Q,R,S,T] refine_E2 (pred_eq P Q T ([x,k:x%A] dep_pred_s P R S x k) (dep_pred_s_sat_s P R S)) ❙
= [A,p,s,P,Q,R] [t:tm, k:t%(A|([x] x =A s))] refine_I (refine_E1 k)
valid_eq_flip R (app_sub_eq A ([x] bool) p s t P (refine_E1 k) (eq_sym (refine_E2 k)) Q)❙
dep_conj_pred_eq_s: {A,s,p} s%A ⟶ ({x} x%A ⟶ p x % bool) ⟶ ⊦p s ⟶ ({t} t%A ⟶ ((p t ∧ (t =(A|([x] p x)) s))) %bool) ❘
= [A,s,p,P,Q,R] [t,k:t%A] and_tp (Q t k) ([l:⊦p t] eq_tp (refine_I A ([x] p x) t k l) (refine_I A ([x] p x) s P R)) ❙
t_sat_dep_conj_pred_eq_s: {A,s,t,p} s%A ⟶ t%A ⟶ ⊦s =A t ⟶ ({x} x%A ⟶ p x % bool) ⟶ ⊦p s ⟶ ⊦ (((p t) ∧ (t =(A|([x] p x)) s))) ❘
= [A,s,t,p,P,Q,R,S,T] refine_E2 (t_sat_pred P Q R ([x,k:x%A] dep_conj_pred_eq_s P S T x k) and_I T (eq_refl (refine_I A ([x] p x) s P T))) ❙
refine_eq_pres: {A,s,t,p} s%A ⟶ t%A ⟶ ⊦s =A t ⟶ ({x} x%A ⟶ p x % bool) ⟶ ⊦p s ⟶ ⊦s =(A|p) t ❘
= [A,s,t,p,P,Q,R,S,T] (eq_sym and_Er dep_pred_s_sat_t P Q S T R) ❙
= [A,s,t,p,P,Q,R,S,T] (eq_sym and_Er t_sat_dep_conj_pred_eq_s P Q R S T) ❙
refine_eq_pres_rev: {A,s,t,p} s%A ⟶ t%A ⟶ ⊦t =A s ⟶ ({x} x%A ⟶ p x % bool) ⟶ ⊦p s ⟶ ⊦t =(A|p) s ❘
= [A,s,t,p,P,Q,R,S,T] eq_sym refine_eq_pres P Q (eq_sym R) S T ❙
app_sub_eq_help: {A,B,f,t,tˈ} ({u} u%A ⟶ (f u) % B) ⟶ ⊦t =A tˈ ⟶ t%A ⟶ tˈ%A ⟶ ⊦ (f t) =B ((λ A [x] f x)@tˈ)❘
= [A,B,f,t,tˈ,P,Q,R,S] prop_trans (P t R) (app_tp (lam_tp eqtp_wf P) R) (app_tp (lam_tp eqtp_wf P) S) (eq_sym (lam_beta ([k,l:k%A] app_tp A ([y] B) (λ A [x] f x) k (lam_tp eqtp_wf P) l) R)) (app_eq (eq_refl lam_tp eqtp_wf P) Q) ❙
app_sub_eq_help2: {A,B,f,t,tˈ} ({u} u%A ⟶ (f u) % B) ⟶ ⊦t =A tˈ ⟶ t%A ⟶ tˈ%A ⟶ ⊦ (f tˈ) =B ((λ A [x] f x)@tˈ)❘
= [A,B,f,t,tˈ,P,Q,R,S] (eq_sym (lam_beta ([k,l:k%A] app_tp A ([y] B) (λ A [x] f x) k (lam_tp eqtp_wf P) l) S)) ❙
= [A,B,f,r,P,Q,R] ([s, k:s%A∕r] (quotient_E k ([x, l:x%A, m: ⊦x =(A∕r) s] Q x l) ([x, y, l:x%A, m:y%A, n: ⊦x =(A∕r) s, o: ⊦y =(A∕r) s] R x y l m (func_trans_quo P k l m n o)))) ❙
// = [A,B,f,r,P,Q,R] ([s, k:s%A∕r] (quotient_E k ([x, l:x%A, m: ⊦x =(A∕r) s] Q x l) ([x, y, l:x%A, m:y%A, n: ⊦x =(A∕r) s, o: ⊦y =(A∕r) s] R x y l m (func_trans_quo P k l m n o)))) ❙
true_props: {F} F%(bool|[x] x =bool true) ⟶ ⊦F =bool true❘
= [F,P] refine_E2 P ❙
props_in_true: {F} F%(bool|[x] x =bool true) ⟶ ⊦F ❘
= [F,P] valid_eq trueI (refine_E2 P)❙
true_props_at_true: {F} F%(bool|[x] x =bool true) ⟶ ⊦F =(bool|[x] x =bool true) true ❘
= [F,P,Q] refine_I P (prop_ext F true ([k:⊦F] trueI) ([l:⊦true] Q))❙
both_true_equals: {F,G} F%bool ⟶ G%bool ⟶ ⊦F ⟶ ⊦G ⟶ ⊦F =(bool|[x] x =bool true) G ❘
= [F,G,P,Q,R,S] prop_trans (props_in_true2 F P R) (props_in_true2 true true_tp trueI) (props_in_true2 G Q S) (true_props_at_true (props_in_true2 F P R)) (eq_sym (true_props_at_true (props_in_true2 G Q S)))❙
= [F,G,P,Q,R,S] eq_trans (props_in_true2 F P R) (props_in_true2 true true_tp trueI) (props_in_true2 G Q S) (true_props_at_true (props_in_true2 F P R)) (eq_sym (true_props_at_true (props_in_true2 G Q S)))❙
both_true_equalsv: {F,G} F%(bool|[x] x =bool true) ⟶ G%(bool|[x] x =bool true) ⟶ ⊦F =(bool|[x] x =bool true) G ❘
= [A,r,P] [x,k:x%A] (exists_tp ([y,l:y%A] (eq_tp (A∕r) y x (quotient_I A y r l P) (quotient_I A x r k P))))❙
...
...
@@ -279,26 +297,215 @@ theory DHOL : ur:?LF =
prop_quo_true: {A,r,s,p} $A∕r ⟶ s%A∕r ⟶ ({x} x%A ⟶ p x%(bool|[x] x =bool true)) ⟶ (p s)%(bool|[x] x =bool true) ❘
= [A,r,s,p,P,Q,R] (quotient_E_quick Q ([z,k:z%A] R z k) ([z,zˈ,k:z%A,l:zˈ%A] both_true_equals (refine_E1 R z k) (refine_E1 R zˈ l) (props_in_true R z k) (props_in_true R zˈ l))) ❙
// quotient_EqRelQuo: {A,s,t,r} s%A ⟶ t%A∕r ⟶ isEqRel A r ⟶ (r s t)%bool❙
quotient_triv: {A} isEqRel A ([x,y] x =A y) ❘
= [A] [x,y,z,w,k:x%A,l:y%A,m:z%A,n:w%A,o:⊦x =A y,p:⊦y =A z] and_I (and_I (eq_refl k) (equivalence_I (impl_I ([u:⊦x =A w] eq_sym u)) (impl_I ([u:⊦w =A x] eq_sym u)))) (prop_trans k l m o p)❙
quotient_eqv: {A,s,t,r} s%A∕r ⟶ t%A∕r ⟶ isEqRel A r ⟶ ⊦(s =(A∕r) t) =bool (r s t) ❘
= [A,s,t,r,P,Q,R] _ ❙
// func_trans_quo: {A,r,x,y,s} $A∕r ⟶ s%A∕r ⟶ x%A ⟶ y%A ⟶ ⊦x =(A∕r) s ⟶ ⊦y =(A∕r) s ⟶ ⊦x =(A∕r) y ❙
// quotient_sub_help: {A,Aˈ,r,rˈ} A<Aˈ ⟶ isEqRel A r ⟶ isEqRel Aˈ rˈ ⟶ ({x,y} x%A ⟶ y%A ⟶ ⊦x =(A∕r) y ⟶ ⊦x =(Aˈ∕rˈ) y) ⟶ isEqRel A rˈ ❙
// = [A,Aˈ,r,rˈ,P,Q,R,S] [x,y,z,w,k:x%A,l:y%A,m:z%A,n:w%A] quotient_E ([x,l:x%A,m:⊦x=(A∕r) s] quotient_I (P x l) (quotient_form R)) ([x,xˈ,l:x%A,m:xˈ%A,n:⊦x=(A∕r) s,o:⊦xˈ=(A∕r) s] func_trans_quo (quotient_form Q) k l m (S x xˈ l m) )❙
quotient_sub: {A,Aˈ,r,rˈ} A<Aˈ ⟶ isEqRel A r ⟶ isEqRel Aˈ rˈ ⟶ ({x,y} x%A ⟶ y%A ⟶ ⊦r x y ⟶ ⊦rˈ x y) ⟶ A∕r < Aˈ∕rˈ ❙
// = [A,Aˈ,r,rˈ,P,Q,R,S] [s,k:s%A∕r] quotient_E ([x,l:x%A,m:⊦x=(A∕r) s] quotient_I (P x l) (quotient_form R)) ([x,xˈ,l:x%A,m:xˈ%A,n:⊦x=(A∕r) s,o:⊦xˈ=(A∕r) s] func_trans_quo (quotient_form Q) k l m (S x xˈ l m) )❙
quotient_sub: {A,Aˈ,r,rˈ} A<Aˈ ⟶ isEqRel A r ⟶ isEqRel Aˈ rˈ ⟶ ({x,y} x%A ⟶ y%A ⟶ ⊦r x y ⟶ ⊦rˈ x y) ⟶ A∕r < Aˈ∕rˈ ❘
= [A,Aˈ,r,rˈ,P,Q,R,S] [s,k:s%A∕r] quotient_E k ([x, l:x%A, m:⊦x=(A∕r) s] quotient_I Aˈ x rˈ (P x l) (quotient_form R)) ([x, xˈ, l:x%A, m:xˈ%A, n:⊦x=(A∕r) s, o:⊦xˈ=(A∕r) s] valid_eq (S x xˈ l m (valid_eq_flip (func_trans_quo A r x xˈ s (quotient_form Q) k l m n o) (quotient_eq l m Q))) (quotient_eq Aˈ x xˈ rˈ (P x l) (P xˈ m) R))❙
quotient_subtp: {A,r} $A∕r ⟶ A < A∕r ❘
= [A,r,P] [x, s: x%A] (quotient_I A x r) s P ❙
two_ary_func_on_quo_help: {A,s,t,r,f} s%A∕r ⟶ t%A ⟶ ({x,y} x%A ⟶ y%A ⟶ (f x y)%(bool|[x] x =bool true)) ⟶ (f s t)%(bool|[x] x =bool true) ❘
= [A,s,t,r,f,P,Q,R] quotient_E_quick P ([k,l:k%A] R k t l Q) ([k,kˈ,l:k%A,lˈ:kˈ%A] both_true_equalsv (R k t l Q) (R kˈ t lˈ Q))❙
two_ary_func_on_quo_help2: {A,s,t,r,f} s%A∕r ⟶ t%A∕r ⟶ ({x,y} x%A∕r ⟶ y%A ⟶ (f x y)%(bool|[x] x =bool true)) ⟶ (f s t)%(bool|[x] x =bool true) ❘
= [A,s,t,r,f,P,Q,R] quotient_E_quick Q ([k,l:k%A] R s k P l) ([k,l, m:k%A,n:l%A] both_true_equalsv (R s k P m) (R s l P n))❙
two_ary_func_on_quo: {A,s,t,r,f} s%A∕r ⟶ t%A∕r ⟶ ({x,y} x%A ⟶ y%A ⟶ (f x y)%(bool|[x] x =bool true)) ⟶ (f s t)%(bool|[x] x =bool true) ❘
= [A,s,t,r,f,P,Q,R] two_ary_func_on_quo_help2 P Q ([k,l, m:k%A∕r,n:l%A] (two_ary_func_on_quo_help m n R)) ❙
quotient_eqv: {A,s,t,r} s%A∕r ⟶ t%A∕r ⟶ isEqRel A r ⟶ ({x,y} x%A ⟶ y%A ⟶ (r x y)%bool) ⟶ ((s =(A∕r) t) =bool (r s t))%(bool|[x] x =bool true) ❘
= [A,s,t,r,P,Q,R,S] two_ary_func_on_quo P Q ([k,l, m:k%A,n:l%A] props_in_true2 (eq_tp (eq_tp (quotient_I m (quotient_form R)) (quotient_I n (quotient_form R))) (S k l m n)) (quotient_eq m n R)) ❙
quotient_eq_rel: {A,Aˈ,r,rˈ} A≡Aˈ ⟶ isEqRel A r ⟶ isEqRel Aˈ rˈ ⟶ ({x,y} x%A ⟶ y%A ⟶ ⊦(r x y) =bool (rˈ x y)) ⟶ A∕r ≡ Aˈ∕rˈ ❘
= [A,Aˈ,r,rˈ,P,Q,R,S] subtp_antisym (quotient_sub (eqtp_subtp P) Q R ([k,l, m:k%A,n:l%A, o:⊦r k l] valid_eq_flip o (S k l m n))) (quotient_sub (eqtp_subtp (eqtp_sym P)) R Q ([k,l, m:k%Aˈ,n:l%Aˈ, o:⊦rˈ k l] valid_eq o (S k l (wftm_eq m (eqtp_sym P)) (wftm_eq n (eqtp_sym P))))) ❙
quotient_eq_triv_quotient: {A} A ≡ A∕([x,y] x=A y) ❘
= [A] subtp_antisym (quotient_subtp (quotient_form quotient_triv)) ([s,k:s%A∕([x,y] x=A y)] quotient_E k ([kˈ,l:kˈ%A,m:⊦kˈ =(A∕([x,y] x=A y)) s] l) ([kˈ,lˈ, m:kˈ%A,n:lˈ%A, o:⊦kˈ =(A∕([x,y] x=A y)) s,p:⊦lˈ =(A∕([x,y] x=A y)) s] valid_eq_flip (eq_trans (quotient_I m (quotient_form quotient_triv)) k (quotient_I n (quotient_form quotient_triv)) o (eq_sym p)) quotient_eq m n quotient_triv)) ❙
quotient_triv_eq: {A,r} isEqRel A r ⟶ isEqRel A ([x,y] x=(A∕r) y) ❘
= [A,r,P] [x,y,z,w, k:x%A,l:y%A,m:z%A,n:w%A] and_I (and_I (eq_refl quotient_I k (quotient_form P)) (equivalence_I ([f:⊦x=(A∕r) w] eq_sym f) ([f:⊦w=(A∕r) x] eq_sym f))) (impl_I ([f:⊦(x=(A∕r) y ∧ y=(A∕r) z)] eq_trans (quotient_I k quotient_form P) (quotient_I l quotient_form P) (quotient_I m quotient_form P) (and_El f) (and_Er f))) ❙
quotient_triv_eq_eq: {A,r} isEqRel A r ⟶ (A∕r) ≡ A∕([x,y] x=(A∕r) y) ❘
= [A,r,P] quotient_eq_rel eqtp_refl P (quotient_triv_eq P) ([x,y, k:x%A,l:y%A] eq_sym quotient_eq k l P ) ❙
EqRel_on_quo: {A,r} isEqRel A r ⟶ isEqRel (A∕r) r ❘
= [A,r,P] [x,y,z,w, k:x%A∕r,l:y%A∕r,m:z%A∕r,n:w%A∕r] and_I (and_I (valid_eq_flip (eq_refl k) (props_in_true (quotient_eqv A x x r k k P ([s,t, f:s%A,g:t%A] EqRel_tp P f g)))) (equivalence_I ([f:⊦r x w] (valid_eq_flip (eq_sym (valid_eq f (props_in_true (quotient_eqv A x w r k n P ([s,t, g:s%A,h:t%A] EqRel_tp P g h))))) (props_in_true (quotient_eqv A w x r n k P ([s,t, g:s%A,h:t%A] EqRel_tp P g h))))) ([f:⊦r w x] (valid_eq_flip (eq_sym (valid_eq f (props_in_true (quotient_eqv A w x r n k P ([s,t, g:s%A,h:t%A] EqRel_tp P g h))))) (props_in_true (quotient_eqv A x w r k n P ([s,t, g:s%A,h:t%A] EqRel_tp P g h))))))) (impl_I ([f:⊦(r x y)∧(r y z)] valid_eq_flip (eq_trans k l m (valid_eq (and_El f) (props_in_true (quotient_eqv A x y r k l P ([s,t, g:s%A,h:t%A] EqRel_tp P g h)))) (valid_eq (and_Er f) (props_in_true (quotient_eqv A y z r l m P ([s,t, g:s%A,h:t%A] EqRel_tp P g h))))) (props_in_true (quotient_eqv A x z r k m P ([s,t, g:s%A,h:t%A] EqRel_tp P g h))))) ❙
quotient_idempotent: {A,r} isEqRel A r ⟶ ((A∕r)∕r) ≡ (A∕r) ❘
= [A,r,P] subtp_antisym ([s,k:s%(A∕r)∕r] quotient_E k ([x,l:x%A∕r, m:⊦x=((A∕r)∕r)s] l) ([x,y, l:x%A∕r,m:y%A∕r, n:⊦x=((A∕r)∕r)s,o:⊦y=((A∕r)∕r)s] valid_eq (valid_eq_flip (eq_trans (quotient_I (A∕r) x r l (quotient_form (EqRel_on_quo P))) k (quotient_I (A∕r) y r m (quotient_form (EqRel_on_quo P))) n (eq_sym o)) (quotient_eq (A∕r) x y r l m (EqRel_on_quo P))) (props_in_true (quotient_eqv l m P ([z,w, g:z%A,h:w%A] EqRel_tp P g h))))) (quotient_subtp quotient_form EqRel_on_quo P) ❙
repeated_ref: {A,p,pˈ} (A|p)|pˈ ≡ A|([x] p x ∧ pˈ x) ❘
repeated_quo_help: {A,r,rˈ} isEqRel A r ⟶ isEqRel (A∕r) rˈ ⟶ isEqRel A rˈ ❘
= [A,r,rˈ,P,Q] [x,y,z,w, k:x%A,l:y%A,m:z%A,n:w%A] and_I (and_I (EqRel_refl Q (quotient_I k (quotient_form P))) (EqRel_sym Q (quotient_I k (quotient_form P)) (quotient_I n (quotient_form P)))) (EqRel_trans Q (quotient_I k (quotient_form P)) (quotient_I l (quotient_form P)) (quotient_I m (quotient_form P)))❙
repeated_quo_help2: {A,r,rˈ} isEqRel A r ⟶ isEqRel (A∕r) rˈ ⟶ A∕rˈ < (A∕r)∕rˈ ❘
= [A,r,rˈ,P,Q] quotient_sub A (A∕r) rˈ rˈ (quotient_subtp quotient_form P) (repeated_quo_help P Q) Q ([x,y, kˈ:x%A,lˈ:y%A, m:⊦rˈ x y] m )❙
repeated_quo_help3: {A,r,rˈ,x,y} isEqRel A r ⟶ isEqRel (A∕r) rˈ ⟶ x%A ⟶ y%A ⟶ ⊦r x y ⟶ ⊦rˈ x y ❘
= [A,r,rˈ,x,y,P,Q,R,S,T] valid_eq_flip (EqRel_refl (repeated_quo_help A r rˈ P Q) R) (app_sub_eq (A∕r) ([z] bool) ([z] rˈ x z) x y (quotient_I R quotient_form P) (quotient_I S quotient_form P) (valid_eq T (quotient_eq R S P)) ([t,u:t%A∕r] EqRel_tp Q (quotient_I R quotient_form P) u)) ❙
repeated_quo_help4: {A,r,rˈ} isEqRel A r ⟶ isEqRel (A∕r) rˈ ⟶ A∕r < A∕rˈ ❘
= [A,r,rˈ,P,Q] quotient_sub (eqtp_subtp eqtp_refl) P (repeated_quo_help P Q) ([x,y, k:x%A,l:y%A, m:⊦r x y] repeated_quo_help3 P Q k l m)❙
repeated_quo_help5: {A,r,rˈ} isEqRel A r ⟶ isEqRel (A∕r) rˈ ⟶ (A∕r)∕rˈ < (A∕rˈ)∕rˈ ❘
= [A,r,rˈ,P,Q] (quotient_sub (A∕r) (A∕rˈ) rˈ rˈ (repeated_quo_help4 A r rˈ P Q) Q (EqRel_on_quo (repeated_quo_help A r rˈ P Q)) ([x,y, k:x%A∕r,l:y%A∕r, m:⊦rˈ x y] m)) ❙
repeated_quo: {A,r,rˈ} isEqRel A r ⟶ isEqRel (A∕r) rˈ ⟶ (A∕r)∕rˈ ≡ A∕rˈ ❘
= [A,r,rˈ,P,Q] subtp_antisym (subtp_trans (repeated_quo_help5 A r rˈ P Q) (eqtp_subtp (quotient_idempotent (repeated_quo_help A r rˈ P Q)))) (repeated_quo_help2 P Q) ❙
quo_in_ref_subtp: {A,r,p} isEqRel A r ⟶ ({x} x%A ⟶ p x%bool) ⟶ isEqRel (A|p) r ❘
= [A,r,p,P,Q] [x,y,z,w, k:x%A|p,l:y%A|p,m:z%A|p,n:w%A|p] and_I (and_I (EqRel_refl P (refine_E1 k)) (EqRel_sym P (refine_E1 k) (refine_E1 n))) (EqRel_trans P (refine_E1 k) (refine_E1 l) (refine_E1 m))❙
repeated_ref_quo_help: {A,r,p} isEqRel A r ⟶ ({x} x%A∕r ⟶ p x%bool) ⟶ (A∕r)|p < (A|p)∕r ❘
([y,l:y%A, m:⊦y=(A∕r)x] quotient_I (A|p) y r (refine_I A p y l (valid_eq (refine_E2 k) (app_sub_eq (A∕r) ([x] bool) p y x (quotient_I A y r l (quotient_form P)) (refine_E1 k) m ([u,v:u%A∕r] Q u v)))) (quotient_form (quo_in_ref_subtp P ([u,v:u%A] Q u quotient_I v quotient_form P))))
= [A,B,r,P] [f,g,h,i, k:f%(Π A ([x] (B x)∕r)),l:g%(Π A ([x] (B x)∕r)),m:h%(Π A ([x] (B x)∕r)),n:i%(Π A ([x] (B x)∕r))]
(and_I (and_I
(
forall_I ([b,c:b%A] EqRel_refl (quo_codomain_EqRel c (P b c)) (app_tp k c))
)
(
equivalence_I
([a:⊦∀ A [x] (r (f@x) (i@x))]
forall_I ([b, c:b%A]
impl_E
(equivalence_El (EqRel_sym (quo_codomain_EqRel c (P b c)) (app_tp k c) (app_tp n c)))
(forall_E a c)
))
([a:⊦∀ A [x] (r (i@x) (f@x))]
forall_I ([b, c:b%A]
impl_E
(equivalence_El (EqRel_sym (quo_codomain_EqRel c (P b c)) (app_tp n c) (app_tp k c)))
(forall_E a c)
))
))
(
impl_I
([a:⊦(∀ A [x] (r (f@x) (g@x))) ∧ (∀ A [x] (r (g@x) (h@x)))]
forall_I ([b, c:b%A]
impl_E (EqRel_trans (quo_codomain_EqRel c (P b c)) (app_tp k c) (app_tp l c) (app_tp m c))
(and_I (forall_E (and_El a) c) (forall_E (and_Er a) c))
))
)
)
❙
quotiented_codomain_ax: {A,B,r} (Π A ([x] (B x)∕r)) < (Π A [x] B x)∕([f,g] ∀ A [x] (r (f@x) (g@x))) ❙
quotiented_codomain: {A,B,r} ({x} x%A ⟶ isEqRel (B x) r) ⟶ isEqRel (Π A [x] B x) ([f,g] ∀ A [x] (r (f@x) (g@x))) ⟶ (Π A [x] B x)∕([f,g] ∀ A [x] (r (f@x) (g@x))) < (Π A ([x] (B x)∕r)) ❘
= [A,B,r,P,Q] [f,k:f%(Π A [x] B x)∕([u,v] ∀ A [x] (r (u@x) (v@x)))]
(quotient_E k
([g,l:g%(Π A [x] B x),m:⊦g=((Π A [x] B x)∕([u,v] ∀ A [x] (r (u@x) (v@x))))f]
exten_tp ([x,n:x%A] quotient_I (app_tp l n) (quotient_form P x n))
)
([g,h, l:g%(Π A [x] B x),m:h%(Π A [x] B x), n:⊦g=((Π A [x] B x)∕([u,v] ∀ A [x] (r (u@x) (v@x))))f,o:⊦h=((Π A [x] B x)∕([u,v] ∀ A [x] (r (u@x) (v@x))))f]
exten_eq ([z,p:z%A]
valid_eq
(forall_E
(
valid_eq_flip
(eq_trans (quotient_I l (quotient_form Q)) k (quotient_I m (quotient_form Q)) n (eq_sym o))
(quotient_eq l m Q)
)
p)
(quotient_eq (app_tp l p) (app_tp m p) (P z p))
))
)
❙
refined_domain: {A,B,p} isEqRel (Π A [x] B x) ([f,g] ∀ A [x] (p x ⇒ (f@x) =(B x) (g@x))) ⟶ (Π A [x] B x)∕([f,g] ∀ A [x] (p x ⇒ (f@x) =(B x) (g@x))) < (Π (A|p) [x] B x) ❘
= [A,B,p,P] [f,k:f%((Π A [x] B x)∕([g,h] ∀ A [x] (p x ⇒ (g@x) =(B x) (h@x))))]
quotient_E k ([g,m:g%(Π A [x] B x), u:⊦g=((Π A [x] B x)∕([h,i] ∀ A [x] (p x ⇒ (h@x) =(B x) (i@x)))) f] exten_tp ([x,l:x%(A|p)] app_tp m (refine_E1 l)))
([g,h, m:g%(Π A [x] B x),n:h%(Π A [x] B x), o:⊦g=((Π A [x] B x)∕([i,j] ∀ A [x] (p x ⇒ (i@x) =(B x) (j@x)))) f,q:⊦h=((Π A [x] B x)∕([i,j] ∀ A [x] (p x ⇒ (i@x) =(B x) (j@x)))) f]
exten_eq ([x,l:x%(A|p)]
impl_E
(forall_E
(
valid_eq_flip
(eq_trans (quotient_I m (quotient_form P)) k (quotient_I n (quotient_form P))
