### Nuprl Lemma : truncation-property

`∀[X,Q:Type].  ∀f:X ⟶ ⇃(Q). ((∀x:X. ((|f| |x|) = (f x) ∈ ⇃(Q))) ∧ (∀g:⇃(X) ⟶ ⇃(Q). (g = |f| ∈ (⇃(X) ⟶ ⇃(Q)))))`

Proof

Definitions occuring in Statement :  truncate-map: `|f|` truncate: `|x|` quotient: `x,y:A//B[x; y]` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` and: `P ∧ Q` true: `True` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` and: `P ∧ Q` cand: `A c∧ B` truncate: `|x|` truncate-map: `|f|` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` uimplies: `b supposing a`
Lemmas referenced :  quotient_wf true_wf equiv_rel_true istype-universe half-squash-equality truncate-map_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut Error :lambdaFormation_alt,  sqequalRule applyEquality hypothesisEquality hypothesis Error :universeIsType,  independent_pairFormation Error :functionIsType,  extract_by_obid sqequalHypSubstitution isectElimination thin Error :lambdaEquality_alt,  Error :inhabitedIsType,  independent_isectElimination dependent_functionElimination productElimination independent_pairEquality axiomEquality Error :functionIsTypeImplies,  Error :isect_memberEquality_alt,  Error :isectIsTypeImplies,  instantiate universeEquality functionExtensionality

Latex:
\mforall{}[X,Q:Type].    \mforall{}f:X  {}\mrightarrow{}  \00D9(Q).  ((\mforall{}x:X.  ((|f|  |x|)  =  (f  x)))  \mwedge{}  (\mforall{}g:\00D9(X)  {}\mrightarrow{}  \00D9(Q).  (g  =  |f|)))

Date html generated: 2019_06_20-PM-00_32_52
Last ObjectModification: 2018_11_16-AM-11_48_53

Theory : quot_1

Home Index