Nuprl Lemma : equiv-bijection_wf
∀[A,B:Type]. ∀[e:{() ⊢ _:Equiv(discr(A);discr(B))}]. (equiv-bijection(e) ∈ A ⟶ B)
Proof
Definitions occuring in Statement :
equiv-bijection: equiv-bijection(e),
cubical-equiv: Equiv(T;A),
discrete-cubical-type: discr(T),
cubical-term: {X ⊢ _:A},
trivial-cube-set: (),
uall: ∀[x:A]. B[x],
member: t ∈ T,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
discrete-cubical-type: discr(T),
cubical-type-at: A(a),
prop: ℙ,
trivial-cube-set: (),
pi1: fst(t),
functor-ob: ob(F),
I_cube: A(I),
unit: Unit,
subtype_rel: A ⊆r B,
equiv-bijection: equiv-bijection(e),
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
cubical-equiv_wf,
cubical-term_wf,
equal-wf-base,
subtype_rel_self,
it_wf,
nat_wf,
empty-fset_wf,
equiv-fun_wf,
discrete-fun_wf,
discrete-cubical-type_wf,
trivial-cube-set_wf,
cubical-term-at_wf
Rules used in proof :
universeEquality,
isect_memberEquality,
equalitySymmetry,
equalityTransitivity,
axiomEquality,
because_Cache,
baseClosed,
intEquality,
applyEquality,
hypothesisEquality,
cumulativity,
functionEquality,
hypothesis,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
sqequalRule,
cut,
introduction,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[A,B:Type]. \mforall{}[e:\{() \mvdash{} \_:Equiv(discr(A);discr(B))\}]. (equiv-bijection(e) \mmember{} A {}\mrightarrow{} B)
Date html generated:
2017_02_21-AM-10_51_50
Last ObjectModification:
2017_02_13-AM-11_54_03
Theory : cubical!type!theory
Home
Index