Mercurial > hg > Members > kono > Proof > category
changeset 394:aa94fdb12f1a
distribution law stacked
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 15 Mar 2016 18:05:06 +0900 |
| parents | 15d28525e756 |
| children | 2821b92e0dc9 |
| files | limit-to.agda |
| diffstat | 1 files changed, 124 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- a/limit-to.agda Tue Mar 15 16:50:11 2016 +0900 +++ b/limit-to.agda Tue Mar 15 18:05:06 2016 +0900 @@ -182,18 +182,137 @@ fobj : Obj I -> Obj A fobj t0 = a fobj t1 = b - fmap1 : {x y : Obj I } -> Hom I x y -> Arrow -> Hom A (fobj x) (fobj y) - fmap1 {_} {_} x f = {!!} + fmap1 : {x y : Obj I } -> Arrow -> Hom A (fobj x) (fobj y) + fmap1 {t0} {t1} arrow-f = f + fmap1 {t0} {t1} arrow-g = f + fmap1 {t0} {t0} id-t0 = id1 A a + fmap1 {t1} {t1} id-t0 = id1 A b + fmap1 {t0} {t0} _ = id1 A a + fmap1 {t0} {t1} _ = nf + fmap1 {t1} {t0} _ = nf-rev + fmap1 {t1} {t1} _ = id1 A b fmap : {x y : Obj I } -> Hom I x y -> Hom A (fobj x) (fobj y) - fmap {x} {y} f = fmap1 {x} {y} f ( Map f) + fmap {x} {y} f = fmap1 {x} {y} ( Map f) open ≈-Reasoning (A) identity : {x : Obj I} → A [ fmap (id1 I x) ≈ id1 A (fobj x) ] identity {t0} = refl-hom 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 = {!!} + 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) + ≈⟨⟩ + fmap1 nil + ≈⟨⟩ + 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} {_} {_} | _ | _ = {!!} + ≈-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 g1 x) + ≈-cong {_} {_} {f1} {g1} f≈g = ≡-cong f≈g (\x -> fmap1 x) --- Equalizer