### Nuprl Lemma : prop-truncation-implies

`∀T:Type. ((∀a,b:T.  (a = b ∈ T)) `` ⇃(T) `` T)`

Proof

Definitions occuring in Statement :  quotient: `x,y:A//B[x; y]` all: `∀x:A. B[x]` implies: `P `` Q` true: `True` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  so_apply: `x[s]` so_lambda: `λ2x.t[x]` uimplies: `b supposing a` so_apply: `x[s1;s2]` so_lambda: `λ2x y.t[x; y]` prop: `ℙ` uall: `∀[x:A]. B[x]` guard: `{T}` label: `...\$L... t` and: `P ∧ Q` quotient: `x,y:A//B[x; y]` member: `t ∈ T` implies: `P `` Q` all: `∀x:A. B[x]`
Lemmas referenced :  equal_wf all_wf equiv_rel_true quotient_wf true_wf equal-wf-base
Rules used in proof :  universeEquality independent_isectElimination lambdaEquality cumulativity because_Cache isectElimination extract_by_obid productEquality equalitySymmetry equalityTransitivity dependent_functionElimination hypothesis thin productElimination cut pertypeElimination sqequalRule sqequalHypSubstitution hypothesisEquality pointwiseFunctionalityForEquality introduction rename lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}T:Type.  ((\mforall{}a,b:T.    (a  =  b))  {}\mRightarrow{}  \00D9(T)  {}\mRightarrow{}  T)

Date html generated: 2017_09_29-PM-06_07_26
Last ObjectModification: 2017_09_04-PM-03_51_03

Theory : continuity

Home Index