Nuprl Lemma : equiv-fun-cubical-id-equiv
∀[G,A:Top]. (equiv-fun(IdEquiv(G;A)) ~ cubical-id-fun(G))
Proof
Definitions occuring in Statement :
cubical-id-equiv: IdEquiv(X;T),
equiv-fun: equiv-fun(f),
cubical-id-fun: cubical-id-fun(X),
uall: ∀[x:A]. B[x],
top: Top,
sqequal: s ~ t
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
cubical-id-fun: cubical-id-fun(X),
cubical-id-equiv: IdEquiv(X;T),
equiv-fun: equiv-fun(f),
cubical-lam: cubical-lam(X;b),
cubical-lambda: (λb),
cubical-id-is-equiv: cubical-id-is-equiv(X;T),
equiv-witness: equiv-witness(f;cntr),
cubical-fst: p.1,
cubical-pair: cubical-pair(u;v),
pi1: fst(t),
member: t ∈ T
Lemmas referenced :
top_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
sqequalRule,
cut,
introduction,
extract_by_obid,
hypothesis
Latex:
\mforall{}[G,A:Top]. (equiv-fun(IdEquiv(G;A)) \msim{} cubical-id-fun(G))
Date html generated:
2017_01_10-AM-09_06_37
Last ObjectModification:
2017_01_04-PM-00_24_03
Theory : cubical!type!theory
Home
Index