Nuprl Lemma : groupoid_wf

Groupoid ∈ 𝕌'


Proof




Definitions occuring in Statement :  groupoid: Groupoid member: t ∈ T universe: Type
Definitions unfolded in proof :  groupoid: Groupoid member: t ∈ T uall: [x:A]. B[x] subtype_rel: A ⊆B so_lambda: λ2x.t[x] prop: and: P ∧ Q so_apply: x[s]
Lemmas referenced :  small-category_wf cat-ob_wf cat-arrow_wf all_wf equal_wf cat-comp_wf cat-id_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep productEquality cut introduction extract_by_obid hypothesis setEquality functionEquality sqequalHypSubstitution isectElimination thin hypothesisEquality applyEquality lambdaEquality cumulativity universeEquality because_Cache functionExtensionality

Latex:
Groupoid  \mmember{}  \mBbbU{}'



Date html generated: 2020_05_20-AM-07_55_04
Last ObjectModification: 2017_07_28-AM-09_20_07

Theory : small!categories


Home Index