Nuprl Lemma : free-group-functor_wf
FreeGp ∈ Functor(TypeCat;Group)
Proof
Definitions occuring in Statement :
free-group-functor: FreeGp,
group-cat: Group,
type-cat: TypeCat,
cat-functor: Functor(C1;C2),
member: t ∈ T
Definitions unfolded in proof :
free-group-functor: FreeGp,
member: t ∈ T,
uall: ∀[x:A]. B[x],
so_lambda: λ2x.t[x],
type-cat: TypeCat,
all: ∀x:A. B[x],
top: Top,
group-cat: Group,
mk-cat: mk-cat,
so_apply: x[s],
so_lambda: so_lambda(x,y,z.t[x; y; z]),
so_apply: x[s1;s2;s3],
uimplies: b supposing a,
compose: f o g,
subtype_rel: A ⊆r B,
free-group: free-group(X),
grp_car: |g|,
pi1: fst(t),
grp: Group{i},
mon: Mon,
implies: P ⇒ Q,
monoid_hom: MonHom(M1,M2),
prop: ℙ,
free-letter: free-letter(x),
fg-lift: fg-lift(G;f),
fg-hom: fg-hom(G;f;w),
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
grp_op: *,
pi2: snd(t),
grp_inv: ~,
grp_id: e,
infix_ap: x f y,
free-0: 0,
free-append: w + w',
free-word-inv: free-word-inv(w),
append: as @ bs,
list_accum: list_accum,
cons: [a / b],
nil: [],
it: ⋅,
list_ind: list_ind,
monoid_hom_p: IsMonHom{M1,M2}(f),
and: P ∧ Q,
fun_thru_2op: FunThru2op(A;B;opa;opb;f)
Lemmas referenced :
mk-functor_wf,
type-cat_wf,
group-cat_wf,
cat_ob_pair_lemma,
free-group_wf,
cat-ob_wf,
cat_arrow_triple_lemma,
cat-arrow_wf,
cat_comp_tuple_lemma,
cat_id_tuple_lemma,
free-letter_wf,
free-word_wf,
grp_car_wf,
grp_wf,
fg-lift_wf,
monoid_hom_wf,
all_wf,
equal_wf,
free-group-generators,
compose_wf_for_mon_hom,
list_accum_cons_lemma,
list_accum_nil_lemma,
list_ind_nil_lemma,
reverse-cons,
reverse_nil_lemma,
free-append_wf,
free-0_wf,
monoid_hom_p_wf
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
cut,
instantiate,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesis,
lambdaEquality,
dependent_functionElimination,
isect_memberEquality,
voidElimination,
voidEquality,
cumulativity,
hypothesisEquality,
because_Cache,
applyEquality,
independent_isectElimination,
lambdaFormation,
functionExtensionality,
functionEquality,
setElimination,
rename,
setEquality,
equalityTransitivity,
equalitySymmetry,
independent_functionElimination,
dependent_set_memberEquality,
independent_pairFormation,
isect_memberFormation,
axiomEquality
Latex:
FreeGp \mmember{} Functor(TypeCat;Group)
Date html generated:
2017_10_05-AM-00_51_39
Last ObjectModification:
2017_07_28-AM-09_20_32
Theory : small!categories
Home
Index