Nuprl Rule : equalityIstype

H  ⊢ istype(a = b ∈ A)

  BY equalityIstype X Y x y u z ()

  H  ⊢ istype(A)
  H  ⊢ a ∈ X
  H  ⊢ b ∈ Y
  H x:Base, y:Base, u:(x = y ∈ X), z:(x ∈ A) ⊢ x = y ∈ A
  H x:Base, y:Base, u:(x = y ∈ Y), z:(x ∈ A) ⊢ x = y ∈ A

Latex:
H \mvdash{} istype(a = b) BY equalityIstype X Y x y u z () H \mvdash{} istype(A) H \mvdash{} a \mmember{} X H \mvdash{} b \mmember{} Y H x:Base, y:Base, u:(x = y), z:(x \mmember{} A) \mvdash{} x = y H x:Base, y:Base, u:(x = y), z:(x \mmember{} A) \mvdash{} x = y Date html generated: 2019_06_20-PM-04_11_52 Last ObjectModification: 2018_11_21-PM-02_51_36 Theory : rules Home Index