---

Comment: Hypothesis Subsumption with pointwise
The rule is
  H x:A, J ⊢ C ext t

  BY hypothesis_subsumption #$i B ()
  
  H  ⊢ B ⊆r A
  H x:A, J ⊢ x ∈ B
  H x:B, J ⊢ C ext t

(Note that from this rule we can derive the rule hyp_replacement
 so that rule could be removed if we rewrite a few tactics.)

Here is the proof that the rule is correct (using pointwise functionality)
  Let Gamma_A be the hypotheses  H x:A J,  and Gamma_B be  H x:B J.
  Let s be a substitution for the variables declared in Gamma.
  A substitution s' "agrees with s mod Gamma" if for each v:T in Gamma,
   s'(v) = s(v) \in s(T)

  s satisfies Gamma if for each v:T in Gamma
  s(v) in s(T)  and  for any s' that agrees with s mod Gamma, 
  s'(T) = s(T) in some universe Ui.

  s satisfies the conclusion (C ext t) if
  s(t) in s(C) and for any s' that agrees with s mod Gamma,
  s'(C) = s(C) in some universe

  A sequent is true if every s that satisfies its hyps also
  satisfies its concl.
 
  Assuming that the three subgoal sequents are true we must show that
  if s satisfies Gamma_A then s satisfies (C ext t)

   Since H x:B, J ⊢ C ext t is assumed true, it is enough to show
   s satisfies Gamma_B.

   Since s satisfies Gamma_A, it is enough to show that
   1) s(x) in s(B)  and 
   2) for any s' that agrees with s mod Gamma_B,  for each v:T in Gamma_B 
      s'(T) = s(T) in some universe.

   From the truth of H x:A, J ⊢ x ∈ B  we get
    Ax \in s(x ∈ B) 
    and for any s' that agrees with s mod Gamma
    s'(x ∈ B) = s'(x ∈ B) in some universe

  The first of these implies that s(x) \in s(B), so we have 1)
  For 2) it is enough to show that if s' agrees with s mod Gamma_B
         then s' agrees with s mod Gamma_A
         and s'(B) = s(B) in some universe

  For that, suppose s' agrees with s mod Gamma_B. Then s' agrees with s mod H
  so since H  ⊢ B ⊆r A is true,
    Ax \in s(B ⊆r A) and s'(B ⊆r A) = s(B ⊆r A) in some universe

  The second of these implies that s'(B) = s(B)
  and the first implies that since s'(x) = s(x) \in s(B) then
   s'(x) = s(x) \in s(A), so s' agrees with s mod Gamma_A

  .
  QED  
.






 ⋅

Comment: Hypothesis Subsumption with pairwise
In pairwise functionality, the rule is simpler than in pointwise functionality
since we don't need to prove H  ⊢ B ⊆r A.
The rule becomes:
  H x:A, J ⊢ C ext t

  BY hypothesis_subsumption #$i B ()
  
  H x:A, J ⊢ x ∈ B
  H x:B, J ⊢ C ext t

Here is the proof:
  Let Gamma be the hypotheses  H x:A J,  and Gamma' be  H x:B J.
  Let s1, s2 be substitutions for the variables declared in Gamma.

  The pair s1,s2 satisfies Gamma if for each v:T in Gamma
  s1(v) = s2(v) in s1(T)  and  s1(T) = s2(T) in some universe Ui.

  The pair s1,s2 satisfies the conclusion (C ext t) if
  s1(t) = s2(t) in s1(C) and  s1(C) = s2(C) in some universe

  A sequent is true in pairwise functionality
  if every pair s1,s2 that satisfies its hyps also
  satisfies its concl.
 
  Assuming that the two subgoal sequents are true (in pairwise functionality) 
  we must show that
  if s1,s2 satisfies Gamma then s1,s2 satisfies (C ext t)

   Since H x:B, J ⊢ C ext t is assumed true, it is enough to show
   s1,s2 satisfies Gamma'.

   Since s1,s2 satisfy Gamma, it is enough to show that
   s1(x) = s2(x) in s1(B)  and  s1(B) = s2(B) in some universe.

   From the truth of H x:A, J ⊢ x ∈ B  we get
    Ax \in s1(x ∈ B) and s1(x ∈ B) = s2(x ∈ B) in some universe

  This implies that  s1(x) = s2(x) in s1(B) and that
        s1(B) = s2(B) in that universe .
  QED  
