---

Definition: per-quotient
x,y:T/per/E[x; y] ==  pertype(λx,y. ((x ∈ T) ∧ (y ∈ T) ∧ E[x; y]))

Lemma: per-quotient_wf
∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  x,y:T/per/E[x;y] ∈ Type supposing EquivRel(T;x,y.E[x;y])

Lemma: subtype_per-quotient
∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  T ⊆r (x,y:T/per/E[x;y]) supposing EquivRel(T;x,y.E[x;y])

Lemma: per-quot_elim
∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (EquivRel(T;x,y.E[x;y]) ⇒ (∀a,b:T.  (a = b ∈ (x,y:T/per/E[x;y]) ⇐⇒ ↓E[a;b])))

Lemma: decidable__per-quotient_equal
∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].
  (EquivRel(T;x,y.E[x;y]) ⇒ (∀x,y:T.  Dec(E[x;y])) ⇒ (∀u,v:x,y:T/per/E[x;y].  Dec(u = v ∈ (x,y:T/per/E[x;y]))))

Lemma: per-quotient-squash
∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  x,y:T/per/E[x;y] ≡ x,y:T/per/(↓E[x;y]) supposing EquivRel(T;x,y.E[x;y])

Lemma: per-quotient-isect-base
∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  x,y:T/per/E[x;y] ⋂ Base ≡ T ⋂ Base supposing EquivRel(T;x,y.E[x;y])

Lemma: per-quotient-isect-base2
∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  x,y:T/per/E[x;y] ⋂ Base ⊆r T ⋂ Base supposing EquivRel(T;x,y.E[x;y])

Lemma: per-quotient-value-type
∀[A:Type]. ∀[E:A ⟶ A ⟶ ℙ].  (value-type(a,b:A/per/E[a;b])) supposing (value-type(A) and EquivRel(A;a,b.E[a;b]))

Lemma: per-quotient-valueall-type
∀[A:Type]. ∀[E:A ⟶ A ⟶ ℙ].  (valueall-type(a,b:A/per/E[a;b])) supposing (valueall-type(A) and EquivRel(A;a,b.E[a;b]))

Lemma: per-isect2_quotient
∀[T:Type]. ∀[E1,E2:T ⟶ T ⟶ ℙ].
  (x,y:T/per/E1[x;y] ⋂ x,y:T/per/E2[x;y] ≡ x,y:T/per/(E1[x;y] ∧ E2[x;y])) supposing 
     (EquivRel(T;x,y.E1[x;y]) and 
     EquivRel(T;x,y.E2[x;y]))

Lemma: equiv_rel-wf-per-quotient
∀[T:Type]. ∀[E1,E2:T ⟶ T ⟶ 𝔹].
  (EquivRel(T;x,y.↑E2[x;y])
  ⇒ EquivRel(T;x,y.↑E1[x;y])
  ⇒ (∀x,y:T.  ((↑E2[x;y]) ⇒ (↑E1[x;y])))
  ⇒ (E1 ∈ (x,y:T/per/(↑E2[x;y])) ⟶ (x,y:T/per/(↑E2[x;y])) ⟶ 𝔹))

Lemma: equiv_rel_per-quotient
∀[T:Type]. ∀[E1,E2:T ⟶ T ⟶ 𝔹].
  (EquivRel(T;x,y.↑E2[x;y])
  ⇒ EquivRel(T;x,y.↑E1[x;y])
  ⇒ (∀x,y:T.  ((↑E2[x;y]) ⇒ (↑E1[x;y])))
  ⇒ EquivRel(x,y:T/per/(↑E2[x;y]);x,y.↑E1[x;y]))



Home Index