---

Definition: pertype
We only need four rules to reason about ⌜pertype(R)⌝

H  ⊢ pertype(R) = pertype(R') ∈ Type

  BY pertypeEquality x y z u v ()
  
  H x:Base, y:Base ⊢ R x y ∈ Type
  H x:Base, y:Base ⊢ R' x y ∈ Type
  H x:Base, y:Base, z:R x y ⊢ R' x y
  H x:Base, y:Base, z:R' x y ⊢ R x y
  H x:Base, y:Base, z:R x y ⊢ R y x
  H x:Base, y:Base, z:Base, u:R x y, v:R y z ⊢ R x z

H  ⊢ t1 = t2 ∈ pertype(R)

  BY pertypeMemberEquality !parameter{i:l}
  
  H  ⊢ pertype(R) ∈ Type
  H  ⊢ R t1 t2
  H  ⊢ t1 ∈ Base
  H  ⊢ t2 ∈ Base

H x:(t1 = t2 ∈ pertype(R)), J ⊢ C ext e

  BY pertypeElimination #$n !parameter{i:l} y ()
  
  H x:(t1 = t2 ∈ pertype(R)), [y:R t1 t2], J ⊢ C ext e
  H  ⊢ R t1 t2 ∈ Type

H z:A, J ⊢ C ext t

  BY pointwiseFunctionality #$i !parameter{j:l} a b c ()
  
  H [a:Base], [b:Base], [c:(a = b ∈ A)], J[a/z] ⊢ C[a/z] ext t
  H a:Base, b:Base, c:(a = b ∈ A), J[a/z] ⊢ C[a/z] = C[b/z] ∈ 𝕌{j}⋅

pertype(R) ==  PRIMITIVE

Comment: rules for per type
We only need four rules to reason about ⌜pertype(R)⌝

H  ⊢ pertype(R) = pertype(R') ∈ Type

  BY pertypeEquality x y z u v ()
  
  H x:Base, y:Base ⊢ R x y ∈ Type
  H x:Base, y:Base ⊢ R' x y ∈ Type
  H x:Base, y:Base, z:R x y ⊢ R' x y
  H x:Base, y:Base, z:R' x y ⊢ R x y
  H x:Base, y:Base, z:R x y ⊢ R y x
  H x:Base, y:Base, z:Base, u:R x y, v:R y z ⊢ R x z

H  ⊢ t1 = t2 ∈ pertype(R)

  BY pertypeMemberEquality !parameter{i:l}
  
  H  ⊢ pertype(R) ∈ Type
  H  ⊢ R t1 t2
  H  ⊢ t1 ∈ Base
  H  ⊢ t2 ∈ Base

H x:(t1 = t2 ∈ pertype(R)), J ⊢ C ext e

  BY pertypeElimination #$n !parameter{i:l} y ()
  
  H x:(t1 = t2 ∈ pertype(R)), [y:R t1 t2], J ⊢ C ext e
  H  ⊢ R t1 t2 ∈ Type

H z:A, J ⊢ C ext t

  BY pointwiseFunctionality #$i !parameter{j:l} a b c ()
  
  H [a:Base], [b:Base], [c:(a = b ∈ A)], J[a/z] ⊢ C[a/z] ext t
  H a:Base, b:Base, c:(a = b ∈ A), J[a/z] ⊢ C[a/z] = C[b/z] ∈ 𝕌{j}⋅

Lemma: pertype_wf
∀[R:Base ⟶ Base ⟶ ℙ]
  (pertype(R) ∈ Type) supposing ((∀x,y:Base.  (R[x;y] ⇒ R[y;x])) and (∀x,y,z:Base.  (R[x;y] ⇒ R[y;z] ⇒ R[x;z])))

Definition: quotient
The quotient type allows us to change the equality for members of a type A
to a given equivalence relation B(x,y). 
It is a special case of the more general pertype.

When B(x,y) is the trival equivalence relation True, then we display
the quotient x,y:A//B as ⌜⇃(A)⌝. We call this the "half squash" of A
since it retains the members of A but "squashes" the equality in A.⋅

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

Definition: usquash
usquash(T) ==  pertype(λx,y. (↓T))

Lemma: usquash_wf
∀[T:ℙ]. (usquash(T) ∈ Type)

Lemma: implies-usquash
∀[T:ℙ]. (T ⇒ (∀x:Top. (x ∈ usquash(T))))

Lemma: implies-usquash2
∀[T:ℙ]. (T ⇒ usquash(T))

Lemma: member-usquash
∀[T:ℙ]. (usquash(T) ⇒ (∀x:Top. (x ∈ usquash(T))))

Lemma: sq_stable_usquash
∀[T:ℙ]. SqStable(usquash(T))

Lemma: squash-implies-usquash
∀[T:ℙ]. ((↓T) ⇒ usquash(T))

Lemma: usquash-implies-squash
∀[T:ℙ]. (usquash(T) ⇒ (↓T))

Lemma: usquash-equality
∀[T:ℙ]. ∀[S:Type].  usquash(T) = usquash(S) ∈ Type supposing ↓T ⇐⇒ ↓S

Lemma: usquash-elim
∀[T:ℙ]. (SqStable(T) ⇒ usquash(T) ⇒ T)



Home Index