Mercurial > hg > Members > kono > Proof > category

comparison monoidal.agda @ 769:43138aead09b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 12 Dec 2017 10:57:56 +0900
parents 9bcdbfbaaa39
children e5850e68be22
comparison
equal deleted inserted replaced
768:9bcdbfbaaa39 769:43138aead09b
261 field 261 field
262 MF : Functor C D 262 MF : Functor C D
263 ψ : Hom D (Monoidal.m-i N) (FObj MF (Monoidal.m-i M) ) 263 ψ : Hom D (Monoidal.m-i N) (FObj MF (Monoidal.m-i M) )
264 isMonodailFunctor : IsMonoidalFunctor M N MF ψ 264 isMonodailFunctor : IsMonoidalFunctor M N MF ψ
265 265
266 -----
267 -- they say it is not possible to prove FreeTheorem in Agda nor Coq
268 -- https://stackoverflow.com/questions/24718567/is-it-possible-to-get-hold-of-free-theorems-as-propositional-equalities
269 -- so we postulate this
270 -- and we cannot indent postulate ...
271 postulate FreeTheorem : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (C : Category c₁ c₂ ℓ) (D : Category c₁' c₂' ℓ') {a b c : Obj C } → (F : Functor C D ) → ( fmap : {a : Obj C } {b : Obj C } → Hom C a b → Hom D (FObj F a) ( FObj F b) ) → {h f : Hom C a b } → {g k : Hom C b c } → C [ C [ g o h ] ≈ C [ k o f ] ] → D [ D [ FMap F g o fmap h ] ≈ D [ fmap k o FMap F f ] ]
272
273 UniquenessOfFunctor : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (C : Category c₁ c₂ ℓ) (D : Category c₁' c₂' ℓ') (F : Functor C D)
274 {a b : Obj C } { f : Hom C a b } → ( fmap : {a : Obj C } {b : Obj C } → Hom C a b → Hom D (FObj F a) ( FObj F b) )
275 → ( {b : Obj C } → D [ fmap (id1 C b) ≈ id1 D (FObj F b) ] )
276 → D [ fmap f ≈ FMap F f ]
277 UniquenessOfFunctor C D F {a} {b} {f} fmap eq = begin
278 fmap f
279 ≈↑⟨ idL ⟩
280 id1 D (FObj F b) o fmap f
281 ≈↑⟨ car ( IsFunctor.identity (isFunctor F )) ⟩
282 FMap F (id1 C b) o fmap f
283 ≈⟨ FreeTheorem C D F fmap (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory C ))) ⟩
284 fmap (id1 C b) o FMap F f
285 ≈⟨ car eq ⟩
286 id1 D (FObj F b) o FMap F f
287 ≈⟨ idL ⟩
288 FMap F f
289 ∎
290 where open ≈-Reasoning D
291 266
292 open import Category.Sets 267 open import Category.Sets
293 268
294 import Relation.Binary.PropositionalEquality 269 import Relation.Binary.PropositionalEquality
295 -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x ) 270 -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x )
364 mρiso : {a : Obj Sets} (x : a ⊗ One ) → (Sets [ mρ← o mρ→ ]) x ≡ id1 Sets (a ⊗ One) x 339 mρiso : {a : Obj Sets} (x : a ⊗ One ) → (Sets [ mρ← o mρ→ ]) x ≡ id1 Sets (a ⊗ One) x
365 mρiso (_ , OneObj ) = refl 340 mρiso (_ , OneObj ) = refl
366 341
367 ≡-cong = Relation.Binary.PropositionalEquality.cong 342 ≡-cong = Relation.Binary.PropositionalEquality.cong
368 343
344 ----
345 --
346 -- HaskellMonoidalFunctor is a monoidal functor on Sets
347 --
348 --
349
369 350
370 record IsHaskellMonoidalFunctor {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) ) 351 record IsHaskellMonoidalFunctor {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
371 ( unit : FObj F One ) 352 ( unit : FObj F One )
372 ( φ : {a b : Obj Sets} → Hom Sets ((FObj F a) * (FObj F b )) ( FObj F ( a * b ) ) ) 353 ( φ : {a b : Obj Sets} → Hom Sets ((FObj F a) * (FObj F b )) ( FObj F ( a * b ) ) )
373 : Set (suc (suc c₁)) where 354 : Set (suc (suc c₁)) where
393 : Set (suc (suc c₁)) where 374 : Set (suc (suc c₁)) where
394 field 375 field
395 unit : FObj F One 376 unit : FObj F One
396 φ : {a b : Obj Sets} → Hom Sets ((FObj F a) * (FObj F b )) ( FObj F ( a * b ) ) 377 φ : {a b : Obj Sets} → Hom Sets ((FObj F a) * (FObj F b )) ( FObj F ( a * b ) )
397 isHaskellMonoidalFunctor : IsHaskellMonoidalFunctor F unit φ 378 isHaskellMonoidalFunctor : IsHaskellMonoidalFunctor F unit φ
379
380
381 ----
382 --
383 -- laws of HaskellMonoidalFunctor are directly mapped to the laws of Monoidal Functor
384 --
385 --
398 386
399 HaskellMonoidalFunctor→MonoidalFunctor : {c : Level} ( F : Functor (Sets {c}) (Sets {c}) ) → (mf : HaskellMonoidalFunctor F ) 387 HaskellMonoidalFunctor→MonoidalFunctor : {c : Level} ( F : Functor (Sets {c}) (Sets {c}) ) → (mf : HaskellMonoidalFunctor F )
400 → MonoidalFunctor {_} {c} {_} {Sets} {Sets} MonoidalSets MonoidalSets 388 → MonoidalFunctor {_} {c} {_} {Sets} {Sets} MonoidalSets MonoidalSets
401 HaskellMonoidalFunctor→MonoidalFunctor {c} F mf = record { 389 HaskellMonoidalFunctor→MonoidalFunctor {c} F mf = record {
402 MF = F 390 MF = F
491 open Relation.Binary.PropositionalEquality.≡-Reasoning 479 open Relation.Binary.PropositionalEquality.≡-Reasoning
492 comm3 : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o 480 comm3 : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o
493 Sets [ φ o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ] ≈ Iso.≅→ (mλ-iso isM) ] 481 Sets [ φ o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ] ≈ Iso.≅→ (mλ-iso isM) ]
494 comm3 {a} {b} = extensionality Sets ( λ x → comm30 {a} {b} x ) 482 comm3 {a} {b} = extensionality Sets ( λ x → comm30 {a} {b} x )
495 483
496 484 -- end