Mercurial > hg > Members > kono > Proof > category

comparison CCCGraph1.agda @ 861:9e6e44ae82be

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 05 Apr 2020 13:00:59 +0900
parents d3cf372ac8cd
children 0c65b4e54d3a
comparison
equal deleted inserted replaced
860:d3cf372ac8cd 861:9e6e44ae82be
83 identityR {_} {_} {iv π' < g , g₁ >} = identityR {_} {_} {g₁} 83 identityR {_} {_} {iv π' < g , g₁ >} = identityR {_} {_} {g₁}
84 identityR {_} {_} {iv ε < f , f₁ >} = cong₂ (λ j k → iv ε < j , k > ) (identityR {_} {_} {f} ) (identityR {_} {_} {f₁}) 84 identityR {_} {_} {iv ε < f , f₁ >} = cong₂ (λ j k → iv ε < j , k > ) (identityR {_} {_} {f} ) (identityR {_} {_} {f₁})
85 identityR {_} {_} {iv (x *) < f , f₁ >} = cong₂ (λ j k → iv (x *) < j , k > ) (identityR {_} {_} {f} ) (identityR {_} {_} {f₁}) 85 identityR {_} {_} {iv (x *) < f , f₁ >} = cong₂ (λ j k → iv (x *) < j , k > ) (identityR {_} {_} {f} ) (identityR {_} {_} {f₁})
86 identityR {_} {_} {iv f (iv g h)} = refl 86 identityR {_} {_} {iv f (iv g h)} = refl
87 87
88 open import Data.Empty
89 open import Relation.Nullary
90
91 assoc-iv : {a b c d : Objs} (x : Arrow c d) (f : Arrows b c) (g : Arrows a b ) → eval (iv x (f ・ g)) ≡ eval (iv x f ・ g)
92 assoc-iv x (id a) g = refl
93 assoc-iv x (○ a) g = refl
94 assoc-iv π < f , f₁ > g = refl
95 assoc-iv π' < f , f₁ > g = refl
96 assoc-iv ε < f , f₁ > g = refl
97 assoc-iv (x *) < f , f₁ > g = refl
98 assoc-iv x (iv f g) h = {!!}
99
88 ==←≡ : {A B : Objs} {f g : Arrows A B} → f ≡ g → f == g 100 ==←≡ : {A B : Objs} {f g : Arrows A B} → f ≡ g → f == g
89 ==←≡ eq = cong (λ k → eval k ) eq 101 ==←≡ eq = cong (λ k → eval k ) eq
90 102
91 PL : Category (c₁ ⊔ c₂) (c₁ ⊔ c₂) (c₁ ⊔ c₂) 103 PL : Category (c₁ ⊔ c₂) (c₁ ⊔ c₂) (c₁ ⊔ c₂)
92 PL = record { 104 PL = record {
111 associative : {a b c d : Objs} (f : Arrows c d) (g : Arrows b c) (h : Arrows a b) → 123 associative : {a b c d : Objs} (f : Arrows c d) (g : Arrows b c) (h : Arrows a b) →
112 (f ・ (g ・ h)) == ((f ・ g) ・ h) 124 (f ・ (g ・ h)) == ((f ・ g) ・ h)
113 associative (id a) g h = refl 125 associative (id a) g h = refl
114 associative (○ a) g h = refl 126 associative (○ a) g h = refl
115 associative (< f , f1 > ) g h = cong₂ ( λ j k → < j , k > ) (associative f g h) (associative f1 g h) 127 associative (< f , f1 > ) g h = cong₂ ( λ j k → < j , k > ) (associative f g h) (associative f1 g h)
116 associative {a} (iv x f) g h = {!!} 128 associative {a} (iv π < f , f1 > ) g h = associative f g h
129 associative {a} (iv π' < f , f1 > ) g h = associative f1 g h
130 associative {a} (iv ε < f , f1 > ) g h = cong ( λ k → iv ε k ) ( associative < f , f1 > g h )
131 associative {a} (iv (x *) < f , f1 > ) g h = cong ( λ k → iv (x *) k ) ( associative < f , f1 > g h )
132 associative {a} (iv x (id _)) g h = begin
133 eval (iv x (id _) ・ (g ・ h))
134 ≡⟨⟩
135 eval (iv x (g ・ h))
136 ≡⟨ assoc-iv x g h ⟩
137 eval (iv x g ・ h)
138 ≡⟨⟩
139 eval ((iv x (id _) ・ g) ・ h)
140 ∎ where open ≡-Reasoning
141 associative {a} (iv x (○ _)) g h = refl
142 associative {a} (iv x (iv y f)) g h = begin
143 eval (iv x (iv y f) ・ (g ・ h))
144 ≡⟨ sym (assoc-iv x (iv y f) ( g ・ h)) ⟩
145 eval (iv x ((iv y f) ・ (g ・ h)))
146 ≡⟨ {!!} ⟩
147 iv x (eval ((iv y f) ・ (g ・ h)))
148 ≡⟨ {!!} ⟩
149 iv x (eval ((iv y f ・ g ) ・ h))
150 ≡⟨ {!!} ⟩
151 eval (iv x ((iv y f ・ g ) ・ h))
152 ≡⟨ {!!} ⟩
153 eval ((iv x (iv y f) ・ g) ・ h)
154 ∎ where open ≡-Reasoning
117 -- cong ( λ k → iv x k ) (associative f g h) 155 -- cong ( λ k → iv x k ) (associative f g h)
118 o-resp-≈ : {A B C : Objs} {f g : Arrows A B} {h i : Arrows B C} → 156 o-resp-≈ : {A B C : Objs} {f g : Arrows A B} {h i : Arrows B C} →
119 f == g → h == i → (h ・ f) == (i ・ g) 157 f == g → h == i → (h ・ f) == (i ・ g)
120 o-resp-≈ f=g h=i = {!!} 158 o-resp-≈ f=g h=i = {!!}