annotate CCChom.agda @ 785:a67959bcd44b

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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
779
6b4bd02efd80 CCC start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Level
6b4bd02efd80 CCC start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Category
784
f27d966939f8 add CCC hom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 783
diff changeset
3 module CCChom where
779
6b4bd02efd80 CCC start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
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
784
f27d966939f8 add CCC hom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 783
diff changeset
7 open import Data.Product renaming (_×_ to _∧_)
f27d966939f8 add CCC hom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 783
diff changeset
8 open import Category.Constructions.Product
780
b44c1c6ce646 CCC in Hom form
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 779
diff changeset
9 open import Relation.Binary.PropositionalEquality
779
6b4bd02efd80 CCC start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10
6b4bd02efd80 CCC start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open Functor
6b4bd02efd80 CCC start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
6b4bd02efd80 CCC start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 -- ccc-1 : Hom A a 1 ≅ {*}
6b4bd02efd80 CCC start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 -- 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
15 -- 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
16
785
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
17 data One : Set where
779
6b4bd02efd80 CCC start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 OneObj : One -- () in Haskell ( or any one object set )
6b4bd02efd80 CCC start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19
780
b44c1c6ce646 CCC in Hom form
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 779
diff changeset
20 OneCat : Category Level.zero Level.zero Level.zero
b44c1c6ce646 CCC in Hom form
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 779
diff changeset
21 OneCat = record {
b44c1c6ce646 CCC in Hom form
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 779
diff changeset
22 Obj = One ;
b44c1c6ce646 CCC in Hom form
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 779
diff changeset
23 Hom = λ a b → One ;
b44c1c6ce646 CCC in Hom form
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 779
diff changeset
24 _o_ = λ{a} {b} {c} x y → OneObj ;
b44c1c6ce646 CCC in Hom form
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 779
diff changeset
25 _≈_ = λ x y → x ≡ y ;
b44c1c6ce646 CCC in Hom form
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 779
diff changeset
26 Id = λ{a} → OneObj ;
b44c1c6ce646 CCC in Hom form
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 779
diff changeset
27 isCategory = record {
b44c1c6ce646 CCC in Hom form
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 779
diff changeset
28 isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ;
b44c1c6ce646 CCC in Hom form
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 779
diff changeset
29 identityL = λ{a b f} → lemma {a} {b} {f} ;
b44c1c6ce646 CCC in Hom form
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 779
diff changeset
30 identityR = λ{a b f} → lemma {a} {b} {f} ;
b44c1c6ce646 CCC in Hom form
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 779
diff changeset
31 o-resp-≈ = λ{a b c f g h i} _ _ → refl ;
b44c1c6ce646 CCC in Hom form
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 779
diff changeset
32 associative = λ{a b c d f g h } → refl
b44c1c6ce646 CCC in Hom form
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 779
diff changeset
33 }
b44c1c6ce646 CCC in Hom form
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 779
diff changeset
34 } where
785
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
35 lemma : {a b : One } → { f : One } → OneObj ≡ f
780
b44c1c6ce646 CCC in Hom form
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 779
diff changeset
36 lemma {a} {b} {f} with f
b44c1c6ce646 CCC in Hom form
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 779
diff changeset
37 ... | OneObj = refl
b44c1c6ce646 CCC in Hom form
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 779
diff changeset
38
783
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
39 record IsoS {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') (a b : Obj A) ( a' b' : Obj B )
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
40 : Set ( c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' ) where
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
41 field
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
42 ≅→ : Hom A a b → Hom B a' b'
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
43 ≅← : Hom B a' b' → Hom A a b
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
44 iso→ : {f : Hom B a' b' } → B [ ≅→ ( ≅← f) ≈ f ]
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
45 iso← : {f : Hom A a b } → A [ ≅← ( ≅→ f) ≈ f ]
779
6b4bd02efd80 CCC start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46
783
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
47
784
f27d966939f8 add CCC hom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 783
diff changeset
48 record IsCCChom {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (1 : Obj A)
780
b44c1c6ce646 CCC in Hom form
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 779
diff changeset
49 ( _*_ : Obj A → Obj A → Obj A ) ( _^_ : Obj A → Obj A → Obj A ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
779
6b4bd02efd80 CCC start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 field
785
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
51 ccc-1 : {a : Obj A} {b c : Obj OneCat} → -- Hom A a 1 ≅ {*}
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
52 IsoS A OneCat a 1 b c
780
b44c1c6ce646 CCC in Hom form
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 779
diff changeset
53 ccc-2 : {a b c : Obj A} → -- Hom A c ( a * b ) ≅ ( Hom A c a ) * ( Hom A c b )
784
f27d966939f8 add CCC hom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 783
diff changeset
54 IsoS A (A × A) c (a * b) (c , c ) (a , b )
780
b44c1c6ce646 CCC in Hom form
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 779
diff changeset
55 ccc-3 : {a b c : Obj A} → -- Hom A a ( c ^ b ) ≅ Hom A ( a * b ) c
b44c1c6ce646 CCC in Hom form
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 779
diff changeset
56 IsoS A A a (c ^ b) (a * b) c
779
6b4bd02efd80 CCC start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57
6b4bd02efd80 CCC start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58
784
f27d966939f8 add CCC hom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 783
diff changeset
59 record CCChom {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
781
340708e8d54f fix for 2.5.4.2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 780
diff changeset
60 field
340708e8d54f fix for 2.5.4.2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 780
diff changeset
61 one : Obj A
340708e8d54f fix for 2.5.4.2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 780
diff changeset
62 _*_ : Obj A → Obj A → Obj A
340708e8d54f fix for 2.5.4.2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 780
diff changeset
63 _^_ : Obj A → Obj A → Obj A
784
f27d966939f8 add CCC hom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 783
diff changeset
64 isCCChom : IsCCChom A one _*_ _^_
783
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
65
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
66 open import HomReasoning
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
67
784
f27d966939f8 add CCC hom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 783
diff changeset
68 open import CCC
779
6b4bd02efd80 CCC start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69
784
f27d966939f8 add CCC hom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 783
diff changeset
70 CCC→hom : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( c : CCC A ) → CCChom A
f27d966939f8 add CCC hom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 783
diff changeset
71 CCC→hom A c = record {
f27d966939f8 add CCC hom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 783
diff changeset
72 one = CCC.1 c
f27d966939f8 add CCC hom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 783
diff changeset
73 ; _*_ = CCC._∧_ c
f27d966939f8 add CCC hom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 783
diff changeset
74 ; _^_ = CCC._<=_ c
f27d966939f8 add CCC hom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 783
diff changeset
75 ; isCCChom = record {
785
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
76 ccc-1 = λ {a} {b} {c'} → record { ≅→ = c101 ; ≅← = c102 ; iso→ = c103 {a} {b} {c'} ; iso← = c104 }
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
77 ; ccc-2 = record { ≅→ = c201 ; ≅← = c202 ; iso→ = c203 ; iso← = c204 }
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
78 ; ccc-3 = record { ≅→ = c301 ; ≅← = c302 ; iso→ = c303 ; iso← = c304 }
784
f27d966939f8 add CCC hom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 783
diff changeset
79 }
785
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
80 } where
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
81 c101 : {a : Obj A} → Hom A a (CCC.1 c) → Hom OneCat OneObj OneObj
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
82 c101 _ = OneObj
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
83 c102 : {a : Obj A} → Hom OneCat OneObj OneObj → Hom A a (CCC.1 c)
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
84 c102 {a} OneObj = CCC.○ c a
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
85 c103 : {a : Obj A } {b c : Obj OneCat} {f : Hom OneCat b b } → _[_≈_] OneCat {b} {c} ( c101 {a} (c102 {a} f) ) f
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
86 c103 {a} {OneObj} {OneObj} {OneObj} = refl
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
87 c104 : {a : Obj A} → {f : Hom A a (CCC.1 c)} → A [ (c102 ( c101 f )) ≈ f ]
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
88 c104 {a} {f} = let open ≈-Reasoning A in HomReasoning.≈-Reasoning.sym A (IsCCC.e2 (CCC.isCCC c) f )
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
89 c201 : { c₁ a b : Obj A} → Hom A c₁ ((c CCC.∧ a) b) → Hom (A × A) (c₁ , c₁) (a , b)
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
90 c201 f = ( A [ CCC.π c o f ] , A [ CCC.π' c o f ] )
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
91 c202 : { c₁ a b : Obj A} → Hom (A × A) (c₁ , c₁) (a , b) → Hom A c₁ ((c CCC.∧ a) b)
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
92 c202 (f , g ) = CCC.<_,_> c f g
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
93 c203 : { c₁ a b : Obj A} → {f : Hom (A × A) (c₁ , c₁) (a , b)} → (A × A) [ (c201 ( c202 f )) ≈ f ]
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
94 c203 = ( IsCCC.e3a (CCC.isCCC c) , IsCCC.e3b (CCC.isCCC c))
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
95 c204 : { c₁ a b : Obj A} → {f : Hom A c₁ ((c CCC.∧ a) b)} → A [ (c202 ( c201 f )) ≈ f ]
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
96 c204 = IsCCC.e3c (CCC.isCCC c)
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
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
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
98 c301 {d} {a} {b} f = A [ CCC.ε c o CCC.<_,_> c ( A [ f o CCC.π c ] ) ( CCC.π' c ) ]
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
99 c302 : { d a b : Obj A} → Hom A ((c CCC.∧ a) b) d → Hom A a ((c CCC.<= d) b)
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
100 c302 f = CCC._* c f
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
101 c303 : { c₁ a b : Obj A} → {f : Hom A ((c CCC.∧ a) b) c₁} → A [ (c301 ( c302 f )) ≈ f ]
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
102 c303 = IsCCC.e4a (CCC.isCCC c)
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
103 c304 : { c₁ a b : Obj A} → {f : Hom A a ((c CCC.<= c₁) b)} → A [ (c302 ( c301 f )) ≈ f ]
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
104 c304 = IsCCC.e4b (CCC.isCCC c)
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
105
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
106 open CCChom
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
107 open IsCCChom
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
108 open IsoS
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
109
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
110 hom→CCC : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( h : CCChom A ) → CCC A
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
111 hom→CCC A h = record {
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
112 1 = 1
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
113 ; ○ = ○
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
114 ; _∧_ = _/\_
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
115 ; <_,_> = <,>
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
116 ; π = π
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
117 ; π' = π'
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
118 ; _<=_ = _<=_
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
119 ; _* = _*
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
120 ; ε = ε
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
121 ; isCCC = isCCC
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
122 } where
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
123 1 : Obj A
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
124 1 = one h
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
125 ○ : (a : Obj A ) → Hom A a 1
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
126 ○ a = ≅← ( ccc-1 (isCCChom h ) {_} {OneObj} {OneObj} ) OneObj
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
127 _/\_ : Obj A → Obj A → Obj A
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
128 _/\_ a b = _*_ h a b
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
129 <,> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c ( a /\ b)
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
130 <,> f g = ≅← ( ccc-2 (isCCChom h ) ) ( f , g )
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
131 π : {a b : Obj A } → Hom A (a /\ b) a
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
132 π {a} {b} = proj₁ ( ≅→ ( ccc-2 (isCCChom h ) ) (id1 A (_*_ h a b) ))
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
133 π' : {a b : Obj A } → Hom A (a /\ b) b
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
134 π' {a} {b} = proj₂ ( ≅→ ( ccc-2 (isCCChom h ) ) (id1 A (_*_ h a b) ))
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
135 _<=_ : (a b : Obj A ) → Obj A
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
136 _<=_ = _^_ h
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
137 _* : {a b c : Obj A } → Hom A (a /\ b) c → Hom A a (c <= b)
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
138 _* = ≅← ( ccc-3 (isCCChom h ) )
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
139 ε : {a b : Obj A } → Hom A ((a <= b ) /\ b) a
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
140 ε {a} {b} = ≅→ ( ccc-3 (isCCChom h ) {_^_ h a b} {b} ) (id1 A ( _^_ h a b ))
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
141 isCCC : CCC.IsCCC A 1 ○ _/\_ <,> π π' _<=_ _* ε
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
142 isCCC = record {
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
143 e2 = e2
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
144 ; e3a = e3a
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
145 ; e3b = e3b
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
146 ; e3c = e3c
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
147 ; π-cong = π-cong
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
148 ; e4a = e4a
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
149 ; e4b = e4b
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
150 } where
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
151 e2 : {a : Obj A} → ∀ ( f : Hom A a 1 ) → A [ f ≈ ○ a ]
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
152 e2 f = {!!}
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
153 e3a : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π o <,> f g ] ≈ f ]
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
154 e3a = {!!}
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
155 e3b : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π' o <,> f g ] ≈ g ]
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
156 e3b = {!!}
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
157 e3c : {a b c : Obj A} → { h : Hom A c (a /\ b) } → A [ <,> ( A [ π o h ] ) ( A [ π' o h ] ) ≈ h ]
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
158 e3c = {!!}
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
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' ]
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
160 π-cong = {!!}
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
161 e4a : {a b c : Obj A} → { h : Hom A (c /\ b) a } → A [ A [ ε o ( <,> ( A [ (h *) o π ] ) π') ] ≈ h ]
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
162 e4a = {!!}
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
163 e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } → A [ ( A [ ε o ( <,> ( A [ k o π ] ) π' ) ] ) * ≈ k ]
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
164 e4b = {!!}
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
165