Mercurial > hg > Members > kono > Proof > category
changeset 851:f4f5ce90d3af
plan B
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 04 Apr 2020 13:40:35 +0900 |
| parents | 40c6e806bda0 |
| children | 425eda25ff8c |
| files | CCCGraph1.agda |
| diffstat | 1 files changed, 37 insertions(+), 21 deletions(-) [+] |
line wrap: on
line diff
--- a/CCCGraph1.agda Sat Apr 04 10:06:20 2020 +0900 +++ b/CCCGraph1.agda Sat Apr 04 13:40:35 2020 +0900 @@ -44,10 +44,17 @@ iv x y ・ id a = iv x y iv f (iv f₁ g) ・ h = iv f ( (iv f₁ g) ・ h ) ○ a ・ g = ○ _ - f ・ id b = f + + eval : {a b : Objs } (f : Arrows a b ) → Arrows a b + eval (id a) = id a + eval (○ a) = ○ a + eval < f , f₁ > = < eval f , eval f₁ > + eval (iv π < f , g > ) = eval f + eval (iv π' < f , g > ) = eval g + eval (iv f g) = iv f (eval g) _==_ : {a b : Objs } → ( x y : Arrows a b ) → Set (c₁ ⊔ c₂) - _==_ {a} {b} x y = (x ・ id _ ) ≡ ( y ・ id _ ) + _==_ {a} {b} x y = eval x ≡ eval y identityR≡ : {A B : Objs} {f : Arrows A B} → (f ・ id A) ≡ f identityR≡ {a} {.a} {id a} = refl @@ -55,19 +62,27 @@ identityR≡ {a} {_} {< f , f₁ >} = cong₂ (λ j k → < j , k > ) identityR≡ identityR≡ identityR≡ {a} {b} {iv x (id a)} = refl identityR≡ {a} {b} {iv x (○ a)} = refl - identityR≡ {a} {_} {iv π < f , g >} = {!!} + identityR≡ {a} {_} {iv π < f , g >} = begin + iv π < f , g > ・ id a + ≡⟨⟩ + f ・ id a + ≡⟨ identityR≡ ⟩ + f + ≡⟨ {!!} ⟩ + iv π < f , g > + ∎ where open ≡-Reasoning identityR≡ {a} {b} {iv π' < f , g >} = {!!} - identityR≡ {a} {b} {iv ε < f , g >} = {!!} - identityR≡ {a} {.(_ <= _)} {iv (x *) < y , y₁ >} = {!!} + identityR≡ {a} {b} {iv ε < f , g >} = cong₂ ( λ j k → iv ε < j , k > ) identityR≡ identityR≡ + identityR≡ {a} {_} {iv (x *) < f , g >} = cong₂ ( λ j k → iv (x *) < j , k > ) identityR≡ identityR≡ identityR≡ {a} {b} {iv x (iv f y)} = refl identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) == f - identityR {a} {b} {f} = cong ( λ k → k ・ id a ) ( identityR≡ {_} {_} {f} ) + identityR {a} {b} {f} = {!!} -- cong ( λ k → k ・ id a ) ( identityR≡ {_} {_} {f} ) ≡←== : {A B : Objs} {f g : Arrows A B} → f == g → f ≡ g - ≡←== eq = subst₂ (λ j k → j ≡ k ) identityR≡ identityR≡ eq + ≡←== eq = subst₂ (λ j k → j ≡ k ) identityR≡ identityR≡ {!!} ==←≡ : {A B : Objs} {f g : Arrows A B} → f ≡ g → f == g - ==←≡ eq = cong (λ k → k ・ id _) eq + ==←≡ eq = {!!} -- cong (λ k → k ・ id _) eq assoc-iv : {a b c d : Objs} (x : Arrow c d ) (f : Arrows b c ) ( g : Arrows a b ) → iv x f ・ g ≡ iv x ( f ・ g ) assoc-iv x f (id _) = begin @@ -136,19 +151,20 @@ associative (id a) g h = refl associative (○ a) g h = refl associative (< f , f1 > ) g h = cong₂ ( λ j k → < j , k > ) (associative f g h) (associative f1 g h) - associative {a} (iv x f) g h = begin - (iv x f ・ (g ・ h)) ・ id a - ≡⟨ cong ( λ k → k ・ id a) (assoc-iv x f ( g ・ h )) ⟩ - iv x (f ・ (g ・ h)) ・ id a - ≡⟨ cong ( λ k → iv x k ・ id a) (≡←== (associative f g h ) ) ⟩ - {!!} - ≡⟨ {!!} ⟩ - iv x ((f ・ g ) ・ h) ・ id a - ≡⟨ sym (cong ( λ k → k ・ id a) (assoc-iv x (f ・ g ) h)) ⟩ - ( iv x (f ・ g ) ・ h) ・ id a - ≡⟨ sym (cong ( λ k → (k ・ h ) ・ id a) (assoc-iv x f g)) ⟩ - ((iv x f ・ g) ・ h) ・ id a - ∎ where open ≡-Reasoning + associative {a} (iv x f) g h = {!!} + -- begin + -- (iv x f ・ (g ・ h)) ・ id a + -- ≡⟨ cong ( λ k → k ・ id a) (assoc-iv x f ( g ・ h )) ⟩ + -- iv x (f ・ (g ・ h)) ・ id a + -- ≡⟨ cong ( λ k → iv x k ・ id a) (≡←== (associative f g h ) ) ⟩ + -- {!!} + -- ≡⟨ {!!} ⟩ + -- iv x ((f ・ g ) ・ h) ・ id a + -- ≡⟨ sym (cong ( λ k → k ・ id a) (assoc-iv x (f ・ g ) h)) ⟩ + -- ( iv x (f ・ g ) ・ h) ・ id a + -- ≡⟨ sym (cong ( λ k → (k ・ h ) ・ id a) (assoc-iv x f g)) ⟩ + -- ((iv x f ・ g) ・ h) ・ id a + -- ∎ where open ≡-Reasoning -- {!!} ( cong ( λ k → iv x k ) ( ≡←== (associative f g h ) ) ) o-resp-≈ : {A B C : Objs} {f g : Arrows A B} {h i : Arrows B C} → f == g → h == i → (h ・ f) == (i ・ g)