diff --git a/libs/cubical-demo b/libs/cubical-demo
index 62cf020..e46610e 160000
--- a/libs/cubical-demo
+++ b/libs/cubical-demo
@@ -1 +1 @@
-Subproject commit 62cf020f9ea7b3e3d78612222402a782f222bb04
+Subproject commit e46610eda0bbdebb072a70b947742f765a335b01
diff --git a/src/Cat.agda b/src/Cat.agda
index 5b4b260..5c62b0f 100644
--- a/src/Cat.agda
+++ b/src/Cat.agda
@@ -3,8 +3,9 @@ module Cat where
 
 open import Agda.Primitive
 open import Prelude.Function
-import Prelude.Equality
+-- import Prelude.Equality
 open import PathPrelude
+open ≡-Reasoning
 
 -- Questions:
 --
@@ -12,18 +13,21 @@ open import PathPrelude
 -- in Agda (like undefined in Haskell).
 --
 -- Does Agda have a way to specify local submodules?
+--
+-- Can I open parts of a record, like say:
+--
+--     open Functor {{...}} ( fmap )
+
 record Functor {a b} (F : Set a → Set b) : Set (lsuc a ⊔ b) where
   field
     -- morphisms
     fmap : ∀ {A B} → (A → B) → F A → F B
     -- laws
-    identity : { A : Set a } -> id ≡ fmap (id { A = A })
-    -- Why does PathPrelude.≡ not agree with Prelude.Equality.≡
-    fusion : { A B C : Set a } ( f : B -> C ) ( g : A -> B ) -> fmap f ∘ fmap g ≡ fmap (f ∘ g)
---    fusion : { A B C : Set a } ( f : B -> C ) ( g : A -> B ) -> fmap f ∘ fmap g Prelude.Equality.≡ fmap (f ∘ g)
+    identity : { A : Set a }
+      -> id ≡ fmap (id { A = A })
+    fusion : { A B C : Set a } ( f : B -> C ) ( g : A -> B )
+      -> fmap f ∘ fmap g ≡ fmap (f ∘ g)
 
--- PathPrelude._≡_      : {a : Level} {A : Set a} → A → A → Set a
--- Prelude.Equality._≡_ : {a : Level} {A : Set a} → A → A → Set a
 open Functor {{ ... }} hiding ( identity )
 
 _<$>_ : {a b : Level} {F : Set a → Set b} {{r : Functor F}} {A B : Set a} → (A → B) → F A → F B
@@ -58,9 +62,34 @@ instance
   Functor.fmap MaybeFunctor f nothing = nothing
   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 }))
-  -- Why can I not use `fun-ext` here?
-  Functor.fusion MaybeFunctor f g = {!!} -- fun-ext (λ { nothing -> refl ; (just x) -> refl })
+  Functor.identity MaybeFunctor = fun-ext (λ { nothing → refl ; (just x) → refl })
+  Functor.fusion MaybeFunctor f g = fun-ext (λ
+    -- Why does inlining `lem₀` give rise to an error?
+    { nothing → lem₀
+    ; (just x) → {! refl!}
+{-    ; (just x) → begin
+      (fmap f ∘ fmap g) (just x)  ≡⟨⟩
+      (fmap f (fmap g (just x)))  ≡⟨⟩
+      (fmap f (just (g x)))       ≡⟨⟩
+      (just (f (g x)))            ≡⟨⟩
+      just ((f ∘ g) x)              ∎-}
+    })
+    where
+      lem₀ : nothing ≡ nothing
+      lem₀ = refl
+      -- `lem₁` and `fusionjust` are the same.
+      lem₁ : {A B C : Set} {f : B → C} {g : A → B} {x : A}
+        → just (f (g x)) ≡ just (f (g x))
+      lem₁ = refl
+      fusionjust : { A B C : Set } { x : A } { f : B -> C } { g : A -> B }
+        -> (fmap f ∘ fmap g) (just x) ≡ just ((f ∘ g) x)
+      fusionjust {x = x} {f = f} {g = g} = begin
+        (fmap f ∘ fmap g) (just x)  ≡⟨⟩
+        (fmap f (fmap g (just x)))  ≡⟨⟩
+        (fmap f (just (g x)))       ≡⟨⟩
+        (just (f (g x)))            ≡⟨⟩
+        just ((f ∘ g) x)              ∎
+
 
 record Applicative {a} (F : Set a -> Set a) : Set (lsuc a) where
   field
