Mercurial > hg > Members > kono > Proof > category
changeset 474:2d32ded94aaf
clean up
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 07 Mar 2017 08:27:33 +0900 |
| parents | f3d6d0275a0a |
| children | 4c0a955b651d |
| files | discrete.agda kleisli.agda limit-to.agda |
| diffstat | 3 files changed, 24 insertions(+), 23 deletions(-) [+] |
line wrap: on
line diff
--- a/discrete.agda Tue Mar 07 03:21:46 2017 +0900 +++ b/discrete.agda Tue Mar 07 08:27:33 2017 +0900 @@ -101,7 +101,7 @@ record DiscreteHom { c₁ : Level} { S : Set c₁} (a : DiscreteObj {c₁} S) (b : DiscreteObj {c₁} S) : Set c₁ where field - discrete : a ≡ b + discrete : a ≡ b -- if f : a → b then a ≡ b dom : DiscreteObj S dom = a @@ -125,7 +125,7 @@ Obj = DiscreteObj {c₁} S ; Hom = λ a b → DiscreteHom {c₁} {S} a b ; _o_ = λ{a} {b} {c} x y → _*_ {c₁ } {S} {a} {b} {c} x y ; - _≈_ = λ x y → dom x ≡ dom y ; + _≈_ = λ x y → dom x ≡ dom y ; -- x ≡ y does not work because refl ≡ discrete f is failed as it should be Id = λ{a} → DiscreteId a ; isCategory = record { isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ;
--- a/kleisli.agda Tue Mar 07 03:21:46 2017 +0900 +++ b/kleisli.agda Tue Mar 07 08:27:33 2017 +0900 @@ -192,12 +192,14 @@ -- Lemma10 : {a b c : Obj A} → (f g : Hom A a (FObj T b) ) → (h i : Hom A b (FObj T c) ) → A [ f ≈ g ] → A [ h ≈ i ] → A [ (join M h f) ≈ (join M i g) ] -Lemma10 {a} {b} {c} f g h i eq-fg eq-hi = let open ≈-Reasoning (A) in +Lemma10 {a} {b} {c} f g h i f≈g h≈i = let open ≈-Reasoning (A) in begin join M h f ≈⟨⟩ TMap μ c o ( FMap T h o f ) - ≈⟨ cdr ( IsCategory.o-resp-≈ (Category.isCategory A) eq-fg ((IsFunctor.≈-cong (isFunctor T)) eq-hi )) ⟩ + ≈⟨ cdr ( car ( fcong T h≈i )) ⟩ + TMap μ c o ( FMap T i o f ) + ≈⟨ cdr ( cdr f≈g ) ⟩ TMap μ c o ( FMap T i o g ) ≈⟨⟩ join M i g @@ -332,7 +334,7 @@ ffmap : {a b : Obj A} (f : Hom A a b) → KHom a b -ffmap f = record { KMap = A [ TMap η (Category.cod A f) o f ] } +ffmap {a} {b} f = record { KMap = A [ TMap η b o f ] } F_T : Functor A KleisliCategory F_T = record { @@ -347,10 +349,10 @@ identity : {a : Obj A} → A [ A [ TMap η a o id1 A a ] ≈ TMap η a ] identity {a} = IsCategory.identityR ( Category.isCategory A) -- Category.cod A f and Category.cod A g are actualy the same b, so we don't need cong-≈, just refl - lemma1 : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → A [ TMap η b ≈ TMap η b ] - lemma1 f≈g = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A )) - ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → A [ A [ TMap η (Category.cod A f) o f ] ≈ A [ TMap η (Category.cod A g) o g ] ] - ≈-cong f≈g = (IsCategory.o-resp-≈ (Category.isCategory A)) f≈g ( lemma1 f≈g ) + lemma1 : {b : Obj A} → A [ TMap η b ≈ TMap η b ] + lemma1 = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A )) + ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → A [ A [ TMap η b o f ] ≈ A [ TMap η b o g ] ] + ≈-cong f≈g = (IsCategory.o-resp-≈ (Category.isCategory A)) f≈g lemma1 distr1 : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → ( ffmap (A [ g o f ]) ⋍ ( ffmap g * ffmap f ) ) distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in
--- a/limit-to.agda Tue Mar 07 03:21:46 2017 +0900 +++ b/limit-to.agda Tue Mar 07 08:27:33 2017 +0900 @@ -241,17 +241,16 @@ discrete-identity : { c₁ : Level} { S : Set c₁} { a : DiscreteObj {c₁} S } → (f : DiscreteHom a a ) → (DiscreteCat S) [ f ≈ id1 (DiscreteCat S) a ] discrete-identity f = refl -pnat : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (S : Set c₁) (comp : Complete A ( DiscreteCat S ) ) +pnat : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (S : Set c₁) → (Γ : Functor (DiscreteCat S ) A ) - → (q : Obj A ) ( qi : (i : Obj ( DiscreteCat S)) → Hom A q (FObj Γ i) ) + → {q : Obj A } ( qi : (i : Obj ( DiscreteCat S)) → Hom A q (FObj Γ i) ) → NTrans (DiscreteCat S )A (K A (DiscreteCat S) q) Γ -pnat A S comp Γ q qi = record { +pnat A S Γ {q} qi = record { TMap = qi ; isNTrans = record { commute = λ {a} {b} {f} → commute {a} {b} {f} } } where commute : {a b : Obj (DiscreteCat S) } {f : Hom ( DiscreteCat S) a b} → - A [ A [ FMap Γ f o qi a ] ≈ - A [ qi b o FMap (K A (DiscreteCat S )q) f ] ] + A [ A [ FMap Γ f o qi a ] ≈ A [ qi b o FMap (K A (DiscreteCat S )q) f ] ] commute {a} {b} {f} with discrete f commute {a} {.a} {f} | refl = let open ≈-Reasoning A in begin FMap Γ f o qi a @@ -284,29 +283,29 @@ p = limit-c comp Γ pi = λ i → TMap (limit-u comp Γ) i iproduct : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → Hom A q p - iproduct {q} qi = limit lim q (pnat A S comp Γ q qi ) + iproduct {q} qi = limit lim q (pnat A S Γ qi ) pif=q : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ∀ { i : I } → A [ A [ ( pi i ) o ( iproduct qi ) ] ≈ (qi i) ] - pif=q {q} qi {i} = t0f=t lim {q} {pnat A S comp Γ q qi } {i} + pif=q {q} qi {i} = t0f=t lim {q} {pnat A S Γ qi } {i} ipu : {i : Obj D} → (q : Obj A) (h : Hom A q p ) → A [ A [ TMap (limit-u comp Γ) i o h ] ≈ A [ pi i o h ] ] ipu {i} q h = let open ≈-Reasoning A in refl-hom ip-uniqueness : {q : Obj A} { h : Hom A q p } → A [ iproduct ( λ (i : I) → A [ (pi i) o h ] ) ≈ h ] - ip-uniqueness {q} {h} = limit-uniqueness lim {q} {pnat A S comp Γ q (λ i → A [ pi i o h ] )} h (ipu q h) + ip-uniqueness {q} {h} = limit-uniqueness lim {q} {pnat A S Γ (λ i → A [ pi i o h ] )} h (ipu q h) ipc : {q : Obj A} → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) } → (i : I ) → A [ qi i ≈ qi' i ] → - A [ A [ TMap (limit-u comp Γ) i o iproduct qi' ] ≈ TMap (pnat A S comp Γ q qi) i ] + A [ A [ TMap (limit-u comp Γ) i o iproduct qi' ] ≈ TMap (pnat A S Γ qi) i ] ipc {q} {qi} {qi'} i qi=qi' = let open ≈-Reasoning A in begin TMap (limit-u comp Γ) i o iproduct qi' ≈⟨⟩ - TMap (limit-u comp Γ) i o limit lim q (pnat A S comp Γ q qi' ) - ≈⟨ t0f=t lim {q} {pnat A S comp Γ q qi'} {i} ⟩ - TMap (pnat A S comp Γ q qi') i + TMap (limit-u comp Γ) i o limit lim q (pnat A S Γ qi' ) + ≈⟨ t0f=t lim {q} {pnat A S Γ qi'} {i} ⟩ + TMap (pnat A S Γ qi') i ≈⟨⟩ qi' i ≈↑⟨ qi=qi' ⟩ qi i ≈⟨⟩ - TMap (pnat A S comp Γ q qi) i + TMap (pnat A S Γ qi) i ∎ ip-cong : {q : Obj A} → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) } → ( ∀ (i : I ) → A [ qi i ≈ qi' i ] ) → A [ iproduct qi ≈ iproduct qi' ] - ip-cong {q} {qi} {qi'} qi=qi' = limit-uniqueness lim {q} {pnat A S comp Γ q qi} (iproduct qi' ) (λ {i} → ipc {q} {qi} {qi'} i (qi=qi' i)) + ip-cong {q} {qi} {qi'} qi=qi' = limit-uniqueness lim {q} {pnat A S Γ qi} (iproduct qi' ) (λ {i} → ipc {q} {qi} {qi'} i (qi=qi' i))