Nuprl Rule : equalityEquality
H  ⊢ (a11 = a12 ∈ A1) = (a21 = a22 ∈ A2) ∈ Type
  BY equalityEquality X Y x y u z ()
  
  H  ⊢ A1 = A2 ∈ Type
  H  ⊢ a11 = a21 ∈ X
  H  ⊢ a12 = a22 ∈ Y
  H x:Base, y:Base, u:(x = y ∈ X), z:(x ∈ A1) ⊢ x = y ∈ A1
  H x:Base, y:Base, u:(x = y ∈ Y), z:(x ∈ A1) ⊢ x = y ∈ A1
Latex:
H    \mvdash{}  (a11  =  a12)  =  (a21  =  a22)
    BY  equalityEquality  X  Y  x  y  u  z  ()
   
    H    \mvdash{}  A1  =  A2
    H    \mvdash{}  a11  =  a21
    H    \mvdash{}  a12  =  a22
    H  x:Base,  y:Base,  u:(x  =  y),  z:(x  \mmember{}  A1)  \mvdash{}  x  =  y
    H  x:Base,  y:Base,  u:(x  =  y),  z:(x  \mmember{}  A1)  \mvdash{}  x  =  y
Date html generated:
2019_06_20-PM-04_12_29
Last ObjectModification:
2018_11_21-AM-09_43_12
Theory : rules
Home
Index