Mercurial > hg > Members > kono > Proof > category
changeset 395:2821b92e0dc9
bad distribution law
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 15 Mar 2016 18:18:06 +0900 |
| parents | aa94fdb12f1a |
| children | 45ecb7b6c396 |
| files | limit-to.agda |
| diffstat | 1 files changed, 19 insertions(+), 98 deletions(-) [+] |
line wrap: on
line diff
--- a/limit-to.agda Tue Mar 15 18:05:06 2016 +0900 +++ b/limit-to.agda Tue Mar 15 18:18:06 2016 +0900 @@ -199,102 +199,6 @@ identity {t1} = refl-hom distr1 : {a₁ : Obj I} {b₁ : Obj I} {c : Obj I} {f₁ : Hom I a₁ b₁} {g₁ : Hom I b₁ c} → A [ fmap (I [ g₁ o f₁ ]) ≈ A [ fmap g₁ o fmap f₁ ] ] distr1 {a1} {b1} {c} {f1} {g1} with Map f1 | Map g1 - distr1 {t0} {t0} {_} {f1} {g1} | fa | id-t0 = begin - fmap1 fa - ≈⟨ sym idL ⟩ - id1 A a o fmap1 fa - ≈⟨⟩ - fmap1 id-t0 o fmap1 fa - ∎ - distr1 {t0} {t0} {_} {f1} {g1} | fa | arrow-f = begin - fmap1 fa - ≈⟨ sym idL ⟩ - id1 A a o fmap1 fa - ≈⟨⟩ - fmap1 id-t0 o fmap1 fa - ∎ - distr1 {t0} {t0} {_} {f1} {g1} | fa | arrow-g = begin - fmap1 fa - ≈⟨ sym idL ⟩ - id1 A a o fmap1 fa - ≈⟨⟩ - fmap1 id-t0 o fmap1 fa - ∎ - distr1 {t0} {t0} {_} {f1} {g1} | fa | nil = begin - fmap1 fa - ≈⟨ sym idL ⟩ - id1 A a o fmap1 fa - ≈⟨⟩ - fmap1 id-t0 o fmap1 fa - ∎ - distr1 {t1} {t1} {_} {f1} {g1} | id-t0 | ga = begin - fmap1 ga - ≈⟨ sym idR ⟩ - fmap1 ga o id1 A b - ≈⟨⟩ - fmap1 ga o id1 A b - ∎ - distr1 {t1} {t1} {_} {f1} {g1} | arrow-f | ga = begin - fmap1 ga - ≈⟨ sym idR ⟩ - fmap1 ga o id1 A b - ≈⟨⟩ - fmap1 ga o id1 A b - ∎ - distr1 {t1} {t1} {_} {f1} {g1} | arrow-g | ga = begin - fmap1 ga - ≈⟨ sym idR ⟩ - fmap1 ga o id1 A b - ≈⟨⟩ - fmap1 ga o id1 A b - ∎ - distr1 {t1} {t1} {_} {f1} {g1} | nil | ga = begin - fmap1 ga - ≈⟨ sym idR ⟩ - fmap1 ga o id1 A b - ≈⟨⟩ - fmap1 ga o id1 A b - ∎ - distr1 {t1} {t0} {t0} {f1} {g1} | id-t0 | ga = begin - fmap1 ga - ≈⟨ sym idL ⟩ - fmap1 ga o id1 A b - ∎ - distr1 {t1} {t0} {t0} {_} {_} | arrow-f | ga = begin - fmap1 ga - ≈⟨ sym idL ⟩ - fmap1 ga o id1 A b - ∎ - distr1 {t1} {t0} {t0} {_} {_} | arrow-g | ga = begin - fmap1 ga - ≈⟨ sym idL ⟩ - fmap1 ga o id1 A b - ∎ - distr1 {t1} {t0} {t0} {_} {_} | nil | ga = begin - fmap1 ga - ≈⟨ sym idL ⟩ - fmap1 ga o id1 A b - ∎ - distr1 {t0} {t1} {t1} {_} {_} | id-t0 | ga = begin - fmap1 ga - ≈⟨ sym idL ⟩ - fmap1 ga o id1 A a - ∎ - distr1 {t0} {t1} {t1} {_} {_} | arrow-f | ga = begin - fmap1 ga - ≈⟨ sym idL ⟩ - fmap1 ga o id1 A a - ∎ - distr1 {t0} {t1} {t1} {_} {_} | arrow-g | ga = begin - fmap1 ga - ≈⟨ sym idL ⟩ - fmap1 ga o id1 A a - ∎ - distr1 {t0} {t1} {t1} {_} {_} | nil | ga = begin - fmap1 ga - ≈⟨ sym idL ⟩ - fmap1 ga o id1 A a - ∎ distr1 {t0} {t1} {t0} {_} {_} | fa | arrow-f = begin fmap1 (twocomp arrow-f fa) ≈⟨⟩ @@ -302,14 +206,31 @@ ≈⟨⟩ id1 A b ≈⟨ {!!} ⟩ - f o nf-rev - ≈⟨⟩ f o fmap1 fa ≈⟨⟩ fmap1 arrow-f o fmap1 fa ∎ distr1 {t0} {t1} {t0} {_} {_} | _ | _ = {!!} + distr1 {t1} {t0} {t1} {_} {_} | arrow-f | ga = begin + fmap1 (twocomp ga arrow-f) + ≈⟨⟩ + id1 A a + ≈⟨ {!!} ⟩ + fmap1 ga o f + ≈⟨⟩ + fmap1 ga o fmap1 arrow-f + ∎ + distr1 {t1} {t0} {t1} {_} {_} | nil | ga = begin + fmap1 (twocomp ga nil ) + ≈⟨⟩ + id1 A a + ≈⟨ {!!} ⟩ + fmap1 ga o nf + ≈⟨⟩ + fmap1 ga o fmap1 nil + ∎ distr1 {t1} {t0} {t1} {_} {_} | _ | _ = {!!} + distr1 {_} {_} {_} {_} {_} | _ | _ = {!!} ≈-cong : {a : Obj I} {b : Obj I} {f g : Hom I a b} → I [ f ≈ g ] → A [ fmap f ≈ fmap g ] ≈-cong {_} {_} {f1} {g1} f≈g = ≡-cong f≈g (\x -> fmap1 x)