|
1097
|
1 Todo
|
|
|
2 ====
|
|
|
3
|
|
|
4 CCCGraph.agda
|
|
|
5 ---
|
|
|
6 CCC generated from Graph (iconmplete) p.55
|
|
|
7
|
|
|
8 cat-graph-univ : {c₁ : Level} → UniversalMapping (Grph {c₁} {c₁}) (CAT {c₁ } {c₁} {c₁}) forgetful.UC
|
|
|
9 ccc-graph-univ : {c₁ : Level} → UniversalMapping (Grph {c₁} {c₁}) (Cart {c₁ } {c₁} {c₁}) forgetful.UX
|
|
|
10
|
|
|
11 Polynominal.agda
|
|
|
12 ---
|
|
|
13 Polynominal Category and functional completeness
|
|
|
14
|
|
|
15 -- an assuption needed in k x phi ≈ k x phi'
|
|
|
16 -- k x (i x) ≈ k x ii
|
|
|
17 postulate
|
|
|
18 xf : {a b c : Obj A } → ( x : Hom A １ a ) → {z : Hom A b c } → ( y : φ {a} x z ) → ( x ∙ π' ) ≈ π
|
|
|
19
|
|
|
20 define Polynominal Category as a graph generated one
|
|
|
21 define Polynominal Category as a coMonad
|
|
|
22
|
|
|
23 Topos
|
|
|
24 ---
|
|
|
25
|
|
|
26 ToposEx.agda Topos Exercise (incomplete) p.141
|
|
|
27 ToposIL.agda Topos Internal Language (incomplete) p.143
|
|
|
28 ToposSub.agda Topos Subobject classifier (incomplete)
|
|
|
29
|
|
|
30 equalizer.agda
|
|
|
31 ---
|
|
|
32 Equalizer example p.21
|
|
|
33
|
|
|
34 Bourroni equations gives an Equalizer
|
|
|
35
|
|
|
36 postulate
|
|
|
37 uniqueness1 : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → {k' : Hom A d c } →
|
|
|
38 A [ A [ (α bur f g ) o k' ] ≈ h ] → A [ k1 {d} h eq ≈ k' ]
|
|
|
39
|
|
|
40 system-f.agda
|
|
|
41 ---
|
|
|
42
|
|
|
43 very incomplete, because this is a meta circular interpreter of Agda
|
|
|
44
|
|
|
45 yoneda.agda
|
|
|
46 ---
|
|
|
47 Yoneda Functor p.11
|
|
|
48
|
|
|
49 ylem0 : {a b : Obj A } → Hom A a a ≡ Hom A a b → a ≡ b
|
|
|
50
|
