### Nuprl Lemma : half-squash-equality

[Q:Type]. ∀[a,b:⇃(Q)].  (a b ∈ ⇃(Q))

Proof

Definitions occuring in Statement :  quotient: x,y:A//B[x; y] uall: [x:A]. B[x] true: True universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T quotient: x,y:A//B[x; y] and: P ∧ Q all: x:A. B[x] implies:  Q so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] uimplies: supposing a true: True prop:
Lemmas referenced :  quotient-member-eq true_wf equiv_rel_true quotient_wf istype-universe
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut pointwiseFunctionalityForEquality because_Cache sqequalHypSubstitution sqequalRule pertypeElimination productElimination thin equalityTransitivity hypothesis equalitySymmetry Error :inhabitedIsType,  Error :lambdaFormation_alt,  rename extract_by_obid isectElimination hypothesisEquality Error :lambdaEquality_alt,  independent_isectElimination dependent_functionElimination independent_functionElimination natural_numberEquality Error :equalityIsType1,  Error :universeIsType,  Error :productIsType,  Error :equalityIsType4,  Error :isect_memberEquality_alt,  axiomEquality Error :isectIsTypeImplies,  instantiate universeEquality

Latex:
\mforall{}[Q:Type].  \mforall{}[a,b:\00D9(Q)].    (a  =  b)

Date html generated: 2019_06_20-PM-00_32_44
Last ObjectModification: 2018_11_16-AM-11_46_10

Theory : quot_1

Home Index