comparison CCC.agda @ 794:ba575c73ea48

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 22 Apr 2019 12:43:49 +0900 (2019-04-22)
parents f37f11e1b871
children
comparison
equal deleted inserted replaced
793:f37f11e1b871 794:ba575c73ea48
50 ≈↑⟨ π-cong idR idR ⟩ 50 ≈↑⟨ π-cong idR idR ⟩
51 < π o id1 A (a ∧ b) , π' o id1 A (a ∧ b) > 51 < π o id1 A (a ∧ b) , π' o id1 A (a ∧ b) >
52 ≈⟨ e3c ⟩ 52 ≈⟨ e3c ⟩
53 id1 A (a ∧ b ) 53 id1 A (a ∧ b )
54 54
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 ] > ] 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 56 distr-π {a} {b} {c} {d} {f} {g} {h} = let open ≈-Reasoning A in begin
57 < f , g > o h 57 < f , g > o h
58 ≈↑⟨ e3c ⟩ 58 ≈↑⟨ e3c ⟩
59 < π o < f , g > o h , π' o < f , g > o h > 59 < π o < f , g > o h , π' o < f , g > o h >
60 ≈⟨ π-cong assoc assoc ⟩ 60 ≈⟨ π-cong assoc assoc ⟩
61 < ( π o < f , g > ) o h , (π' o < f , g > ) o h > 61 < ( π o < f , g > ) o h , (π' o < f , g > ) o h >
62 ≈⟨ π-cong (car e3a ) (car e3b) ⟩ 62 ≈⟨ π-cong (car e3a ) (car e3b) ⟩
63 < f o h , g o h > 63 < f o h , g o h >
64 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 ) 65 _×_ : { a b c d : Obj A } ( f : Hom A a c ) (g : Hom A b d ) → Hom A (a ∧ b) ( c ∧ d )
66 f × g = λ h → < A [ f o A [ π o h ] ] , A [ g o A [ π' o h ] ] > 66 f × g = < (A [ f o π ] ) , (A [ g o π' ]) >
67 distr-* : {a b c d : Obj A } { h : Hom A (a ∧ b) c } { k : Hom A d a } → A [ A [ h * o k ] ≈ ( A [ h o < A [ k o π ] , π' > ] ) * ]
68 distr-* {a} {b} {c} {d} {h} {k} = begin
69 h * o k
70 ≈↑⟨ e4b ⟩
71 ( ε o < (h * o k ) o π , π' > ) *
72 ≈⟨ *-cong ( begin
73 ε o < (h * o k ) o π , π' >
74 ≈↑⟨ cdr ( π-cong assoc refl-hom ) ⟩
75 ε o ( < h * o ( k o π ) , π' > )
76 ≈↑⟨ cdr ( π-cong (cdr e3a) e3b ) ⟩
77 ε o ( < h * o ( π o < k o π , π' > ) , π' o < k o π , π' > > )
78 ≈⟨ cdr ( π-cong assoc refl-hom) ⟩
79 ε o ( < (h * o π) o < k o π , π' > , π' o < k o π , π' > > )
80 ≈↑⟨ cdr ( distr-π ) ⟩
81 ε o ( < h * o π , π' > o < k o π , π' > )
82 ≈⟨ assoc ⟩
83 ( ε o < h * o π , π' > ) o < k o π , π' >
84 ≈⟨ car e4a ⟩
85 h o < k o π , π' >
86 ∎ ) ⟩
87 ( h o < k o π , π' > ) *
88 ∎ where open ≈-Reasoning A
89 α : {a b c : Obj A } → Hom A (( a ∧ b ) ∧ c ) ( a ∧ ( b ∧ c ) )
90 α = < A [ π o π ] , < A [ π' o π ] , π' > >
91 α' : {a b c : Obj A } → Hom A ( a ∧ ( b ∧ c ) ) (( a ∧ b ) ∧ c )
92 α' = < < π , A [ π o π' ] > , A [ π' o π' ] >
93 β : {a b c d : Obj A } { f : Hom A a b} { g : Hom A a c } { h : Hom A a d } → A [ A [ α o < < f , g > , h > ] ≈ < f , < g , h > > ]
94 β {a} {b} {c} {d} {f} {g} {h} = begin
95 α o < < f , g > , h >
96 ≈⟨⟩
97 ( < ( π o π ) , < ( π' o π ) , π' > > ) o < < f , g > , h >
98 ≈⟨ distr-π ⟩
99 < ( ( π o π ) o < < f , g > , h > ) , ( < ( π' o π ) , π' > o < < f , g > , h > ) >
100 ≈⟨ π-cong refl-hom distr-π ⟩
101 < ( ( π o π ) o < < f , g > , h > ) , ( < ( ( π' o π ) o < < f , g > , h > ) , ( π' o < < f , g > , h > ) > ) >
102 ≈↑⟨ π-cong assoc ( π-cong assoc refl-hom ) ⟩
103 < ( π o (π o < < f , g > , h >) ) , ( < ( π' o ( π o < < f , g > , h > ) ) , ( π' o < < f , g > , h > ) > ) >
104 ≈⟨ π-cong (cdr e3a ) ( π-cong (cdr e3a ) e3b ) ⟩
105 < ( π o < f , g > ) , < ( π' o < f , g > ) , h > >
106 ≈⟨ π-cong e3a ( π-cong e3b refl-hom ) ⟩
107 < f , < g , h > >
108 ∎ where open ≈-Reasoning A
109
67 110
68 record CCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where 111 record CCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
69 field 112 field
70 1 : Obj A 113 1 : Obj A
71 ○ : (a : Obj A ) → Hom A a 1 114 ○ : (a : Obj A ) → Hom A a 1