---

Step * 1 of Lemma psdcff-inj-bijection


1. [C] : SmallCategory
2. [A] : Type
3. [B] : Type
4. [X] : ps_context{j:l}(C)
5. [I] : cat-ob(C)
6. [a] : X(I)
⊢ Surj(presheaf-fun-family(C; X; discr(A); discr(B); I; a);A ⟶ B;λw.psdcff-inj(I;w))
BY
{ ((D 0 THENA Auto) THEN D 0 With ⌜λJ,f. b⌝  THEN Auto) }

1
.....wf..... 
1. C : SmallCategory
2. A : Type
3. B : Type
4. X : ps_context{j:l}(C)
5. I : cat-ob(C)
6. a : X(I)
7. b : A ⟶ B
⊢ λJ,f. b ∈ presheaf-fun-family(C; X; discr(A); discr(B); I; a)

---

Latex:

---

Latex:

1.  [C]  :  SmallCategory
2.  [A]  :  Type
3.  [B]  :  Type
4.  [X]  :  ps\_context\{j:l\}(C)
5.  [I]  :  cat-ob(C)
6.  [a]  :  X(I)
\mvdash{}  Surj(presheaf-fun-family(C;  X;  discr(A);  discr(B);  I;  a);A  {}\mrightarrow{}  B;\mlambda{}w.psdcff-inj(I;w))


By

---

Latex:
((D  0  THENA  Auto)  THEN  D  0  With  \mkleeneopen{}\mlambda{}J,f.  b\mkleeneclose{}    THEN  Auto)

---

Home Index