Mercurial > hg > Members > kono > Proof > category
view HomReasoning.agda @ 948:dca4b29553cb
mp-flatten
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 22 Aug 2020 10:45:40 +0900 |
| parents | ca5eba647990 |
| children |
line wrap: on
line source
module HomReasoning where -- Shinji KONO <kono@ie.u-ryukyu.ac.jp> open import Category -- https://github.com/konn/category-agda open import Level open Functor -- F(f) -- F(a) ---→ F(b) -- | | -- |t(a) |t(b) G(f)t(a) = t(b)F(f) -- | | -- v v -- G(a) ---→ G(b) -- G(f) record IsNTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (D : Category c₁ c₂ ℓ) (C : Category c₁′ c₂′ ℓ′) ( F G : Functor D C ) (TMap : (A : Obj D) → Hom C (FObj F A) (FObj G A)) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where field commute : {a b : Obj D} {f : Hom D a b} → C [ C [ ( FMap G f ) o ( TMap a ) ] ≈ C [ (TMap b ) o (FMap F f) ] ] record NTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′) (F G : Functor domain codomain ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where field TMap : (A : Obj domain) → Hom codomain (FObj F A) (FObj G A) isNTrans : IsNTrans domain codomain F G TMap module ≈-Reasoning {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) where open import Relation.Binary.Core _o_ : {a b c : Obj A } ( x : Hom A a b ) ( y : Hom A c a ) → Hom A c b x o y = A [ x o y ] _≈_ : {a b : Obj A } → Rel (Hom A a b) ℓ x ≈ y = A [ x ≈ y ] infixr 9 _o_ infix 4 _≈_ refl-hom : {a b : Obj A } { x : Hom A a b } → x ≈ x refl-hom = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A )) trans-hom : {a b : Obj A } { x y z : Hom A a b } → x ≈ y → y ≈ z → x ≈ z trans-hom b c = ( IsEquivalence.trans (IsCategory.isEquivalence ( Category.isCategory A ))) b c -- some short cuts car : {a b c : Obj A } {x y : Hom A a b } { f : Hom A c a } → x ≈ y → ( x o f ) ≈ ( y o f ) car eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) ( refl-hom ) eq car1 : { c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b c : Obj A } {x y : Hom A a b } { f : Hom A c a } → A [ x ≈ y ] → A [ A [ x o f ] ≈ A [ y o f ] ] car1 A eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) ( IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A )) ) eq cdr : {a b c : Obj A } {x y : Hom A a b } { f : Hom A b c } → x ≈ y → f o x ≈ f o y cdr eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) eq (refl-hom ) cdr1 : { c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b c : Obj A } {x y : Hom A a b } { f : Hom A b c } → A [ x ≈ y ] → A [ A [ f o x ] ≈ A [ f o y ] ] cdr1 A eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) eq (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A )) ) id : (a : Obj A ) → Hom A a a id a = (Id {_} {_} {_} {A} a) idL : {a b : Obj A } { f : Hom A a b } → id b o f ≈ f idL = IsCategory.identityL (Category.isCategory A) idR : {a b : Obj A } { f : Hom A a b } → f o id a ≈ f idR = IsCategory.identityR (Category.isCategory A) sym : {a b : Obj A } { f g : Hom A a b } → f ≈ g → g ≈ f sym = IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory A)) sym-hom = sym -- working on another cateogry idL1 : { c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A b a } → A [ A [ Id {_} {_} {_} {A} a o f ] ≈ f ] idL1 A = IsCategory.identityL (Category.isCategory A) idR1 : { c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A a b } → A [ A [ f o Id {_} {_} {_} {A} a ] ≈ f ] idR1 A = IsCategory.identityR (Category.isCategory A) open import Relation.Binary.PropositionalEquality using ( _≡_ ) ≈←≡ : {a b : Obj A } { x y : Hom A a b } → (x≈y : x ≡ y ) → x ≈ y ≈←≡ _≡_.refl = refl-hom -- Ho← to prove this? -- ≡←≈ : {a b : Obj A } { x y : Hom A a b } → (x≈y : x ≈ y ) → x ≡ y -- ≡←≈ x≈y = irr x≈y ≡-cong : { c₁′ c₂′ ℓ′ : Level} {B : Category c₁′ c₂′ ℓ′} {x y : Obj B } { a b : Hom B x y } {x' y' : Obj A } → (f : Hom B x y → Hom A x' y' ) → a ≡ b → f a ≈ f b ≡-cong f _≡_.refl = ≈←≡ _≡_.refl -- cong-≈ : { c₁′ c₂′ ℓ′ : Level} {B : Category c₁′ c₂′ ℓ′} {x y : Obj B } { a b : Hom B x y } {x' y' : Obj A } → -- B [ a ≈ b ] → (f : Hom B x y → Hom A x' y' ) → f a ≈ f b -- cong-≈ eq f = {!!} assoc : {a b c d : Obj A } {f : Hom A c d} {g : Hom A b c} {h : Hom A a b} → f o ( g o h ) ≈ ( f o g ) o h assoc = IsCategory.associative (Category.isCategory A) -- working on another cateogry assoc1 : { c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b c d : Obj A } {f : Hom A c d} {g : Hom A b c} {h : Hom A a b} → A [ A [ f o ( A [ g o h ] ) ] ≈ A [ ( A [ f o g ] ) o h ] ] assoc1 A = IsCategory.associative (Category.isCategory A) distr : { c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} { c₁′ c₂′ ℓ′ : Level} {D : Category c₁′ c₂′ ℓ′} (T : Functor D A) → {a b c : Obj D} {g : Hom D b c} { f : Hom D a b } → A [ FMap T ( D [ g o f ] ) ≈ A [ FMap T g o FMap T f ] ] distr T = IsFunctor.distr ( isFunctor T ) resp : {a b c : Obj A} {f g : Hom A a b} {h i : Hom A b c} → f ≈ g → h ≈ i → (h o f) ≈ (i o g) resp = IsCategory.o-resp-≈ (Category.isCategory A) fcong : { c₁ c₂ ℓ : Level} {C : Category c₁ c₂ ℓ} { c₁′ c₂′ ℓ′ : Level} {D : Category c₁′ c₂′ ℓ′} {a b : Obj C} {f g : Hom C a b} → (T : Functor C D) → C [ f ≈ g ] → D [ FMap T f ≈ FMap T g ] fcong T = IsFunctor.≈-cong (isFunctor T) open NTrans nat : { c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} { c₁′ c₂′ ℓ′ : Level} {D : Category c₁′ c₂′ ℓ′} {a b : Obj D} {f : Hom D a b} {F G : Functor D A } → (η : NTrans D A F G ) → A [ A [ FMap G f o TMap η a ] ≈ A [ TMap η b o FMap F f ] ] nat η = IsNTrans.commute ( isNTrans η ) nat1 : { c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} { c₁′ c₂′ ℓ′ : Level} {D : Category c₁′ c₂′ ℓ′} {a b : Obj D} {F G : Functor D A } → (η : NTrans D A F G ) → (f : Hom D a b) → A [ A [ FMap G f o TMap η a ] ≈ A [ TMap η b o FMap F f ] ] nat1 η f = IsNTrans.commute ( isNTrans η ) infix 3 _∎ infixr 2 _≈⟨_⟩_ _≈⟨⟩_ infixr 2 _≈↑⟨_⟩_ infix 1 begin_ ------ If we have this, for example, as an axiom of a category, we can use ≡-Reasoning directly -- ≈-to-≡ : {a b : Obj A } { x y : Hom A a b } → A [ x ≈ y ] → x ≡ y -- ≈-to-≡ refl-hom = refl data _IsRelatedTo_ { a b : Obj A } ( x y : Hom A a b ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where relTo : (x≈y : x ≈ y ) → x IsRelatedTo y begin_ : { a b : Obj A } { x y : Hom A a b } → x IsRelatedTo y → x ≈ y begin relTo x≈y = x≈y _≈⟨_⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y z : Hom A a b } → x ≈ y → y IsRelatedTo z → x IsRelatedTo z _ ≈⟨ x≈y ⟩ relTo y≈z = relTo (trans-hom x≈y y≈z) _≈↑⟨_⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y z : Hom A a b } → y ≈ x → y IsRelatedTo z → x IsRelatedTo z _ ≈↑⟨ y≈x ⟩ relTo y≈z = relTo (trans-hom ( sym y≈x ) y≈z) _≈⟨⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y : Hom A a b } → x IsRelatedTo y → x IsRelatedTo y _ ≈⟨⟩ x∼y = x∼y _∎ : { a b : Obj A } ( x : Hom A a b ) → x IsRelatedTo x _∎ _ = relTo refl-hom --- -- to avoid assoc storm, flatten composition according to the template -- data MP : { a b : Obj A } ( x : Hom A a b ) → Set (c₁ ⊔ c₂ ⊔ ℓ ) where am : { a b : Obj A } → (x : Hom A a b ) → MP x _repl_by_ : { a b : Obj A } → (x y : Hom A a b ) → x ≈ y → MP y _∙_ : { a b c : Obj A } {x : Hom A b c } { y : Hom A a b } → MP x → MP y → MP ( x o y ) open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) mp-before : { a b : Obj A } { f : Hom A a b } → MP f → Hom A a b mp-before (am x) = x mp-before (x repl y by x₁) = x mp-before (m ∙ m₁) = mp-before m o mp-before m₁ mp-after : { a b : Obj A } { f : Hom A a b } → MP f → Hom A a b mp-after (am x) = x mp-after (x repl y by x₁) = y mp-after (m ∙ m₁) = mp-before m o mp-before m₁ mp≈ : { a b : Obj A } { f g : Hom A a b } → (m : MP f ) → mp-before m ≈ mp-after m mp≈ {a} {b} {f} {g} (am x) = refl-hom mp≈ {a} {b} {f} {g} (x repl y by x=y ) = x=y mp≈ {a} {b} {f} {g} (m ∙ m₁) = resp refl-hom refl-hom mpf : {a b c : Obj A } {y : Hom A b c } → (m : MP y ) → Hom A a b → Hom A a c mpf (am x) y = x o y mpf (x repl y by eq ) z = y o z mpf (m ∙ m₁) y = mpf m ( mpf m₁ y ) mp-flatten : {a b : Obj A } {x : Hom A a b } → (m : MP x ) → Hom A a b mp-flatten m = mpf m (id _) mpl1 : {a b c : Obj A } → Hom A b c → {y : Hom A a b } → MP y → Hom A a c mpl1 x (am y) = x o y mpl1 x (z repl y by eq ) = x o y mpl1 x (y ∙ y1) = mpl1 ( mpl1 x y ) y1 mpl : {a b c : Obj A } {x : Hom A b c } {z : Hom A a b } → MP x → MP z → Hom A a c mpl (am x) m = mpl1 x m mpl (y repl x by eq ) m = mpl1 x m mpl (m ∙ m1) m2 = mpl m (m1 ∙ m2) mp-flattenl : {a b : Obj A } {x : Hom A a b } → (m : MP x ) → Hom A a b mp-flattenl m = mpl m (am (id _)) _⁻¹ : {a b : Obj A } ( f : Hom A a b ) → Set c₂ _⁻¹ {a} {b} f = Hom A b a test1 : {a b c : Obj A } ( f : Hom A b c ) ( g : Hom A a b ) → ( _⁻¹ : {a b : Obj A } ( f : Hom A a b ) → Hom A b a ) → Hom A c a test1 f g _⁻¹ = mp-flattenl ((am (g ⁻¹) ∙ am (f ⁻¹) ) ∙ ( (am f ∙ am g) ∙ am ((f o g) ⁻¹ ))) test2 : {a b c : Obj A } ( f : Hom A b c ) ( g : Hom A a b ) → ( _⁻¹ : {a b : Obj A } ( f : Hom A a b ) → Hom A b a ) → test1 f g _⁻¹ ≈ ((((g ⁻¹ o f ⁻¹ )o f ) o g ) o (f o g) ⁻¹ ) o id _ test2 f g _⁻¹ = refl-hom test3 : {a b c : Obj A } ( f : Hom A b c ) ( g : Hom A a b ) → ( _⁻¹ : {a b : Obj A } ( f : Hom A a b ) → Hom A b a ) → Hom A c a test3 f g _⁻¹ = mp-flatten ((am (g ⁻¹) ∙ am (f ⁻¹) ) ∙ ( (am f ∙ am g) ∙ am ((f o g) ⁻¹ ))) test4 : {a b c : Obj A } ( f : Hom A b c ) ( g : Hom A a b ) → ( _⁻¹ : {a b : Obj A } ( f : Hom A a b ) → Hom A b a ) → test3 f g _⁻¹ ≈ g ⁻¹ o (f ⁻¹ o (f o (g o ((f o g) ⁻¹ o id _)))) test4 f g _⁻¹ = refl-hom o-flatten : {a b : Obj A } {x : Hom A a b } → (m : MP x ) → x ≈ mp-flatten m o-flatten (am y) = sym-hom (idR ) o-flatten (y repl x by eq) = sym-hom (idR ) o-flatten (am x ∙ q) = resp ( o-flatten q ) refl-hom o-flatten ((y repl x by eq) ∙ q) = resp ( o-flatten q ) refl-hom -- d <- c <- b <- a ( p ∙ q ) ∙ r , ( x o y ) o z o-flatten {a} {d} (_∙_ {a} {b} {d} {xy} {z} (_∙_ {b} {c} {d} {x} {y} p q) r) = lemma9 _ _ _ ( o-flatten {b} {d} {x o y } (p ∙ q )) ( o-flatten {a} {b} {z} r ) where mp-cong : { a b c : Obj A } → {p : Hom A b c} {q r : Hom A a b} → (P : MP p) → q ≈ r → mpf P q ≈ mpf P r mp-cong (am x) q=r = resp q=r refl-hom mp-cong (y repl x by eq) q=r = resp q=r refl-hom mp-cong (P ∙ P₁) q=r = mp-cong P ( mp-cong P₁ q=r ) mp-assoc : {a b c d : Obj A } {p : Hom A c d} {q : Hom A b c} {r : Hom A a b} → (P : MP p) → mpf P q o r ≈ mpf P (q o r ) mp-assoc (am x) = sym-hom assoc mp-assoc (y repl x by eq ) = sym-hom assoc mp-assoc {_} {_} {_} {_} {p} {q} {r} (P ∙ P₁) = begin mpf P (mpf P₁ q) o r ≈⟨ mp-assoc P ⟩ mpf P (mpf P₁ q o r) ≈⟨ mp-cong P (mp-assoc P₁) ⟩ mpf P ((mpf P₁) (q o r)) ∎ lemma9 : (x : Hom A c d) (y : Hom A b c) (z : Hom A a b) → x o y ≈ mpf p (mpf q (id _)) → z ≈ mpf r (id _) → (x o y) o z ≈ mp-flatten ((p ∙ q) ∙ r) lemma9 x y z t s = begin (x o y) o z ≈⟨ resp refl-hom t ⟩ mpf p (mpf q (id _)) o z ≈⟨ mp-assoc p ⟩ mpf p (mpf q (id _) o z) ≈⟨ mp-cong p (mp-assoc q ) ⟩ mpf p (mpf q ((id _) o z)) ≈⟨ mp-cong p (mp-cong q idL) ⟩ mpf p (mpf q z) ≈⟨ mp-cong p (mp-cong q s) ⟩ mpf p (mpf q (mpf r (id _))) ∎ -- an example Lemma61 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → { a : Obj A } ( b : Obj A ) → ( f : Hom A a b ) → A [ A [ (Id {_} {_} {_} {A} b) o f ] ≈ f ] Lemma61 c b g = -- IsCategory.identityL (Category.isCategory c) let open ≈-Reasoning (c) in begin c [ ( Id {_} {_} {_} {c} b ) o g ] ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩ g ∎ Lemma62 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → { a b : Obj A } → ( f g : Hom A a b ) → A [ A [ (Id {_} {_} {_} {A} b) o f ] ≈ A [ (Id {_} {_} {_} {A} b) o g ] ] → A [ g ≈ f ] Lemma62 A {a} {b} f g 1g=1f = let open ≈-Reasoning A in begin g ≈↑⟨ idL ⟩ id b o g ≈↑⟨ 1g=1f ⟩ id b o f ≈⟨ idL ⟩ f ∎