diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -6,6 +6,17 @@
 and this project adheres to the
 [Haskell Package Versioning Policy](https://pvp.haskell.org/).
 
+## v0.5.1 — 2022-06-29
+
+This version fixes `Unit` type and makes some changes to documentation:
+
+- Fix computation for `Unit` (see [2f7d6295]( https://github.com/fizruk/rzk/commit/2f7d6295 ));
+- Update documentation (see [ea2d176b]( https://github.com/fizruk/rzk/commit/ea2d176b ));
+- Use mike to deploy versioned docs (see [99cf721a]( https://github.com/fizruk/rzk/commit/99cf721a ));
+- Replace MkDocs hook with the published plugin (see [#58]( https://github.com/fizruk/rzk/pull/58 ));
+- Switch to Material theme for MkDocs (see [#57]( https://github.com/fizruk/rzk/pull/57 ));
+- Fix links to `*.rzk.md` in `mkdocs.yml` (see [8ba1c55b]( https://github.com/fizruk/rzk/commit/8ba1c55b ));
+
 ## v0.5 — 2022-06-20
 
 This version contains the following changes:
diff --git a/rzk.cabal b/rzk.cabal
--- a/rzk.cabal
+++ b/rzk.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           rzk
-version:        0.5
+version:        0.5.1
 synopsis:       An experimental proof assistant for synthetic ∞-categories
 description:    Please see the README on GitHub at <https://github.com/fizruk/rzk#readme>
 category:       Dependent Types
diff --git a/src/Rzk/TypeCheck.hs b/src/Rzk/TypeCheck.hs
--- a/src/Rzk/TypeCheck.hs
+++ b/src/Rzk/TypeCheck.hs
@@ -1257,6 +1257,11 @@
     UniverseCubeT{} -> nfTope tt
     UniverseTopeT{} -> nfTope tt
 
+    -- CubeUnitT{} -> pure cubeUnitStarT -- compute an expression of 1 cube to its only point
+    TypeUnitT{} -> pure unitT -- compute an expression of Unit type to unit
+    -- FIXME: next line is ad hoc, should be improved!
+    TypeRestrictedT _info TypeUnitT{} _rs -> pure unitT -- compute an expression of Unit type to unit
+
     -- check if we have cube point term (if so, compute NF)
     typeOf_tt -> typeOf typeOf_tt >>= \case
       UniverseCubeT{} -> nfTope tt