Step
*
of Lemma
A-face-image_wf
∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[I,K:Cname List]. ∀[f:name-morph(I;K)]. ∀[alpha:X(I)]. ∀[face:A-face(X;A;I;alpha)].
A-face-image(X;A;I;K;f;alpha;face) ∈ A-face(X;A;K;f(alpha)) supposing ↑isname(f (fst(face)))
BY
{ (Intros
THEN Unhide
THEN Unfold `A-face-image` 0
THEN DVar `face'
THEN DVar `f1'
THEN Reduce 0
THEN Unfold `A-face` 0
THEN Reduce (-1)
THEN DVar `x'
THEN (FLemma `assert-isname` [-1] THENA Auto)
THEN (Assert ⌜f ∈ name-morph(I-[x];K-[f x])⌝⋅ THENA (BLemma `name-morph_subtype_remove1` ⋅ THEN Auto))
THEN (Assert ⌜A(f((x:=i)(alpha))) = A((f x:=i)(f(alpha))) ∈ Type⌝⋅
THENA (RWO "cube-set-restriction-comp" 0 THEN Auto)
)
THEN Auto) }
Latex:
Latex:
\mforall{}[X:CubicalSet]. \mforall{}[A:\{X \mvdash{} \_\}]. \mforall{}[I,K:Cname List]. \mforall{}[f:name-morph(I;K)]. \mforall{}[alpha:X(I)].
\mforall{}[face:A-face(X;A;I;alpha)].
A-face-image(X;A;I;K;f;alpha;face) \mmember{} A-face(X;A;K;f(alpha)) supposing \muparrow{}isname(f (fst(face)))
By
Latex:
(Intros
THEN Unhide
THEN Unfold `A-face-image` 0
THEN DVar `face'
THEN DVar `f1'
THEN Reduce 0
THEN Unfold `A-face` 0
THEN Reduce (-1)
THEN DVar `x'
THEN (FLemma `assert-isname` [-1] THENA Auto)
THEN (Assert \mkleeneopen{}f \mmember{} name-morph(I-[x];K-[f x])\mkleeneclose{}\mcdot{}
THENA (BLemma `name-morph\_subtype\_remove1` \mcdot{} THEN Auto)
)
THEN (Assert \mkleeneopen{}A(f((x:=i)(alpha))) = A((f x:=i)(f(alpha)))\mkleeneclose{}\mcdot{}
THENA (RWO "cube-set-restriction-comp" 0 THEN Auto)
)
THEN Auto)
Home
Index