Nuprl Lemma : comb_for_compose_wf

λA,B,C,f,g,z. (f g) ∈ A:Type ⟶ B:Type ⟶ C:Type ⟶ f:(B ⟶ C) ⟶ g:(A ⟶ B) ⟶ (↓True) ⟶ A ⟶ C


Proof




Definitions occuring in Statement :  compose: g squash: T true: True member: t ∈ T lambda: λx.A[x] function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  member: t ∈ T squash: T uall: [x:A]. B[x] prop:
Lemmas referenced :  compose_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 :functionIsType,  Error :inhabitedIsType,  universeEquality

Latex:
\mlambda{}A,B,C,f,g,z.  (f  o  g)  \mmember{}  A:Type  {}\mrightarrow{}  B:Type  {}\mrightarrow{}  C:Type  {}\mrightarrow{}  f:(B  {}\mrightarrow{}  C)  {}\mrightarrow{}  g:(A  {}\mrightarrow{}  B)  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  A  {}\mrightarrow{}  C



Date html generated: 2019_06_20-PM-00_26_16
Last ObjectModification: 2018_09_28-PM-11_40_36

Theory : fun_1


Home Index