Nuprl Definition : fibrant-type
FibrantType(X) == A:{X ⊢ _} × X ⊢ CompOp(A)
Definitions occuring in Statement :
composition-op: Gamma ⊢ CompOp(A),
cubical-type: {X ⊢ _},
product: x:A × B[x]
Definitions occuring in definition :
composition-op: Gamma ⊢ CompOp(A),
cubical-type: {X ⊢ _},
product: x:A × B[x]
FDL editor aliases :
fibrant-type
Latex:
FibrantType(X) == A:\{X \mvdash{} \_\} \mtimes{} X \mvdash{} CompOp(A)
Date html generated:
2016_06_16-PM-02_23_01
Last ObjectModification:
2016_06_13-AM-10_23_31
Theory : cubical!type!theory
Home
Index