### Nuprl Lemma : comp_assoc

`∀[A,B,C,D:Type]. ∀[f:A ⟶ B]. ∀[g:B ⟶ C]. ∀[h:C ⟶ D].  ((h o (g o f)) = ((h o g) o f) ∈ (A ⟶ D))`

Proof

Definitions occuring in Statement :  compose: `f o g` uall: `∀[x:A]. B[x]` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  compose: `f o g` member: `t ∈ T` uall: `∀[x:A]. B[x]`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity sqequalRule lambdaEquality applyEquality hypothesisEquality Error :functionIsType,  Error :universeIsType,  functionEquality because_Cache Error :inhabitedIsType,  universeEquality Error :isect_memberFormation_alt,  introduction cut hypothesis sqequalHypSubstitution isect_memberEquality isectElimination thin axiomEquality

Latex:
\mforall{}[A,B,C,D:Type].  \mforall{}[f:A  {}\mrightarrow{}  B].  \mforall{}[g:B  {}\mrightarrow{}  C].  \mforall{}[h:C  {}\mrightarrow{}  D].    ((h  o  (g  o  f))  =  ((h  o  g)  o  f))

Date html generated: 2019_06_20-PM-00_26_16
Last ObjectModification: 2018_09_26-AM-11_50_35

Theory : fun_1

Home Index