From 3d55e7c859d805e24cab4192f9d025dc0fcbfd46 Mon Sep 17 00:00:00 2001 From: Rahul Chhabra Date: Tue, 9 Apr 2024 04:34:40 +0530 Subject: [PATCH] Change predicate --- src/Realizability/Tripos/Prealgebra/Predicate/Base.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Realizability/Tripos/Prealgebra/Predicate/Base.agda b/src/Realizability/Tripos/Prealgebra/Predicate/Base.agda index b8a4963..e89afc3 100644 --- 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 ℓ ℓ') ℓ'')