Mercurial > hg > Members > kono > Proof > category
changeset 446:b9dec59bc706
bad case on distr
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 14 Oct 2016 21:02:12 +0900 |
| parents | 00cf84846d81 |
| children | aba05b0ba203 |
| files | limit-to.agda |
| diffstat | 1 files changed, 28 insertions(+), 11 deletions(-) [+] |
line wrap: on
line diff
--- a/limit-to.agda Fri Oct 14 19:44:59 2016 +0900 +++ b/limit-to.agda Fri Oct 14 21:02:12 2016 +0900 @@ -121,17 +121,34 @@ identity {t3} = 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 {t0} {t0} {t0} {f1} {g1} = begin - id1 A a - ≈↑⟨ idL ⟩ - A [ id1 A a o id1 A a ] - ∎ - distr1 {t1} {t1} {t1} {f1} {g1} = sym idL - distr1 {t2} {t2} {t2} {f1} {g1} = sym idL - distr1 {t3} {t3} {t3} {f1} {g1} = sym idL - distr1 {t0} {t1} {t1} {f1} {g1} = sym idL - distr1 {t0} {t1} {_} {f1} {g1} = ? - distr1 {a1} {b1} {c1} {f1} {g1} = {!!} + distr1 {t0} {t0} {c1} {f1} {g1} = sym idR + distr1 {t1} {t1} {c1} {f1} {g1} = sym idR + distr1 {t2} {t2} {c1} {f1} {g1} = sym idR + distr1 {t3} {t3} {c1} {f1} {g1} = sym idR + distr1 {t0} {t1} {t0} {f1} {g1} = sym ( trans-hom ( nil-idL none ) ( nil-id none ) ) + distr1 {t0} {t1} {t1} {f1} {g1} = sym idL + distr1 {t0} {t1} {t2} {f1} {g1} = sym ( nil-idL none ) + distr1 {t0} {t1} {t3} {f1} {g1} = sym ( nil-idL none ) + distr1 {t2} {t3} {t0} {f1} {g1} = sym (nil-idL none) + distr1 {t2} {t3} {t1} {f1} {g1} = sym (nil-idL none) + distr1 {t2} {t3} {t2} {f1} {g1} = sym ( trans-hom ( nil-idL none ) ( nil-id none ) ) + distr1 {t2} {t3} {t3} {f1} {g1} = sym idL + distr1 {t0} {t2} {t0} {_} {_} = sym ( trans-hom ( nil-idL none ) ( nil-id none ) ) + distr1 {t0} {t2} {t1} {_} {_} = {!!} -- bad case + distr1 {t0} {t3} {t1} {_} {_} = {!!} -- bad case + distr1 {t0} {t2} {t2} {_} {_} = ? + distr1 {t0} {t2} {t3} {_} {_} = {!!} + distr1 {t0} {t3} {c1} {_} {_} = {!!} + distr1 {t1} {t0} {c1} {_} {_} = {!!} + distr1 {t1} {t2} {c1} {_} {_} = {!!} + distr1 {t1} {t3} {c1} {_} {_} = {!!} + distr1 {t2} {t0} {c1} {_} {_} = {!!} + distr1 {t2} {t1} {c1} {_} {_} = {!!} + distr1 {t3} {t0} {c1} {_} {_} = {!!} + distr1 {t3} {t1} {c1} {_} {_} = {!!} + distr1 {t3} {t2} {c1} {_} {_} = {!!} + + --- Equalizer --- f