diff --git a/Changelog.md b/Changelog.md
new file mode 100644
--- /dev/null
+++ b/Changelog.md
@@ -0,0 +1,20 @@
+Changelog
+==========
+
+## 0.7.0.2
+
+- Supports GHC 9.8
+- Drops support for GHC <9
+
+## 0.6.0.3
+
+- Support for GHC >= 8.10
+
+## 0.6.0.2
+
+- Adds support for th-desugar-1.11
+
+## 0.6.0.1
+
+- Supports GHC 8.8.
+- Adds support for th-desugar-1.10 (Thanks: Justin Le @mstksg)
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,30 @@
+Agda-style Equational Reasoning in Haskell by Data Kinds
+=========================================================
+[![Build Status](https://travis-ci.org/konn/equational-reasoning-in-haskell.svg)](https://travis-ci.org/konn/equational-reasoning-in-haskell) [![Hackage](https://img.shields.io/hackage/v/equational-reasoning.svg)](https://hackage.haskell.org/package/equational-reasoning)
+
+What is this?
+--------------
+This library provides means to prove equations in Haskell.
+You can prove equations in Agda's EqReasoning like style.
+
+See blow for an example:
+
+```haskell
+plusZeroL :: SNat m -> Zero :+: m :=: m
+plusZeroL SZero = Refl
+plusZeroL (SSucc m) =
+  start (SZero %+ (SSucc m))
+    === SSucc (SZero %+ m)    `because`   plusSuccR SZero m
+    === SSucc m               `because`   succCongEq (plusZeroL m)
+
+```
+
+It also provides some utility functions to use an induction.
+
+For more detail, please read source codes!
+
+
+TODOs
+------
+
+* Automatic generation for induction schema for any inductive types.
diff --git a/equational-reasoning.cabal b/equational-reasoning.cabal
--- a/equational-reasoning.cabal
+++ b/equational-reasoning.cabal
@@ -1,28 +1,27 @@
-name:          equational-reasoning
-version:       0.7.0.2
-synopsis:      Proof assistant for Haskell using DataKinds & PolyKinds
+cabal-version: 3.4
+name: equational-reasoning
+version: 0.7.0.3
+synopsis: Proof assistant for Haskell using DataKinds & PolyKinds
 description:
   A simple convenient library to write equational / preorder proof as in Agda.
   Since 0.6.0.0, this no longer depends on @singletons@ package, and the @Proof.Induction@ module goes to @equational-reasoning-induction@ package.
 
-license:       BSD3
-license-file:  LICENSE
-author:        Hiromi ISHII
-maintainer:    konn.jinro_at_gmail.com
-copyright:     (c) Hiromi ISHII 2013-2020
-category:      Math
-build-type:    Simple
+license: BSD-3-Clause
+license-file: LICENSE
+author: Hiromi ISHII
+maintainer: konn.jinro_at_gmail.com
+copyright: (c) Hiromi ISHII 2013-2020
+category: Math
+build-type: Simple
 tested-with:
-  GHC ==9.0.2
-   || ==9.2.8
-   || ==9.4.8
-   || ==9.6.3
-   || ==9.8.1
+  ghc ==9.0.2 || ==9.2.8 || ==9.4.8 || ==9.6.5 || ==9.8.2
 
-cabal-version: >=1.10
+extra-doc-files:
+  Changelog.md
+  README.md
 
 source-repository head
-  type:     git
+  type: git
   location: git://github.com/konn/equational-reasoning-in-haskell.git
 
 library
@@ -32,13 +31,13 @@
     Proof.Propositional.Empty
     Proof.Propositional.Inhabited
 
-  other-modules:    Proof.Propositional.TH
-  ghc-options:      -Wall
+  other-modules: Proof.Propositional.TH
+  ghc-options: -Wall
   build-depends:
-      base              >=4    && <5
-    , containers        >=0.5  && <0.7
-    , template-haskell  >=2.11 && <2.22
-    , void              >=0.6  && <0.8
-    , th-desugar >=1.8 && <1.17
+    base >=4 && <5,
+    containers >=0.5 && <0.7,
+    template-haskell >=2.11 && <2.23,
+    th-desugar >=1.8 && <1.18,
+    void >=0.6 && <0.8,
 
   default-language: Haskell2010