---

Step * of Lemma pscm-ap-id-type

No Annotations
∀[C:SmallCategory]. ∀[Gamma:ps_context{j:l}(C)]. ∀[A:{Gamma ⊢ _}].  ((A)1(Gamma) = A ∈ {Gamma ⊢ _})
BY
{ (Auto THEN Symmetry THEN D -1 THEN EqTypeCD THEN Try (Trivial) THEN Auto) }

1
1. C : SmallCategory
2. Gamma : ps_context{j:l}(C)
3. A : A:I:cat-ob(C) ⟶ Gamma(I) ⟶ Type × (I:cat-ob(C)
                                           ⟶ J:cat-ob(C)
                                           ⟶ f:(cat-arrow(C) J I)
                                           ⟶ a:Gamma(I)
                                           ⟶ (A I a)
                                           ⟶ (A J f(a)))
4. let A,F = A 
   in (∀I:cat-ob(C). ∀a:Gamma(I). ∀u:A I a.  ((F I I (cat-id(C) I) a u) = u ∈ (A I a)))
      ∧ (∀I,J,K:cat-ob(C). ∀f:cat-arrow(C) J I. ∀g:cat-arrow(C) K J. ∀a:Gamma(I). ∀u:A I a.
           ((F I K (cat-comp(C) K J I g f) a u) = (F J K g f(a) (F I J f a u)) ∈ (A K cat-comp(C) K J I g f(a))))
⊢ A
= (A)1(Gamma)
∈ (A:I:cat-ob(C) ⟶ Gamma(I) ⟶ Type × (I:cat-ob(C)
                                       ⟶ J:cat-ob(C)
                                       ⟶ f:(cat-arrow(C) J I)
                                       ⟶ a:Gamma(I)
                                       ⟶ (A I a)
                                       ⟶ (A J f(a))))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[Gamma:ps\_context\{j:l\}(C)].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].    ((A)1(Gamma)  =  A)


By

---

Latex:
(Auto  THEN  Symmetry  THEN  D  -1  THEN  EqTypeCD  THEN  Try  (Trivial)  THEN  Auto)

---

Home Index