### Nuprl Lemma : groupoid-nerve-functor-flip

`∀[G:Groupoid]. ∀[I:Cname List]. ∀[u:nameset(I)]. ∀[K:Cname List]. ∀[f:name-morph(I;K)]. ∀[f1:name-morph(K;[])].`
`  ∀x1:nameset(I)`
`    ∀[F:Functor(poset-cat(I-[x1]);cat(G))]`
`      (F (f o f1) flip((f o f1);u) (λx.Ax))`
`      = (f(F) f1 flip(f1;f u) (λx.Ax))`
`      ∈ (cat-arrow(cat(G)) (F (f o f1)) (F (f o flip(f1;f u)))) `
`      supposing (↑isname(f u)) ∧ ((f1 (f u)) = 0 ∈ ℕ2)`

Proof

Definitions occuring in Statement :  cubical-nerve: `cubical-nerve(X)` poset-cat: `poset-cat(J)` cube-set-restriction: `f(s)` name-morph-flip: `flip(f;y)` name-comp: `(f o g)` name-morph: `name-morph(I;J)` isname: `isname(z)` nameset: `nameset(L)` cname_deq: `CnameDeq` coordinate_name: `Cname` groupoid-cat: `cat(G)` groupoid: `Groupoid` functor-arrow: `arrow(F)` functor-ob: `ob(F)` cat-functor: `Functor(C1;C2)` cat-arrow: `cat-arrow(C)` list-diff: `as-bs` cons: `[a / b]` nil: `[]` list: `T List` int_seg: `{i..j-}` assert: `↑b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` and: `P ∧ Q` apply: `f a` lambda: `λx.A[x]` natural_number: `\$n` equal: `s = t ∈ T` axiom: `Ax`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` uimplies: `b supposing a` member: `t ∈ T` nameset: `nameset(L)` and: `P ∧ Q` name-morph: `name-morph(I;J)` uiff: `uiff(P;Q)` cubical-nerve: `cubical-nerve(X)` cube-set-restriction: `f(s)` pi2: `snd(t)` poset-functor: `poset-functor(J;K;f)` functor-comp: `functor-comp(F;G)` functor-arrow: `arrow(F)` functor-ob: `ob(F)` top: `Top` squash: `↓T` prop: `ℙ` subtype_rel: `A ⊆r B` true: `True` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2;s3]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` poset-cat: `poset-cat(J)` cat-ob: `cat-ob(C)` pi1: `fst(t)` name-comp: `(f o g)` compose: `f o g` uext: `uext(g)` ifthenelse: `if b then t else f fi ` btrue: `tt` int_seg: `{i..j-}` coordinate_name: `Cname` int_upper: `{i...}` lelt: `i ≤ j < k` decidable: `Dec(P)` or: `P ∨ Q` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False`
Lemmas referenced :  cat-functor_wf poset-cat_wf list-diff_wf coordinate_name_wf cname_deq_wf cons_wf nil_wf groupoid-cat_wf name-morph_wf nameset_wf list_wf groupoid_wf assert-isname ob_pair_lemma istype-void arrow_pair_lemma name-morph-ext name-comp_wf name-morph-flip_wf equal_wf squash_wf true_wf istype-universe extd-nameset_wf name-comp-flip subtype_rel_self iff_weakening_equal arrow_mk_functor_lemma functor-arrow_wf name-morph_subtype nameset_subtype list-diff-subset member-poset-cat-arrow poset-cat-arrow-flip cat-ob_wf isname-name int_seg_properties decidable__equal_int full-omega-unsat intformand_wf intformnot_wf intformeq_wf itermVar_wf itermConstant_wf istype-int int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_wf poset-cat-arrow_subtype subtype_rel_wf cat-arrow_wf istype-assert isname_wf int_seg_wf extd-nameset-nil
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaFormation_alt universeIsType cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis hypothesisEquality setElimination rename because_Cache productElimination applyEquality independent_isectElimination sqequalRule dependent_functionElimination isect_memberEquality_alt voidElimination equalitySymmetry lambdaEquality_alt imageElimination equalityTransitivity inhabitedIsType instantiate universeEquality natural_numberEquality imageMemberEquality baseClosed independent_functionElimination applyLambdaEquality unionElimination approximateComputation dependent_pairFormation_alt int_eqEquality independent_pairFormation hyp_replacement productIsType equalityIsType3

Latex:
\mforall{}[G:Groupoid].  \mforall{}[I:Cname  List].  \mforall{}[u:nameset(I)].  \mforall{}[K:Cname  List].  \mforall{}[f:name-morph(I;K)].
\mforall{}[f1:name-morph(K;[])].
\mforall{}x1:nameset(I)
\mforall{}[F:Functor(poset-cat(I-[x1]);cat(G))]
(F  (f  o  f1)  flip((f  o  f1);u)  (\mlambda{}x.Ax))  =  (f(F)  f1  flip(f1;f  u)  (\mlambda{}x.Ax))
supposing  (\muparrow{}isname(f  u))  \mwedge{}  ((f1  (f  u))  =  0)

Date html generated: 2019_11_05-PM-00_39_25
Last ObjectModification: 2018_11_10-PM-03_22_44

Theory : cubical!sets

Home Index