chore(library/hott) add note referring to missing substitution lemma
This commit is contained in:
parent
7dbd7b31f6
commit
f1cc0c4bd8
1 changed files with 1 additions and 3 deletions
|
@ -285,9 +285,7 @@ namespace Equiv
|
|||
end
|
||||
|
||||
-- calc enviroment
|
||||
-- TODO: transport lemma without univalence?
|
||||
-- theorem foo (P : Type → Type) (A B : Type) (H : A ≃ B) : P A → P B := sorry
|
||||
-- calc_subst foo
|
||||
-- Note: Calculating with substitutions needs univalence
|
||||
calc_trans compose
|
||||
calc_refl id
|
||||
calc_symm inv_closed
|
||||
|
|
Loading…
Reference in a new issue