From 7836367f4a8a59d627f3bdb328c98c210298ec58 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Thu, 19 Jul 2018 20:22:17 +0200 Subject: [PATCH] Use HEAD version of cubical and stdlib --- .gitmodules | 2 +- libs/agda-stdlib | 2 +- libs/cubical | 2 +- src/Cat/Categories/Cube.agda | 4 ++-- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/.gitmodules b/.gitmodules index 95b778a..f7aa395 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,6 +1,6 @@ [submodule "libs/cubical"] path = libs/cubical - url = git@github.com:fredefox/cubical.git + url = git@github.com:Saizan/cubical-demo.git [submodule "libs/agda-stdlib"] path = libs/agda-stdlib url = git@github.com:agda/agda-stdlib.git diff --git a/libs/agda-stdlib b/libs/agda-stdlib index 2096269..f091aac 160000 --- a/libs/agda-stdlib +++ b/libs/agda-stdlib @@ -1 +1 @@ -Subproject commit 209626953d56294e9bd3d8892eda43b844b0edf9 +Subproject commit f091aac94a07005ce032a26bc932af07f2dffcdf diff --git a/libs/cubical b/libs/cubical index dfa196a..b112c29 160000 --- a/libs/cubical +++ b/libs/cubical @@ -1 +1 @@ -Subproject commit dfa196a4da79b41c9ee30f825b86a5eb6181e632 +Subproject commit b112c292ded61b02fa32a1b65cac77314a1e9698 diff --git a/src/Cat/Categories/Cube.agda b/src/Cat/Categories/Cube.agda index 121cb24..f21e551 100644 --- a/src/Cat/Categories/Cube.agda +++ b/src/Cat/Categories/Cube.agda @@ -54,9 +54,9 @@ module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where → case (f i) of λ { (inj₁ (fi , _)) → case (f j) of λ { (inj₁ (fj , _)) → fi ≡ fj → i ≡ j - ; (inj₂ _) → Lift ⊤ + ; (inj₂ _) → Lift _ ⊤ } - ; (inj₂ _) → Lift ⊤ + ; (inj₂ _) → Lift _ ⊤ } Hom = Σ Hom' rules