.






 ⋅

Lemma: sq_stable__subtype_rel
∀[A,B:Type].  SqStable(A ⊆r B)

Lemma: subtype_rel_universe1
Type ⊆r 𝕌'

Lemma: subtype_rel_universe2
Type ⊆r 𝕌''

Lemma: subtype_rel_function
∀[A,B,C,D:Type].  ((A ⟶ B) ⊆r (C ⟶ D)) supposing ((B ⊆r D) and (C ⊆r A))

Lemma: subtype_rel_dep_function
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[C:Type]. ∀[D:C ⟶ Type].
  ((a:A ⟶ B[a]) ⊆r (c:C ⟶ D[c])) supposing ((∀a:C. (B[a] ⊆r D[a])) and (C ⊆r A))

Lemma: subtype_rel_product
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[C:Type]. ∀[D:C ⟶ Type].
  ((a:A × B[a]) ⊆r (c:C × D[c])) supposing ((∀a:A. (B[a] ⊆r D[a])) and (A ⊆r C))

Lemma: subtype_rel_image
∀[A,B:Type]. ∀[f:Base].  Image(A,f) ⊆r Image(B,f) supposing A ⊆r B

Lemma: subtype_rel_tunion
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[C:Type]. ∀[D:C ⟶ Type].
  (⋃a:A.B[a] ⊆r ⋃c:C.D[c]) supposing ((∀a:A. (B[a] ⊆r D[a])) and (A ⊆r C))

Lemma: subtype_rel_simple_product
∀[A,B,C,D:Type].  ((A × B) ⊆r (C × D)) supposing ((B ⊆r D) and (A ⊆r C))

Lemma: subtype_rel_union
∀[A,B,C,D:Type].  ((A + B) ⊆r (C + D)) supposing ((B ⊆r D) and (A ⊆r C))

Lemma: subtype_rel_dep_product_iff
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[C:Type]. ∀[D:C ⟶ Type].
  uiff(∀[a:A]. (B[a] ⊆r D[a]);(a:A × B[a]) ⊆r (c:C × D[c])) supposing A ⊆r C

Lemma: subtype_rel_sum
∀[A,B,C,D:Type].  ((A + B) ⊆r (C + D)) supposing ((B ⊆r D) and (A ⊆r C))

Lemma: subtype_rel_set
∀[A,B:Type]. ∀[P:A ⟶ ℙ].  {a:A| P[a]}  ⊆r B supposing A ⊆r B

Lemma: subtype_rel_set_simple
∀[A:Type]. ∀[P:A ⟶ ℙ].  ({a:A| P[a]}  ⊆r A)

Lemma: subtype_rel_sets
∀[A,B:Type]. ∀[P:A ⟶ ℙ]. ∀[Q:B ⟶ ℙ].  ({a:A| P[a]}  ⊆r {b:B| Q[b]} ) supposing ((∀a:A. (P[a] ⇒ Q[a])) and ({a:A| P[a]\000C}  ⊆r B))

Lemma: subtype_rel_sets_simple
∀[A:Type]. ∀[P,Q:A ⟶ ℙ].  {a:A| P[a]}  ⊆r {b:A| Q[b]}  supposing ∀a:A. (P[a] ⇒ Q[a])

Lemma: subtype_rel_transitivity
∀[A,B,C:Type].  (A ⊆r C) supposing ((B ⊆r C) and (A ⊆r B))

Lemma: subtype_rel_nested_set
∀[A,B:Type]. ∀[P:B ⟶ ℙ]. ∀[Q:{b:B| P[b]}  ⟶ ℙ].  A ⊆r {b:{b:B| P[b]} | Q[b]}  supposing A ⊆r {b:B| P[b] ∧ Q[b]} 

