### Nuprl Lemma : comb_for_pi1_wf

`λA,B,p,z. (fst(p)) ∈ A:Type ⟶ B:(A ⟶ Type) ⟶ p:(a:A × B[a]) ⟶ (↓True) ⟶ A`

Proof

Definitions occuring in Statement :  so_apply: `x[s]` pi1: `fst(t)` squash: `↓T` true: `True` member: `t ∈ T` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` product: `x:A × B[x]` universe: `Type`
Definitions unfolded in proof :  member: `t ∈ T` squash: `↓T` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]`
Lemmas referenced :  pi1_wf squash_wf true_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaEquality_alt,  sqequalHypSubstitution imageElimination cut introduction extract_by_obid isectElimination thin hypothesisEquality equalityTransitivity hypothesis equalitySymmetry Error :universeIsType,  Error :productIsType,  applyEquality Error :functionIsType,  Error :inhabitedIsType,  universeEquality

Latex:
\mlambda{}A,B,p,z.  (fst(p))  \mmember{}  A:Type  {}\mrightarrow{}  B:(A  {}\mrightarrow{}  Type)  {}\mrightarrow{}  p:(a:A  \mtimes{}  B[a])  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  A

Date html generated: 2019_06_20-AM-11_18_19
Last ObjectModification: 2018_09_27-PM-05_34_15

Theory : core_2

Home Index