Mercurial > hg > Members > kono > Proof > category

annotate src/CCCGraph.agda @ 995:1d365952dde4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 06 Mar 2021 23:02:33 +0900
parents 485bc7560a75
children d89f2c8cf0f4
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
949
ac53803b3b2a reorganization for apkg
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 948
diff changeset
1 module CCCgraph where
ac53803b3b2a reorganization for apkg
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 948
diff changeset
2
779
6b4bd02efd80 CCC start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Level
6b4bd02efd80 CCC start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Category
6b4bd02efd80 CCC start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import HomReasoning
6b4bd02efd80 CCC start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import cat-utility
795
030c5b87ed78 ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 794
diff changeset
7 open import Data.Product renaming (_×_ to _/\_ ) hiding ( <_,_> )
784
f27d966939f8 add CCC hom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 783
diff changeset
8 open import Category.Constructions.Product
949
ac53803b3b2a reorganization for apkg
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 948
diff changeset
9 open import Relation.Binary.PropositionalEquality hiding ( [_] )
817
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 816
diff changeset
10 open import CCC
779
6b4bd02efd80 CCC start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
6b4bd02efd80 CCC start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 open Functor
6b4bd02efd80 CCC start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
6b4bd02efd80 CCC start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 -- ccc-1 : Hom A a 1 ≅ {*}
6b4bd02efd80 CCC start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 -- ccc-2 : Hom A c (a × b) ≅ (Hom A c a ) × ( Hom A c b )
6b4bd02efd80 CCC start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 -- ccc-3 : Hom A a (c ^ b) ≅ Hom A (a × b) c
6b4bd02efd80 CCC start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
790
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
18 open import Category.Sets
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
19
815
bb9fd483f560 simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 814
diff changeset
20 -- Sets is a CCC
bb9fd483f560 simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 814
diff changeset
21
949
ac53803b3b2a reorganization for apkg
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 948
diff changeset
22 import Axiom.Extensionality.Propositional
ac53803b3b2a reorganization for apkg
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 948
diff changeset
23 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂
790
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
24
931
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 930
diff changeset
25 data One {c : Level } : Set c where
817
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 816
diff changeset
26 OneObj : One -- () in Haskell ( or any one object set )
790
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
27
932
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
28 sets : {c : Level } → CCC (Sets {c})
929
1e8ed7dedc03 ... simpler level on CCC Graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 928
diff changeset
29 sets = record {
817
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 816
diff changeset
30 １ = One
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 816
diff changeset
31 ; ○ = λ _ → λ _ → OneObj
795
030c5b87ed78 ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 794
diff changeset
32 ; _∧_ = _∧_
790
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
33 ; <_,_> = <,>
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
34 ; π = π
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
35 ; π' = π'
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
36 ; _<=_ = _<=_
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
37 ; _* = _*
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
38 ; ε = ε
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
39 ; isCCC = isCCC
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
40 } where
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
41 １ : Obj Sets
817
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 816
diff changeset
42 １ = One
790
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
43 ○ : (a : Obj Sets ) → Hom Sets a １
817
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 816
diff changeset
44 ○ a = λ _ → OneObj
795
030c5b87ed78 ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 794
diff changeset
45 _∧_ : Obj Sets → Obj Sets → Obj Sets
030c5b87ed78 ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 794
diff changeset
46 _∧_ a b = a /\ b
030c5b87ed78 ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 794
diff changeset
47 <,> : {a b c : Obj Sets } → Hom Sets c a → Hom Sets c b → Hom Sets c ( a ∧ b)
790
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
48 <,> f g = λ x → ( f x , g x )
795
030c5b87ed78 ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 794
diff changeset
49 π : {a b : Obj Sets } → Hom Sets (a ∧ b) a
790
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
50 π {a} {b} = proj₁
795
030c5b87ed78 ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 794
diff changeset
51 π' : {a b : Obj Sets } → Hom Sets (a ∧ b) b
790
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
52 π' {a} {b} = proj₂
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
53 _<=_ : (a b : Obj Sets ) → Obj Sets
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
54 a <= b = b → a
795
030c5b87ed78 ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 794
diff changeset
55 _* : {a b c : Obj Sets } → Hom Sets (a ∧ b) c → Hom Sets a (c <= b)
790
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
56 f * = λ x → λ y → f ( x , y )
795
030c5b87ed78 ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 794
diff changeset
57 ε : {a b : Obj Sets } → Hom Sets ((a <= b ) ∧ b) a
790
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
58 ε {a} {b} = λ x → ( proj₁ x ) ( proj₂ x )
795
030c5b87ed78 ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 794
diff changeset
59 isCCC : CCC.IsCCC Sets １ ○ _∧_ <,> π π' _<=_ _* ε
790
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
60 isCCC = record {
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
61 e2 = e2
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
62 ; e3a = λ {a} {b} {c} {f} {g} → e3a {a} {b} {c} {f} {g}
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
63 ; e3b = λ {a} {b} {c} {f} {g} → e3b {a} {b} {c} {f} {g}
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
64 ; e3c = e3c
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
65 ; π-cong = π-cong
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
66 ; e4a = e4a
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
67 ; e4b = e4b
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
68 ; *-cong = *-cong
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
69 } where
793
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
70 e2 : {a : Obj Sets} {f : Hom Sets a １} → Sets [ f ≈ ○ a ]
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
71 e2 {a} {f} = extensionality Sets ( λ x → e20 x )
790
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
72 where
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
73 e20 : (x : a ) → f x ≡ ○ a x
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
74 e20 x with f x
817
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 816
diff changeset
75 e20 x | OneObj = refl
790
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
76 e3a : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} →
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
77 Sets [ ( Sets [ π o ( <,> f g) ] ) ≈ f ]
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
78 e3a = refl
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
79 e3b : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} →
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
80 Sets [ Sets [ π' o ( <,> f g ) ] ≈ g ]
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
81 e3b = refl
795
030c5b87ed78 ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 794
diff changeset
82 e3c : {a b c : Obj Sets} {h : Hom Sets c (a ∧ b)} →
790
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
83 Sets [ <,> (Sets [ π o h ]) (Sets [ π' o h ]) ≈ h ]
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
84 e3c = refl
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
85 π-cong : {a b c : Obj Sets} {f f' : Hom Sets c a} {g g' : Hom Sets c b} →
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
86 Sets [ f ≈ f' ] → Sets [ g ≈ g' ] → Sets [ <,> f g ≈ <,> f' g' ]
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
87 π-cong refl refl = refl
795
030c5b87ed78 ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 794
diff changeset
88 e4a : {a b c : Obj Sets} {h : Hom Sets (c ∧ b) a} →
790
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
89 Sets [ Sets [ ε o <,> (Sets [ h * o π ]) π' ] ≈ h ]
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
90 e4a = refl
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
91 e4b : {a b c : Obj Sets} {k : Hom Sets c (a <= b)} →
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
92 Sets [ (Sets [ ε o <,> (Sets [ k o π ]) π' ]) * ≈ k ]
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
93 e4b = refl
795
030c5b87ed78 ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 794
diff changeset
94 *-cong : {a b c : Obj Sets} {f f' : Hom Sets (a ∧ b) c} →
790
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
95 Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ]
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
96 *-cong refl = refl
787
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
97
995
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 994
diff changeset
98 -- ○ b
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 994
diff changeset
99 -- b -----------→ 1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 994
diff changeset
100 -- | |
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 994
diff changeset
101 -- m | | ⊤
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 994
diff changeset
102 -- ↓ char m ↓
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 994
diff changeset
103 -- a -----------→ Ω
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 994
diff changeset
104 -- h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 994
diff changeset
105
994
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
106 data II {c : Level } : Set c where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
107 true : II
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
108 false : II
932
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
109
994
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
110 data Tker {c : Level} {a : Set c} ( f : a → II {c} ) : Set c where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
111 isTrue : (x : a ) → f x ≡ true → Tker f
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
112
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
113 topos : {c : Level } → Topos (Sets {c}) sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
114 topos = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
115 Ω = II
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
116 ; ⊤ = λ _ → true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
117 ; Ker = tker
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
118 ; char = tchar
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
119 ; isTopos = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
120 char-uniqueness = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
121 ; ker-iso = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
122 }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
123 } where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
124 etker : {a : Obj Sets} (h : Hom Sets a II) → Hom Sets ( Tker h ) a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
125 etker h (isTrue x eq) = x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
126 e-eq : {a : Obj Sets} (h : Hom Sets a II) → Sets [ Sets [ h o etker h ] ≈ Sets [ Sets [ (λ _ → true) o CCC.○ sets a ] o etker h ] ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
127 e-eq h = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
128 tker : {a : Obj Sets} (h : Hom Sets a II) → Equalizer Sets h (Sets [ (λ _ → true) o CCC.○ sets a ])
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
129 tker {a} h = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
130 equalizer-c = Tker h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
131 ; equalizer = etker h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
132 ; isEqualizer = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
133 fe=ge = e-eq h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
134 ; k = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
135 ; ek=h = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
136 ; uniqueness = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
137 }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
138 }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
139 tchar : {a b : Obj Sets} (m : Hom Sets b a) → Mono Sets m → Hom Sets a II
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
140 tchar {a} {b} m mono x = true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
141
933
e702aa8be9dd level try and CCC bad approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 932
diff changeset
142
e702aa8be9dd level try and CCC bad approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 932
diff changeset
143
911
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
144 open import graph
932
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
145 module ccc-from-graph {c₁ c₂ : Level } (G : Graph {c₁} {c₂}) where
787
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
146
802
7bc41fc7b563 graph with positive logic to Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 801
diff changeset
147 open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] )
803
984d20c10c87 simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 802
diff changeset
148 open Graph
984d20c10c87 simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 802
diff changeset
149
991
e7848ad0c6f9 remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 986
diff changeset
150 V = vertex G
e7848ad0c6f9 remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 986
diff changeset
151 E : V → V → Set c₂
e7848ad0c6f9 remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 986
diff changeset
152 E = edge G
e7848ad0c6f9 remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 986
diff changeset
153
e7848ad0c6f9 remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 986
diff changeset
154 data Objs : Set c₁ where
e7848ad0c6f9 remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 986
diff changeset
155 atom : V → Objs
911
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
156 ⊤ : Objs
991
e7848ad0c6f9 remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 986
diff changeset
157 _∧_ : Objs → Objs → Objs
911
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
158 _<=_ : Objs → Objs → Objs
803
984d20c10c87 simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 802
diff changeset
159
991
e7848ad0c6f9 remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 986
diff changeset
160 data Arrows : (b c : Objs ) → Set (c₁ ⊔ c₂)
e7848ad0c6f9 remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 986
diff changeset
161 data Arrow : Objs → Objs → Set (c₁ ⊔ c₂) where --- case i
e7848ad0c6f9 remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 986
diff changeset
162 arrow : {a b : V} → E a b → Arrow (atom a) (atom b)
911
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
163 π : {a b : Objs } → Arrow ( a ∧ b ) a
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
164 π' : {a b : Objs } → Arrow ( a ∧ b ) b
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
165 ε : {a b : Objs } → Arrow ((a <= b) ∧ b ) a
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
166 _* : {a b c : Objs } → Arrows (c ∧ b ) a → Arrow c ( a <= b ) --- case v
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
167
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
168 data Arrows where
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
169 id : ( a : Objs ) → Arrows a a --- case i
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
170 ○ : ( a : Objs ) → Arrows a ⊤ --- case i
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
171 <_,_> : {a b c : Objs } → Arrows c a → Arrows c b → Arrows c (a ∧ b) -- case iii
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
172 iv : {b c d : Objs } ( f : Arrow d c ) ( g : Arrows b d ) → Arrows b c -- cas iv
803
984d20c10c87 simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 802
diff changeset
173
911
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
174 _・_ : {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
175 id a ・ g = g
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
176 ○ a ・ g = ○ _
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
177 < f , g > ・ h = < f ・ h , g ・ h >
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
178 iv f g ・ h = iv f ( g ・ h )
819
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 818
diff changeset
179
933
e702aa8be9dd level try and CCC bad approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 932
diff changeset
180
911
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
181 identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) ≡ f
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
182 identityL = refl
819
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 818
diff changeset
183
911
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
184 identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) ≡ f
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
185 identityR {a} {a} {id a} = refl
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
186 identityR {a} {⊤} {○ a} = refl
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
187 identityR {a} {_} {< f , f₁ >} = cong₂ (λ j k → < j , k > ) identityR identityR
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
188 identityR {a} {b} {iv f g} = cong (λ k → iv f k ) identityR
819
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 818
diff changeset
189
911
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
190 assoc≡ : {a b c d : Objs} (f : Arrows c d) (g : Arrows b c) (h : Arrows a b) →
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
191 (f ・ (g ・ h)) ≡ ((f ・ g) ・ h)
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
192 assoc≡ (id a) g h = refl
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
193 assoc≡ (○ a) g h = refl
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
194 assoc≡ < f , f₁ > g h = cong₂ (λ j k → < j , k > ) (assoc≡ f g h) (assoc≡ f₁ g h)
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
195 assoc≡ (iv f f1) g h = cong (λ k → iv f k ) ( assoc≡ f1 g h )
819
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 818
diff changeset
196
911
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
197 -- positive intutionistic calculus
991
e7848ad0c6f9 remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 986
diff changeset
198 PL : Category c₁ (c₁ ⊔ c₂) (c₁ ⊔ c₂)
911
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
199 PL = record {
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
200 Obj = Objs;
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
201 Hom = λ a b → Arrows a b ;
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
202 _o_ = λ{a} {b} {c} x y → x ・ y ;
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
203 _≈_ = λ x y → x ≡ y ;
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
204 Id = λ{a} → id a ;
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
205 isCategory = record {
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
206 isEquivalence = record {refl = refl ; trans = trans ; sym = sym} ;
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
207 identityL = λ {a b f} → identityL {a} {b} {f} ;
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
208 identityR = λ {a b f} → identityR {a} {b} {f} ;
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
209 o-resp-≈ = λ {a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ;
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
210 associative = λ{a b c d f g h } → assoc≡ f g h
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
211 }
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
212 } where
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
213 o-resp-≈ : {A B C : Objs} {f g : Arrows A B} {h i : Arrows B C} →
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
214 f ≡ g → h ≡ i → (h ・ f) ≡ (i ・ g)
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
215 o-resp-≈ refl refl = refl
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
216
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
217 --------
819
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 818
diff changeset
218 --
911
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
219 -- Functor from Positive Logic to Sets
819
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 818
diff changeset
220 --
911
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
221
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
222 -- open import Category.Sets
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
223 -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionalit y c₂ c₂
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
224
932
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
225 open import Data.List
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
226
911
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
227 C = graphtocat.Chain G
819
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 818
diff changeset
228
911
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
229 tr : {a b : vertex G} → edge G a b → ((y : vertex G) → C y a) → (y : vertex G) → C y b
932
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
230 tr f x y = graphtocat.next f (x y)
911
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
231
932
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
232 fobj : ( a : Objs ) → Set (c₁ ⊔ c₂)
911
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
233 fobj (atom x) = ( y : vertex G ) → C y x
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
234 fobj ⊤ = One
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
235 fobj (a ∧ b) = ( fobj a /\ fobj b)
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
236 fobj (a <= b) = fobj b → fobj a
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
237
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
238 fmap : { a b : Objs } → Hom PL a b → fobj a → fobj b
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
239 amap : { a b : Objs } → Arrow a b → fobj a → fobj b
932
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
240 amap (arrow x) y = tr x y -- tr x
911
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
241 amap π ( x , y ) = x
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
242 amap π' ( x , y ) = y
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
243 amap ε (f , x ) = f x
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
244 amap (f *) x = λ y → fmap f ( x , y )
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
245 fmap (id a) x = x
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
246 fmap (○ a) x = OneObj
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
247 fmap < f , g > x = ( fmap f x , fmap g x )
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
248 fmap (iv x f) a = amap x ( fmap f a )
819
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 818
diff changeset
249
911
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
250 -- CS is a map from Positive logic to Sets
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
251 -- Sets is CCC, so we have a cartesian closed category generated by a graph
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
252 -- as a sub category of Sets
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
253
932
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
254 CS : Functor PL (Sets {c₁ ⊔ c₂})
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
255 FObj CS a = fobj a
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
256 FMap CS {a} {b} f = fmap {a} {b} f
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
257 isFunctor CS = isf where
911
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
258 _+_ = Category._o_ PL
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
259 ++idR = IsCategory.identityR ( Category.isCategory PL )
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
260 distr : {a b c : Obj PL} { f : Hom PL a b } { g : Hom PL b c } → (z : fobj a ) → fmap (g + f) z ≡ fmap g (fmap f z)
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
261 distr {a} {a₁} {a₁} {f} {id a₁} z = refl
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
262 distr {a} {a₁} {⊤} {f} {○ a₁} z = refl
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
263 distr {a} {b} {c ∧ d} {f} {< g , g₁ >} z = cong₂ (λ j k → j , k ) (distr {a} {b} {c} {f} {g} z) (distr {a} {b} {d} {f} {g₁} z)
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
264 distr {a} {b} {c} {f} {iv {_} {_} {d} x g} z = adistr (distr {a} {b} {d} {f} {g} z) x where
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
265 adistr : fmap (g + f) z ≡ fmap g (fmap f z) →
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
266 ( x : Arrow d c ) → fmap ( iv x (g + f) ) z ≡ fmap ( iv x g ) (fmap f z )
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
267 adistr eq x = cong ( λ k → amap x k ) eq
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
268 isf : IsFunctor PL Sets fobj fmap
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
269 IsFunctor.identity isf = extensionality Sets ( λ x → refl )
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
270 IsFunctor.≈-cong isf refl = refl
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
271 IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z )
819
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 818
diff changeset
272
818
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 817
diff changeset
273 ---
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 817
diff changeset
274 --- SubCategoy SC F A is a category with Obj = FObj F, Hom = FMap
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 817
diff changeset
275 ---
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 817
diff changeset
276 --- CCC ( SC (CS G)) Sets have to be proved
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 817
diff changeset
277 --- SM can be eliminated if we have
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 817
diff changeset
278 --- sobj (a : vertex g ) → {a} a set have only a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 817
diff changeset
279 --- smap (a b : vertex g ) → {a} → {b}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 817
diff changeset
280
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 817
diff changeset
281
932
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
282 record CCCObj {c₁ c₂ ℓ : Level} : Set (suc (ℓ ⊔ (c₂ ⊔ c₁))) where
818
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 817
diff changeset
283 field
932
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
284 cat : Category c₁ c₂ ℓ
911
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
285 ≡←≈ : {a b : Obj cat } → { f g : Hom cat a b } → cat [ f ≈ g ] → f ≡ g
818
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 817
diff changeset
286 ccc : CCC cat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 817
diff changeset
287
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 817
diff changeset
288 open CCCObj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 817
diff changeset
289
932
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
290 record CCCMap {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (A : CCCObj {c₁} {c₂} {ℓ} ) (B : CCCObj {c₁′} {c₂′}{ℓ′} ) : Set (suc (ℓ′ ⊔ (c₂′ ⊔ c₁′) ⊔ ℓ ⊔ (c₂ ⊔ c₁))) where
818
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 817
diff changeset
291 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 817
diff changeset
292 cmap : Functor (cat A ) (cat B )
820
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 819
diff changeset
293 ccf : CCC (cat A) → CCC (cat B)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 819
diff changeset
294
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 819
diff changeset
295 open import Category.Cat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 819
diff changeset
296
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 819
diff changeset
297 open CCCMap
949
ac53803b3b2a reorganization for apkg
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 948
diff changeset
298 open import Relation.Binary
818
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 817
diff changeset
299
932
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
300 Cart : {c₁ c₂ ℓ : Level} → Category (suc (c₁ ⊔ c₂ ⊔ ℓ)) (suc (ℓ ⊔ (c₂ ⊔ c₁))) (suc (ℓ ⊔ c₁ ⊔ c₂))
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
301 Cart {c₁} {c₂} {ℓ} = record {
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
302 Obj = CCCObj {c₁} {c₂} {ℓ}
820
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 819
diff changeset
303 ; Hom = CCCMap
824
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 823
diff changeset
304 ; _o_ = λ {A} {B} {C} f g → record { cmap = (cmap f) ○ ( cmap g ) ; ccf = λ _ → ccf f ( ccf g (ccc A )) }
820
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 819
diff changeset
305 ; _≈_ = λ {a} {b} f g → cmap f ≃ cmap g
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 819
diff changeset
306 ; Id = λ {a} → record { cmap = identityFunctor ; ccf = λ x → x }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 819
diff changeset
307 ; isCategory = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 819
diff changeset
308 isEquivalence = λ {A} {B} → record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 819
diff changeset
309 refl = λ {f} → let open ≈-Reasoning (CAT) in refl-hom {cat A} {cat B} {cmap f}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 819
diff changeset
310 ; sym = λ {f} {g} → let open ≈-Reasoning (CAT) in sym-hom {cat A} {cat B} {cmap f} {cmap g}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 819
diff changeset
311 ; trans = λ {f} {g} {h} → let open ≈-Reasoning (CAT) in trans-hom {cat A} {cat B} {cmap f} {cmap g} {cmap h} }
821
fbbc9c03bfed Grp and Cart
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 820
diff changeset
312 ; identityL = λ {x} {y} {f} → let open ≈-Reasoning (CAT) in idL {cat x} {cat y} {cmap f} {_} {_}
fbbc9c03bfed Grp and Cart
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 820
diff changeset
313 ; identityR = λ {x} {y} {f} → let open ≈-Reasoning (CAT) in idR {cat x} {cat y} {cmap f}
fbbc9c03bfed Grp and Cart
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 820
diff changeset
314 ; o-resp-≈ = λ {x} {y} {z} {f} {g} {h} {i} → IsCategory.o-resp-≈ ( Category.isCategory CAT) {cat x}{cat y}{cat z} {cmap f} {cmap g} {cmap h} {cmap i}
fbbc9c03bfed Grp and Cart
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 820
diff changeset
315 ; associative = λ {a} {b} {c} {d} {f} {g} {h} → let open ≈-Reasoning (CAT) in assoc {cat a} {cat b} {cat c} {cat d} {cmap f} {cmap g} {cmap h}
824
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 823
diff changeset
316 }}
818
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 817
diff changeset
317
825
8f41ad966eaa rename discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 824
diff changeset
318 open import graph
818
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 817
diff changeset
319 open Graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 817
diff changeset
320
932
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
321 record GMap {c₁ c₂ c₁' c₂' : Level} (x : Graph {c₁} {c₂} ) (y : Graph {c₁'} {c₂'} ) : Set (c₁ ⊔ c₂ ⊔ c₁' ⊔ c₂') where
820
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 819
diff changeset
322 field
818
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 817
diff changeset
323 vmap : vertex x → vertex y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 817
diff changeset
324 emap : {a b : vertex x} → edge x a b → edge y (vmap a) (vmap b)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 817
diff changeset
325
820
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 819
diff changeset
326 open GMap
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 819
diff changeset
327
821
fbbc9c03bfed Grp and Cart
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 820
diff changeset
328 open import Relation.Binary.HeterogeneousEquality using (_≅_;refl ) renaming ( sym to ≅-sym ; trans to ≅-trans ; cong to ≅-cong )
fbbc9c03bfed Grp and Cart
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 820
diff changeset
329
932
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
330 data [_]_==_ {c₁ c₂ : Level} (C : Graph {c₁} {c₂}) {A B : vertex C} (f : edge C A B)
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
331 : ∀{X Y : vertex C} → edge C X Y → Set (c₁ ⊔ c₂ ) where
824
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 823
diff changeset
332 mrefl : {g : edge C A B} → (eqv : f ≡ g ) → [ C ] f == g
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 823
diff changeset
333
938
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 937
diff changeset
334 eq-vertex1 : {c₁ c₂ : Level} (C : Graph {c₁} {c₂}) {A B : vertex C} {f : edge C A B}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 937
diff changeset
335 {X Y : vertex C} → {g : edge C X Y } → ( [ C ] f == g ) → A ≡ X
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 937
diff changeset
336 eq-vertex1 _ (mrefl refl) = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 937
diff changeset
337
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 937
diff changeset
338 eq-vertex2 : {c₁ c₂ : Level} (C : Graph {c₁} {c₂}) {A B : vertex C} {f : edge C A B}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 937
diff changeset
339 {X Y : vertex C} → {g : edge C X Y } → ( [ C ] f == g ) → B ≡ Y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 937
diff changeset
340 eq-vertex2 _ (mrefl refl) = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 937
diff changeset
341
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 937
diff changeset
342 eq-edge : {c₁ c₂ : Level} (C : Graph {c₁} {c₂}) {A B : vertex C} {f : edge C A B}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 937
diff changeset
343 {X Y : vertex C} → {g : edge C X Y } → ( [ C ] f == g ) → f ≅ g
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 937
diff changeset
344 eq-edge C eq with eq-vertex1 C eq | eq-vertex2 C eq
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 937
diff changeset
345 eq-edge C (mrefl refl) | refl | refl = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 937
diff changeset
346
932
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
347 _=m=_ : {c₁ c₂ c₁' c₂' : Level} {C : Graph {c₁} {c₂} } {D : Graph {c₁'} {c₂'} }
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
348 → (F G : GMap C D) → Set (c₁ ⊔ c₂ ⊔ c₁' ⊔ c₂')
824
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 823
diff changeset
349 _=m=_ {C = C} {D = D} F G = ∀{A B : vertex C} → (f : edge C A B) → [ D ] emap F f == emap G f
821
fbbc9c03bfed Grp and Cart
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 820
diff changeset
350
934
cce9e539486e workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 933
diff changeset
351 _&_ : {c₁ c₂ c₁' c₂' c₁'' c₂'' : Level} {x : Graph {c₁} {c₂}} {y : Graph {c₁'} {c₂'}} {z : Graph {c₁''} {c₂''} } ( f : GMap y z ) ( g : GMap x y ) → GMap x z
821
fbbc9c03bfed Grp and Cart
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 820
diff changeset
352 f & g = record { vmap = λ x → vmap f ( vmap g x ) ; emap = λ x → emap f ( emap g x ) }
fbbc9c03bfed Grp and Cart
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 820
diff changeset
353
932
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
354 Grph : {c₁ c₂ : Level} → Category (suc (c₁ ⊔ c₂)) (c₁ ⊔ c₂) (c₁ ⊔ c₂)
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
355 Grph {c₁} {c₂} = record {
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
356 Obj = Graph {c₁} {c₂}
929
1e8ed7dedc03 ... simpler level on CCC Graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 928
diff changeset
357 ; Hom = GMap
821
fbbc9c03bfed Grp and Cart
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 820
diff changeset
358 ; _o_ = _&_
fbbc9c03bfed Grp and Cart
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 820
diff changeset
359 ; _≈_ = _=m=_
820
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 819
diff changeset
360 ; Id = record { vmap = λ y → y ; emap = λ f → f }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 819
diff changeset
361 ; isCategory = record {
824
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 823
diff changeset
362 isEquivalence = λ {A} {B} → ise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 823
diff changeset
363 ; identityL = λ e → mrefl refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 823
diff changeset
364 ; identityR = λ e → mrefl refl
821
fbbc9c03bfed Grp and Cart
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 820
diff changeset
365 ; o-resp-≈ = m--resp-≈
824
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 823
diff changeset
366 ; associative = λ e → mrefl refl
821
fbbc9c03bfed Grp and Cart
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 820
diff changeset
367 }} where
932
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
368 msym : {x y : Graph {c₁} {c₂} } { f g : GMap x y } → f =m= g → g =m= f
929
1e8ed7dedc03 ... simpler level on CCC Graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 928
diff changeset
369 msym {x} {y} f=g f = lemma ( f=g f ) where
824
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 823
diff changeset
370 lemma : ∀{a b c d} {f : edge y a b} {g : edge y c d} → [ y ] f == g → [ y ] g == f
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 823
diff changeset
371 lemma (mrefl Ff≈Gf) = mrefl (sym Ff≈Gf)
932
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
372 mtrans : {x y : Graph {c₁} {c₂} } { f g h : GMap x y } → f =m= g → g =m= h → f =m= h
929
1e8ed7dedc03 ... simpler level on CCC Graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 928
diff changeset
373 mtrans {x} {y} f=g g=h f = lemma ( f=g f ) ( g=h f ) where
824
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 823
diff changeset
374 lemma : ∀{a b c d e f} {p : edge y a b} {q : edge y c d} → {r : edge y e f} → [ y ] p == q → [ y ] q == r → [ y ] p == r
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 823
diff changeset
375 lemma (mrefl eqv) (mrefl eqv₁) = mrefl ( trans eqv eqv₁ )
932
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
376 ise : {x y : Graph {c₁} {c₂} } → IsEquivalence {_} {c₁ ⊔ c₂} {_} ( _=m=_ {_} {_} {_} {_} {x} {y})
821
fbbc9c03bfed Grp and Cart
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 820
diff changeset
377 ise = record {
824
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 823
diff changeset
378 refl = λ f → mrefl refl
821
fbbc9c03bfed Grp and Cart
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 820
diff changeset
379 ; sym = msym
fbbc9c03bfed Grp and Cart
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 820
diff changeset
380 ; trans = mtrans
fbbc9c03bfed Grp and Cart
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 820
diff changeset
381 }
932
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
382 m--resp-≈ : {A B C : Graph {c₁} {c₂} }
824
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 823
diff changeset
383 {f g : GMap A B} {h i : GMap B C} → f =m= g → h =m= i → ( h & f ) =m= ( i & g )
929
1e8ed7dedc03 ... simpler level on CCC Graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 928
diff changeset
384 m--resp-≈ {A} {B} {C} {f} {g} {h} {i} f=g h=i e =
824
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 823
diff changeset
385 lemma (emap f e) (emap g e) (emap i (emap g e)) (f=g e) (h=i ( emap g e )) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 823
diff changeset
386 lemma : {a b c d : vertex B } {z w : vertex C } (ϕ : edge B a b) (ψ : edge B c d) (π : edge C z w) →
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 823
diff changeset
387 [ B ] ϕ == ψ → [ C ] (emap h ψ) == π → [ C ] (emap h ϕ) == π
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 823
diff changeset
388 lemma _ _ _ (mrefl refl) (mrefl refl) = mrefl refl
820
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 819
diff changeset
389
821
fbbc9c03bfed Grp and Cart
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 820
diff changeset
390 --- Forgetful functor
fbbc9c03bfed Grp and Cart
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 820
diff changeset
391
991
e7848ad0c6f9 remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 986
diff changeset
392 module forgetful {c₁ : Level} where
927
2c5ae3015a05 level hell
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 926
diff changeset
393
992
c1576827404e forgetful functor in Graph done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 991
diff changeset
394 ≃-cong : {c₁ ℓ : Level} (B : Category c₁ c₁ ℓ ) → {a b a' b' : Obj B }
822
4c0580d9dda4 from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 821
diff changeset
395 → { f f' : Hom B a b }
4c0580d9dda4 from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 821
diff changeset
396 → { g g' : Hom B a' b' }
4c0580d9dda4 from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 821
diff changeset
397 → [_]_~_ B f g → B [ f ≈ f' ] → B [ g ≈ g' ] → [_]_~_ B f' g'
927
2c5ae3015a05 level hell
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 926
diff changeset
398 ≃-cong B {a} {b} {a'} {b'} {f} {f'} {g} {g'} (refl {g2} eqv) f=f' g=g' = let open ≈-Reasoning B in refl {_} {_} {_} {B} {a'} {b'} {f'} {g'} ( begin
822
4c0580d9dda4 from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 821
diff changeset
399 f'
4c0580d9dda4 from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 821
diff changeset
400 ≈↑⟨ f=f' ⟩
4c0580d9dda4 from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 821
diff changeset
401 f
4c0580d9dda4 from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 821
diff changeset
402 ≈⟨ eqv ⟩
4c0580d9dda4 from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 821
diff changeset
403 g
4c0580d9dda4 from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 821
diff changeset
404 ≈⟨ g=g' ⟩
4c0580d9dda4 from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 821
diff changeset
405 g'
4c0580d9dda4 from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 821
diff changeset
406 ∎ )
4c0580d9dda4 from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 821
diff changeset
407
992
c1576827404e forgetful functor in Graph done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 991
diff changeset
408 ≃→a=a : {c₁ ℓ : Level} (B : Category c₁ c₁ ℓ ) → {a b a' b' : Obj B }
c1576827404e forgetful functor in Graph done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 991
diff changeset
409 → ( f : Hom B a b )
c1576827404e forgetful functor in Graph done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 991
diff changeset
410 → ( g : Hom B a' b' )
c1576827404e forgetful functor in Graph done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 991
diff changeset
411 → [_]_~_ B f g → a ≡ a'
c1576827404e forgetful functor in Graph done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 991
diff changeset
412 ≃→a=a B f g (refl eqv) = refl
c1576827404e forgetful functor in Graph done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 991
diff changeset
413
c1576827404e forgetful functor in Graph done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 991
diff changeset
414 ≃→b=b : {c₁ ℓ : Level} (B : Category c₁ c₁ ℓ ) → {a b a' b' : Obj B }
c1576827404e forgetful functor in Graph done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 991
diff changeset
415 → ( f : Hom B a b )
c1576827404e forgetful functor in Graph done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 991
diff changeset
416 → ( g : Hom B a' b' )
c1576827404e forgetful functor in Graph done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 991
diff changeset
417 → [_]_~_ B f g → b ≡ b'
c1576827404e forgetful functor in Graph done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 991
diff changeset
418 ≃→b=b B f g (refl eqv) = refl
c1576827404e forgetful functor in Graph done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 991
diff changeset
419
934
cce9e539486e workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 933
diff changeset
420 -- Grph does not allow morph on different level graphs
991
e7848ad0c6f9 remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 986
diff changeset
421 -- simply assumes c₁ and c₂ has the same
934
cce9e539486e workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 933
diff changeset
422
991
e7848ad0c6f9 remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 986
diff changeset
423 uobj : Obj (Cart {c₁ } {c₁} {c₁}) → Obj Grph
945
94ece478b583 cobj and cmap connected
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 944
diff changeset
424 uobj a = record { vertex = Obj (cat a) ; edge = Hom (cat a) }
991
e7848ad0c6f9 remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 986
diff changeset
425 umap : {a b : Obj (Cart {c₁ } {c₁} {c₁} ) } → Hom (Cart ) a b → Hom (Grph {c₁} {c₁}) (( uobj a )) (( uobj b ))
945
94ece478b583 cobj and cmap connected
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 944
diff changeset
426 umap {a} {b} f = record {
991
e7848ad0c6f9 remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 986
diff changeset
427 vmap = λ e → FObj (cmap f) e
e7848ad0c6f9 remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 986
diff changeset
428 ; emap = λ e → FMap (cmap f) e }
934
cce9e539486e workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 933
diff changeset
429
991
e7848ad0c6f9 remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 986
diff changeset
430 UX : Functor (Cart {c₁} {c₁} {c₁}) (Grph {c₁} {c₁})
e7848ad0c6f9 remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 986
diff changeset
431 FObj UX a = (uobj a)
945
94ece478b583 cobj and cmap connected
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 944
diff changeset
432 FMap UX f = umap f
934
cce9e539486e workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 933
diff changeset
433 isFunctor UX = isf where
991
e7848ad0c6f9 remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 986
diff changeset
434 isf : IsFunctor Cart Grph (λ z → (uobj z)) umap
935
92f8f57467e3 add fig
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 934
diff changeset
435 IsFunctor.identity isf {a} {b} {f} = begin
945
94ece478b583 cobj and cmap connected
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 944
diff changeset
436 umap (id1 Cart a)
935
92f8f57467e3 add fig
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 934
diff changeset
437 ≈⟨⟩
945
94ece478b583 cobj and cmap connected
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 944
diff changeset
438 umap {a} {a} (record { cmap = identityFunctor ; ccf = λ x → x })
935
92f8f57467e3 add fig
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 934
diff changeset
439 ≈⟨⟩
92f8f57467e3 add fig
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 934
diff changeset
440 record { vmap = λ y → y ; emap = λ f → f }
92f8f57467e3 add fig
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 934
diff changeset
441 ≈⟨⟩
991
e7848ad0c6f9 remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 986
diff changeset
442 id1 Grph ((uobj a))
935
92f8f57467e3 add fig
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 934
diff changeset
443 ∎ where open ≈-Reasoning Grph
92f8f57467e3 add fig
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 934
diff changeset
444 IsFunctor.distr isf {a} {b} {c} {f} {g} = begin
992
c1576827404e forgetful functor in Graph done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 991
diff changeset
445 umap ( Cart [ g o f ] ) -- FMap (cmap g) (FMap (cmap f) x) = FMap (cmap g) (FMap (cmap f) x)
c1576827404e forgetful functor in Graph done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 991
diff changeset
446 ≈⟨ (λ x → mrefl refl ) ⟩
945
94ece478b583 cobj and cmap connected
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 944
diff changeset
447 Grph [ umap g o umap f ]
992
c1576827404e forgetful functor in Graph done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 991
diff changeset
448 ∎ where open ≈-Reasoning Grph -- FMap (cmap f) e emap (umap f) e = emap (umap g) e <- Cart [ f ≈ g ]
c1576827404e forgetful functor in Graph done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 991
diff changeset
449 IsFunctor.≈-cong isf {a} {b} {f} {g} f=g e with
c1576827404e forgetful functor in Graph done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 991
diff changeset
450 f=g e
c1576827404e forgetful functor in Graph done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 991
diff changeset
451 | ≃→a=a (cat b) (FMap (cmap f) e) (FMap (cmap g) e) (f=g e)
c1576827404e forgetful functor in Graph done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 991
diff changeset
452 | ≃→b=b (cat b) (FMap (cmap f) e) (FMap (cmap g) e) (f=g e)
c1576827404e forgetful functor in Graph done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 991
diff changeset
453 ... | eq | eqa | eqb = cc11 (FMap (cmap f) e) (FMap (cmap g) e) eq eqa eqb where
c1576827404e forgetful functor in Graph done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 991
diff changeset
454 cc11 : {a c a' c' : Obj (cat b) } → ( f : Hom (cat b) a c ) → ( g : Hom (cat b) a' c' )
c1576827404e forgetful functor in Graph done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 991
diff changeset
455 → [ cat b ] f ~ g → a ≡ a' → c ≡ c' → [ uobj b ] f == g
c1576827404e forgetful functor in Graph done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 991
diff changeset
456 cc11 f g (refl eqv) refl refl = mrefl (≡←≈ b eqv)
821
fbbc9c03bfed Grp and Cart
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 820
diff changeset
457
911
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
458 open ccc-from-graph.Objs
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
459 open ccc-from-graph.Arrow
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
460 open ccc-from-graph.Arrows
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
461 open graphtocat.Chain
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
462
932
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
463 Sets0 : {c₂ : Level } → Category (suc c₂) c₂ c₂
f19425b54aba introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 931
diff changeset
464 Sets0 {c₂} = Sets {c₂}
930
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 929
diff changeset
465
944
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 943
diff changeset
466 module fcat {c₁ c₂ : Level} ( g : Graph {c₁} {c₂} ) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 943
diff changeset
467
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 943
diff changeset
468 open ccc-from-graph g
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 943
diff changeset
469
991
e7848ad0c6f9 remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 986
diff changeset
470 FCat : Obj (Cart {c₁} {c₁ ⊔ c₂} {c₁ ⊔ c₂})
944
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 943
diff changeset
471 FCat = record { cat = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 943
diff changeset
472 Obj = Obj PL
945
94ece478b583 cobj and cmap connected
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 944
diff changeset
473 ; Hom = λ a b → Hom B (FObj CS a) (FObj CS b)
944
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 943
diff changeset
474 ; _o_ = Category._o_ B
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 943
diff changeset
475 ; _≈_ = Category._≈_ B
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 943
diff changeset
476 ; Id = λ {a} → id1 B (FObj CS a)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 943
diff changeset
477 ; isCategory = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 943
diff changeset
478 isEquivalence = IsCategory.isEquivalence (Category.isCategory B) ;
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 943
diff changeset
479 identityL = λ {a b f} → IsCategory.identityL (Category.isCategory B) ;
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 943
diff changeset
480 identityR = λ {a b f} → IsCategory.identityR (Category.isCategory B) ;
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 943
diff changeset
481 o-resp-≈ = λ {a b c f g h i} → IsCategory.o-resp-≈ (Category.isCategory B);
993
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 992
diff changeset
482 associative = λ {a} {b} {c} {f} {g} {h} → {!!} -- IsCategory.associative (Category.isCategory B) {{!!}} {{!!}} {{!!}} {{!!}} {{!!}} {{!!}}
944
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 943
diff changeset
483 }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 943
diff changeset
484 } ;
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 943
diff changeset
485 ≡←≈ = λ eq → eq ;
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 943
diff changeset
486 ccc = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 943
diff changeset
487 } where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 943
diff changeset
488 B = Sets {c₁ ⊔ c₂}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 943
diff changeset
489
947
095fd0829ccf use postulate on Hom of FCat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 946
diff changeset
490 -- Hom FCat is an image of Fucntor CS, but I don't know how to write it
095fd0829ccf use postulate on Hom of FCat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 946
diff changeset
491 postulate
095fd0829ccf use postulate on Hom of FCat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 946
diff changeset
492 fcat-pl : {a b : Obj (cat FCat) } → Hom (cat FCat) a b → Hom PL a b
095fd0829ccf use postulate on Hom of FCat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 946
diff changeset
493 fcat-eq : {a b : Obj (cat FCat) } → (f : Hom (cat FCat) a b ) → FMap CS (fcat-pl f) ≡ f
095fd0829ccf use postulate on Hom of FCat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 946
diff changeset
494
944
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 943
diff changeset
495
991
e7848ad0c6f9 remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 986
diff changeset
496 ccc-graph-univ : {c₁ : Level} → UniversalMapping (Grph {c₁} {c₁}) (Cart {c₁ } {c₁} {c₁}) forgetful.UX
e7848ad0c6f9 remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 986
diff changeset
497 ccc-graph-univ {c₁} = record {
933
e702aa8be9dd level try and CCC bad approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 932
diff changeset
498 F = F ;
948
dca4b29553cb mp-flatten
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 947
diff changeset
499 η = η ;
927
2c5ae3015a05 level hell
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 926
diff changeset
500 _* = solution ;
911
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
501 isUniversalMapping = record {
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
502 universalMapping = {!!} ;
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
503 uniquness = {!!}
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
504 }
b8c5f15ee561 small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 825
diff changeset
505 } where
929
1e8ed7dedc03 ... simpler level on CCC Graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 928
diff changeset
506 open forgetful
926
a7332c329b57 remove CSC and subcat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 925
diff changeset
507 open ccc-from-graph
937
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 936
diff changeset
508 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 936
diff changeset
509 --
935
92f8f57467e3 add fig
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 934
diff changeset
510 -- η : Hom Grph a (FObj UX (F a))
993
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 992
diff changeset
511 -- f : edge g x y -----------------------------------> (record {vertex = fobj (atom x) ; edge = fmap h }) : Graph
935
92f8f57467e3 add fig
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 934
diff changeset
512 -- Graph g x ----------------------> y : vertex g ↑
92f8f57467e3 add fig
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 934
diff changeset
513 -- arrow f : Hom (PL g) (atom x) (atom y) |
92f8f57467e3 add fig
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 934
diff changeset
514 -- PL g atom x ------------------> atom y : Obj (PL g) | UX : Functor Sets Graph
92f8f57467e3 add fig
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 934
diff changeset
515 -- | |
92f8f57467e3 add fig
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 934
diff changeset
516 -- | Functor (CS g) |
92f8f57467e3 add fig
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 934
diff changeset
517 -- ↓ |
92f8f57467e3 add fig
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 934
diff changeset
518 -- Sets ((z : vertx g) → C z x) ----> ((z : vertx g) → C z y) = h : Hom Sets (fobj (atom x)) (fobj (atom y))
92f8f57467e3 add fig
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 934
diff changeset
519 --
991
e7848ad0c6f9 remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 986
diff changeset
520 F : Obj (Grph {c₁} {c₁}) → Obj (Cart {c₁} {c₁} {c₁})
947
095fd0829ccf use postulate on Hom of FCat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 946
diff changeset
521 F g = FCat where open fcat g
991
e7848ad0c6f9 remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 986
diff changeset
522 η : (a : Obj (Grph {c₁} {c₁}) ) → Hom Grph a (FObj UX (F a))
993
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 992
diff changeset
523 η a = record { vmap = λ y → vm y ; emap = λ f → em f } where
991
e7848ad0c6f9 remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 986
diff changeset
524 fo : Graph {c₁ } {c₁}
e7848ad0c6f9 remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 986
diff changeset
525 fo = uobj {c₁} (F a)
993
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 992
diff changeset
526 vm : (y : vertex a ) → vertex (FObj UX (F a))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 992
diff changeset
527 vm y = atom y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 992
diff changeset
528 em : { x y : vertex a } (f : edge a x y ) → edge (FObj UX (F a)) (vm x) (vm y)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 992
diff changeset
529 em {x} {y} f = fmap a (iv (arrow f) (id _))
991
e7848ad0c6f9 remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 986
diff changeset
530 cobj : {g : Obj (Grph {c₁} {c₁} ) } {c : Obj Cart} → Hom Grph g (FObj UX c) → Objs g → Obj (cat c)
993
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 992
diff changeset
531 cobj {g} {c} f (atom x) = vmap f x
945
94ece478b583 cobj and cmap connected
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 944
diff changeset
532 cobj {g} {c} f ⊤ = CCC.１ (ccc c)
94ece478b583 cobj and cmap connected
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 944
diff changeset
533 cobj {g} {c} f (x ∧ y) = CCC._∧_ (ccc c) (cobj {g} {c} f x) (cobj {g} {c} f y)
94ece478b583 cobj and cmap connected
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 944
diff changeset
534 cobj {g} {c} f (b <= a) = CCC._<=_ (ccc c) (cobj {g} {c} f b) (cobj {g} {c} f a)
94ece478b583 cobj and cmap connected
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 944
diff changeset
535 c-map : {g : Obj (Grph )} {c : Obj Cart} {A B : Objs g}
94ece478b583 cobj and cmap connected
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 944
diff changeset
536 → (f : Hom Grph g (FObj UX c) ) → (fobj g A → fobj g B) → Hom (cat c) (cobj {g} {c} f A) (cobj {g} {c} f B)
994
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
537 --- from x to b chain. but we forgot how we come here ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
538 c-map {g} {c} {atom x} {atom b} f y = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
539 --- next three cases cannot be negerated
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
540 c-map {g} {c} {⊤} {atom b} f y = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
541 c-map {g} {c} {a ∧ a₁} {atom b} f y = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 993
diff changeset
542 c-map {g} {c} {a <= a₁} {atom b} f y = {!!}
945
94ece478b583 cobj and cmap connected
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 944
diff changeset
543 c-map {g} {c} {a} {⊤} f x = CCC.○ (ccc c) (cobj f a)
946
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 945
diff changeset
544 c-map {g} {c} {a} {x ∧ y} f z = CCC.<_,_> (ccc c) (c-map f (λ k → proj₁ (z k))) (c-map f (λ k → proj₂ (z k)))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 945
diff changeset
545 c-map {g} {c} {d} {b <= a} f x = CCC._* (ccc c) ( c-map f (λ k → x (proj₁ k) (proj₂ k)))
935
92f8f57467e3 add fig
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 934
diff changeset
546 solution : {g : Obj Grph } {c : Obj Cart } → Hom Grph g (FObj UX c) → Hom Cart (F g) c
937
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 936
diff changeset
547 solution {g} {c} f = record { cmap = record {
945
94ece478b583 cobj and cmap connected
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 944
diff changeset
548 FObj = λ x → cobj {g} {c} f x ;
94ece478b583 cobj and cmap connected
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 944
diff changeset
549 FMap = λ {x} {y} h → c-map {g} {c} {x} {y} f h ;
937
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 936
diff changeset
550 isFunctor = {!!} } ;
949
ac53803b3b2a reorganization for apkg
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 948
diff changeset
551 ccf = {!!} }