Nuprl Definition : rev-type-line-comp
(cA)- ==  (cA)(p;1-(q))
Definitions occuring in Statement : 
csm-composition: (comp)sigma
, 
interval-rev: 1-(r)
, 
csm-adjoin: (s;u)
, 
cc-snd: q
, 
cc-fst: p
Definitions occuring in definition : 
cc-snd: q
, 
interval-rev: 1-(r)
, 
cc-fst: p
, 
csm-adjoin: (s;u)
, 
csm-composition: (comp)sigma
FDL editor aliases : 
rev-type-line-comp
Latex:
(cA)-  ==    (cA)(p;1-(q))
Date html generated:
2017_01_10-AM-09_28_26
Last ObjectModification:
2016_12_04-PM-07_46_46
Theory : cubical!type!theory
Home
Index