Comment: quot_1_summary
The quotient type used to be primitive type with
about nine rules for reasoning about it.

We can now define the quotient type using pertype(R)

x,y:A//B[x; y] ==  pertype(λx,y. ((x ∈ A) ∧ (y ∈ A) ∧ B[x; y]))

All the reasoning about quotient can be accomplished using the

(These rules have all been proved correct in Coq by Vincent Rahli)

Comment: quot_1_intro
Basic support for quotient type. 


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

Lemma: quotient-equality
[T:Type]. ∀[E1,E2:T ⟶ T ⟶ ℙ].
  ((x,y:T//E1[x;y]) (x,y:T//E2[x;y]) ∈ Type) supposing (EquivRel(T;x,y.E1[x;y]) and (∀x,y:T.  (E2[x;y] ⇐⇒ E1[x;y])))

Lemma: subtype_quotient
[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  T ⊆(x,y:T//E[x;y]) supposing EquivRel(T;x,y.E[x;y])

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

Lemma: quotient_qinc
[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  T ⊆(x,y:T//E[x;y]) supposing EquivRel(T;x,y.E[x;y])

Lemma: type_inj_wf_for_quot
[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  ∀[a:T]. ([a]{x,y:T//E[x;y]} ∈ x,y:T//E[x;y]) supposing EquivRel(T;x,y.E[x;y])

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

Lemma: all_quot_elim
[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].
   (∀[F:(x,y:T//E[x;y]) ⟶ ℙ]. ((∀w:x,y:T//E[x;y]. SqStable(F w))  (∀z:x,y:T//E[x;y]. F[z] ⇐⇒ ∀z:T. F[z]))))

Lemma: dec_iff_ex_bvfun
[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (∀x,y:T.  Dec(E[x;y]) ⇐⇒ ∃f:T ⟶ T ⟶ 𝔹. ∀x,y:T.  (↑(x y) ⇐⇒ E[x;y]))

Lemma: decidable__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//E[x;y].  Dec(u v ∈ (x,y:T//E[x;y]))))

Lemma: subtype_rel_quotient
[A,B:Type]. ∀[E:B ⟶ B ⟶ ℙ].  ((x,y:A//E[x;y]) ⊆(x,y:B//E[x;y])) supposing (EquivRel(B;x,y.E[x;y]) and (A ⊆B))

Lemma: quotient_subtype_quotient
[A,B:Type]. ∀[EA:A ⟶ A ⟶ ℙ]. ∀[EB:B ⟶ B ⟶ ℙ].
  ((x,y:A//EA[x;y]) ⊆(x,y:B//EB[x;y])) supposing 
     ((∀x,y:A.  (EA[x;y]  EB[x;y])) and 
     EquivRel(A;x,y.EA[x;y]) and 
     EquivRel(B;x,y.EB[x;y]) and 
     (A ⊆B))

Lemma: subtype_rel_quotient_trivial
[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  T ⊆(x,y:T//E[x;y]) supposing EquivRel(T;x,y.E[x;y])

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

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

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

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

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

Lemma: quotient-mono
[T:Type]. (mono(T)  (∀E:T ⟶ T ⟶ ℙ(EquivRel(T;x,y.E[x;y])  mono(x,y:T//E[x;y]))))

Lemma: respects-equality-quotient
[X,T:Type]. ∀[E1:X ⟶ X ⟶ ℙ]. ∀[E2:T ⟶ T ⟶ ℙ].
  (respects-equality(x,y:X//E1[x;y];x,y:T//E2[x;y])) supposing 
     ((∀x,y:X.  (E1[x;y]  (x ∈ T)  ((y ∈ T) ∧ E2[x;y]))) and 
     respects-equality(X;T) and 
     EquivRel(X;x,y.E1[x;y]) and 

Lemma: respects-equality-quotient1
[X,T:Type]. ∀[E:T ⟶ T ⟶ ℙ].
  (respects-equality(X;x,y:T//E[x;y])) supposing (respects-equality(X;T) and EquivRel(T;x,y.E[x;y]))

Definition: equiv-class
equiv-class(A;a,b.E[a; b];t) ==  {b:A| ↑E[t; b]} 

Lemma: equiv-class_wf
[A:Type]. ∀[E:A ⟶ A ⟶ 𝔹].
  ∀[t:x,y:A//(↑E[x;y])]. (equiv-class(A;x,y.E[x;y];t) ∈ Type) supposing EquivRel(A;x,y.↑E[x;y])

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

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

Lemma: equiv_rel_quotient
[T:Type]. ∀[E1,E2:T ⟶ T ⟶ 𝔹].
   (∀x,y:T.  ((↑E2[x;y])  (↑E1[x;y])))

Lemma: quotient-dep-function-subtype
  ∀[A:X ⟶ Type]. ∀[E:x:X ⟶ A[x] ⟶ A[x] ⟶ ℙ].
    ((∀x:X. EquivRel(A[x];a,b.E[x;a;b]))
     ((x:X ⟶ (a,b:A[x]//E[x;a;b])) ⊆(f,g:x:X ⟶ A[x]//(∀x:X. (↓E[x;f x;g x]))))) 
  supposing X ⊆Base

Lemma: not-has-value-decidable-quot
[E:(∀x:Base. ((x)↓ ∨ (x)↓))) ⟶ (∀x:Base. ((x)↓ ∨ (x)↓))) ⟶ ℙ]
  ¬(f,g:∀x:Base. ((x)↓ ∨ (x)↓))//E[f;g]) supposing EquivRel(∀x:Base. ((x)↓ ∨ (x)↓));f,g.E[f;g])

Lemma: disjoint-quotient_subtype
  ∀[E:(A B) ⟶ (A B) ⟶ ℙ]
    (x,y:A B//E[x;y]) ⊆(a1,a2:A//E[inl a1;inl a2] (b1,b2:B//E[inr b1 ;inr b2 ])) 
    supposing EquivRel(A B;x,y.E[x;y]) 
  supposing ¬(A ∧ B)

Lemma: or-quotient-true
P:ℙ(⇃(P ∨ P))  (⇃(P) ∨ ⇃P)))

Lemma: implies-quotient-true
[P,Q:ℙ].  ((P  Q)  {⇃(P)  ⇃(Q)})

Lemma: implies-quotient-true2
[P,Q:ℙ].  ((P  ⇃(Q))  {⇃(P)  ⇃(Q)})

Lemma: quotient-implies-squash
[P,Q:ℙ].  ((P  Q)  {⇃(P)  (↓Q)})

Lemma: squash-from-quotient
[Q:ℙ]. (⇃(Q)  (↓Q))

Lemma: trivial-quotient-true
[P:ℙ]. (P  ⇃(P))

Lemma: quotient-bind
A,B:Type.  (⇃(A)  (A  ⇃(B))  ⇃(B))

Lemma: quotient-bind-ext
A,B:Type. ∀a:⇃(A). ∀f:A ⟶ ⇃(B).  (f a ∈ ⇃(B))

Lemma: eq-in-quot
A:Type. ∀a,b:⇃(A).  (a b ∈ ⇃(A))

Lemma: quotient-bind-ext2
A,B:Type. ∀a:⇃(A). ∀f:A ⟶ ⇃(B).  (f a ∈ ⇃(B))

Lemma: not-quotient-true
[P:ℙ]. (¬⇃(P) ⇐⇒ ¬P)

Lemma: two-implies-quotient-true
[P,Q,R:ℙ].  ((P   R)  {⇃(P)  ⇃(Q)  ⇃(R)})

Lemma: or-quotient-true-subtype
P:ℙ(⇃(P ∨ P)) ⊆(⇃(P) ∨ ⇃P)))

Lemma: no-excluded-middle-quot-true1
¬(∀P:ℙ. ⇃(P ∨ P)))

Lemma: no-excluded-middle-quot-true
¬(∀P:ℙ. ⇃(P ∨ (↓¬P)))

Lemma: no-excluded-middle-quot-true2
¬(∀P:ℙ. ⇃(P ∨ P)))

Lemma: not-not-excluded-middle-quot-true
P:ℙ(¬¬⇃(P ∨ P)))

Definition: half-squash-stable
half-squash-stable(P) ==  ⇃(P)  P

Lemma: half-squash-stable_wf
[P:ℙ]. (half-squash-stable(P) ∈ ℙ)

Lemma: half-squash-stable__and
[P,Q:ℙ].  (half-squash-stable(P)  half-squash-stable(Q)  half-squash-stable(P ∧ Q))

Lemma: half-squash-stable__all
[T:Type]. ∀[P:T ⟶ ℙ].  ((∀x:T. half-squash-stable(P[x]))  half-squash-stable(∀x:T. P[x]))

Lemma: half-squash-stable__half-squash
[P:ℙ]. half-squash-stable(⇃(P))

Lemma: sq_stable-implies-half-squash-stable
[P:ℙ]. (SqStable(P)  half-squash-stable(P))

Lemma: half-squash-equality
[Q:Type]. ∀[a,b:⇃(Q)].  (a b ∈ ⇃(Q))

Definition: truncate
|x| ==  x

Lemma: truncate_wf
[X:Type]. ∀[x:X].  (|x| ∈ ⇃(X))

Definition: truncate-map
|f| ==  f

Lemma: truncate-map_wf
[X,Q:Type].  ∀f:X ⟶ ⇃(Q). (|f| ∈ ⇃(X) ⟶ ⇃(Q))

Lemma: truncation-property
[X,Q:Type].  ∀f:X ⟶ ⇃(Q). ((∀x:X. ((|f| |x|) (f x) ∈ ⇃(Q))) ∧ (∀g:⇃(X) ⟶ ⇃(Q). (g |f| ∈ (⇃(X) ⟶ ⇃(Q)))))

Lemma: un-half-squash-test
[P,Q,R:ℙ].  (((P ∧ R)  Q)  ⇃(R)  half-squash-stable(Q)  ⇃(P)  True  {Q ∧ ⇃(P) ∧ (∀n:ℕQ)})

Definition: qsquash
==  ⇃(T)

Lemma: qsquash_wf
[T:Type]. (⇃T ∈ Type)

Definition: fun-equiv
fun-equiv(X;a,b.E[a; b];f;g) ==  ∀x:X. E[f x; x]

Lemma: fun-equiv_wf
[X,A:Type]. ∀[E:A ⟶ A ⟶ ℙ]. ∀[f,g:X ⟶ A].  (fun-equiv(X;a,b.E[a;b];f;g) ∈ ℙ)

Lemma: fun-equiv-rel
[X,A:Type]. ∀[E:A ⟶ A ⟶ ℙ].  (EquivRel(A;a,b.E[a;b])  EquivRel(X ⟶ A;f,;a,b.E[a;b];f;g)))

Definition: dep-fun-equiv
                        b];f;g) ==

Lemma: dep-fun-equiv_wf
[X:Type]. ∀[A:X ⟶ Type]. ∀[E:x:X ⟶ A[x] ⟶ A[x] ⟶ ℙ]. ∀[f,g:x:X ⟶ A[x]].  (dep-fun-equiv(X;x,f,g.E[x;f;g];f;g) ∈ ℙ)

Lemma: dep-fun-equiv-rel
[X:Type]. ∀[A:X ⟶ Type]. ∀[E:x:X ⟶ A[x] ⟶ A[x] ⟶ ℙ].
  ((∀x:X. EquivRel(A[x];a,b.E[x;a;b]))  EquivRel(x:X ⟶ A[x];f,g.dep-fun-equiv(X;x,a,b.E[x;a;b];f;g)))

Lemma: quotient-function-subtype
  ∀[A:Type]. ∀[E:A ⟶ A ⟶ ℙ].
    (EquivRel(A;a,b.E[a;b])  ((X ⟶ (a,b:A//E[a;b])) ⊆(f,g:X ⟶ A//fun-equiv(X;a,b.↓E[a;b];f;g)))) 
  supposing X ⊆Base

Lemma: not-quotient-function-subtype
¬(∀[X,A:Type]. ∀[E:A ⟶ A ⟶ ℙ].
    (EquivRel(A;a,b.E[a;b])  ((X ⟶ (a,b:A//E[a;b])) ⊆(f,g:X ⟶ A//fun-equiv(X;a,b.↓E[a;b];f;g)))))

Lemma: not_has-value_decidable_on_base_quot_true
¬(∀t:Base. ⇃((t)↓ ∨ (t)↓)))

Lemma: quotient-top-prod-top
(Top × Top) ⊆(Top × Top)

Lemma: quotient-top-union-top
(Top Top) ⋂ Base ⊆(Top Top)

Lemma: quotient-top-union-top-not-subtype
¬(⇃(Top Top) ⊆(Top Top))

Definition: injective-quotient
T//x.f[x] ==  x,y:T//(f[x] f[y] ∈ S)

Lemma: injective-quotient_wf
[T,S:Type]. ∀[f:T ⟶ S].  (T//x.f[x] ∈ Type)

Lemma: injective-quotient-typing
[T,S:Type]. ∀[f:T ⟶ S].  (f ∈ T//x.f[x] ⟶ S)

Lemma: injective-quotient-inject
[T,S:Type]. ∀[f:T ⟶ S].  Inj(T//x.f[x];S;λx.f[x])

Lemma: equiv-on-quotient
T:Type. ∀R:T ⟶ T ⟶ ℙ.
  (EquivRel(T;x,y.x y)
   (∀Q:(x,y:T//(x y)) ⟶ (x,y:T//(x y)) ⟶ ℙ(EquivRel(x,y:T//(x y);u,v.u v)  EquivRel(T;x,y.x y))))

Lemma: quotient-of-quotient
T:Type. ∀R:T ⟶ T ⟶ ℙ.
  (EquivRel(T;x,y.x y)
   (∀Q:(x,y:T//(x y)) ⟶ (x,y:T//(x y)) ⟶ ℙ
        (EquivRel(x,y:T//(x y);u,v.u v)  u,v:x,y:T//(x y)//(u v) ≡ x,y:T//(x y))))

Definition: preima_of_rel
R_f ==  λx,y. ((f x) (f y))

Lemma: preima_of_rel_wf
A,B:Type. ∀f:A ⟶ B. ∀R:B ⟶ B ⟶ ℙ.  (R_f ∈ A ⟶ A ⟶ ℙ)

Lemma: preima_of_equiv_rel
A,B:Type. ∀f:A ⟶ B. ∀R:B ⟶ B ⟶ ℙ.  (EquivRel(B;x,y.x y)  EquivRel(A;x,y.x R_f y))

Definition: quo-lift
quo-lift(f) ==  f

Lemma: quo-lift_wf
A,B:Type. ∀f:A ⟶ B. ∀R:B ⟶ B ⟶ ℙ.  (EquivRel(B;x,y.x y)  (quo-lift(f) ∈ (x,y:A//(x R_f y)) ⟶ (x,y:B//(x y))))

Lemma: biject-quotient
A,B:Type. ∀f:A ⟶ B. ∀R:B ⟶ B ⟶ ℙ.
  (Bij(A;B;f)  EquivRel(B;x,y.x y)  Bij(x,y:A//(x R_f y);x,y:B//(x y);quo-lift(f)))

Lemma: extend-type-equiv
[T:Type]. EquivRel(Base;x,y.(x ∈ ⇐⇒ y ∈ T) ∧ ((x ∈ T)  (x y ∈ T)))

Definition: extend-type
(T)+ ==  x,y:Base//((x ∈ ⇐⇒ y ∈ T) ∧ ((x ∈ T)  (x y ∈ T)))

Lemma: extend-type_wf
[T:Type]. ((T)+ ∈ Type)

Lemma: extend-type-property
[T:Type]. ((T ⊆(T)+) ∧ respects-equality((T)+;T) ∧ (∀X:Type. (respects-equality(X;T)  (X ⊆(T)+))))

Home Index