Mercurial > hg > Members > kono > Proof > category
changeset 1015:e01a1d29492b
Functional Completeness
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 21 Mar 2021 10:16:57 +0900 |
| parents | 4f1db956d3b4 |
| children | bbbe97d2a5ea |
| files | src/Polynominal.agda src/cokleisli.agda |
| diffstat | 2 files changed, 187 insertions(+), 164 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Polynominal.agda Sun Mar 21 00:47:00 2021 +0900 +++ b/src/Polynominal.agda Sun Mar 21 10:16:57 2021 +0900 @@ -1,101 +1,18 @@ open import Category open import CCC open import Level -open import HomReasoning +open import HomReasoning open import cat-utility module Polynominal { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( C : CCC A ) where - module coKleisli { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { S : Functor A A } (SM : coMonad A S) where - - open coMonad - - open Functor - open NTrans - --- --- Hom in Kleisli Category --- - - record SHom (a : Obj A) (b : Obj A) - : Set c₂ where - field - SMap : Hom A ( FObj S a ) b - - open SHom - - S-id : (a : Obj A) → SHom a a - S-id a = record { SMap = TMap (ε SM) a } - - open import Relation.Binary - - _⋍_ : { a : Obj A } { b : Obj A } (f g : SHom a b ) → Set ℓ - _⋍_ {a} {b} f g = A [ SMap f ≈ SMap g ] - - _*_ : { a b c : Obj A } → ( SHom b c) → ( SHom a b) → SHom a c - _*_ {a} {b} {c} g f = record { SMap = coJoin SM {a} {b} {c} (SMap g) (SMap f) } - - isSCat : IsCategory ( Obj A ) SHom _⋍_ _*_ (λ {a} → S-id a) - isSCat = record { isEquivalence = isEquivalence - ; identityL = SidL - ; identityR = SidR - ; o-resp-≈ = So-resp - ; associative = Sassoc - } - where - open ≈-Reasoning A - isEquivalence : { a b : Obj A } → IsEquivalence {_} {_} {SHom a b} _⋍_ - isEquivalence {C} {D} = record { refl = refl-hom ; sym = sym ; trans = trans-hom } - SidL : {a b : Obj A} → {f : SHom a b} → (S-id _ * f) ⋍ f - SidL {a} {b} {f} = begin - SMap (S-id _ * f) ≈⟨⟩ - (TMap (ε SM) b o (FMap S (SMap f))) o TMap (δ SM) a ≈↑⟨ car (nat (ε SM)) ⟩ - (SMap f o TMap (ε SM) (FObj S a)) o TMap (δ SM) a ≈↑⟨ assoc ⟩ - SMap f o TMap (ε SM) (FObj S a) o TMap (δ SM) a ≈⟨ cdr (IsCoMonad.unity1 (isCoMonad SM)) ⟩ - SMap f o id1 A _ ≈⟨ idR ⟩ - SMap f ∎ - SidR : {C D : Obj A} → {f : SHom C D} → (f * S-id _ ) ⋍ f - SidR {a} {b} {f} = begin - SMap (f * S-id a) ≈⟨⟩ - (SMap f o FMap S (TMap (ε SM) a)) o TMap (δ SM) a ≈↑⟨ assoc ⟩ - SMap f o (FMap S (TMap (ε SM) a) o TMap (δ SM) a) ≈⟨ cdr (IsCoMonad.unity2 (isCoMonad SM)) ⟩ - SMap f o id1 A _ ≈⟨ idR ⟩ - SMap f ∎ - So-resp : {a b c : Obj A} → {f g : SHom a b } → {h i : SHom b c } → - f ⋍ g → h ⋍ i → (h * f) ⋍ (i * g) - So-resp {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi = resp refl-hom (resp (fcong S eq-fg ) eq-hi ) - Sassoc : {a b c d : Obj A} → {f : SHom c d } → {g : SHom b c } → {h : SHom a b } → - (f * (g * h)) ⋍ ((f * g) * h) - Sassoc {a} {b} {c} {d} {f} {g} {h} = begin - SMap (f * (g * h)) ≈⟨ car (cdr (distr S)) ⟩ - (SMap f o ( FMap S (SMap g o FMap S (SMap h)) o FMap S (TMap (δ SM) a) )) o TMap (δ SM) a ≈⟨ car assoc ⟩ - ((SMap f o FMap S (SMap g o FMap S (SMap h))) o FMap S (TMap (δ SM) a) ) o TMap (δ SM) a ≈↑⟨ assoc ⟩ - (SMap f o FMap S (SMap g o FMap S (SMap h))) o (FMap S (TMap (δ SM) a) o TMap (δ SM) a ) ≈↑⟨ cdr (IsCoMonad.assoc (isCoMonad SM)) ⟩ - (SMap f o (FMap S (SMap g o FMap S (SMap h)))) o ( TMap (δ SM) (FObj S a) o TMap (δ SM) a ) ≈⟨ assoc ⟩ - ((SMap f o (FMap S (SMap g o FMap S (SMap h)))) o TMap (δ SM) (FObj S a) ) o TMap (δ SM) a ≈⟨ car (car (cdr (distr S))) ⟩ - ((SMap f o (FMap S (SMap g) o FMap S (FMap S (SMap h)))) o TMap (δ SM) (FObj S a) ) o TMap (δ SM) a ≈↑⟨ car assoc ⟩ - (SMap f o ((FMap S (SMap g) o FMap S (FMap S (SMap h))) o TMap (δ SM) (FObj S a) )) o TMap (δ SM) a ≈↑⟨ assoc ⟩ - SMap f o (((FMap S (SMap g) o FMap S (FMap S (SMap h))) o TMap (δ SM) (FObj S a) ) o TMap (δ SM) a) ≈↑⟨ cdr (car assoc ) ⟩ - SMap f o ((FMap S (SMap g) o (FMap S (FMap S (SMap h)) o TMap (δ SM) (FObj S a) )) o TMap (δ SM) a) ≈⟨ cdr (car (cdr (nat (δ SM)))) ⟩ - SMap f o ((FMap S (SMap g) o ( TMap (δ SM) b o FMap S (SMap h))) o TMap (δ SM) a) ≈⟨ assoc ⟩ - (SMap f o (FMap S (SMap g) o ( TMap (δ SM) b o FMap S (SMap h)))) o TMap (δ SM) a ≈⟨ car (cdr assoc) ⟩ - (SMap f o ((FMap S (SMap g) o TMap (δ SM) b ) o FMap S (SMap h))) o TMap (δ SM) a ≈⟨ car assoc ⟩ - ((SMap f o (FMap S (SMap g) o TMap (δ SM) b )) o FMap S (SMap h)) o TMap (δ SM) a ≈⟨ car (car assoc) ⟩ - (((SMap f o FMap S (SMap g)) o TMap (δ SM) b ) o FMap S (SMap h)) o TMap (δ SM) a ≈⟨⟩ - SMap ((f * g) * h) ∎ - - SCat : Category c₁ c₂ ℓ - SCat = record { Obj = Obj A ; Hom = SHom ; _o_ = _*_ ; _≈_ = _⋍_ ; Id = λ {a} → S-id a ; isCategory = isSCat } - - module coKleisli' { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { S : Functor A A } (SM : coMonad A S) where - open CCC.CCC C open coMonad open Functor open NTrans open import Category.Cat - open ≈-Reasoning A + open ≈-Reasoning A hiding (_∙_) SA : (a : Obj A) → Functor A A SA a = record { FObj = λ x → a ∧ x @@ -162,37 +79,48 @@ < π , < π , id1 A _ > o ( π' o < π , id1 A _ > ) > ≈↑⟨ IsCCC.π-cong isCCC (IsCCC.e3a isCCC) (sym assoc) ⟩ < π o < π , id1 A _ > , (< π , id1 A _ > o π' ) o < π , id1 A _ > > ≈↑⟨ IsCCC.distr-π isCCC ⟩ FMap (SA a) < π , id1 A (a ∧ x) > o < π , id1 A _ > ∎ + -- + -- coKleisli category of SM should give the fucntional completeness + -- - + _∙_ = _[_o_] A - -- open import deductive A C - - _・_ = _[_o_] A - - -- every proof b → c with assumption a has following forms + -- + -- Polynominal (p.57) in Introduction to Higher order categorical logic + -- + -- Given object a₀ and a of a caterisian closed category A, how does one adjoin an interminate arraow x : a₀ → a to A? + -- A[x] based on the `assumption' x, as was done in Section 2 (data φ). The formulas of A[x] are the objects of A and the + -- proofs of A[x] are formed from the arrows of A and the new arrow x : a₀ → a by the appropriate ules of inference. -- -- Here, A is actualy A[x]. It contains x and all the arrow generated from x. - -- If we can put constraints on rule i, then A is strictly smaller than A[x]. + -- If we can put constraints on rule i (sub : Hom A b c → Set), then A is strictly smaller than A[x], + -- that is, a subscategory of A[x]. + -- + -- i : {b c : Obj A} {k : Hom A b c } → sub k → φ x k + -- + -- this makes a few changes, but we don't care. + -- from page. 51 -- data φ {a ⊤ : Obj A } ( x : Hom A ⊤ a ) : {b c : Obj A } → Hom A b c → Set ( c₁ ⊔ c₂ ⊔ ℓ) where - i : {b c : Obj A} {k : Hom A b c } → φ x k + i : {b c : Obj A} {k : Hom A b c } → φ x k ii : φ x {⊤} {a} x iii : {b c' c'' : Obj A } { f : Hom A b c' } { g : Hom A b c'' } (ψ : φ x f ) (χ : φ x g ) → φ x {b} {c' ∧ c''} < f , g > - iv : {b c d : Obj A } { f : Hom A d c } { g : Hom A b d } (ψ : φ x f ) (χ : φ x g ) → φ x ( f ・ g ) + iv : {b c d : Obj A } { f : Hom A d c } { g : Hom A b d } (ψ : φ x f ) (χ : φ x g ) → φ x ( f ∙ g ) v : {b c' c'' : Obj A } { f : Hom A (b ∧ c') c'' } (ψ : φ x f ) → φ x {b} {c'' <= c'} ( f * ) φ-cong : {b c : Obj A} {k k' : Hom A b c } → A [ k ≈ k' ] → φ x k → φ x k' α : {a b c : Obj A } → Hom A (( a ∧ b ) ∧ c ) ( a ∧ ( b ∧ c ) ) - α = < π ・ π , < π' ・ π , π' > > + α = < π ∙ π , < π' ∙ π , π' > > -- genetate (a ∧ b) → c proof from proof b → c with assumption a + -- from page. 51 k : {a ⊤ b c : Obj A } → ( x∈a : Hom A ⊤ a ) → {z : Hom A b c } → ( y : φ {a} x∈a z ) → Hom A (a ∧ b) c - k x∈a {k} i = k ・ π' + k x∈a {k} i = k ∙ π' k x∈a ii = π k x∈a (iii ψ χ ) = < k x∈a ψ , k x∈a χ > - k x∈a (iv ψ χ ) = k x∈a ψ ・ < π , k x∈a χ > - k x∈a (v ψ ) = ( k x∈a ψ ・ α ) * + k x∈a (iv ψ χ ) = k x∈a ψ ∙ < π , k x∈a χ > + k x∈a (v ψ ) = ( k x∈a ψ ∙ α ) * k x∈a (φ-cong eq ψ) = k x∈a ψ toφ : {a ⊤ b c : Obj A } → ( x∈a : Hom A ⊤ a ) → (z : Hom A b c ) → φ {a} x∈a z @@ -204,18 +132,13 @@ phi : φ x {b} {c} hom open PHom - -- open import HomReasoning - -- open import cat-utility - -- date _≅_ : {a b c : Hom A} → { x : Hom A ⊤ a } → (f g : PHom b c ) → Set (c₁ ⊔ c₂ ⊔ ℓ) where - -- pcomp : { a b c : Hom A } → A [ A [ hom g o hom f ] ≈ hom h ] → (A [ hom g o hom f ]) ≅ hom h - - -- this is too easy, so what is A[x]? + -- A is A[x] Polynominal : {a ⊤ : Obj A } ( x : Hom A ⊤ a ) → Category c₁ (c₁ ⊔ c₂ ⊔ ℓ) ℓ Polynominal {a} {⊤} x = record { Obj = Obj A; Hom = λ b c → PHom {a} {⊤} {x} b c ; - _o_ = λ{a} {b} {c} x y → record { hom = A [ hom x o hom y ] ; phi = iv (phi x) (phi y) } ; + _o_ = λ{a} {b} {c} x y → record { hom = hom x ∙ hom y ; phi = iv (phi x) (phi y) } ; _≈_ = λ x y → A [ hom x ≈ hom y ] ; Id = λ{a} → record { hom = id1 A a ; phi = i } ; isCategory = record { @@ -238,90 +161,103 @@ } } + -- + -- Proposition 6.1 + -- + -- For every polynominal ψ(x) : b → c in an indeterminate x : 1 → a over a cartesian or cartesian closed + -- category A there is a unique arrow f : a ∧ b → c in A such that f ∙ < x ∙ ○ b , id1 A b > ≈ ψ(x). + -- + record Functional-completeness {a : Obj A} ( x : Hom A １ a ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where field fun : {b c : Obj A} → PHom {a} {１} {x} b c → Hom A (a ∧ b) c - fp : {b c : Obj A} → (p : PHom b c) → A [ A [ fun p o < A [ x o ○ b ] , id1 A b > ] ≈ hom p ] - uniq : {b c : Obj A} → (p : PHom b c) → (f : Hom A (a ∧ b) c) → A [ A [ f o < A [ x o ○ b ] , id1 A b > ] ≈ hom p ] + fp : {b c : Obj A} → (p : PHom b c) → A [ fun p ∙ < x ∙ ○ b , id1 A b > ≈ hom p ] + uniq : {b c : Obj A} → (p : PHom b c) → (f : Hom A (a ∧ b) c) → A [ f ∙ < x ∙ ○ b , id1 A b > ≈ hom p ] → A [ f ≈ fun p ] + π-cong = IsCCC.π-cong isCCC + e2 = IsCCC.e2 isCCC + {-# TERMINATING #-} functional-completeness : {a : Obj A} ( x : Hom A １ a ) → Functional-completeness x functional-completeness {a} x = record { fun = λ y → k x (phi y) ; fp = fc0 ; uniq = uniq - } where + } where open φ - fc0 : {b c : Obj A} (p : PHom b c) → A [ A [ k x (phi p) o < A [ x o ○ b ] , id1 A b > ] ≈ hom p ] + fc0 : {b c : Obj A} (p : PHom b c) → A [ k x (phi p) ∙ < x ∙ ○ b , id1 A b > ≈ hom p ] fc0 {b} {c} p with phi p ... | i {_} {_} {s} = begin - (s o π') o < ( x o ○ b ) , id1 A b > ≈↑⟨ assoc ⟩ - s o (π' o < ( x o ○ b ) , id1 A b >) ≈⟨ cdr (IsCCC.e3b isCCC ) ⟩ - s o id1 A b ≈⟨ idR ⟩ + (s ∙ π') ∙ < ( x ∙ ○ b ) , id1 A b > ≈↑⟨ assoc ⟩ + s ∙ (π' ∙ < ( x ∙ ○ b ) , id1 A b >) ≈⟨ cdr (IsCCC.e3b isCCC ) ⟩ + s ∙ id1 A b ≈⟨ idR ⟩ s ∎ ... | ii = begin - π o < ( x o ○ b ) , id1 A b > ≈⟨ IsCCC.e3a isCCC ⟩ - x o ○ b ≈↑⟨ cdr (IsCCC.e2 isCCC ) ⟩ - x o id1 A b ≈⟨ idR ⟩ + π ∙ < ( x ∙ ○ b ) , id1 A b > ≈⟨ IsCCC.e3a isCCC ⟩ + x ∙ ○ b ≈↑⟨ cdr (e2 ) ⟩ + x ∙ id1 A b ≈⟨ idR ⟩ x ∎ ... | iii {_} {_} {_} {f} {g} y z = begin - < k x y , k x z > o < (x o ○ b ) , id1 A b > ≈⟨ IsCCC.distr-π isCCC ⟩ - < k x y o < (x o ○ b ) , id1 A b > , k x z o < (x o ○ b ) , id1 A b > > - ≈⟨ IsCCC.π-cong isCCC (fc0 record { hom = f ; phi = y } ) (fc0 record { hom = g ; phi = z } ) ⟩ + < k x y , k x z > ∙ < (x ∙ ○ b ) , id1 A b > ≈⟨ IsCCC.distr-π isCCC ⟩ + < k x y ∙ < (x ∙ ○ b ) , id1 A b > , k x z ∙ < (x ∙ ○ b ) , id1 A b > > + ≈⟨ π-cong (fc0 record { hom = f ; phi = y } ) (fc0 record { hom = g ; phi = z } ) ⟩ < f , g > ≈⟨⟩ hom p ∎ ... | iv {_} {_} {d} {f} {g} y z = begin - (k x y o < π , k x z >) o < ( x o ○ b ) , id1 A b > ≈↑⟨ assoc ⟩ - k x y o ( < π , k x z > o < ( x o ○ b ) , id1 A b > ) ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩ - k x y o ( < π o < ( x o ○ b ) , id1 A b > , k x z o < ( x o ○ b ) , id1 A b > > ) - ≈⟨ cdr (IsCCC.π-cong isCCC (IsCCC.e3a isCCC) (fc0 record { hom = g ; phi = z} ) ) ⟩ - k x y o ( < x o ○ b , g > ) ≈↑⟨ cdr (IsCCC.π-cong isCCC (cdr (IsCCC.e2 isCCC)) refl-hom ) ⟩ - k x y o ( < x o ( ○ d o g ) , g > ) ≈⟨ cdr (IsCCC.π-cong isCCC assoc (sym idL)) ⟩ - k x y o ( < (x o ○ d) o g , id1 A d o g > ) ≈↑⟨ cdr (IsCCC.distr-π isCCC) ⟩ - k x y o ( < x o ○ d , id1 A d > o g ) ≈⟨ assoc ⟩ - (k x y o < x o ○ d , id1 A d > ) o g ≈⟨ car (fc0 record { hom = f ; phi = y }) ⟩ - f o g ∎ + (k x y ∙ < π , k x z >) ∙ < ( x ∙ ○ b ) , id1 A b > ≈↑⟨ assoc ⟩ + k x y ∙ ( < π , k x z > ∙ < ( x ∙ ○ b ) , id1 A b > ) ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩ + k x y ∙ ( < π ∙ < ( x ∙ ○ b ) , id1 A b > , k x z ∙ < ( x ∙ ○ b ) , id1 A b > > ) + ≈⟨ cdr (π-cong (IsCCC.e3a isCCC) (fc0 record { hom = g ; phi = z} ) ) ⟩ + k x y ∙ ( < x ∙ ○ b , g > ) ≈↑⟨ cdr (π-cong (cdr (e2)) refl-hom ) ⟩ + k x y ∙ ( < x ∙ ( ○ d ∙ g ) , g > ) ≈⟨ cdr (π-cong assoc (sym idL)) ⟩ + k x y ∙ ( < (x ∙ ○ d) ∙ g , id1 A d ∙ g > ) ≈↑⟨ cdr (IsCCC.distr-π isCCC) ⟩ + k x y ∙ ( < x ∙ ○ d , id1 A d > ∙ g ) ≈⟨ assoc ⟩ + (k x y ∙ < x ∙ ○ d , id1 A d > ) ∙ g ≈⟨ car (fc0 record { hom = f ; phi = y }) ⟩ + f ∙ g ∎ ... | v {_} {_} {_} {f} y = begin - ( (k x y o < π o π , < π' o π , π' > >) *) o < x o (○ b) , id1 A b > ≈⟨ IsCCC.distr-* isCCC ⟩ - ( (k x y o < π o π , < π' o π , π' > >) o < < x o ○ b , id1 A _ > o π , π' > ) * ≈⟨ IsCCC.*-cong isCCC ( begin - ( k x y o < π o π , < π' o π , π' > >) o < < x o ○ b , id1 A _ > o π , π' > ≈↑⟨ assoc ⟩ - k x y o ( < π o π , < π' o π , π' > > o < < x o ○ b , id1 A _ > o π , π' > ) ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩ - k x y o < (π o π) o < < x o ○ b , id1 A _ > o π , π' > , < π' o π , π' > o < < x o ○ b , id1 A _ > o π , π' > > - ≈⟨ cdr (IsCCC.π-cong isCCC (sym assoc) (IsCCC.distr-π isCCC )) ⟩ - k x y o < π o (π o < < x o ○ b , id1 A _ > o π , π' > ) , - < (π' o π) o < < x o ○ b , id1 A _ > o π , π' > , π' o < < x o ○ b , id1 A _ > o π , π' > > > - ≈⟨ cdr ( IsCCC.π-cong isCCC (cdr (IsCCC.e3a isCCC))( IsCCC.π-cong isCCC (sym assoc) (IsCCC.e3b isCCC) )) ⟩ - k x y o < π o ( < x o ○ b , id1 A _ > o π ) , < π' o (π o < < x o ○ b , id1 A _ > o π , π' >) , π' > > - ≈⟨ cdr ( IsCCC.π-cong isCCC refl-hom ( IsCCC.π-cong isCCC (cdr (IsCCC.e3a isCCC)) refl-hom )) ⟩ - k x y o < (π o < x o ○ b , id1 A _ > o π ) , < π' o (< x o ○ b , id1 A _ > o π ) , π' > > - ≈⟨ cdr ( IsCCC.π-cong isCCC assoc (IsCCC.π-cong isCCC assoc refl-hom )) ⟩ - k x y o < (π o < x o ○ b , id1 A _ > ) o π , < (π' o < x o ○ b , id1 A _ > ) o π , π' > > - ≈⟨ cdr (IsCCC.π-cong isCCC (car (IsCCC.e3a isCCC)) (IsCCC.π-cong isCCC (car (IsCCC.e3b isCCC)) refl-hom )) ⟩ - k x y o < ( (x o ○ b ) o π ) , < id1 A _ o π , π' > > ≈⟨ cdr (IsCCC.π-cong isCCC (sym assoc) (IsCCC.π-cong isCCC idL refl-hom )) ⟩ - k x y o < x o (○ b o π ) , < π , π' > > ≈⟨ cdr (IsCCC.π-cong isCCC (cdr (IsCCC.e2 isCCC)) (IsCCC.π-id isCCC) ) ⟩ - k x y o < x o ○ _ , id1 A _ > ≈⟨ fc0 record { hom = f ; phi = y} ⟩ + ( (k x y ∙ < π ∙ π , < π' ∙ π , π' > >) *) ∙ < x ∙ (○ b) , id1 A b > ≈⟨ IsCCC.distr-* isCCC ⟩ + ( (k x y ∙ < π ∙ π , < π' ∙ π , π' > >) ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' > ) * ≈⟨ IsCCC.*-cong isCCC ( begin + ( k x y ∙ < π ∙ π , < π' ∙ π , π' > >) ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' > ≈↑⟨ assoc ⟩ + k x y ∙ ( < π ∙ π , < π' ∙ π , π' > > ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' > ) ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩ + k x y ∙ < (π ∙ π) ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' > , < π' ∙ π , π' > ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' > > + ≈⟨ cdr (π-cong (sym assoc) (IsCCC.distr-π isCCC )) ⟩ + k x y ∙ < π ∙ (π ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' > ) , + < (π' ∙ π) ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' > , π' ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' > > > + ≈⟨ cdr ( π-cong (cdr (IsCCC.e3a isCCC))( π-cong (sym assoc) (IsCCC.e3b isCCC) )) ⟩ + k x y ∙ < π ∙ ( < x ∙ ○ b , id1 A _ > ∙ π ) , < π' ∙ (π ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' >) , π' > > + ≈⟨ cdr ( π-cong refl-hom ( π-cong (cdr (IsCCC.e3a isCCC)) refl-hom )) ⟩ + k x y ∙ < (π ∙ ( < x ∙ ○ b , id1 A _ > ∙ π ) ) , < π' ∙ (< x ∙ ○ b , id1 A _ > ∙ π ) , π' > > + ≈⟨ cdr ( π-cong assoc (π-cong assoc refl-hom )) ⟩ + k x y ∙ < (π ∙ < x ∙ ○ b , id1 A _ > ) ∙ π , < (π' ∙ < x ∙ ○ b , id1 A _ > ) ∙ π , π' > > + ≈⟨ cdr (π-cong (car (IsCCC.e3a isCCC)) (π-cong (car (IsCCC.e3b isCCC)) refl-hom )) ⟩ + k x y ∙ < ( (x ∙ ○ b ) ∙ π ) , < id1 A _ ∙ π , π' > > ≈⟨ cdr (π-cong (sym assoc) (π-cong idL refl-hom )) ⟩ + k x y ∙ < x ∙ (○ b ∙ π ) , < π , π' > > ≈⟨ cdr (π-cong (cdr (e2)) (IsCCC.π-id isCCC) ) ⟩ + k x y ∙ < x ∙ ○ _ , id1 A _ > ≈⟨ fc0 record { hom = f ; phi = y} ⟩ f ∎ ) ⟩ f * ∎ ... | φ-cong {_} {_} {f} {f'} f=f' y = trans-hom (fc0 record { hom = f ; phi = y}) f=f' + -- + -- f ∙ < x ∙ ○ b , id1 A b > ≈ hom p → f ≈ k x (phi p) + -- uniq : {b c : Obj A} (p : PHom b c) (f : Hom A (a ∧ b) c) → - A [ A [ f o < A [ x o ○ b ] , id1 A b > ] ≈ hom p ] → A [ f ≈ k x (phi p) ] - uniq {b} {c} p f fx=p with phi p - ... | i {_} {_} {s} = begin -- f o < x o ○ b , id1 A b > ≈ s - f ≈↑⟨ idR ⟩ - f o id1 A (a ∧ b) ≈⟨ {!!} ⟩ - f o (< x o ○ b , id1 A b > o π' ) ≈⟨ assoc ⟩ - (f o < x o ○ b , id1 A b > ) o π' ≈⟨ car fx=p ⟩ - s o π' ∎ - ... | ii = begin -- fx=p : f o < x o ○ b , id1 A b > ≈ x - f ≈⟨ {!!} ⟩ - π ∎ - ... | iii {_} {_} {_} {g} {h} y z = begin -- fx=p : f o < x o ○ b , id1 A b > ≈ < g , h > - f ≈⟨ {!!} ⟩ - < k x y , k x z > ∎ - ... | iv t t₁ = {!!} - ... | v t = {!!} - ... | φ-cong x t = {!!} - + A [ f ∙ < x ∙ ○ b , id1 A b > ≈ hom p ] → A [ f ≈ k x (phi p) ] + uniq {b} {c} p f fx=p = sym (begin + k x (phi p) ≈⟨ fc1 p ⟩ + k x {hom p} i ≈⟨⟩ + hom p ∙ π' ≈↑⟨ car fx=p ⟩ + (f ∙ < x ∙ ○ b , id1 A b > ) ∙ π' ≈↑⟨ assoc ⟩ + f ∙ (< x ∙ ○ b , id1 A b > ∙ π') ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩ + f ∙ < (x ∙ ○ b) ∙ π' , id1 A b ∙ π' > ≈⟨⟩ + f ∙ < k x {x ∙ ○ b} i , id1 A b ∙ π' > ≈⟨ cdr (π-cong (sym (fc1 record { hom = x ∙ ○ b ; phi = iv ii i } )) refl-hom) ⟩ + f ∙ < k x (phi record { hom = x ∙ ○ b ; phi = iv ii i }) , id1 A b ∙ π' > ≈⟨ cdr (π-cong refl-hom idL) ⟩ + f ∙ < π ∙ < π , (○ b ∙ π' ) > , π' > ≈⟨ cdr (π-cong (IsCCC.e3a isCCC) refl-hom) ⟩ + f ∙ < π , π' > ≈⟨ cdr (IsCCC.π-id isCCC) ⟩ + f ∙ id1 A _ ≈⟨ idR ⟩ + f ∎ ) where + fc1 : {b c : Obj A} (p : PHom b c) → A [ k x (phi p) ≈ k x {hom p} i ] -- it looks like (*) in page 60 + fc1 {b} {c} p = uniq record { hom = hom p ; phi = i } ( k x (phi p)) ( begin -- non terminating because of the record, which we may avoid + k x (phi p) ∙ < x ∙ ○ b , id1 A b > ≈⟨ fc0 p ⟩ + hom p ∎ ) -- end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/cokleisli.agda Sun Mar 21 10:16:57 2021 +0900 @@ -0,0 +1,87 @@ +open import Category +open import Level +open import HomReasoning +open import cat-utility + + +module coKleisli { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { S : Functor A A } (SM : coMonad A S) where + + open coMonad + + open Functor + open NTrans + +-- +-- Hom in Kleisli Category +-- + + record SHom (a : Obj A) (b : Obj A) + : Set c₂ where + field + SMap : Hom A ( FObj S a ) b + + open SHom + + S-id : (a : Obj A) → SHom a a + S-id a = record { SMap = TMap (ε SM) a } + + open import Relation.Binary + + _⋍_ : { a : Obj A } { b : Obj A } (f g : SHom a b ) → Set ℓ + _⋍_ {a} {b} f g = A [ SMap f ≈ SMap g ] + + _*_ : { a b c : Obj A } → ( SHom b c) → ( SHom a b) → SHom a c + _*_ {a} {b} {c} g f = record { SMap = coJoin SM {a} {b} {c} (SMap g) (SMap f) } + + isSCat : IsCategory ( Obj A ) SHom _⋍_ _*_ (λ {a} → S-id a) + isSCat = record { isEquivalence = isEquivalence + ; identityL = SidL + ; identityR = SidR + ; o-resp-≈ = So-resp + ; associative = Sassoc + } + where + open ≈-Reasoning A + isEquivalence : { a b : Obj A } → IsEquivalence {_} {_} {SHom a b} _⋍_ + isEquivalence {C} {D} = record { refl = refl-hom ; sym = sym ; trans = trans-hom } + SidL : {a b : Obj A} → {f : SHom a b} → (S-id _ * f) ⋍ f + SidL {a} {b} {f} = begin + SMap (S-id _ * f) ≈⟨⟩ + (TMap (ε SM) b o (FMap S (SMap f))) o TMap (δ SM) a ≈↑⟨ car (nat (ε SM)) ⟩ + (SMap f o TMap (ε SM) (FObj S a)) o TMap (δ SM) a ≈↑⟨ assoc ⟩ + SMap f o TMap (ε SM) (FObj S a) o TMap (δ SM) a ≈⟨ cdr (IsCoMonad.unity1 (isCoMonad SM)) ⟩ + SMap f o id1 A _ ≈⟨ idR ⟩ + SMap f ∎ + SidR : {C D : Obj A} → {f : SHom C D} → (f * S-id _ ) ⋍ f + SidR {a} {b} {f} = begin + SMap (f * S-id a) ≈⟨⟩ + (SMap f o FMap S (TMap (ε SM) a)) o TMap (δ SM) a ≈↑⟨ assoc ⟩ + SMap f o (FMap S (TMap (ε SM) a) o TMap (δ SM) a) ≈⟨ cdr (IsCoMonad.unity2 (isCoMonad SM)) ⟩ + SMap f o id1 A _ ≈⟨ idR ⟩ + SMap f ∎ + So-resp : {a b c : Obj A} → {f g : SHom a b } → {h i : SHom b c } → + f ⋍ g → h ⋍ i → (h * f) ⋍ (i * g) + So-resp {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi = resp refl-hom (resp (fcong S eq-fg ) eq-hi ) + Sassoc : {a b c d : Obj A} → {f : SHom c d } → {g : SHom b c } → {h : SHom a b } → + (f * (g * h)) ⋍ ((f * g) * h) + Sassoc {a} {b} {c} {d} {f} {g} {h} = begin + SMap (f * (g * h)) ≈⟨ car (cdr (distr S)) ⟩ + (SMap f o ( FMap S (SMap g o FMap S (SMap h)) o FMap S (TMap (δ SM) a) )) o TMap (δ SM) a ≈⟨ car assoc ⟩ + ((SMap f o FMap S (SMap g o FMap S (SMap h))) o FMap S (TMap (δ SM) a) ) o TMap (δ SM) a ≈↑⟨ assoc ⟩ + (SMap f o FMap S (SMap g o FMap S (SMap h))) o (FMap S (TMap (δ SM) a) o TMap (δ SM) a ) ≈↑⟨ cdr (IsCoMonad.assoc (isCoMonad SM)) ⟩ + (SMap f o (FMap S (SMap g o FMap S (SMap h)))) o ( TMap (δ SM) (FObj S a) o TMap (δ SM) a ) ≈⟨ assoc ⟩ + ((SMap f o (FMap S (SMap g o FMap S (SMap h)))) o TMap (δ SM) (FObj S a) ) o TMap (δ SM) a ≈⟨ car (car (cdr (distr S))) ⟩ + ((SMap f o (FMap S (SMap g) o FMap S (FMap S (SMap h)))) o TMap (δ SM) (FObj S a) ) o TMap (δ SM) a ≈↑⟨ car assoc ⟩ + (SMap f o ((FMap S (SMap g) o FMap S (FMap S (SMap h))) o TMap (δ SM) (FObj S a) )) o TMap (δ SM) a ≈↑⟨ assoc ⟩ + SMap f o (((FMap S (SMap g) o FMap S (FMap S (SMap h))) o TMap (δ SM) (FObj S a) ) o TMap (δ SM) a) ≈↑⟨ cdr (car assoc ) ⟩ + SMap f o ((FMap S (SMap g) o (FMap S (FMap S (SMap h)) o TMap (δ SM) (FObj S a) )) o TMap (δ SM) a) ≈⟨ cdr (car (cdr (nat (δ SM)))) ⟩ + SMap f o ((FMap S (SMap g) o ( TMap (δ SM) b o FMap S (SMap h))) o TMap (δ SM) a) ≈⟨ assoc ⟩ + (SMap f o (FMap S (SMap g) o ( TMap (δ SM) b o FMap S (SMap h)))) o TMap (δ SM) a ≈⟨ car (cdr assoc) ⟩ + (SMap f o ((FMap S (SMap g) o TMap (δ SM) b ) o FMap S (SMap h))) o TMap (δ SM) a ≈⟨ car assoc ⟩ + ((SMap f o (FMap S (SMap g) o TMap (δ SM) b )) o FMap S (SMap h)) o TMap (δ SM) a ≈⟨ car (car assoc) ⟩ + (((SMap f o FMap S (SMap g)) o TMap (δ SM) b ) o FMap S (SMap h)) o TMap (δ SM) a ≈⟨⟩ + SMap ((f * g) * h) ∎ + + SCat : Category c₁ c₂ ℓ + SCat = record { Obj = Obj A ; Hom = SHom ; _o_ = _*_ ; _≈_ = _⋍_ ; Id = λ {a} → S-id a ; isCategory = isSCat } +