Nuprl Lemma : nh-comp-assoc
∀I,J,K,H:fset(ℕ). ∀f:I ⟶ J. ∀g:J ⟶ K. ∀h:K ⟶ H. (h ⋅ g ⋅ f = h ⋅ g ⋅ f ∈ I ⟶ H)
Proof
Definitions occuring in Statement :
nh-comp: g ⋅ f,
names-hom: I ⟶ J,
fset: fset(T),
nat: ℕ,
all: ∀x:A. B[x],
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
names-hom: I ⟶ J,
dM: dM(I),
nh-comp: g ⋅ f,
uall: ∀[x:A]. B[x],
member: t ∈ T
Lemmas referenced :
dma-lift-compose-assoc,
names_wf,
names-deq_wf,
names-hom_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
sqequalHypSubstitution,
lemma_by_obid,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
because_Cache
Latex:
\mforall{}I,J,K,H:fset(\mBbbN{}). \mforall{}f:I {}\mrightarrow{} J. \mforall{}g:J {}\mrightarrow{} K. \mforall{}h:K {}\mrightarrow{} H. (h \mcdot{} g \mcdot{} f = h \mcdot{} g \mcdot{} f)
Date html generated:
2016_05_18-AM-11_59_42
Last ObjectModification:
2015_12_28-PM-03_06_59
Theory : cubical!type!theory
Home
Index