|
779
|
1 open import Level
|
|
|
2 open import Category
|
|
|
3 module CCC where
|
|
|
4
|
|
|
5 open import HomReasoning
|
|
|
6 open import cat-utility
|
|
780
|
7 open import Relation.Binary.PropositionalEquality
|
|
779
|
8
|
|
783
|
9
|
|
|
10 open import HomReasoning
|
|
|
11
|
|
784
|
12 record IsCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
|
|
783
|
13 ( １ : Obj A )
|
|
|
14 ( ○ : (a : Obj A ) → Hom A a １ )
|
|
|
15 ( _∧_ : Obj A → Obj A → Obj A )
|
|
|
16 ( <_,_> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c (a ∧ b) )
|
|
|
17 ( π : {a b : Obj A } → Hom A (a ∧ b) a )
|
|
|
18 ( π' : {a b : Obj A } → Hom A (a ∧ b) b )
|
|
|
19 ( _<=_ : (a b : Obj A ) → Obj A )
|
|
|
20 ( _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b) )
|
|
|
21 ( ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a )
|
|
|
22 : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
|
|
|
23 field
|
|
|
24 -- cartesian
|
|
|
25 e2 : {a : Obj A} → ∀ ( f : Hom A a １ ) → A [ f ≈ ○ a ]
|
|
|
26 e3a : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π o < f , g > ] ≈ f ]
|
|
|
27 e3b : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π' o < f , g > ] ≈ g ]
|
|
|
28 e3c : {a b c : Obj A} → { h : Hom A c (a ∧ b) } → A [ < A [ π o h ] , A [ π' o h ] > ≈ h ]
|
|
785
|
29 π-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' > ]
|
|
783
|
30 -- closed
|
|
|
31 e4a : {a b c : Obj A} → { h : Hom A (c ∧ b) a } → A [ A [ ε o < A [ (h *) o π ] , π' > ] ≈ h ]
|
|
|
32 e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } → A [ ( A [ ε o < A [ k o π ] , π' > ] ) * ≈ k ]
|
|
787
|
33 *-cong : {a b c : Obj A} → { f f' : Hom A (a ∧ b) c } → A [ f ≈ f' ] → A [ f * ≈ f' * ]
|
|
779
|
34
|
|
783
|
35 e'2 : A [ ○ １ ≈ id1 A １ ]
|
|
|
36 e'2 = let open ≈-Reasoning A in begin
|
|
|
37 ○ １
|
|
|
38 ≈↑⟨ e2 (id1 A １ ) ⟩
|
|
|
39 id1 A １
|
|
|
40 ∎
|
|
|
41 e''2 : {a b : Obj A} {f : Hom A a b } → A [ A [ ○ b o f ] ≈ ○ a ]
|
|
|
42 e''2 {a} {b} {f} = let open ≈-Reasoning A in begin
|
|
|
43 ○ b o f
|
|
|
44 ≈⟨ e2 (○ b o f) ⟩
|
|
|
45 ○ a
|
|
|
46 ∎
|
|
789
|
47 π-id : {a b : Obj A} → A [ < π , π' > ≈ id1 A (a ∧ b ) ]
|
|
|
48 π-id {a} {b} = let open ≈-Reasoning A in begin
|
|
|
49 < π , π' >
|
|
|
50 ≈↑⟨ π-cong idR idR ⟩
|
|
|
51 < π o id1 A (a ∧ b) , π' o id1 A (a ∧ b) >
|
|
|
52 ≈⟨ e3c ⟩
|
|
|
53 id1 A (a ∧ b )
|
|
|
54 ∎
|
|
783
|
55 distr : {a b c d : Obj A} {f : Hom A c a }{g : Hom A c b } {h : Hom A d c } → A [ A [ < f , g > o h ] ≈ < A [ f o h ] , A [ g o h ] > ]
|
|
|
56 distr {a} {b} {c} {d} {f} {g} {h} = let open ≈-Reasoning A in begin
|
|
|
57 < f , g > o h
|
|
|
58 ≈↑⟨ e3c ⟩
|
|
|
59 < π o < f , g > o h , π' o < f , g > o h >
|
|
785
|
60 ≈⟨ π-cong assoc assoc ⟩
|
|
|
61 < ( π o < f , g > ) o h , (π' o < f , g > ) o h >
|
|
|
62 ≈⟨ π-cong (car e3a ) (car e3b) ⟩
|
|
783
|
63 < f o h , g o h >
|
|
|
64 ∎
|
|
|
65 _×_ : { a b c d e : Obj A } ( f : Hom A a d ) (g : Hom A b e ) ( h : Hom A c (a ∧ b) ) → Hom A c ( d ∧ e )
|
|
|
66 f × g = λ h → < A [ f o A [ π o h ] ] , A [ g o A [ π' o h ] ] >
|
|
|
67
|
|
784
|
68 record CCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
|
|
781
|
69 field
|
|
783
|
70 １ : Obj A
|
|
|
71 ○ : (a : Obj A ) → Hom A a １
|
|
|
72 _∧_ : Obj A → Obj A → Obj A
|
|
|
73 <_,_> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c (a ∧ b)
|
|
|
74 π : {a b : Obj A } → Hom A (a ∧ b) a
|
|
|
75 π' : {a b : Obj A } → Hom A (a ∧ b) b
|
|
|
76 _<=_ : (a b : Obj A ) → Obj A
|
|
|
77 _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b)
|
|
|
78 ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a
|
|
784
|
79 isCCC : IsCCC A １ ○ _∧_ <_,_> π π' _<=_ _* ε
|
|
781
|
80
|
|
783
|
81
|
|
|
82
|
|
|
83
|
|
|
84
|
