---

Step * 1 of Lemma cat-isomorphic_inversion


1. C : SmallCategory@i'
2. a : cat-ob(C)@i
3. b : cat-ob(C)@i
4. f : cat-arrow(C) a b@i
5. g : cat-arrow(C) b a@i
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@i'
2.  a  :  cat-ob(C)@i
3.  b  :  cat-ob(C)@i
4.  f  :  cat-arrow(C)  a  b@i
5.  g  :  cat-arrow(C)  b  a@i
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