fredefox/cat
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Mark questions

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2017-06-07 22:24:35 +02:00
parent 38fd690839
commit 0f114b1029
1 changed files with 4 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/Cat.agda
View file

@ -3,7 +3,6 @@ module Cat where
open import Agda.Primitive open import Agda.Primitive
open import Prelude.Function open import Prelude.Function
-- import Prelude.Equality
open import PathPrelude open import PathPrelude
open ≡-Reasoning open ≡-Reasoning
@ -52,19 +51,13 @@ data Maybe ( A : Set ) : Set where
nothing : Maybe A nothing : Maybe A
just : A -> Maybe A just : A -> Maybe A
-- postulate
-- fun-ext : ∀ {a b} {A : Set a} {B : A → Set b} → {f g : (x : A) → B x}
-- → (∀ x → (f x) ≡ (g x)) → f ≡ g
-- fun-ext p = λ i → \ x → p x i
instance instance
MaybeFunctor : Functor Maybe MaybeFunctor : Functor Maybe
Functor.fmap MaybeFunctor f nothing = nothing Functor.fmap MaybeFunctor f nothing = nothing
Functor.fmap MaybeFunctor f (just x) = just (f x) Functor.fmap MaybeFunctor f (just x) = just (f x)
-- how the heck can I use `fun-ext` which produces `Path id (fmap id)` wheras the type of the whole is `id ≡ fmap id`.
Functor.identity MaybeFunctor = fun-ext (λ { nothing → refl ; (just x) → refl }) Functor.identity MaybeFunctor = fun-ext (λ { nothing → refl ; (just x) → refl })
Functor.fusion MaybeFunctor f g = fun-ext (λ Functor.fusion MaybeFunctor f g = fun-ext (λ
-- Why does inlining `lem₀` give rise to an error? -- QUESTION: Why does inlining `lem₀` give rise to an error?
{ nothing → lem₀ { nothing → lem₀
; (just x) → {! refl!} ; (just x) → {! refl!}
{- ; (just x) → begin {- ; (just x) → begin
@ -118,7 +111,7 @@ instance
Applicative.homomorphism IdentityApplicative = refl Applicative.homomorphism IdentityApplicative = refl
Applicative.interchange IdentityApplicative _ _ = refl Applicative.interchange IdentityApplicative _ _ = refl
-- Is this provable? How? -- QUESTION: Is this provable? How?
-- I suppose this would be `≡`'s functor-instance. -- I suppose this would be `≡`'s functor-instance.
equiv-app : {A B : Set} -> {f g : A -> B} -> {a : A} -> f ≡ g -> f a ≡ g a equiv-app : {A B : Set} -> {f g : A -> B} -> {a : A} -> f ≡ g -> f a ≡ g a
equiv-app f≡g = {!!} equiv-app f≡g = {!!}
@ -128,7 +121,7 @@ instance
Applicative.pure MaybeApplicative = just Applicative.pure MaybeApplicative = just
Applicative.ap MaybeApplicative nothing _ = nothing Applicative.ap MaybeApplicative nothing _ = nothing
Applicative.ap MaybeApplicative (just f) x = fmap f x Applicative.ap MaybeApplicative (just f) x = fmap f x
-- Why does termination-check fail when I use `refl` in both cases below? -- QUESTION: Why does termination-check fail when I use `refl` in both cases below?
Applicative.ap-identity MaybeApplicative = fun-ext (λ Applicative.ap-identity MaybeApplicative = fun-ext (λ
{ nothing → {!refl!} { nothing → {!refl!}
; (just x) → {!refl!} ; (just x) → {!refl!}
@ -139,6 +132,7 @@ instance
-- Applicative.composition MaybeApplicative {u = just f} {just g} {nothing} = refl -- Applicative.composition MaybeApplicative {u = just f} {just g} {nothing} = refl
-- Applicative.composition MaybeApplicative {u = just f} {just g} {just x} = refl -- Applicative.composition MaybeApplicative {u = just f} {just g} {just x} = refl
-- Re-use mode: -- Re-use mode:
-- QUESTION: What's wrong here?
Applicative.composition MaybeApplicative (just f) (just g) w = sym (equiv-app lem) Applicative.composition MaybeApplicative (just f) (just g) w = sym (equiv-app lem)
where where
lem : ∀ {A B C} {f : B → C} {g : A → B} {w : Maybe A} → lem : ∀ {A B C} {f : B → C} {g : A → B} {w : Maybe A} →