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

fix(library/hott) make universe index in ua.lean variable

Browse source
This commit is contained in:
Jakob von Raumer 2014-11-06 20:02:10 -05:00
parent b8ec1a1649
commit 754901cf64
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/hott/axioms/ua.lean
View file

@ -6,7 +6,7 @@ import hott.path hott.equiv
open path Equiv open path Equiv
--Ensure that the types compared are in the same universe --Ensure that the types compared are in the same universe
universe l universe variable l
variables (A B : Type.{l}) variables (A B : Type.{l})
private definition isequiv_path (H : A ≈ B) := private definition isequiv_path (H : A ≈ B) :=