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