Mercurial > hg > Members > kono > Proof > category
changeset 397:dd3fa0680897
inconsistent distribution law on nil x arrow-g
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 16 Mar 2016 15:44:46 +0900 |
| parents | 45ecb7b6c396 |
| children | 64aa49a18469 |
| files | limit-to.agda |
| diffstat | 1 files changed, 137 insertions(+), 58 deletions(-) [+] |
line wrap: on
line diff
--- a/limit-to.agda Wed Mar 16 13:02:51 2016 +0900 +++ b/limit-to.agda Wed Mar 16 15:44:46 2016 +0900 @@ -29,6 +29,7 @@ id-t0 : Arrow arrow-f : Arrow arrow-g : Arrow + nil : Arrow record RawHom {c₁ ℓ : Level} (a : TwoObject {c₁} ) (b : TwoObject {c₁} ) : Set (c₁ ⊔ ℓ) where field @@ -54,7 +55,7 @@ twocomp : {ℓ : Level } -> Arrow {ℓ } -> Arrow {ℓ } -> Arrow {ℓ } twocomp id-t0 f = f twocomp f id-t0 = f -twocomp _ _ = arrow-f +twocomp _ _ = nil twocmp-associative : {ℓ : Level } -> ( f : Arrow {ℓ } ) -> ( g : Arrow {ℓ } ) -> ( h : Arrow {ℓ } ) → twocomp f (twocomp g h) ≡ twocomp (twocomp f g) h twocmp-associative id-t0 _ _ = refl @@ -62,16 +63,41 @@ twocmp-associative arrow-f arrow-f id-t0 = refl twocmp-associative arrow-f arrow-f arrow-f = refl twocmp-associative arrow-f arrow-f arrow-g = refl +twocmp-associative arrow-f arrow-f nil = refl twocmp-associative arrow-g id-t0 _ = refl +twocmp-associative arrow-f arrow-g nil = refl twocmp-associative arrow-f arrow-g id-t0 = refl twocmp-associative arrow-f arrow-g arrow-f = refl twocmp-associative arrow-f arrow-g arrow-g = refl +twocmp-associative arrow-f nil nil = refl +twocmp-associative arrow-f nil id-t0 = refl +twocmp-associative arrow-f nil arrow-f = refl +twocmp-associative arrow-f nil arrow-g = refl +twocmp-associative arrow-g arrow-f nil = refl twocmp-associative arrow-g arrow-f id-t0 = refl twocmp-associative arrow-g arrow-f arrow-f = refl twocmp-associative arrow-g arrow-f arrow-g = refl +twocmp-associative arrow-g arrow-g nil = refl twocmp-associative arrow-g arrow-g id-t0 = refl twocmp-associative arrow-g arrow-g arrow-f = refl twocmp-associative arrow-g arrow-g arrow-g = refl +twocmp-associative arrow-g nil nil = refl +twocmp-associative arrow-g nil id-t0 = refl +twocmp-associative arrow-g nil arrow-f = refl +twocmp-associative arrow-g nil arrow-g = refl +twocmp-associative nil id-t0 _ = refl +twocmp-associative nil nil nil = refl +twocmp-associative nil nil id-t0 = refl +twocmp-associative nil nil arrow-f = refl +twocmp-associative nil nil arrow-g = refl +twocmp-associative nil arrow-f nil = refl +twocmp-associative nil arrow-f id-t0 = refl +twocmp-associative nil arrow-f arrow-f = refl +twocmp-associative nil arrow-f arrow-g = refl +twocmp-associative nil arrow-g nil = refl +twocmp-associative nil arrow-g id-t0 = refl +twocmp-associative nil arrow-g arrow-f = refl +twocmp-associative nil arrow-g arrow-g = refl _×_ : { c₁ ℓ : Level } -> {A B C : TwoObject { c₁} } → Two-Hom { c₁} {ℓ} B C → Two-Hom { c₁} {ℓ} A B → Two-Hom { c₁} {ℓ} A C @@ -84,6 +110,7 @@ arrow-iso id-t0 = refl arrow-iso arrow-f = refl arrow-iso arrow-g = refl + arrow-iso nil = refl open Two-Hom @@ -110,11 +137,13 @@ identityL {_} {_} {f} | id-t0 = refl identityL {_} {_} {f} | arrow-f = refl identityL {_} {_} {f} | arrow-g = refl + identityL {_} {_} {f} | nil = refl identityR : {A B : TwoObject} {f : Two-Hom A B} → Map ( f × Two-id A ) ≡ Map f identityR {a} {b} {f} with Map f identityR {_} {_} {f} | id-t0 = refl identityR {_} {_} {f} | arrow-f = refl identityR {_} {_} {f} | arrow-g = refl + identityR {_} {_} {f} | nil = refl o-resp-≈ : {A B C : TwoObject} {f g : Two-Hom A B} {h i : Two-Hom B C} → Map f ≡ Map g → Map h ≡ Map i → Map ( h × f ) ≡ Map ( i × g ) o-resp-≈ {a} {b} {c} {f} {g} {h} {i} f≡g h≡i = let open ≡-Reasoning in @@ -137,27 +166,15 @@ Map ( (f × g) × h ) ∎ --- --- --- f' --- <----------- --- -----------> --- | f ^ g o fg = f --- fg | | gf gf o g = f --- v | f o gf'= g --- -----------> gf'o f = g --- g --- --- indexFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) - ( a b : Obj A ) ( f g : Hom A a b ) ( f' : Hom A b a ) ( fg fg' : Hom A a a ) ( gf gf' : Hom A b b ) + ( a b : Obj A ) ( f g : Hom A a b ) ( f' : Hom A b a ) ( f-iso : A [ A [ f o f' ] ≈ id1 A b ]) ( f'-iso : A [ A [ f' o f ] ≈ id1 A a ]) ( g-iso : A [ A [ g o f' ] ≈ id1 A b ]) ( g'-iso : A [ A [ f' o g ] ≈ id1 A a ]) -> Functor (TwoCat {c₁} {c₂} {ℓ} ) A -indexFunctor {c₁} {c₂} {ℓ} A a b f g f' fg fg' gf gf' f-iso f'-iso g-iso g'-iso = record { +indexFunctor {c₁} {c₂} {ℓ} A a b f g f' f-iso f'-iso g-iso g'-iso = record { FObj = λ a → fobj a ; FMap = λ f → fmap f ; isFunctor = record { @@ -175,12 +192,10 @@ fmap1 {t0} {t1} arrow-g = g fmap1 {t0} {t0} id-t0 = id1 A a fmap1 {t1} {t1} id-t0 = id1 A b - fmap1 {t0} {t0} arrow-f = fg - fmap1 {t0} {t0} arrow-g = fg' + fmap1 {t0} {t0} _ = id1 A a fmap1 {t0} {t1} _ = f fmap1 {t1} {t0} _ = f' - fmap1 {t1} {t1} arrow-f = gf - fmap1 {t1} {t1} arrow-g = gf' + 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} ( Map f) open ≈-Reasoning (A) @@ -189,47 +204,111 @@ 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} {t1} {t0} {_} {_} | arrow-f | arrow-f = {!!} - distr1 {t0} {t1} {t0} {_} {_} | arrow-f | arrow-g = {!!} - distr1 {t0} {t1} {t0} {_} {_} | arrow-f | id-t0 = {!!} - distr1 {t0} {t1} {t0} {_} {_} | arrow-g | arrow-f = {!!} - distr1 {t0} {t1} {t0} {_} {_} | arrow-g | arrow-g = {!!} - distr1 {t0} {t1} {t0} {_} {_} | arrow-g | id-t0 = {!!} - distr1 {t0} {t1} {t0} {_} {_} | id-t0 | arrow-f = {!!} - distr1 {t0} {t1} {t0} {_} {_} | id-t0 | arrow-g = {!!} - distr1 {t0} {t1} {t0} {_} {_} | id-t0 | id-t0 = sym f'-iso - distr1 {t1} {t0} {t1} {_} {_} | arrow-f | arrow-f = {!!} - distr1 {t1} {t0} {t1} {_} {_} | arrow-f | arrow-g = {!!} - distr1 {t1} {t0} {t1} {_} {_} | arrow-f | id-t0 = {!!} - distr1 {t1} {t0} {t1} {_} {_} | arrow-g | arrow-f = {!!} - distr1 {t1} {t0} {t1} {_} {_} | arrow-g | arrow-g = {!!} - distr1 {t1} {t0} {t1} {_} {_} | arrow-g | id-t0 = {!!} - distr1 {t1} {t0} {t1} {_} {_} | id-t0 | arrow-f = {!!} - distr1 {t1} {t0} {t1} {_} {_} | id-t0 | arrow-g = {!!} - distr1 {t1} {t0} {t1} {_} {_} | id-t0 | id-t0 = sym f-iso - distr1 {t0} {t0} {t0} {f1} {g1} | fa | id-t0 = sym idL - distr1 {t0} {t0} {t1} {f1} {g1} | arrow-f | id-t0 = {!!} - distr1 {t0} {t0} {t1} {f1} {g1} | arrow-g | id-t0 = begin - fmap1 {t0} {t1} arrow-g + distr1 {t0} {t1} {t0} {_} {_} | arrow-f | arrow-f = sym f'-iso + distr1 {t0} {t1} {t0} {_} {_} | arrow-f | arrow-g = sym f'-iso + distr1 {t0} {t1} {t0} {_} {_} | arrow-f | id-t0 = sym f'-iso + distr1 {t0} {t1} {t0} {_} {_} | arrow-f | nil = sym f'-iso + distr1 {t0} {t1} {t0} {_} {_} | arrow-g | id-t0 = sym g'-iso + distr1 {t0} {t1} {t0} {_} {_} | arrow-g | arrow-f = sym g'-iso + distr1 {t0} {t1} {t0} {_} {_} | arrow-g | arrow-g = sym g'-iso + distr1 {t0} {t1} {t0} {_} {_} | arrow-g | nil = sym g'-iso + distr1 {t0} {t1} {t0} {_} {_} | id-t0 | arrow-f = sym f'-iso + distr1 {t0} {t1} {t0} {_} {_} | id-t0 | arrow-g = sym f'-iso + distr1 {t0} {t1} {t0} {_} {_} | id-t0 | id-t0 = sym f'-iso + distr1 {t0} {t1} {t0} {_} {_} | id-t0 | nil = sym f'-iso + distr1 {t0} {t1} {t0} {_} {_} | nil | arrow-f = sym f'-iso + distr1 {t0} {t1} {t0} {_} {_} | nil | arrow-g = sym f'-iso + distr1 {t0} {t1} {t0} {_} {_} | nil | id-t0 = sym f'-iso + distr1 {t0} {t1} {t0} {_} {_} | nil | nil = sym f'-iso + + distr1 {t1} {t0} {t1} {_} {_} | arrow-f | id-t0 = sym f-iso + distr1 {t1} {t0} {t1} {_} {_} | arrow-f | arrow-f = sym f-iso + distr1 {t1} {t0} {t1} {_} {_} | arrow-f | arrow-g = sym g-iso + distr1 {t1} {t0} {t1} {_} {_} | arrow-f | nil = sym f-iso + distr1 {t1} {t0} {t1} {_} {_} | arrow-g | id-t0 = sym f-iso + distr1 {t1} {t0} {t1} {_} {_} | arrow-g | arrow-f = sym f-iso + distr1 {t1} {t0} {t1} {_} {_} | arrow-g | arrow-g = sym g-iso + distr1 {t1} {t0} {t1} {_} {_} | arrow-g | nil = sym f-iso + distr1 {t1} {t0} {t1} {_} {_} | id-t0 | nil = sym f-iso + distr1 {t1} {t0} {t1} {_} {_} | id-t0 | arrow-f = sym f-iso + distr1 {t1} {t0} {t1} {_} {_} | id-t0 | arrow-g = sym g-iso + distr1 {t1} {t0} {t1} {_} {_} | id-t0 | id-t0 = sym f-iso + distr1 {t1} {t0} {t1} {_} {_} | nil | nil = sym f-iso + distr1 {t1} {t0} {t1} {_} {_} | nil | arrow-f = sym f-iso + distr1 {t1} {t0} {t1} {_} {_} | nil | arrow-g = sym g-iso + distr1 {t1} {t0} {t1} {_} {_} | nil | id-t0 = sym f-iso + + distr1 {_} {t0} {t0} {f1} {g1} | fa | id-t0 = sym idL -- * + distr1 {t1} {t1} {t0} {f1} {g1} | id-t0 | ga = sym idR -- * + + distr1 {t1} {t1} {t1} {f1} {g1} | id-t0 | id-t0 = sym idR -- * + distr1 {t1} {t1} {t1} {f1} {g1} | id-t0 | nil = sym idR + distr1 {t1} {t1} {t1} {f1} {g1} | id-t0 | arrow-f = sym idR -- * + distr1 {t1} {t1} {t1} {f1} {g1} | id-t0 | arrow-g = sym idR -- * + + distr1 {t1} {t1} {t0} {f1} {g1} | nil | ga = sym idR + distr1 {t1} {t1} {t0} {f1} {g1} | arrow-f | ga = sym idR + distr1 {t1} {t1} {t0} {f1} {g1} | arrow-g | ga = sym idR + distr1 {t1} {t0} {t0} {f1} {g1} | fa | nil = sym idL + distr1 {t1} {t0} {t0} {f1} {g1} | fa | arrow-f = sym idL + distr1 {t1} {t0} {t0} {f1} {g1} | fa | arrow-g = sym idL + + distr1 {t0} {t0} {t0} {f1} {g1} | id-t0 | arrow-f = sym idR + distr1 {t0} {t0} {t0} {f1} {g1} | id-t0 | arrow-g = sym idR + distr1 {t0} {t0} {t0} {f1} {g1} | id-t0 | nil = sym idR + distr1 {t0} {t0} {t0} {f1} {g1} | nil | arrow-f = sym idR + distr1 {t0} {t0} {t0} {f1} {g1} | nil | arrow-g = sym idR + distr1 {t0} {t0} {t0} {f1} {g1} | nil | nil = sym idR + distr1 {t0} {t0} {t0} {f1} {g1} | arrow-f | nil = sym idR + distr1 {t0} {t0} {t0} {f1} {g1} | arrow-f | arrow-f = sym idR + distr1 {t0} {t0} {t0} {f1} {g1} | arrow-f | arrow-g = sym idR + distr1 {t0} {t0} {t0} {f1} {g1} | arrow-g | nil = sym idR + distr1 {t0} {t0} {t0} {f1} {g1} | arrow-g | arrow-f = sym idR + distr1 {t0} {t0} {t0} {f1} {g1} | arrow-g | arrow-g = sym idR + + distr1 {t1} {t1} {t1} {f1} {g1} | arrow-f | id-t0 = sym idR -- * + distr1 {t1} {t1} {t1} {f1} {g1} | arrow-f | nil = sym idR + distr1 {t1} {t1} {t1} {f1} {g1} | arrow-f | arrow-f = sym idR + distr1 {t1} {t1} {t1} {f1} {g1} | arrow-f | arrow-g = sym idR + distr1 {t1} {t1} {t1} {f1} {g1} | arrow-g | id-t0 = sym idR -- * + distr1 {t1} {t1} {t1} {f1} {g1} | arrow-g | nil = sym idR + distr1 {t1} {t1} {t1} {f1} {g1} | arrow-g | arrow-f = sym idR + distr1 {t1} {t1} {t1} {f1} {g1} | arrow-g | arrow-g = sym idR + distr1 {t1} {t1} {t1} {f1} {g1} | nil | id-t0 = sym idR + distr1 {t1} {t1} {t1} {f1} {g1} | nil | nil = sym idR + distr1 {t1} {t1} {t1} {f1} {g1} | nil | arrow-g = sym idR + distr1 {t1} {t1} {t1} {f1} {g1} | nil | arrow-f = sym idR + + distr1 {t0} {t0} {t1} {f1} {g1} | nil | arrow-f = sym idR + distr1 {t0} {t0} {t1} {f1} {g1} | arrow-f | arrow-f = sym idR + distr1 {t0} {t0} {t1} {f1} {g1} | arrow-g | arrow-f = sym idR + distr1 {t0} {t0} {t1} {f1} {g1} | id-t0 | arrow-f = sym idR -- * + distr1 {t0} {t0} {t1} {f1} {g1} | arrow-f | arrow-g = {!!} + distr1 {t0} {t0} {t1} {f1} {g1} | arrow-g | arrow-g = {!!} + distr1 {t0} {t0} {t1} {f1} {g1} | id-t0 | arrow-g = sym idR -- * + distr1 {t0} {t0} {t1} {f1} {g1} | nil | arrow-g = begin + f + ≈⟨ {!!} ⟩ + g o id1 A a ≈⟨⟩ - g - ≈⟨ {!!} ⟩ - {!!} + g o fmap1 {t0} {t0} nil + ≈⟨⟩ + fmap1 {t0} {t1} arrow-g o fmap1 {t0} {t0} nil ∎ - distr1 {t0} {t0} {t1} {f1} {g1} | id-t0 | id-t0 = {!!} - distr1 {t0} {t0} {_} {f1} {g1} | fa | arrow-f = {!!} - distr1 {t0} {t0} {_} {f1} {g1} | fa | arrow-g = {!!} - distr1 {t1} {t1} {_} {f1} {g1} | id-t0 | ga = {!!} - distr1 {t1} {t1} {_} {f1} {g1} | arrow-f | ga = {!!} - distr1 {t1} {t1} {_} {f1} {g1} | arrow-g | ga = {!!} - distr1 {t1} {t0} {t0} {f1} {g1} | id-t0 | ga = {!!} - distr1 {t1} {t0} {t0} {_} {_} | arrow-f | ga = {!!} - distr1 {t1} {t0} {t0} {_} {_} | arrow-g | ga = {!!} - distr1 {t0} {t1} {t1} {_} {_} | id-t0 | ga = {!!} - distr1 {t0} {t1} {t1} {_} {_} | arrow-f | ga = {!!} - distr1 {t0} {t1} {t1} {_} {_} | arrow-g | ga = {!!} + distr1 {t0} {t0} {t1} {f1} {g1} | fa | ga-g = {!!} + distr1 {t0} {t1} {t1} {f1} {g1} | nil | arrow-f = sym idL + distr1 {t0} {t1} {t1} {f1} {g1} | nil | arrow-g = sym idL + distr1 {t0} {t1} {t1} {f1} {g1} | arrow-f | id-t0 = sym idL -- * + distr1 {t0} {t1} {t1} {f1} {g1} | arrow-g | id-t0 = sym idL -- * + distr1 {t0} {t1} {t1} {f1} {g1} | arrow-g | arrow-g = {!!} + distr1 {t0} {t1} {t1} {f1} {g1} | fa | ga = begin + {!!} + ≈⟨ {!!} ⟩ + fmap1 {t1} {t1} ga o fmap1 {t0} {t1} fa + ∎ + ≈-cong : {a : Obj I} {b : Obj I} {f g : Hom I a b} → I [ f ≈ g ] → A [ fmap f ≈ fmap g ] - ≈-cong {a} {b} {f1} {g1} f≈g = ≡-cong {_} {_} {_} {_} {_} {_} f≈g (\x -> fmap1 {a} {b} x) + ≈-cong {_} {_} {f1} {g1} f≈g = ≡-cong f≈g (\x -> fmap1 x) --- Equalizer @@ -257,7 +336,7 @@ ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k' } where I = TwoCat {c₁} {c₂} {ℓ } - Γ = indexFunctor A a b f g nf-rev {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} + Γ = indexFunctor A a b f g {!!} {!!} {!!} {!!} {!!} nmap : (x : Obj I) ( d : Obj A ) (h : Hom A d a ) -> Hom A (FObj (K A I d) x) (FObj Γ x) nmap x d h = {!!} commute1 : {x y : Obj I} {f' : Hom I x y} (d : Obj A) (h : Hom A d a ) -> A [ A [ f o h ] ≈ A [ g o h ] ]