Nuprl Definition : name-morph-satisfies
(psi f) = 1 ==  (psi)<f> = 1 ∈ Point(face_lattice(J))
Definitions occuring in Statement : 
fl-morph: <f>
, 
face_lattice: face_lattice(I)
, 
lattice-1: 1
, 
lattice-point: Point(l)
, 
apply: f a
, 
equal: s = t ∈ T
Definitions occuring in definition : 
equal: s = t ∈ T
, 
lattice-point: Point(l)
, 
apply: f a
, 
fl-morph: <f>
, 
lattice-1: 1
, 
face_lattice: face_lattice(I)
FDL editor aliases : 
name-morph-satisfies
Latex:
(psi  f)  =  1  ==    (psi)<f>  =  1
Date html generated:
2016_05_18-PM-00_19_50
Last ObjectModification:
2015_10_27-PM-06_48_10
Theory : cubical!type!theory
Home
Index