---

Step * of Lemma functor-is-isomorphism

∀[A,B:SmallCategory].
  ∀f:Functor(A;B)
    (cat-isomorphism(Cat;A;B;f)
    ⇐⇒ Bij(cat-ob(A);cat-ob(B);ob(f))
        ∧ (∀x,y:cat-ob(A).  Bij(cat-arrow(A) x y;cat-arrow(B) (ob(f) x) (ob(f) y);arrow(f) x y)))
BY
{ ((RepeatFor 3 (Intro) THEN RepUR ``cat-isomorphism cat-cat cat-inverse`` 0) THEN RepeatFor 2 ((D 0 THENA Auto))) }

1
1. [A] : SmallCategory
2. [B] : SmallCategory
3. f : Functor(A;B)
4. ∃g:Functor(B;A). ((functor-comp(f;g) = 1 ∈ Functor(A;A)) ∧ (functor-comp(g;f) = 1 ∈ Functor(B;B)))
⊢ Bij(cat-ob(A);cat-ob(B);ob(f))
∧ (∀x,y:cat-ob(A).  Bij(cat-arrow(A) x y;cat-arrow(B) (ob(f) x) (ob(f) y);arrow(f) x y))

2
1. [A] : SmallCategory
2. [B] : SmallCategory
3. f : Functor(A;B)
4. Bij(cat-ob(A);cat-ob(B);ob(f))
∧ (∀x,y:cat-ob(A).  Bij(cat-arrow(A) x y;cat-arrow(B) (ob(f) x) (ob(f) y);arrow(f) x y))
⊢ ∃g:Functor(B;A). ((functor-comp(f;g) = 1 ∈ Functor(A;A)) ∧ (functor-comp(g;f) = 1 ∈ Functor(B;B)))

---

Latex:

---

Latex:
\mforall{}[A,B:SmallCategory].
    \mforall{}f:Functor(A;B)
        (cat-isomorphism(Cat;A;B;f)
        \mLeftarrow{}{}\mRightarrow{}  Bij(cat-ob(A);cat-ob(B);ob(f))
                \mwedge{}  (\mforall{}x,y:cat-ob(A).    Bij(cat-arrow(A)  x  y;cat-arrow(B)  (ob(f)  x)  (ob(f)  y);arrow(f)  x  y)))


By

---

Latex:
((RepeatFor  3  (Intro)  THEN  RepUR  ``cat-isomorphism  cat-cat  cat-inverse``  0)
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  )

---

Home Index