Step
*
2
of Lemma
presheaf-type-iso_wf
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. F : (I:cat-ob(C) × X(I)) ⟶ 𝕌'
4. x1 : x:(I:cat-ob(C) × X(I))
⟶ y:(I:cat-ob(C) × X(I))
⟶ let A,a = y
in let B,b = x
in {f:cat-arrow(C) A B| f(b) = a ∈ (X A)}
⟶ (F x)
⟶ (F y)
5. ∀x:I:cat-ob(C) × X(I). ((x1 x x (cat-id(C) (fst(x)))) = (λx.x) ∈ ((F x) ⟶ (F x)))
6. ∀x,y,z:I:cat-ob(C) × X(I). ∀f:let A,a = y
in let B,b = x
in {f:cat-arrow(C) A B| f(b) = a ∈ (X A)} . ∀g:let A,a = z
in let B,b = y
in {f:cat-arrow(C) A B|
f(b) = a ∈ (X A)} .
((x1 x z (cat-comp(C) (fst(z)) (fst(y)) (fst(x)) g f)) = ((x1 y z g) o (x1 x y f)) ∈ ((F x) ⟶ (F z)))
7. I : cat-ob(C)
8. J : cat-ob(C)
9. K : cat-ob(C)
10. f : cat-arrow(C) J I
11. g : cat-arrow(C) K J
12. a : X(I)
13. u : F <I, a>
⊢ (x1 <I, a> <K, cat-comp(C) K J I g f(a)> (cat-comp(C) K J I g f) u)
= (x1 <J, f(a)> <K, g(f(a))> g (x1 <I, a> <J, f(a)> f u))
∈ (F <K, cat-comp(C) K J I g f(a)>)
BY
{ ((InstHyp [⌜<I, a>⌝;⌜<J, f(a)>⌝;⌜<K, cat-comp(C) K J I g f(a)>⌝] 6⋅ THENA Auto)
THEN Reduce -1
THEN (InstHyp [⌜f⌝] (-1)⋅ THENA (Fold `I_set` 0 THEN Auto))
THEN (InstHyp [⌜g⌝] (-1)⋅ THENA (Fold `I_set` 0 THEN Auto))
THEN (Assert C ∈ SmallCategory BY
Auto)
THEN DCat 1
THEN RepeatFor 2 (DVar `X')
THEN All (RepUR ``type-cat op-cat cat-ob cat-arrow cat-comp functor-arrow compose``)) }
1
1. Cob : Type
2. Carrow : Cob ⟶ Cob ⟶ Type
3. Cid : x:Cob ⟶ (Carrow x x)
4. Ccomp : x:Cob ⟶ y:Cob ⟶ z:Cob ⟶ (Carrow x y) ⟶ (Carrow y z) ⟶ (Carrow x z)
5. ∀x,y:Cob. ∀f:Carrow x y.
(((Ccomp x x y (Cid x) f) = f ∈ (Carrow x y)) ∧ ((Ccomp x y y f (Cid y)) = f ∈ (Carrow x y)))
6. ∀x,y,z,w:Cob. ∀f:Carrow x y. ∀g:Carrow y z. ∀h:Carrow z w.
((Ccomp x z w (Ccomp x y z f g) h) = (Ccomp x y w f (Ccomp y z w g h)) ∈ (Carrow x w))
7. F1 : Cob ⟶ 𝕌{j'}
8. X1 : x:Cob ⟶ y:Cob ⟶ (Carrow y x) ⟶ (F1 x) ⟶ (F1 y)
9. (∀x:Cob. ((X1 x x (Cid x)) = (λx.x) ∈ ((F1 x) ⟶ (F1 x))))
∧ (∀x,y,z:Cob. ∀f:Carrow y x. ∀g:Carrow z y.
((X1 x z (Ccomp z y x g f)) = (λx@0.(X1 y z g (X1 x y f x@0))) ∈ ((F1 x) ⟶ (F1 z))))
10. F : (I:Cob × (F1 I)) ⟶ 𝕌'
11. x1 : x:(I:Cob × (F1 I))
⟶ y:(I:Cob × (F1 I))
⟶ let A,a = y
in let B,b = x
in {f:Carrow A B| (X1 B A f b) = a ∈ (F1 A)}
⟶ (F x)
⟶ (F y)
12. ∀x:I:Cob × (F1 I). ((x1 x x (Cid (fst(x)))) = (λx.x) ∈ ((F x) ⟶ (F x)))
13. ∀x,y,z:I:Cob × (F1 I). ∀f:let A,a = y
in let B,b = x
in {f:Carrow A B| (X1 B A f b) = a ∈ (F1 A)} . ∀g:let A,a = z
in let B,b = y
in {f:Carrow A B|
(X1 B A f b) = a ∈ (F1 A)} .
((x1 x z (Ccomp (fst(z)) (fst(y)) (fst(x)) g f)) = (λx@0.(x1 y z g (x1 x y f x@0))) ∈ ((F x) ⟶ (F z)))
14. I : Cob
15. J : Cob
16. K : Cob
17. f : Carrow J I
18. g : Carrow K J
19. a : <F1, X1>(I)
20. u : F <I, a>
21. ∀f@0:{f@0:Carrow J I| (X1 I J f@0 a) = (X1 I J f a) ∈ (F1 J)} . ∀g@0:{f@0:Carrow K J|
(X1 J K f@0 (X1 I J f a))
= (X1 I K (Ccomp K J I g f) a)
∈ (F1 K)} .
((x1 <I, a> <K, X1 I K (Ccomp K J I g f) a> (Ccomp K J I g@0 f@0))
= (λx.(x1 <J, X1 I J f a> <K, X1 I K (Ccomp K J I g f) a> g@0 (x1 <I, a> <J, X1 I J f a> f@0 x)))
∈ ((F <I, a>) ⟶ (F <K, X1 I K (Ccomp K J I g f) a>)))
22. ∀g@0:{f@0:Carrow K J| (X1 J K f@0 (X1 I J f a)) = (X1 I K (Ccomp K J I g f) a) ∈ (F1 K)}
((x1 <I, a> <K, X1 I K (Ccomp K J I g f) a> (Ccomp K J I g@0 f))
= (λx.(x1 <J, X1 I J f a> <K, X1 I K (Ccomp K J I g f) a> g@0 (x1 <I, a> <J, X1 I J f a> f x)))
∈ ((F <I, a>) ⟶ (F <K, X1 I K (Ccomp K J I g f) a>)))
23. (x1 <I, a> <K, X1 I K (Ccomp K J I g f) a> (Ccomp K J I g f))
= (λx.(x1 <J, X1 I J f a> <K, X1 I K (Ccomp K J I g f) a> g (x1 <I, a> <J, X1 I J f a> f x)))
∈ ((F <I, a>) ⟶ (F <K, X1 I K (Ccomp K J I g f) a>))
24. <Cob, Carrow, Cid, Ccomp> ∈ SmallCategory
⊢ (x1 <I, a> <K, X1 I K (Ccomp K J I g f) a> (Ccomp K J I g f) u)
= (x1 <J, X1 I J f a> <K, X1 J K g (X1 I J f a)> g (x1 <I, a> <J, X1 I J f a> f u))
∈ (F <K, X1 I K (Ccomp K J I g f) a>)
Latex:
Latex:
1. C : SmallCategory
2. X : ps\_context\{j:l\}(C)
3. F : (I:cat-ob(C) \mtimes{} X(I)) {}\mrightarrow{} \mBbbU{}'
4. x1 : x:(I:cat-ob(C) \mtimes{} X(I))
{}\mrightarrow{} y:(I:cat-ob(C) \mtimes{} X(I))
{}\mrightarrow{} let A,a = y
in let B,b = x
in \{f:cat-arrow(C) A B| f(b) = a\}
{}\mrightarrow{} (F x)
{}\mrightarrow{} (F y)
5. \mforall{}x:I:cat-ob(C) \mtimes{} X(I). ((x1 x x (cat-id(C) (fst(x)))) = (\mlambda{}x.x))
6. \mforall{}x,y,z:I:cat-ob(C) \mtimes{} X(I). \mforall{}f:let A,a = y
in let B,b = x
in \{f:cat-arrow(C) A B| f(b) = a\} . \mforall{}g:let A,a = z
in let B,b = y
in \{f:cat-arrow(C) A
B|
f(b) = a\} .
((x1 x z (cat-comp(C) (fst(z)) (fst(y)) (fst(x)) g f)) = ((x1 y z g) o (x1 x y f)))
7. I : cat-ob(C)
8. J : cat-ob(C)
9. K : cat-ob(C)
10. f : cat-arrow(C) J I
11. g : cat-arrow(C) K J
12. a : X(I)
13. u : F <I, a>
\mvdash{} (x1 <I, a> <K, cat-comp(C) K J I g f(a)> (cat-comp(C) K J I g f) u) = (x1 <J, f(a)> <K, g(f(a))> g\000C (x1 <I, a> <J, f(a)> f u))
By
Latex:
((InstHyp [\mkleeneopen{}<I, a>\mkleeneclose{};\mkleeneopen{}<J, f(a)>\mkleeneclose{};\mkleeneopen{}<K, cat-comp(C) K J I g f(a)>\mkleeneclose{}] 6\mcdot{} THENA Auto)
THEN Reduce -1
THEN (InstHyp [\mkleeneopen{}f\mkleeneclose{}] (-1)\mcdot{} THENA (Fold `I\_set` 0 THEN Auto))
THEN (InstHyp [\mkleeneopen{}g\mkleeneclose{}] (-1)\mcdot{} THENA (Fold `I\_set` 0 THEN Auto))
THEN (Assert C \mmember{} SmallCategory BY
Auto)
THEN DCat 1
THEN RepeatFor 2 (DVar `X')
THEN All (RepUR ``type-cat op-cat cat-ob cat-arrow cat-comp functor-arrow compose``))
Home
Index