michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(hott/init): minimize number of universe parameters

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-19 20:50:53 -08:00
parent d6f79423e9
commit 2e93e5d6a7
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
hott/init/default.hlean
View file

@ -10,4 +10,4 @@ import init.bool init.num init.priority init.relation init.wf
import init.types.sigma init.types.prod init.types.empty import init.types.sigma init.types.prod init.types.empty
import init.trunc init.path init.equiv init.util import init.trunc init.path init.equiv init.util
import init.axioms.ua init.axioms.funext init.axioms.funext_from_ua import init.axioms.ua init.axioms.funext init.axioms.funext_from_ua
import init.hedberg import init.hedberg init.nat

4
hott/init/logic.hlean
View file

@ -7,7 +7,7 @@ Authors: Leonardo de Moura
prelude prelude
import init.datatypes init.reserved_notation import init.datatypes init.reserved_notation
definition not (a : Type) := a → empty definition not.{l} (a : Type.{l}) := a → empty.{l}
prefix `¬` := not prefix `¬` := not
definition absurd {a : Type} {b : Type} (H₁ : a) (H₂ : ¬a) : b := definition absurd {a : Type} {b : Type} (H₁ : a) (H₂ : ¬a) : b :=
@ -203,7 +203,7 @@ end inhabited
-- decidable -- decidable
-- --------- -- ---------
inductive decidable [class] (p : Type) : Type := inductive decidable.{l} [class] (p : Type.{l}) : Type.{l} :=
inl : p → decidable p, inl : p → decidable p,
inr : ¬p → decidable p inr : ¬p → decidable p