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

chore(library/hott) move function extensionality into new axioms folder, adjust file(s) using it

Browse source
This commit is contained in:
Jakob von Raumer 2014-11-06 13:34:57 -05:00
parent 9ad75108a3
commit 28d1c6c5e4
2 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/hott/funext.lean → library/hott/axioms/funext.lean
View file

@ -3,9 +3,8 @@
-- Author: Jeremy Avigad, Jakob von Raumer -- Author: Jeremy Avigad, Jakob von Raumer
-- Ported from Coq HoTT -- Ported from Coq HoTT
-- TODO: move this to an "axioms" folder
-- TODO: take a look at the Coq tricks -- TODO: take a look at the Coq tricks
import .path .equiv import hott.path hott.equiv
open path open path
-- Funext -- Funext

2
library/hott/equiv_precomp.lean
View file

@ -2,7 +2,7 @@
-- Released under Apache 2.0 license as described in the file LICENSE. -- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Jakob von Raumer -- Author: Jakob von Raumer
-- Ported from Coq HoTT -- Ported from Coq HoTT
import .equiv .funext import hott.equiv hott.axioms.funext
open path function open path function
namespace IsEquiv namespace IsEquiv