Step
*
of Lemma
presheaf-type-equal
No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:A:I:cat-ob(C) ⟶ X(I) ⟶ Type × (I:cat-ob(C)
⟶ J:cat-ob(C)
⟶ f:(cat-arrow(C) J I)
⟶ a:X(I)
⟶ (A I a)
⟶ (A J f(a)))].
A = B ∈ {X ⊢ _}
supposing A
= B
∈ (A:I:cat-ob(C) ⟶ X(I) ⟶ Type × (I:cat-ob(C)
⟶ J:cat-ob(C)
⟶ f:(cat-arrow(C) J I)
⟶ a:X(I)
⟶ (A I a)
⟶ (A J f(a))))
BY
{ (Auto THEN DVar `A' THEN EqTypeCD THEN Auto) }
Latex:
Latex:
No Annotations
\mforall{}[C:SmallCategory]. \mforall{}[X:ps\_context\{j:l\}(C)]. \mforall{}[A:\{X \mvdash{} \_\}].
\mforall{}[B:A:I:cat-ob(C) {}\mrightarrow{} X(I) {}\mrightarrow{} Type \mtimes{} (I:cat-ob(C)
{}\mrightarrow{} J:cat-ob(C)
{}\mrightarrow{} f:(cat-arrow(C) J I)
{}\mrightarrow{} a:X(I)
{}\mrightarrow{} (A I a)
{}\mrightarrow{} (A J f(a)))].
A = B supposing A = B
By
Latex:
(Auto THEN DVar `A' THEN EqTypeCD THEN Auto)
Home
Index