Mercurial > hg > Members > kono > Proof > category

comparison src/applicative.agda @ 1106:270f0ba65b88

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
unify yoneda functor
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 10 Mar 2023 16:19:46 +0900
parents ac53803b3b2a
children 71049ed05151
comparison
equal deleted inserted replaced
1105:3cf570d5c285 1106:270f0ba65b88
24 -- To show Applicative functor is monoidal functor, uniquness of Functor is necessary, which is derived from the free theorem. 24 -- To show Applicative functor is monoidal functor, uniquness of Functor is necessary, which is derived from the free theorem.
25 -- 25 --
26 -- they say it is not possible to prove FreeTheorem in Agda nor Coq 26 -- they say it is not possible to prove FreeTheorem in Agda nor Coq
27 -- https://stackoverflow.com/questions/24718567/is-it-possible-to-get-hold-of-free-theorems-as-propositional-equalities 27 -- https://stackoverflow.com/questions/24718567/is-it-possible-to-get-hold-of-free-theorems-as-propositional-equalities
28 -- so we postulate this 28 -- so we postulate this
29 -- and we cannot indent a postulate ...
30 29
31 open Functor 30 open Functor
32 31
33 postulate 32 postulate
34 FreeTheorem : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (C : Category c₁ c₂ ℓ) (D : Category c₁' c₂' ℓ') {a b c : Obj C } 33 FreeTheorem : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (C : Category c₁ c₂ ℓ) (D : Category c₁' c₂' ℓ') {a b c : Obj C }
56 ∎ 55 ∎
57 where open ≈-Reasoning D 56 where open ≈-Reasoning D
58 57
59 open import Category.Sets 58 open import Category.Sets
60 import Relation.Binary.PropositionalEquality 59 import Relation.Binary.PropositionalEquality
61
62 60
63 _・_ : {c₁ : Level} { a b c : Obj (Sets {c₁} ) } → (b → c) → (a → b) → a → c 61 _・_ : {c₁ : Level} { a b c : Obj (Sets {c₁} ) } → (b → c) → (a → b) → a → c
64 _・_ f g = λ x → f ( g x ) 62 _・_ f g = λ x → f ( g x )
65 63
66 record IsApplicative {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) ) 64 record IsApplicative {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )