1 files changed, 1 insertions, 1 deletions
diff --git a/BFF.agda b/BFF.agda
index 5bf756d..f5573ba 100644
--- a/BFF.agda
+++ b/BFF.agda
@@ -38,7 +38,7 @@ module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where
   denumerate = flip lookupV
 
 
-  bff : (G : Get) → ({i : Setoid.Carrier (Get.I G)} → Vec Carrier (to (Get.gl₁ G) ⟨$⟩ i) → Vec Carrier ((Get.gl₂ G) ⟨$⟩ i) → Maybe (Vec Carrier (to (Get.gl₁ G) ⟨$⟩ i)))
+  bff : (G : Get) → ({i : Get.|I| G} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G i) → Maybe (Vec Carrier (Get.|gl₁| G i)))
   bff G s v = let   s′ = enumerate s
                     t′ = Get.get G s′
                     g  = fromFunc (denumerate s)