@@ -70,18 +99,58 @@ record Applicative {a} (F : Set a -> Set a) : Set (lsuc a) where
     -- laws
     -- `ap-identity` is paraphrased from the documentation for Applicative on hackage.
     ap-identity : { A : Set a } -> ap (pure (id { A = A })) ≡ id
-    composition : { A B C : Set a } { u : F (B -> C) } { v : F (A -> B) } { w : F A }
+    composition : { A B C : Set a } ( u : F (B -> C) ) ( v : F (A -> B) ) ( w : F A )
       -> ap (ap (ap (pure _∘′_) u) v) w ≡ ap u (ap v w)
     homomorphism : { A B : Set a } { a : A } { f : A -> B }
       -> ap (pure f) (pure a) ≡ pure (f a)
-    interchange : { A B : Set a } { u : F (A -> B) } { a : A }
+    interchange : { A B : Set a } ( u : F (A -> B) ) ( a : A )
       -> ap u (pure a) ≡ ap (pure (_$ a)) u
 
+open Applicative {{...}}
+_<*>_ = ap
+
 instance
   IdentityApplicative : Applicative Identity
   Applicative.pure IdentityApplicative = identity
   Applicative.ap IdentityApplicative (identity f) (identity a) = identity (f a)
   Applicative.ap-identity IdentityApplicative = refl
-  Applicative.composition IdentityApplicative = refl
+  Applicative.composition IdentityApplicative _ _ _ = refl
   Applicative.homomorphism IdentityApplicative = refl
-  Applicative.interchange IdentityApplicative = refl
+  Applicative.interchange IdentityApplicative _ _ = refl
+
+-- Is this provable? How?
+-- 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 f≡g = {!!}
+
+instance
+  MaybeApplicative : Applicative Maybe
+  Applicative.pure MaybeApplicative = just
+  Applicative.ap MaybeApplicative nothing _ = nothing
+  Applicative.ap MaybeApplicative (just f) x = fmap f x
+  -- Why does termination-check fail when I use `refl` in both cases below?
+  Applicative.ap-identity MaybeApplicative = fun-ext (λ
+    { nothing → {!refl!}
+    ; (just x) → {!refl!}
+    })
+  Applicative.composition MaybeApplicative nothing v w = refl
+  Applicative.composition MaybeApplicative (just x) nothing w = refl
+  -- Easy-mode:
+  --  Applicative.composition MaybeApplicative {u = just f} {just g} {nothing} = refl
+  --  Applicative.composition MaybeApplicative {u = just f} {just g} {just x} = refl
+  -- Re-use mode:
+  Applicative.composition MaybeApplicative (just f) (just g) w = sym (equiv-app lem)
+    where
+    lem : ∀ {A B C} {f : B → C} {g : A → B} {w : Maybe A} →
+      (fmap f) ∘ (fmap g) ≡
+      (Functor.fmap MaybeFunctor (f ∘ g))
+    lem = Functor.fusion MaybeFunctor _ _
+{-
+  Applicative.composition MaybeApplicative { u = u } { v = v } { w = w } = begin
+    ap (ap (ap (pure _∘′_) u) v) w ≡⟨⟩
+    ap (ap (fmap _∘′_      u) v) w ≡⟨ {!!} ⟩
+    {!!} ∎
+-}
+  Applicative.homomorphism MaybeApplicative = refl
+  Applicative.interchange MaybeApplicative nothing a = refl
+  Applicative.interchange MaybeApplicative (just x) a = refl