---

Step * 2 1 1 of Lemma functor-is-isomorphism


1. [A] : SmallCategory
2. [B] : SmallCategory
3. f : Functor(A;B)@i
4. Bij(cat-ob(A);cat-ob(B);ob(f))
5. ∀x,y:cat-ob(A).  Bij(cat-arrow(A) x y;cat-arrow(B) (f x) (f y);f x y)
6. g : cat-ob(B) ⟶ cat-ob(A)
7. ∀b:cat-ob(B). ((f (g b)) = b ∈ cat-ob(B))
8. ∀a:cat-ob(A). ((g (f a)) = a ∈ cat-ob(A))
⊢ ∃g:Functor(B;A). ((functor-comp(f;g) = 1 ∈ Functor(A;A)) ∧ (functor-comp(g;f) = 1 ∈ Functor(B;B)))
BY
{ (Assert ∀x,y:cat-ob(B).  Bij(cat-arrow(A) (g x) (g y);cat-arrow(B) x y;f (g x) (g y)) BY
         (Intros THEN (InstHyp [⌜g x⌝;⌜g y⌝] 5⋅ THENA Auto) THEN NthHypEq (-1) THEN RepeatFor 2 (EqCDA) THEN Auto)) }

1
1. [A] : SmallCategory
2. [B] : SmallCategory
3. f : Functor(A;B)@i
4. Bij(cat-ob(A);cat-ob(B);ob(f))
5. ∀x,y:cat-ob(A).  Bij(cat-arrow(A) x y;cat-arrow(B) (f x) (f y);f x y)
6. g : cat-ob(B) ⟶ cat-ob(A)
7. ∀b:cat-ob(B). ((f (g b)) = b ∈ cat-ob(B))
8. ∀a:cat-ob(A). ((g (f a)) = a ∈ cat-ob(A))
9. ∀x,y:cat-ob(B).  Bij(cat-arrow(A) (g x) (g y);cat-arrow(B) x y;f (g x) (g y))
⊢ ∃g:Functor(B;A). ((functor-comp(f;g) = 1 ∈ Functor(A;A)) ∧ (functor-comp(g;f) = 1 ∈ Functor(B;B)))

---

Latex:

---

Latex:

1.  [A]  :  SmallCategory
2.  [B]  :  SmallCategory
3.  f  :  Functor(A;B)@i
4.  Bij(cat-ob(A);cat-ob(B);ob(f))
5.  \mforall{}x,y:cat-ob(A).    Bij(cat-arrow(A)  x  y;cat-arrow(B)  (f  x)  (f  y);f  x  y)
6.  g  :  cat-ob(B)  {}\mrightarrow{}  cat-ob(A)
7.  \mforall{}b:cat-ob(B).  ((f  (g  b))  =  b)
8.  \mforall{}a:cat-ob(A).  ((g  (f  a))  =  a)
\mvdash{}  \mexists{}g:Functor(B;A).  ((functor-comp(f;g)  =  1)  \mwedge{}  (functor-comp(g;f)  =  1))


By

---

Latex:
(Assert  \mforall{}x,y:cat-ob(B).    Bij(cat-arrow(A)  (g  x)  (g  y);cat-arrow(B)  x  y;f  (g  x)  (g  y))  BY
              (Intros
                THEN  (InstHyp  [\mkleeneopen{}g  x\mkleeneclose{};\mkleeneopen{}g  y\mkleeneclose{}]  5\mcdot{}  THENA  Auto)
                THEN  NthHypEq  (-1)
                THEN  RepeatFor  2  (EqCDA)
                THEN  Auto))

---

Home Index