From 32e7290fe9283663fcdd5145330d3fcd9846c945 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 8 May 2018 18:01:34 +0200 Subject: [PATCH] Prove missing link for univalence via new branch of `cubical` --- libs/agda-stdlib | 2 +- libs/cubical | 2 +- src/Cat/Category.agda | 9 ++++----- 3 files changed, 6 insertions(+), 7 deletions(-) diff --git a/libs/agda-stdlib b/libs/agda-stdlib index fbd8ba7..4493cf2 160000 --- a/libs/agda-stdlib +++ b/libs/agda-stdlib @@ -1 +1 @@ -Subproject commit fbd8ba7ea84c4b643fd08797b4031b18a59f561d +Subproject commit 4493cf249a1648be2ad365fe94ece337bfbcb5d9 diff --git a/libs/cubical b/libs/cubical index 5b35333..4e5d43a 160000 --- a/libs/cubical +++ b/libs/cubical @@ -1 +1 @@ -Subproject commit 5b35333dbbd8fa523e478c1cfe60657321ca38fe +Subproject commit 4e5d43a9c75286b3a8750567d75a930674d7720d diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 1561aab..749ba42 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -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 - -- 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