Prove missing link for univalence via new branch of cubical

This commit is contained in:
Frederik Hanghøj Iversen 2018-05-08 18:01:34 +02:00
parent e5d55c7b2b
commit 32e7290fe9
3 changed files with 6 additions and 7 deletions

@ -1 +1 @@
Subproject commit fbd8ba7ea84c4b643fd08797b4031b18a59f561d
Subproject commit 4493cf249a1648be2ad365fe94ece337bfbcb5d9

@ -1 +1 @@
Subproject commit 5b35333dbbd8fa523e478c1cfe60657321ca38fe
Subproject commit 4e5d43a9c75286b3a8750567d75a930674d7720d

View file

@ -137,11 +137,10 @@ record RawCategory (a b : Level) : Set (lsuc (a ⊔ b)) where
Univalent[Contr] : Set _
Univalent[Contr] = A isContr (Σ[ X Object ] A X)
-- From: Thierry Coquand <Thierry.Coquand@cse.gu.se>
-- Date: Wed, Mar 21, 2018 at 3:12 PM
--
-- This is not so straight-forward so you can assume it
postulate from[Contr] : Univalent[Contr] Univalent
from[Contr] : Univalent[Contr] Univalent
from[Contr] = ContrToUniv.lemma _ _
where
open import Cubical.Fiberwise
univalenceFrom≃ : Univalent≃ Univalent
univalenceFrom≃ = from[Contr] step