From 9848fac6726e40f21259b820fb3cfe5ce5db5036 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 22 May 2018 16:31:26 +0200 Subject: [PATCH] Provide grpdSig --- src/Cat/Prelude.agda | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/Cat/Prelude.agda b/src/Cat/Prelude.agda index a546c75..00064d4 100644 --- a/src/Cat/Prelude.agda +++ b/src/Cat/Prelude.agda @@ -33,7 +33,7 @@ open import Cubical.NType.Properties propIsContr : {ℓ : Level} → {A : Set ℓ} → isProp (isContr A) propIsContr = propHasLevel ⟨-2⟩ -open import Cubical.Sigma using (setSig ; sigPresSet ; sigPresNType ; grpdSig) public +open import Cubical.Sigma using (setSig ; sigPresSet ; sigPresNType) public module _ (ℓ : Level) where -- FIXME Ask if we can push upstream. @@ -135,3 +135,8 @@ module _ {ℓ : Level} {A : Set ℓ} where propGrpd = ntypeCumulative {suc zero} {suc (suc (suc zero))} (≤′-step (≤′-step ≤′-refl)) + +module _ {ℓa ℓb : Level} {A : Set ℓa} {B : A → Set ℓb} where + open TLevel + grpdSig : isGrpd A → (∀ a → isGrpd (B a)) → isGrpd (Σ A B) + grpdSig = sigPresNType {n = S (S (S ⟨-2⟩))}