Mercurial > hg > Members > kono > Proof > category

comparison CCCGraph1.agda @ 881:da0a1dd0c2ee

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 Sat, 11 Apr 2020 17:29:45 +0900
parents 543ceeb10191
children 6c69d48e6015
comparison
equal deleted inserted replaced
880:543ceeb10191 881:da0a1dd0c2ee
132 o-resp-≈ = λ {a b c f g h i} → ore {a} {b} {c} f g h i ; 132 o-resp-≈ = λ {a b c f g h i} → ore {a} {b} {c} f g h i ;
133 associative = λ{a b c d f g h } → cong (λ k → eval k ) (associative f g h ) 133 associative = λ{a b c d f g h } → cong (λ k → eval k ) (associative f g h )
134 } 134 }
135 } where 135 } where
136 iv-e : { a b c : Objs } → (x : Arrow b c ) ( g : Arrows a b ) → eval (iv x g) ≡ iv x (eval g) 136 iv-e : { a b c : Objs } → (x : Arrow b c ) ( g : Arrows a b ) → eval (iv x g) ≡ iv x (eval g)
137 iv-e = ? 137 iv-e = {!!}
138 iv-e-arrow : { a : Objs } → {b c : vertex G } → (x : edge G b c ) ( g : Arrows a (atom b) )
139 → eval (iv (arrow x) g) ≡ iv (arrow x) (eval g)
140 iv-e-arrow x (id (atom _)) = refl
141 iv-e-arrow x (iv f g) with eval (iv f g)
142 iv-e-arrow x (iv f g) | id (atom _) = refl
143 iv-e-arrow x (iv f g) | iv f₁ t = refl
138 iv-d : { a b c : Objs } → (x : Arrow b c ) ( g : Arrows a b ) → eval (iv x g) ≡ eval (iv x (eval g)) 144 iv-d : { a b c : Objs } → (x : Arrow b c ) ( g : Arrows a b ) → eval (iv x g) ≡ eval (iv x (eval g))
139 iv-d (arrow x) g = begin 145 iv-d (arrow x) g = begin
140 eval (iv (arrow x) g) 146 eval (iv (arrow x) g)
141 ≡⟨ {!!} ⟩ 147 ≡⟨ iv-e-arrow x g ⟩
142 iv (arrow x) (eval g) 148 iv (arrow x) (eval g)
143 ≡⟨ {!!} ⟩ 149 ≡⟨ cong (λ k → iv (arrow x) k ) ( sym ( idem-eval g) ) ⟩
150 iv (arrow x) (eval (eval g))
151 ≡⟨ sym (iv-e-arrow x (eval g)) ⟩
144 eval (iv (arrow x) (eval g)) 152 eval (iv (arrow x) (eval g))
145 ∎ where open ≡-Reasoning 153 ∎ where open ≡-Reasoning
146 iv-d π (id _) = refl 154 iv-d π (id _) = refl
147 iv-d π < g , g₁ > = sym (idem-eval g) 155 iv-d π < g , g₁ > = sym (idem-eval g)
148 iv-d π (iv f g) = {!!} 156 iv-d π (iv f g) = {!!}