---

Step * 1 of Lemma cat-isomorphic_inversion


1. C : SmallCategory
2. a : cat-ob(C)
3. b : cat-ob(C)
4. f : cat-arrow(C) a b
5. g : cat-arrow(C) b a
6. fg=1
7. gf=1
⊢ cat-isomorphic(C;b;a)
BY
{ ((D 0 With ⌜g⌝  THEN Auto) THEN D 0 With ⌜f⌝  THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  a  :  cat-ob(C)
3.  b  :  cat-ob(C)
4.  f  :  cat-arrow(C)  a  b
5.  g  :  cat-arrow(C)  b  a
6.  fg=1
7.  gf=1
\mvdash{}  cat-isomorphic(C;b;a)


By

---

Latex:
((D  0  With  \mkleeneopen{}g\mkleeneclose{}    THEN  Auto)  THEN  D  0  With  \mkleeneopen{}f\mkleeneclose{}    THEN  Auto)

---

Home Index