Provide grpdPiImpl

src/Cat/Prelude.agda

@@ -1,3 +1,4 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 -- | Custom prelude for this module
 module Cat.Prelude where
 
@@ -105,3 +106,28 @@ module _ {ℓ : Level} {A : Set ℓ} where
   ntypeCumulative : ∀ {n m} → n ≤′ m → HasLevel ⟨ n ⟩₋₂ A → HasLevel ⟨ m ⟩₋₂ A
   ntypeCumulative {m}         ≤′-refl      lvl = lvl
   ntypeCumulative {n} {suc m} (≤′-step le) lvl = HasLevel+1 ⟨ m ⟩₋₂ (ntypeCumulative le lvl)
+
+  grpdPi : {ℓa ℓb : Level} {A : Set ℓa} {B : A → Set ℓb}
+    → ((a : A) → isGrpd (B a)) → isGrpd ((a : A) → (B a))
+  grpdPi = piPresNType (S (S (S ⟨-2⟩)))
+
+  grpdPiImpl : {ℓa ℓb : Level} {A : Set ℓa} {B : A → Set ℓb}
+    → ({a : A} → isGrpd (B a)) → isGrpd ({a : A} → (B a))
+  grpdPiImpl {A = A} {B} g = equivPreservesNType {A = Expl} {B = Impl} {n = one} e (grpdPi (λ a → g))
+    where
+    one = (S (S (S ⟨-2⟩)))
+    t : ({a : A} → HasLevel one (B a))
+    t = g
+    Impl = {a : A} → B a
+    Expl = (a : A) → B a
+    expl : Impl → Expl
+    expl f a = f {a}
+    impl : Expl → Impl
+    impl f {a} = f a
+    e : Expl ≃ Impl
+    e = impl , (gradLemma impl expl (λ f → refl) (λ f → refl))
+
+  setGrpd : isSet A → isGrpd A
+  setGrpd = ntypeCumulative
+    {suc (suc zero)} {suc (suc (suc zero))}
+    (≤′-step ≤′-refl)