Change predicate

rahulc29 · Apr 8, 2024 · 3d55e7c · 3d55e7c
1 parent 9238eb7
commit 3d55e7c
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Realizability/Tripos/Prealgebra/Predicate/Base.agda b/src/Realizability/Tripos/Prealgebra/Predicate/Base.agda
@@ -14,7 +14,7 @@ open CombinatoryAlgebra ca
 open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a)
 
 record Predicate (X : Type ℓ') : Type (ℓ-max (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ')) (ℓ-suc ℓ'')) where
-  constructor consPredicate
+  constructor makePredicate
   field
     isSetX : isSet X
     ∣_∣ : X → A → Type (ℓ-max (ℓ-max ℓ ℓ') ℓ'')