annotate CCChom.agda @ 793:f37f11e1b871

Hom a,b = Hom 1 b^a
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 22 Apr 2019 02:41:53 +0900
parents 1e7319868d77
children ba575c73ea48
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
790
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
9 open import Relation.Binary.PropositionalEquality hiding ( [_] )
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 ]
787
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
46 cong→ : {f g : Hom A a b } → A [ f ≈ g ] → B [ ≅→ f ≈ ≅→ g ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
47 cong← : {f g : Hom B a' b'} → B [ f ≈ g ] → A [ ≅← f ≈ ≅← g ]
779
6b4bd02efd80 CCC start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48
783
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
49
784
f27d966939f8 add CCC hom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 783
diff changeset
50 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
51 ( _*_ : 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
52 field
785
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
53 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
54 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
55 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
56 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
57 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
58 IsoS A A a (c ^ b) (a * b) c
788
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
59 nat-2 : {a b c : Obj A} → {f : Hom A (b * c) (b * c) } → {g : Hom A a (b * c) }
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
60 → (A × A) [ (A × A) [ IsoS.≅→ ccc-2 f o (g , g) ] ≈ IsoS.≅→ ccc-2 ( A [ f o g ] ) ]
789
4e1e2f7199c8 CCC Hom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 788
diff changeset
61 nat-3 : {a b c : Obj A} → { k : Hom A c (a ^ b ) } → A [ A [ IsoS.≅→ (ccc-3) (id1 A (a ^ b)) o
4e1e2f7199c8 CCC Hom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 788
diff changeset
62 (IsoS.≅← (ccc-2 ) (A [ k o (proj₁ ( IsoS.≅→ ccc-2 (id1 A (c * b)))) ] ,
4e1e2f7199c8 CCC Hom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 788
diff changeset
63 (proj₂ ( IsoS.≅→ ccc-2 (id1 A (c * b) ))))) ] ≈ IsoS.≅→ (ccc-3 ) k ]
788
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
64
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
65 open import CCC
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
66
779
6b4bd02efd80 CCC start
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67
784
f27d966939f8 add CCC hom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 783
diff changeset
68 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
69 field
340708e8d54f fix for 2.5.4.2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 780
diff changeset
70 one : Obj A
340708e8d54f fix for 2.5.4.2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 780
diff changeset
71 _*_ : 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
72 _^_ : Obj A → Obj A → Obj A
784
f27d966939f8 add CCC hom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 783
diff changeset
73 isCCChom : IsCCChom A one _*_ _^_
783
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
74
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
75 open import HomReasoning
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
76
784
f27d966939f8 add CCC hom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 783
diff changeset
77 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
78 CCC→hom A c = record {
f27d966939f8 add CCC hom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 783
diff changeset
79 one = CCC.1 c
f27d966939f8 add CCC hom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 783
diff changeset
80 ; _*_ = CCC._∧_ c
f27d966939f8 add CCC hom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 783
diff changeset
81 ; _^_ = CCC._<=_ c
f27d966939f8 add CCC hom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 783
diff changeset
82 ; isCCChom = record {
787
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
83 ccc-1 = λ {a} {b} {c'} → record { ≅→ = c101 ; ≅← = c102 ; iso→ = c103 {a} {b} {c'} ; iso← = c104 ; cong← = c105 ; cong→ = c106 }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
84 ; ccc-2 = record { ≅→ = c201 ; ≅← = c202 ; iso→ = c203 ; iso← = c204 ; cong← = c205; cong→ = c206 }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
85 ; ccc-3 = record { ≅→ = c301 ; ≅← = c302 ; iso→ = c303 ; iso← = c304 ; cong← = c305 ; cong→ = c306 }
789
4e1e2f7199c8 CCC Hom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 788
diff changeset
86 ; nat-2 = nat-2 ; nat-3 = nat-3
784
f27d966939f8 add CCC hom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 783
diff changeset
87 }
785
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
88 } where
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
89 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
90 c101 _ = OneObj
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
91 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
92 c102 {a} OneObj = CCC.○ c a
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
93 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
94 c103 {a} {OneObj} {OneObj} {OneObj} = refl
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
95 c104 : {a : Obj A} → {f : Hom A a (CCC.1 c)} → A [ (c102 ( c101 f )) ≈ f ]
793
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
96 c104 {a} {f} = let open ≈-Reasoning A in HomReasoning.≈-Reasoning.sym A (IsCCC.e2 (CCC.isCCC c) )
785
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
97 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
98 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
99 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
100 c202 (f , g ) = CCC.<_,_> c f g
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
101 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
102 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
103 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
104 c204 = IsCCC.e3c (CCC.isCCC c)
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
105 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
106 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
107 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
108 c302 f = CCC._* c f
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
109 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
110 c303 = IsCCC.e4a (CCC.isCCC c)
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
111 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
112 c304 = IsCCC.e4b (CCC.isCCC c)
787
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
113 c105 : {a : Obj A } {f g : Hom OneCat OneObj OneObj} → _[_≈_] OneCat {OneObj} {OneObj} f g → A [ c102 {a} f ≈ c102 {a} g ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
114 c105 refl = let open ≈-Reasoning A in refl-hom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
115 c106 : { a : Obj A } {f g : Hom A a (CCC.1 c)} → A [ f ≈ g ] → _[_≈_] OneCat {OneObj} {OneObj} OneObj OneObj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
116 c106 _ = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
117 c205 : { a b c₁ : Obj A } {f g : Hom (A × A) (c₁ , c₁) (a , b)} → (A × A) [ f ≈ g ] → A [ c202 f ≈ c202 g ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
118 c205 f=g = IsCCC.π-cong (CCC.isCCC c ) (proj₁ f=g ) (proj₂ f=g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
119 c206 : { a b c₁ : Obj A } {f g : Hom A c₁ ((c CCC.∧ a) b)} → A [ f ≈ g ] → (A × A) [ c201 f ≈ c201 g ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
120 c206 {a} {b} {c₁} {f} {g} f=g = ( begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
121 CCC.π c o f
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
122 ≈⟨ cdr f=g ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
123 CCC.π c o g
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
124 ∎ ) , ( begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
125 CCC.π' c o f
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
126 ≈⟨ cdr f=g ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
127 CCC.π' c o g
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
128 ∎ ) where open ≈-Reasoning A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
129 c305 : { a b c₁ : Obj A } {f g : Hom A ((c CCC.∧ a) b) c₁} → A [ f ≈ g ] → A [ (c CCC.*) f ≈ (c CCC.*) g ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
130 c305 f=g = IsCCC.*-cong (CCC.isCCC c ) f=g
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
131 c306 : { a b c₁ : Obj A } {f g : Hom A a ((c CCC.<= c₁) b)} → A [ f ≈ g ] → A [ c301 f ≈ c301 g ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
132 c306 {a} {b} {c₁} {f} {g} f=g = begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
133 CCC.ε c o CCC.<_,_> c ( f o CCC.π c ) ( CCC.π' c )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
134 ≈⟨ cdr ( IsCCC.π-cong (CCC.isCCC c ) (car f=g ) refl-hom) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
135 CCC.ε c o CCC.<_,_> c ( g o CCC.π c ) ( CCC.π' c )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
136 ∎ where open ≈-Reasoning A
788
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
137 nat-2 : {a b : Obj A} {c = c₁ : Obj A} {f : Hom A ((c CCC.∧ b) c₁) ((c CCC.∧ b) c₁)}
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
138 {g : Hom A a ((c CCC.∧ b) c₁)} → (A × A) [ (A × A) [ c201 f o g , g ] ≈ c201 (A [ f o g ]) ]
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
139 nat-2 {a} {b} {c₁} {f} {g} = ( begin
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
140 ( CCC.π c o f) o g
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
141 ≈↑⟨ assoc ⟩
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
142 ( CCC.π c ) o (f o g)
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
143 ∎ ) , (sym-hom assoc) where open ≈-Reasoning A
789
4e1e2f7199c8 CCC Hom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 788
diff changeset
144 nat-3 : {a b : Obj A} {c = c₁ : Obj A} {k : Hom A c₁ ((c CCC.<= a) b)} →
4e1e2f7199c8 CCC Hom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 788
diff changeset
145 A [ A [ c301 (id1 A ((c CCC.<= a) b)) o c202 (A [ k o proj₁ (c201 (id1 A ((c CCC.∧ c₁) b))) ] , proj₂ (c201 (id1 A ((c CCC.∧ c₁) b)))) ]
4e1e2f7199c8 CCC Hom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 788
diff changeset
146 ≈ c301 k ]
4e1e2f7199c8 CCC Hom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 788
diff changeset
147 nat-3 {a} {b} { c₁} {k} = begin
4e1e2f7199c8 CCC Hom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 788
diff changeset
148 c301 (id1 A ((c CCC.<= a) b)) o c202 ( k o proj₁ (c201 (id1 A ((c CCC.∧ c₁) b))) , proj₂ (c201 (id1 A ((c CCC.∧ c₁) b))))
4e1e2f7199c8 CCC Hom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 788
diff changeset
149 ≈⟨⟩
4e1e2f7199c8 CCC Hom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 788
diff changeset
150 ( CCC.ε c o CCC.<_,_> c ((id1 A (CCC._<=_ c a b )) o CCC.π c) (CCC.π' c))
4e1e2f7199c8 CCC Hom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 788
diff changeset
151 o (CCC.<_,_> c (k o ( CCC.π c o (id1 A (CCC._∧_ c c₁ b )))) ( CCC.π' c o (id1 A (CCC._∧_ c c₁ b))))
4e1e2f7199c8 CCC Hom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 788
diff changeset
152 ≈↑⟨ assoc ⟩
4e1e2f7199c8 CCC Hom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 788
diff changeset
153 (CCC.ε c) o (( CCC.<_,_> c ((id1 A (CCC._<=_ c a b )) o CCC.π c) (CCC.π' c))
4e1e2f7199c8 CCC Hom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 788
diff changeset
154 o (CCC.<_,_> c (k o ( CCC.π c o (id1 A (CCC._∧_ c c₁ b )))) ( CCC.π' c o (id1 A (CCC._∧_ c c₁ b)))))
4e1e2f7199c8 CCC Hom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 788
diff changeset
155 ≈⟨ cdr (car (IsCCC.π-cong (CCC.isCCC c ) idL refl-hom ) ) ⟩
4e1e2f7199c8 CCC Hom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 788
diff changeset
156 (CCC.ε c) o ( CCC.<_,_> c (CCC.π c) (CCC.π' c)
4e1e2f7199c8 CCC Hom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 788
diff changeset
157 o (CCC.<_,_> c (k o ( CCC.π c o (id1 A (CCC._∧_ c c₁ b )))) ( CCC.π' c o (id1 A (CCC._∧_ c c₁ b)))))
4e1e2f7199c8 CCC Hom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 788
diff changeset
158 ≈⟨ cdr (car (IsCCC.π-id (CCC.isCCC c))) ⟩
4e1e2f7199c8 CCC Hom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 788
diff changeset
159 (CCC.ε c) o ( id1 A (CCC._∧_ c ((c CCC.<= a) b) b )
4e1e2f7199c8 CCC Hom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 788
diff changeset
160 o (CCC.<_,_> c (k o ( CCC.π c o (id1 A (CCC._∧_ c c₁ b )))) ( CCC.π' c o (id1 A (CCC._∧_ c c₁ b)))))
4e1e2f7199c8 CCC Hom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 788
diff changeset
161 ≈⟨ cdr ( cdr ( IsCCC.π-cong (CCC.isCCC c) (cdr idR) idR )) ⟩
4e1e2f7199c8 CCC Hom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 788
diff changeset
162 (CCC.ε c) o ( id1 A (CCC._∧_ c ((c CCC.<= a) b) b ) o (CCC.<_,_> c (k o ( CCC.π c )) ( CCC.π' c )))
4e1e2f7199c8 CCC Hom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 788
diff changeset
163 ≈⟨ cdr idL ⟩
4e1e2f7199c8 CCC Hom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 788
diff changeset
164 (CCC.ε c) o (CCC.<_,_> c ( k o (CCC.π c) ) (CCC.π' c))
4e1e2f7199c8 CCC Hom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 788
diff changeset
165 ≈⟨⟩
4e1e2f7199c8 CCC Hom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 788
diff changeset
166 c301 k
4e1e2f7199c8 CCC Hom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 788
diff changeset
167 ∎ where open ≈-Reasoning A
788
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
168
793
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
169 lemma1 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( ccc : CCC A ) → {a b c : Obj A} → -- Hom A 1 ( c ^ b ) ≅ Hom A b c
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
170 IsoS A A (CCC.1 ccc ) (CCC._<=_ ccc c b) b c
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
171 lemma1 A ccc {a} {b} {c} = record {
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
172 ≅→ = λ f → A [ CCC.ε ccc o CCC.<_,_> ccc ( A [ f o CCC.○ ccc b ] ) ( id1 A b ) ]
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
173 ; ≅← = λ f → CCC._* ccc ( A [ f o CCC.π' ccc ] )
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
174 ; iso→ = iso→
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
175 ; iso← = iso←
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
176 ; cong→ = cong*
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
177 ; cong← = cong2
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
178 } where
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
179 cc = IsCCChom.ccc-3 ( CCChom.isCCChom (CCC→hom A ccc ) )
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
180 -- e4a : {a b c : Obj A} → { k : Hom A (c /\ b) a } → A [ A [ ε o ( <,> ( A [ (k *) o π ] ) π') ] ≈ k ]
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
181 iso→ : {f : Hom A b c} → A [
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
182 (A Category.o CCC.ε ccc) (CCC.< ccc , (A Category.o (ccc CCC.*) ((A Category.o f) (CCC.π' ccc))) (CCC.○ ccc b) > (Category.Category.Id A)) ≈ f ]
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
183 iso→ {f} = begin
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
184 CCC.ε ccc o (CCC.<_,_> ccc (CCC._* ccc ( f o (CCC.π' ccc)) o (CCC.○ ccc b)) (id1 A b ) )
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
185 ≈↑⟨ cdr ( IsCCC.π-cong ( CCC.isCCC ccc ) refl-hom (IsCCC.e3b (CCC.isCCC ccc) ) ) ⟩
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
186 CCC.ε ccc o ( CCC.<_,_> ccc (CCC._* ccc (f o CCC.π' ccc) o CCC.○ ccc b) ((CCC.π' ccc) o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) ) )
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
187 ≈↑⟨ cdr ( IsCCC.π-cong ( CCC.isCCC ccc ) (cdr (IsCCC.e3a (CCC.isCCC ccc))) refl-hom ) ⟩
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
188 CCC.ε ccc o ( CCC.<_,_> ccc (CCC._* ccc (f o CCC.π' ccc) o ( CCC.π ccc o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) ) ) ((CCC.π' ccc) o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) ) )
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
189 ≈⟨ cdr ( IsCCC.π-cong ( CCC.isCCC ccc ) assoc refl-hom ) ⟩
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
190 CCC.ε ccc o ( CCC.<_,_> ccc ((CCC._* ccc (f o CCC.π' ccc) o CCC.π ccc ) o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) ) ((CCC.π' ccc) o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) ) )
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
191 ≈↑⟨ cdr ( IsCCC.distr ( CCC.isCCC ccc ) ) ⟩
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
192 CCC.ε ccc o ( CCC.<_,_> ccc (CCC._* ccc (f o CCC.π' ccc) o CCC.π ccc ) (CCC.π' ccc) o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) )
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
193 ≈⟨ assoc ⟩
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
194 ( CCC.ε ccc o CCC.<_,_> ccc (CCC._* ccc (f o CCC.π' ccc) o CCC.π ccc ) (CCC.π' ccc) ) o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b)
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
195 ≈⟨ car ( IsCCC.e4a (CCC.isCCC ccc) ) ⟩
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
196 ( f o CCC.π' ccc ) o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b)
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
197 ≈↑⟨ assoc ⟩
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
198 f o ( CCC.π' ccc o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) )
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
199 ≈⟨ cdr (IsCCC.e3b (CCC.isCCC ccc)) ⟩
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
200 f o id1 A b
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
201 ≈⟨ idR ⟩
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
202 f
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
203 ∎ where open ≈-Reasoning A
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
204 lemma : {f : Hom A (CCC.1 ccc) ((ccc CCC.<= c) b)} → A [ A [ A [ f o (CCC.○ ccc b) ] o (CCC.π' ccc) ] ≈ A [ f o (CCC.π ccc) ] ]
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
205 lemma {f} = begin
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
206 ( f o (CCC.○ ccc b) ) o (CCC.π' ccc)
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
207 ≈↑⟨ assoc ⟩
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
208 f o ( (CCC.○ ccc b) o (CCC.π' ccc) )
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
209 ≈⟨ cdr ( IsCCC.e2 (CCC.isCCC ccc) ) ⟩
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
210 f o (CCC.○ ccc ( CCC._∧_ ccc (CCC.1 ccc) b ) )
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
211 ≈↑⟨ cdr ( IsCCC.e2 (CCC.isCCC ccc) ) ⟩
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
212 f o ( (CCC.○ ccc) (CCC.1 ccc) o (CCC.π ccc) )
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
213 ≈↑⟨ cdr ( car ( IsCCC.e2 (CCC.isCCC ccc) )) ⟩
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
214 f o ( id1 A (CCC.1 ccc) o (CCC.π ccc) )
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
215 ≈⟨ cdr (idL) ⟩
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
216 f o (CCC.π ccc)
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
217 ∎ where open ≈-Reasoning A
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
218 -- e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } → A [ ( A [ ε o ( <,> ( A [ k o π ] ) π' ) ] ) * ≈ k ]
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
219 iso← : {f : Hom A (CCC.1 ccc) ((ccc CCC.<= c) b)} → A [ (ccc CCC.*) ((A Category.o (A Category.o CCC.ε ccc) (CCC.< ccc , (A Category.o f) (CCC.○ ccc b) >
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
220 (Category.Category.Id A))) (CCC.π' ccc)) ≈ f ]
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
221 iso← {f} = begin
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
222 CCC._* ccc (( CCC.ε ccc o ( CCC.<_,_> ccc ( f o (CCC.○ ccc b) ) (id1 A b ))) o (CCC.π' ccc))
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
223 ≈↑⟨ IsCCC.*-cong ( CCC.isCCC ccc ) assoc ⟩
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
224 CCC._* ccc ( CCC.ε ccc o (( CCC.<_,_> ccc ( f o (CCC.○ ccc b) ) (id1 A b )) o (CCC.π' ccc)))
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
225 ≈⟨ IsCCC.*-cong ( CCC.isCCC ccc ) (cdr ( IsCCC.distr ( CCC.isCCC ccc ) ) ) ⟩
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
226 CCC._* ccc ( CCC.ε ccc o CCC.<_,_> ccc ( (f o (CCC.○ ccc b)) o CCC.π' ccc ) (id1 A b o CCC.π' ccc) )
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
227 ≈⟨ IsCCC.*-cong ( CCC.isCCC ccc ) (cdr ( IsCCC.π-cong ( CCC.isCCC ccc ) lemma idL )) ⟩
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
228 CCC._* ccc ( CCC.ε ccc o CCC.<_,_> ccc ( f o CCC.π ccc ) (CCC.π' ccc) )
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
229 ≈⟨ IsCCC.e4b (CCC.isCCC ccc) ⟩
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
230 f
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
231 ∎ where open ≈-Reasoning A
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
232 cong* : {f g : Hom A (CCC.1 ccc) ((ccc CCC.<= c) b)} →
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
233 A [ f ≈ g ] → A [ (A Category.o CCC.ε ccc) (CCC.< ccc , (A Category.o f) (CCC.○ ccc b) > (Category.Category.Id A))
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
234 ≈ (A Category.o CCC.ε ccc) (CCC.< ccc , (A Category.o g) (CCC.○ ccc b) > (Category.Category.Id A)) ]
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
235 cong* {f} {g} f≈g = begin
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
236 CCC.ε ccc o ( CCC.<_,_> ccc ( f o ( CCC.○ ccc b )) (id1 A b ))
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
237 ≈⟨ cdr (IsCCC.π-cong ( CCC.isCCC ccc ) (car f≈g) refl-hom ) ⟩
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
238 CCC.ε ccc o ( CCC.<_,_> ccc ( g o ( CCC.○ ccc b )) (id1 A b ))
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
239 ∎ where open ≈-Reasoning A
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
240 cong2 : {f g : Hom A b c} → A [ f ≈ g ] →
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
241 A [ (ccc CCC.*) ((A Category.o f) (CCC.π' ccc)) ≈ (ccc CCC.*) ((A Category.o g) (CCC.π' ccc)) ]
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
242 cong2 {f} {g} f≈g = begin
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
243 CCC._* ccc ( f o (CCC.π' ccc) )
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
244 ≈⟨ IsCCC.*-cong ( CCC.isCCC ccc ) (car f≈g ) ⟩
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
245 CCC._* ccc ( g o (CCC.π' ccc) )
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
246 ∎ where open ≈-Reasoning A
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
247
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
248
787
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
249
785
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
250
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
251 open CCChom
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
252 open IsCCChom
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
253 open IsoS
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
254
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
255 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
256 hom→CCC A h = record {
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
257 1 = 1
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
258 ; ○ = ○
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
259 ; _∧_ = _/\_
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
260 ; <_,_> = <,>
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
261 ; π = π
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
262 ; π' = π'
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
263 ; _<=_ = _<=_
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
264 ; _* = _*
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
265 ; ε = ε
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
266 ; isCCC = isCCC
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
267 } where
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
268 1 : Obj A
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
269 1 = one h
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
270 ○ : (a : Obj A ) → Hom A a 1
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
271 ○ 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
272 _/\_ : Obj A → Obj A → Obj A
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
273 _/\_ a b = _*_ h a b
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
274 <,> : {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
275 <,> 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
276 π : {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
277 π {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
278 π' : {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
279 π' {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
280 _<=_ : (a b : Obj A ) → Obj A
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
281 _<=_ = _^_ h
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
282 _* : {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
283 _* = ≅← ( ccc-3 (isCCChom h ) )
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
284 ε : {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
285 ε {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
286 isCCC : CCC.IsCCC A 1 ○ _/\_ <,> π π' _<=_ _* ε
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
287 isCCC = record {
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
288 e2 = e2
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
289 ; e3a = e3a
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
290 ; e3b = e3b
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
291 ; e3c = e3c
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
292 ; π-cong = π-cong
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
293 ; e4a = e4a
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
294 ; e4b = e4b
787
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
295 ; *-cong = *-cong
785
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
296 } where
786
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
297 e20 : ∀ ( f : Hom OneCat OneObj OneObj ) → _[_≈_] OneCat {OneObj} {OneObj} f OneObj
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
298 e20 OneObj = refl
793
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
299 e2 : {a : Obj A} → ∀ { f : Hom A a 1 } → A [ f ≈ ○ a ]
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
300 e2 {a} {f} = begin
786
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
301 f
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
302 ≈↑⟨ iso← ( ccc-1 (isCCChom h )) ⟩
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
303 ≅← ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj}) ( ≅→ ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) f )
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
304 ≈⟨ ≡-cong {Level.zero} {Level.zero} {Level.zero} {OneCat} {OneObj} {OneObj} (
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
305 λ y → ≅← ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) y ) (e20 ( ≅→ ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) f) ) ⟩
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
306 ≅← ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) OneObj
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
307 ≈⟨⟩
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
308 ○ a
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
309 ∎ where open ≈-Reasoning A
787
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
310 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
311 -- g id
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
312 -- a -------------> b * c ------> b * c
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
313 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
314 -- a -------------> b * c ------> b
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
315 -- a -------------> b * c ------> c
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
316 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
317 cong-proj₁ : {a b c d : Obj A} → { f g : Hom (A × A) ( a , b ) ( c , d ) } → (A × A) [ f ≈ g ] → A [ proj₁ f ≈ proj₁ g ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
318 cong-proj₁ eq = proj₁ eq
788
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
319 cong-proj₂ : {a b c d : Obj A} → { f g : Hom (A × A) ( a , b ) ( c , d ) } → (A × A) [ f ≈ g ] → A [ proj₂ f ≈ proj₂ g ]
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
320 cong-proj₂ eq = proj₂ eq
785
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
321 e3a : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π o <,> f g ] ≈ f ]
786
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
322 e3a {a} {b} {c} {f} {g} = begin
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
323 π o <,> f g
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
324 ≈⟨⟩
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
325 proj₁ (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b) )) o (≅← (ccc-2 (isCCChom h)) (f , g))
788
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
326 ≈⟨ cong-proj₁ (nat-2 (isCCChom h)) ⟩
787
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
327 proj₁ (≅→ (ccc-2 (isCCChom h)) (( id1 A ( _*_ h a b )) o ( ≅← (ccc-2 (isCCChom h)) (f , g) ) ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
328 ≈⟨ cong-proj₁ ( cong→ (ccc-2 (isCCChom h)) idL ) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
329 proj₁ (≅→ (ccc-2 (isCCChom h)) ( ≅← (ccc-2 (isCCChom h)) (f , g) ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
330 ≈⟨ cong-proj₁ ( iso→ (ccc-2 (isCCChom h))) ⟩
786
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
331 proj₁ ( f , g )
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
332 ≈⟨⟩
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
333 f
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
334 ∎ where open ≈-Reasoning A
785
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
335 e3b : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π' o <,> f g ] ≈ g ]
788
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
336 e3b {a} {b} {c} {f} {g} = begin
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
337 π' o <,> f g
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
338 ≈⟨⟩
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
339 proj₂ (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b) )) o (≅← (ccc-2 (isCCChom h)) (f , g))
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
340 ≈⟨ cong-proj₂ (nat-2 (isCCChom h)) ⟩
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
341 proj₂ (≅→ (ccc-2 (isCCChom h)) (( id1 A ( _*_ h a b )) o ( ≅← (ccc-2 (isCCChom h)) (f , g) ) ))
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
342 ≈⟨ cong-proj₂ ( cong→ (ccc-2 (isCCChom h)) idL ) ⟩
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
343 proj₂ (≅→ (ccc-2 (isCCChom h)) ( ≅← (ccc-2 (isCCChom h)) (f , g) ))
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
344 ≈⟨ cong-proj₂ ( iso→ (ccc-2 (isCCChom h))) ⟩
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
345 proj₂ ( f , g )
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
346 ≈⟨⟩
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
347 g
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
348 ∎ where open ≈-Reasoning A
785
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
349 e3c : {a b c : Obj A} → { h : Hom A c (a /\ b) } → A [ <,> ( A [ π o h ] ) ( A [ π' o h ] ) ≈ h ]
788
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
350 e3c {a} {b} {c} {f} = begin
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
351 <,> ( π o f ) ( π' o f )
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
352 ≈⟨⟩
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
353 ≅← (ccc-2 (isCCChom h)) ( ( proj₁ (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b) ))) o f
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
354 , ( proj₂ (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b)))) o f )
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
355 ≈⟨⟩
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
356 ≅← (ccc-2 (isCCChom h)) (_[_o_] (A × A) (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b) )) (f , f ) )
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
357 ≈⟨ cong← (ccc-2 (isCCChom h)) (nat-2 (isCCChom h)) ⟩
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
358 ≅← (ccc-2 (isCCChom h)) (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b) o f ))
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
359 ≈⟨ cong← (ccc-2 (isCCChom h)) (cong→ (ccc-2 (isCCChom h)) idL ) ⟩
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
360 ≅← (ccc-2 (isCCChom h)) (≅→ (ccc-2 (isCCChom h)) f )
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
361 ≈⟨ iso← (ccc-2 (isCCChom h)) ⟩
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
362 f
a3e124e36acf nat in ccc-2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 787
diff changeset
363 ∎ where open ≈-Reasoning A
785
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
364 π-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' ]
786
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
365 π-cong {a} {b} {c} {f} {f'} {g} {g'} eq1 eq2 = begin
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
366 <,> f g
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
367 ≈⟨⟩
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
368 ≅← (ccc-2 (isCCChom h)) (f , g)
787
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
369 ≈⟨ cong← (ccc-2 (isCCChom h)) ( eq1 , eq2 ) ⟩
786
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
370 ≅← (ccc-2 (isCCChom h)) (f' , g')
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
371 ≈⟨⟩
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
372 <,> f' g'
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
373 ∎ where open ≈-Reasoning A
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
374 e4a : {a b c : Obj A} → { k : Hom A (c /\ b) a } → A [ A [ ε o ( <,> ( A [ (k *) o π ] ) π') ] ≈ k ]
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
375 e4a {a} {b} {c} {k} = begin
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
376 ε o ( <,> ((k *) o π ) π' )
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
377 ≈⟨⟩
787
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
378 ≅→ (ccc-3 (isCCChom h)) (id1 A (_^_ h a b)) o (≅← (ccc-2 (isCCChom h)) ((( ≅← (ccc-3 (isCCChom h)) k) o π ) , π'))
789
4e1e2f7199c8 CCC Hom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 788
diff changeset
379 ≈⟨ nat-3 (isCCChom h) ⟩
787
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
380 ≅→ (ccc-3 (isCCChom h)) (≅← (ccc-3 (isCCChom h)) k)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
381 ≈⟨ iso→ (ccc-3 (isCCChom h)) ⟩
786
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
382 k
287d25c87b60 on going CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 785
diff changeset
383 ∎ where open ≈-Reasoning A
785
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
384 e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } → A [ ( A [ ε o ( <,> ( A [ k o π ] ) π' ) ] ) * ≈ k ]
787
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
385 e4b {a} {b} {c} {k} = begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
386 ( ε o ( <,> ( k o π ) π' ) ) *
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
387 ≈⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
388 ≅← (ccc-3 (isCCChom h)) ( ≅→ ( ccc-3 (isCCChom h ) {_^_ h a b} {b} ) (id1 A ( _^_ h a b )) o (≅← (ccc-2 (isCCChom h)) ( k o π , π')))
789
4e1e2f7199c8 CCC Hom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 788
diff changeset
389 ≈⟨ cong← (ccc-3 (isCCChom h)) (nat-3 (isCCChom h)) ⟩
787
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
390 ≅← (ccc-3 (isCCChom h)) (≅→ (ccc-3 (isCCChom h)) k)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
391 ≈⟨ iso← (ccc-3 (isCCChom h)) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
392 k
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
393 ∎ where open ≈-Reasoning A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
394 *-cong : {a b c : Obj A} {f f' : Hom A (a /\ b) c} → A [ f ≈ f' ] → A [ f * ≈ f' * ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
395 *-cong eq = cong← ( ccc-3 (isCCChom h )) eq
785
a67959bcd44b ccc → hom on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 784
diff changeset
396
790
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
397 open import Category.Sets
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
398
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
399 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
400
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
401 data One' {l : Level} : Set l where
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
402 OneObj' : One' -- () in Haskell ( or any one object set )
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
403
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
404 sets : {l : Level } → CCC (Sets {l})
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
405 sets {l} = record {
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
406 1 = One'
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
407 ; ○ = λ _ → λ _ → OneObj'
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
408 ; _∧_ = _/\_
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
409 ; <_,_> = <,>
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
410 ; π = π
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
411 ; π' = π'
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
412 ; _<=_ = _<=_
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
413 ; _* = _*
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
414 ; ε = ε
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
415 ; isCCC = isCCC
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
416 } where
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
417 1 : Obj Sets
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
418 1 = One'
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
419 ○ : (a : Obj Sets ) → Hom Sets a 1
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
420 ○ a = λ _ → OneObj'
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
421 _/\_ : Obj Sets → Obj Sets → Obj Sets
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
422 _/\_ a b = a ∧ b
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
423 <,> : {a b c : Obj Sets } → Hom Sets c a → Hom Sets c b → Hom Sets c ( a /\ b)
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
424 <,> f g = λ x → ( f x , g x )
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
425 π : {a b : Obj Sets } → Hom Sets (a /\ b) a
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
426 π {a} {b} = proj₁
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
427 π' : {a b : Obj Sets } → Hom Sets (a /\ b) b
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
428 π' {a} {b} = proj₂
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
429 _<=_ : (a b : Obj Sets ) → Obj Sets
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
430 a <= b = b → a
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
431 _* : {a b c : Obj Sets } → Hom Sets (a /\ b) c → Hom Sets a (c <= b)
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
432 f * = λ x → λ y → f ( x , y )
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
433 ε : {a b : Obj Sets } → Hom Sets ((a <= b ) /\ b) a
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
434 ε {a} {b} = λ x → ( proj₁ x ) ( proj₂ x )
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
435 isCCC : CCC.IsCCC Sets 1 ○ _/\_ <,> π π' _<=_ _* ε
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
436 isCCC = record {
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
437 e2 = e2
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
438 ; 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
439 ; 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
440 ; e3c = e3c
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
441 ; π-cong = π-cong
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
442 ; e4a = e4a
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
443 ; e4b = e4b
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
444 ; *-cong = *-cong
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
445 } where
793
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
446 e2 : {a : Obj Sets} {f : Hom Sets a 1} → Sets [ f ≈ ○ a ]
f37f11e1b871 Hom a,b = Hom 1 b^a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 790
diff changeset
447 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
448 where
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
449 e20 : (x : a ) → f x ≡ ○ a x
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
450 e20 x with f x
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
451 e20 x | OneObj' = refl
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
452 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
453 Sets [ ( Sets [ π o ( <,> f g) ] ) ≈ f ]
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
454 e3a = refl
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
455 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
456 Sets [ Sets [ π' o ( <,> f g ) ] ≈ g ]
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
457 e3b = refl
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
458 e3c : {a b c : Obj Sets} {h : Hom Sets c (a /\ b)} →
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
459 Sets [ <,> (Sets [ π o h ]) (Sets [ π' o h ]) ≈ h ]
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
460 e3c = refl
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
461 π-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
462 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
463 π-cong refl refl = refl
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
464 e4a : {a b c : Obj Sets} {h : Hom Sets (c /\ b) a} →
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
465 Sets [ Sets [ ε o <,> (Sets [ h * o π ]) π' ] ≈ h ]
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
466 e4a = refl
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
467 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
468 Sets [ (Sets [ ε o <,> (Sets [ k o π ]) π' ]) * ≈ k ]
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
469 e4b = refl
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
470 *-cong : {a b c : Obj Sets} {f f' : Hom Sets (a /\ b) c} →
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
471 Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ]
1e7319868d77 Sets is CCC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 789
diff changeset
472 *-cong refl = refl
787
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
473
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 786
diff changeset
474