---

Comment: quot_1_summary
The quotient type used to be a 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
rules 
  pointwiseFunctionality
  pertypeEquality
  pertypeMemberEquality
  pertypeElimination

(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 ⊆r (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 ⊆r (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 ⟶ ℙ].
  (EquivRel(T;x,y.E[x;y])
  ⇒ (∀[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 f 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]) ⊆r (x,y:B//E[x;y])) supposing (EquivRel(B;x,y.E[x;y]) and (A ⊆r B))

Lemma: quotient_subtype_quotient
∀[A,B:Type]. ∀[EA:A ⟶ A ⟶ ℙ]. ∀[EB:B ⟶ B ⟶ ℙ].
  ((x,y:A//EA[x;y]) ⊆r (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 ⊆r B))

Lemma: subtype_rel_quotient_trivial
∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  T ⊆r (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 ⊆r 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 
     EquivRel(T;x,y.E2[x;y]))

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 
     EquivRel(T;x,y.E2[x;y]))

Lemma: equiv_rel-wf-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//(↑E2[x;y])) ⟶ (x,y:T//(↑E2[x;y])) ⟶ 𝔹))

Lemma: equiv_rel_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//(↑E2[x;y]);x,y.↑E1[x;y]))

Lemma: quotient-dep-function-subtype
∀[X:Type]
  ∀[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])) ⊆r (f,g:x:X ⟶ A[x]//(∀x:X. (↓E[x;f x;g x]))))) 
  supposing X ⊆r 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
∀[A,B:Type].
  ∀[E:(A + B) ⟶ (A + B) ⟶ ℙ]
    (x,y:A + B//E[x;y]) ⊆r (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 ⇒ Q ⇒ R) ⇒ {⇃(P) ⇒ ⇃(Q) ⇒ ⇃(R)})

Lemma: or-quotient-true-subtype
∀P:ℙ. (⇃(P ∨ (¬P)) ⊆r (⇃(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 ==  ⇃(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; g 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,g.fun-equiv(X;a,b.E[a;b];f;g)))

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

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
∀[X:Type]
  ∀[A:Type]. ∀[E:A ⟶ A ⟶ ℙ].
    (EquivRel(A;a,b.E[a;b]) ⇒ ((X ⟶ (a,b:A//E[a;b])) ⊆r (f,g:X ⟶ A//fun-equiv(X;a,b.↓E[a;b];f;g)))) 
  supposing X ⊆r 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])) ⊆r (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) ⊆r (Top × Top)

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

Lemma: quotient-top-union-top-not-subtype
¬(⇃(Top + Top) ⊆r (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 R y)
  ⇒ (∀Q:(x,y:T//(x R y)) ⟶ (x,y:T//(x R y)) ⟶ ℙ. (EquivRel(x,y:T//(x R y);u,v.u Q v) ⇒ EquivRel(T;x,y.x Q y))))

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

Definition: preima_of_rel
R_f ==  λx,y. ((f x) R (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 R 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 R y) ⇒ (quo-lift(f) ∈ (x,y:A//(x R_f y)) ⟶ (x,y:B//(x R y))))

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

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

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

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

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



Home Index