Nuprl Definition : equiv_term
equiv f [phi ⊢→ (t,c)] a == equiv f [phi ⊢→ (t, c)] a
Definitions occuring in Statement :
equiv-term: equiv f [phi ⊢→ (t, c)] a,
fiber-comp: fiber-comp(X;T;A;w;a;cT;cA),
equiv-fun: equiv-fun(f)
Definitions occuring in definition :
equiv-fun: equiv-fun(f),
fiber-comp: fiber-comp(X;T;A;w;a;cT;cA),
equiv-term: equiv f [phi ⊢→ (t, c)] a
FDL editor aliases :
equiv_term
Latex:
equiv f [phi \mvdash{}\mrightarrow{} (t,c)] a == equiv f [phi \mvdash{}\mrightarrow{} (t, c)] a
Date html generated:
2016_05_19-AM-11_11_58
Last ObjectModification:
2016_05_02-PM-01_30_12
Theory : cubical!type!theory
Home
Index