Mercurial > hg > Members > kono > Proof > category

comparison CCChom.agda @ 785:a67959bcd44b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ccc → hom on going
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 17 Apr 2019 21:32:56 +0900
parents f27d966939f8
children 287d25c87b60
comparison
equal deleted inserted replaced
784:f27d966939f8 785:a67959bcd44b
12 12
13 -- ccc-1 : Hom A a 1 ≅ {*} 13 -- ccc-1 : Hom A a 1 ≅ {*}
14 -- ccc-2 : Hom A c (a × b) ≅ (Hom A c a ) × ( Hom A c b ) 14 -- ccc-2 : Hom A c (a × b) ≅ (Hom A c a ) × ( Hom A c b )
15 -- ccc-3 : Hom A a (c ^ b) ≅ Hom A (a × b) c 15 -- ccc-3 : Hom A a (c ^ b) ≅ Hom A (a × b) c
16 16
17 data One {c : Level} : Set c where 17 data One : Set where
18 OneObj : One -- () in Haskell ( or any one object set ) 18 OneObj : One -- () in Haskell ( or any one object set )
19 19
20 OneCat : Category Level.zero Level.zero Level.zero 20 OneCat : Category Level.zero Level.zero Level.zero
21 OneCat = record { 21 OneCat = record {
22 Obj = One ; 22 Obj = One ;
30 identityR = λ{a b f} → lemma {a} {b} {f} ; 30 identityR = λ{a b f} → lemma {a} {b} {f} ;
31 o-resp-≈ = λ{a b c f g h i} _ _ → refl ; 31 o-resp-≈ = λ{a b c f g h i} _ _ → refl ;
32 associative = λ{a b c d f g h } → refl 32 associative = λ{a b c d f g h } → refl
33 } 33 }
34 } where 34 } where
35 lemma : {a b : One {Level.zero}} → { f : One {Level.zero}} → OneObj ≡ f 35 lemma : {a b : One } → { f : One } → OneObj ≡ f
36 lemma {a} {b} {f} with f 36 lemma {a} {b} {f} with f
37 ... | OneObj = refl 37 ... | OneObj = refl
38 38
39 record IsoS {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') (a b : Obj A) ( a' b' : Obj B ) 39 record IsoS {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') (a b : Obj A) ( a' b' : Obj B )
40 : Set ( c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' ) where 40 : Set ( c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' ) where
46 46
47 47
48 record IsCCChom {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (１ : Obj A) 48 record IsCCChom {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (１ : Obj A)
49 ( _*_ : Obj A → Obj A → Obj A ) ( _^_ : Obj A → Obj A → Obj A ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where 49 ( _*_ : Obj A → Obj A → Obj A ) ( _^_ : Obj A → Obj A → Obj A ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
50 field 50 field
51 ccc-1 : {a : Obj A} → -- Hom A a １ ≅ {*} 51 ccc-1 : {a : Obj A} {b c : Obj OneCat} → -- Hom A a １ ≅ {*}
52 IsoS A OneCat a １ OneObj OneObj 52 IsoS A OneCat a １ b c
53 ccc-2 : {a b c : Obj A} → -- Hom A c ( a * b ) ≅ ( Hom A c a ) * ( Hom A c b ) 53 ccc-2 : {a b c : Obj A} → -- Hom A c ( a * b ) ≅ ( Hom A c a ) * ( Hom A c b )
54 IsoS A (A × A) c (a * b) (c , c ) (a , b ) 54 IsoS A (A × A) c (a * b) (c , c ) (a , b )
55 ccc-3 : {a b c : Obj A} → -- Hom A a ( c ^ b ) ≅ Hom A ( a * b ) c 55 ccc-3 : {a b c : Obj A} → -- Hom A a ( c ^ b ) ≅ Hom A ( a * b ) c
56 IsoS A A a (c ^ b) (a * b) c 56 IsoS A A a (c ^ b) (a * b) c
57 57
71 CCC→hom A c = record { 71 CCC→hom A c = record {
72 one = CCC.１ c 72 one = CCC.１ c
73 ; _*_ = CCC._∧_ c 73 ; _*_ = CCC._∧_ c
74 ; _^_ = CCC._<=_ c 74 ; _^_ = CCC._<=_ c
75 ; isCCChom = record { 75 ; isCCChom = record {
76 ccc-1 = {!!} 76 ccc-1 = λ {a} {b} {c'} → record { ≅→ = c101 ; ≅← = c102 ; iso→ = c103 {a} {b} {c'} ; iso← = c104 }
77 ; ccc-2 = {!!} 77 ; ccc-2 = record { ≅→ = c201 ; ≅← = c202 ; iso→ = c203 ; iso← = c204 }
78 ; ccc-3 = {!!} 78 ; ccc-3 = record { ≅→ = c301 ; ≅← = c302 ; iso→ = c303 ; iso← = c304 }
79 } 79 }
80 } 80 } where
81 c101 : {a : Obj A} → Hom A a (CCC.１ c) → Hom OneCat OneObj OneObj
82 c101 _ = OneObj
83 c102 : {a : Obj A} → Hom OneCat OneObj OneObj → Hom A a (CCC.１ c)
84 c102 {a} OneObj = CCC.○ c a
85 c103 : {a : Obj A } {b c : Obj OneCat} {f : Hom OneCat b b } → _[_≈_] OneCat {b} {c} ( c101 {a} (c102 {a} f) ) f
86 c103 {a} {OneObj} {OneObj} {OneObj} = refl
87 c104 : {a : Obj A} → {f : Hom A a (CCC.１ c)} → A [ (c102 ( c101 f )) ≈ f ]
88 c104 {a} {f} = let open ≈-Reasoning A in HomReasoning.≈-Reasoning.sym A (IsCCC.e2 (CCC.isCCC c) f )
89 c201 : { c₁ a b : Obj A} → Hom A c₁ ((c CCC.∧ a) b) → Hom (A × A) (c₁ , c₁) (a , b)
90 c201 f = ( A [ CCC.π c o f ] , A [ CCC.π' c o f ] )
91 c202 : { c₁ a b : Obj A} → Hom (A × A) (c₁ , c₁) (a , b) → Hom A c₁ ((c CCC.∧ a) b)
92 c202 (f , g ) = CCC.<_,_> c f g
93 c203 : { c₁ a b : Obj A} → {f : Hom (A × A) (c₁ , c₁) (a , b)} → (A × A) [ (c201 ( c202 f )) ≈ f ]
94 c203 = ( IsCCC.e3a (CCC.isCCC c) , IsCCC.e3b (CCC.isCCC c))
95 c204 : { c₁ a b : Obj A} → {f : Hom A c₁ ((c CCC.∧ a) b)} → A [ (c202 ( c201 f )) ≈ f ]
96 c204 = IsCCC.e3c (CCC.isCCC c)
97 c301 : { d a b : Obj A} → Hom A a ((c CCC.<= d) b) → Hom A ((c CCC.∧ a) b) d -- a -> d <= b -> (a ∧ b ) -> d
98 c301 {d} {a} {b} f = A [ CCC.ε c o CCC.<_,_> c ( A [ f o CCC.π c ] ) ( CCC.π' c ) ]
99 c302 : { d a b : Obj A} → Hom A ((c CCC.∧ a) b) d → Hom A a ((c CCC.<= d) b)
100 c302 f = CCC._* c f
101 c303 : { c₁ a b : Obj A} → {f : Hom A ((c CCC.∧ a) b) c₁} → A [ (c301 ( c302 f )) ≈ f ]
102 c303 = IsCCC.e4a (CCC.isCCC c)
103 c304 : { c₁ a b : Obj A} → {f : Hom A a ((c CCC.<= c₁) b)} → A [ (c302 ( c301 f )) ≈ f ]
104 c304 = IsCCC.e4b (CCC.isCCC c)
105
106 open CCChom
107 open IsCCChom
108 open IsoS
109
110 hom→CCC : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( h : CCChom A ) → CCC A
111 hom→CCC A h = record {
112 １ = １
113 ; ○ = ○
114 ; _∧_ = _/\_
115 ; <_,_> = <,>
116 ; π = π
117 ; π' = π'
118 ; _<=_ = _<=_
119 ; _* = _*
120 ; ε = ε
121 ; isCCC = isCCC
122 } where
123 １ : Obj A
124 １ = one h
125 ○ : (a : Obj A ) → Hom A a １
126 ○ a = ≅← ( ccc-1 (isCCChom h ) {_} {OneObj} {OneObj} ) OneObj
127 _/\_ : Obj A → Obj A → Obj A
128 _/\_ a b = _*_ h a b
129 <,> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c ( a /\ b)
130 <,> f g = ≅← ( ccc-2 (isCCChom h ) ) ( f , g )
131 π : {a b : Obj A } → Hom A (a /\ b) a
132 π {a} {b} = proj₁ ( ≅→ ( ccc-2 (isCCChom h ) ) (id1 A (_*_ h a b) ))
133 π' : {a b : Obj A } → Hom A (a /\ b) b
134 π' {a} {b} = proj₂ ( ≅→ ( ccc-2 (isCCChom h ) ) (id1 A (_*_ h a b) ))
135 _<=_ : (a b : Obj A ) → Obj A
136 _<=_ = _^_ h
137 _* : {a b c : Obj A } → Hom A (a /\ b) c → Hom A a (c <= b)
138 _* = ≅← ( ccc-3 (isCCChom h ) )
139 ε : {a b : Obj A } → Hom A ((a <= b ) /\ b) a
140 ε {a} {b} = ≅→ ( ccc-3 (isCCChom h ) {_^_ h a b} {b} ) (id1 A ( _^_ h a b ))
141 isCCC : CCC.IsCCC A １ ○ _/\_ <,> π π' _<=_ _* ε
142 isCCC = record {
143 e2 = e2
144 ; e3a = e3a
145 ; e3b = e3b
146 ; e3c = e3c
147 ; π-cong = π-cong
148 ; e4a = e4a
149 ; e4b = e4b
150 } where
151 e2 : {a : Obj A} → ∀ ( f : Hom A a １ ) → A [ f ≈ ○ a ]
152 e2 f = {!!}
153 e3a : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π o <,> f g ] ≈ f ]
154 e3a = {!!}
155 e3b : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π' o <,> f g ] ≈ g ]
156 e3b = {!!}
157 e3c : {a b c : Obj A} → { h : Hom A c (a /\ b) } → A [ <,> ( A [ π o h ] ) ( A [ π' o h ] ) ≈ h ]
158 e3c = {!!}
159 π-cong : {a b c : Obj A} → { f f' : Hom A c a }{ g g' : Hom A c b } → A [ f ≈ f' ] → A [ g ≈ g' ] → A [ <,> f g ≈ <,> f' g' ]
160 π-cong = {!!}
161 e4a : {a b c : Obj A} → { h : Hom A (c /\ b) a } → A [ A [ ε o ( <,> ( A [ (h *) o π ] ) π') ] ≈ h ]
162 e4a = {!!}
163 e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } → A [ ( A [ ε o ( <,> ( A [ k o π ] ) π' ) ] ) * ≈ k ]
164 e4b = {!!}
165