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