lean2/hott/core.hlean

/-
Copyright (c) 2015 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn

The core of the HoTT library
-/

import types cubical homotopy hit choice
feat(hott): add core.hlean and types/default.hlean 2015-04-10 02:14:19 +00:00			`/-`
			`Copyright (c) 2015 Floris van Doorn. All rights reserved.`
			`Released under Apache 2.0 license as described in the file LICENSE.`
			`Authors: Floris van Doorn`

			`The core of the HoTT library`
			`-/`

chore(hott): update default files and some markdown files 2016-05-13 19:17:50 +00:00			`import types cubical homotopy hit choice`