Lemma: subtype_rel_nested_set2
∀[A,B:Type]. ∀[P:B ⟶ ℙ]. ∀[Q:{b:B| P[b]}  ⟶ ℙ].  {b:{b:B| P[b]} | Q[b]}  ⊆r A supposing {b:B| P[b] ∧ Q[b]}  ⊆r A

Lemma: subtype_rel_isect_general
∀[A,T:Type]. ∀[C:A ⟶ Type]. ∀[B:T ⟶ Type].  (⋂x:A. C[x]) ⊆r (⋂x:T. B[x]) supposing (T ⊆r A) ∧ (∀x:T. (C[x] ⊆r B[x]))

Lemma: subtype_rel_isect
∀[A,T:Type]. ∀[B:T ⟶ Type].  uiff(A ⊆r (⋂x:T. B[x]);∀[x:T]. (A ⊆r B[x]))

Lemma: subtype_rel_isect_as_subtyping_lemma
∀[A,T:Type]. ∀[B:T ⟶ Type].  A ⊆r (⋂x:T. B[x]) supposing ∀[x:T]. (A ⊆r B[x])

Lemma: subtype_rel_isect-2
∀[A:Type]. ∀[B1,B2:A ⟶ Type].  (⋂x:A. B1[x]) ⊆r (⋂x:A. B2[x]) supposing ∀[x:A]. (B1[x] ⊆r B2[x])

Lemma: subtype_rel_double_isect
∀[A,T1,T2:Type]. ∀[B:T1 ⟶ T2 ⟶ Type].  uiff(A ⊆r (⋂x:T1. ⋂y:T2.  B[x;y]);∀[x:T1]. ∀[y:T2].  (A ⊆r B[x;y]))

Lemma: subtype_rel_not
∀[P,Q:ℙ].  (¬P) ⊆r (¬Q) supposing Q ⇒ (↓P)

Lemma: isect_subtype_rel_trivial
∀[A,C:Type]. ∀[B:A ⟶ Type].  (⋂x:A. B[x]) ⊆r C supposing ∃x:A. (B[x] ⊆r C)

Lemma: isect_subtype_rel
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[x:A].  ((⋂x:A. B[x]) ⊆r B[x])

Lemma: double_isect_subtype_rel
∀[T1,T2:Type]. ∀[B:T1 ⟶ T2 ⟶ Type]. ∀[x:T1]. ∀[y:T2].  ((⋂x:T1. ⋂y:T2.  B[x;y]) ⊆r B[x;y])

Definition: rev_subtype_rel
A ⊇r B ==  B ⊆r A

Lemma: rev_subtype_rel_wf
∀[A,B:Type].  (A ⊇r B ∈ ℙ)

Definition: ext-eq
A ≡ B ==  (A ⊆r B) ∧ (B ⊆r A)

Lemma: ext-eq_wf
∀[A,B:Type].  (A ≡ B ∈ ℙ)

Lemma: sq_stable__ext-eq
∀[A,B:Type].  SqStable(A ≡ B)

Lemma: ext-eq_weakening
∀[A,B:Type].  A ≡ B supposing A = B ∈ Type

Lemma: ext-eq_inversion
∀[A,B:Type].  B ≡ A supposing A ≡ B

Lemma: ext-eq_transitivity
∀[A,B,C:Type].  (A ≡ C) supposing (B ≡ C and A ≡ B)

Lemma: iff_weakening_ext-eq
∀[A,B:Type].  {A ⇐⇒ B} supposing A ≡ B

Lemma: subtype_rel_functionality_wrt_iff
∀[A,B,C,D:Type].  ({uiff(A ⊆r B;C ⊆r D)}) supposing (B ≡ D and A ≡ C)

Lemma: subtype_rel_functionality_wrt_implies
∀[A,B,C,D:Type].  ({C ⊆r D supposing A ⊆r B}) supposing ((B ⊆r D) and (A ⊇r C))

