--- a/src/applicative.agda	Wed Jan 25 10:59:28 2023 +0900
+++ b/src/applicative.agda	Fri Mar 10 16:19:46 2023 +0900
@@ -26,7 +26,6 @@
 -- they say it is not possible to prove FreeTheorem in Agda nor Coq
 --    https://stackoverflow.com/questions/24718567/is-it-possible-to-get-hold-of-free-theorems-as-propositional-equalities
 -- so we postulate this
---    and we cannot indent a postulate ...
 
 open Functor
 
@@ -59,7 +58,6 @@
 open import Category.Sets
 import Relation.Binary.PropositionalEquality
 
-
 _・_ : {c₁ : Level} { a b c : Obj (Sets {c₁} ) } → (b → c) → (a → b) → a → c
 _・_ f g = λ x → f ( g x )