Nuprl 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

Rules referencing : pertypeEquality, pertypeMemberEquality, pertypeElimination
FDL editor aliases : pertype

Latex:
pertype(R) == PRIMITIVE Date html generated: 2016_07_08-PM-04_47_15 Last ObjectModification: 2015_12_22-PM-04_07_02 Theory : per!type!1 Home Index