Lemma: subtype_rel_weakening
∀[A,B:Type].  A ⊆r B supposing A ≡ B

Lemma: rev_subtype_rel_weakening
∀[A,B:Type].  A ⊇r B supposing A ≡ B

Lemma: subtype-top
∀[T:Type]. uiff(T ⊆r Top;True)

Lemma: subtype_rel-equal
∀[A,B:Type].  A ⊆r B supposing A = B ∈ Type

Lemma: subtype_rel_self
∀[A:Type]. (A ⊆r A)

Lemma: void-product
∀[T,S:Type].  T × S ≡ Void supposing S ≡ Void

Lemma: void-dep-product
∀[S:Type]. ∀[F:S ⟶ Type].  m:S × (F m) ≡ Void supposing S ≡ Void

Lemma: product_subtype_base
∀[A:Type]. ∀[B:A ⟶ Type].  ((a:A × B[a]) ⊆r Base) supposing ((∀a:A. (B[a] ⊆r Base)) and (A ⊆r Base))

Lemma: simple-product_subtype_base
∀[A,B:Type].  ((A × B) ⊆r Base) supposing ((B ⊆r Base) and (A ⊆r Base))

Lemma: union_subtype_base
∀[A,B:Type].  ((A + B) ⊆r Base) supposing ((B ⊆r Base) and (A ⊆r Base))

Lemma: set_subtype_base
∀[A:Type]. ∀[P:A ⟶ ℙ].  {a:A| P[a]}  ⊆r Base supposing A ⊆r Base

Lemma: isect_subtype_base
∀[A:Type]. ∀[B:A ⟶ Type].  (⋂a:A. B[a]) ⊆r Base supposing ∃a:A. (B[a] ⊆r Base)

Lemma: tunion_subtype_base
∀[A:Type]. ∀[B:A ⟶ Type].  ⋃a:A.B[a] ⊆r Base supposing ∀a:A. (B[a] ⊆r Base)

Lemma: baseof_subtype
∀[T:Type]. (baseof(T) ⊆r T)

Lemma: baseof_subtype_base
∀[T:Type]. (baseof(T) ⊆r Base)

Lemma: subtype_top
∀[T:Type]. (T ⊆r Top)

Lemma: uall_instance_test
∀[F:Type ⟶ ℤ ⟶ ℤ ⟶ ℙ]. ∀x:∀[A:Type]. ∀[m,c:ℤ].  F[A;m;c]. ∀B:Type. ∀n,b:ℤ.  (x ∈ F[B;n;b])

Lemma: tunion-is-image
∀[A:Type]. ∀[B:A ⟶ Type].  (⋃a:A.B[a] ~ Image((a:A × B[a]),(λp.(snd(p)))))

Lemma: set-is-image
∀[A:Type]. ∀[B:A ⟶ Type].  {a:A| B[a]}  ≡ Image((a:A × B[a]),(λp.(fst(p))))

Lemma: equal_functionality_wrt_subtype_rel
∀[A,B:Type]. ∀[x,y:A].  {x = y ∈ B supposing x = y ∈ A} supposing A ⊆r B

Lemma: equal_functionality_wrt_subtype_rel2
∀[A,B:Type]. ∀[x,y:A].  {(x = y ∈ A) ⇒ (x = y ∈ B)} supposing A ⊆r B

Lemma: decidable-subtype
∀[P,Q:ℙ].  (Dec(P) ⊆r Dec(Q)) supposing ((Q ⇒ P) and (P ⊆r Q))

Lemma: subtype-respects-equality
∀[A,B:Type].  respects-equality(B;A) supposing B ⊆r A

Lemma: general-subtype-respects-equality
∀[A,B,C:Type].  (respects-equality(B;C)) supposing (respects-equality(A;C) and (B ⊆r A))

Lemma: subtype-base-respects-equality
∀[A,B:Type].  respects-equality(B;A) supposing B ⊆r Base



Home Index