Revert to preorder predicates

src/Realizability/Topos/Object.agda

@@ -2,16 +2,11 @@ open import Realizability.ApplicativeStructure renaming (Term to ApplStrTerm)
 open import Realizability.CombinatoryAlgebra
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Structure
-open import Cubical.Foundations.HLevels
-open import Cubical.Foundations.Isomorphism
-open import Cubical.Foundations.Equiv
-open import Cubical.HITs.PropositionalTruncation
 open import Cubical.Data.Vec
 open import Cubical.Data.Nat
-open import Cubical.Data.FinData
+open import Cubical.Data.FinData renaming (zero to fzero)
 open import Cubical.Data.Sigma
 open import Cubical.Data.Empty
-open import Cubical.Reflection.RecordEquiv
 
 module Realizability.Topos.Object
   {ℓ ℓ' ℓ''}
@@ -22,58 +17,18 @@ module Realizability.Topos.Object
 
 open import Realizability.Tripos.Logic.Syntax {ℓ = ℓ'}
 open import Realizability.Tripos.Logic.Semantics {ℓ' = ℓ'} {ℓ'' = ℓ''} ca
-open import Realizability.Tripos.Algebra.Base {ℓ' = ℓ'} {ℓ'' = ℓ''} ca renaming (AlgebraicPredicate to Predicate)
+open import Realizability.Tripos.Prealgebra.Predicate {ℓ' = ℓ'} {ℓ'' = ℓ''} ca
 open CombinatoryAlgebra ca
 open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a)
-
-record isPartialEquivalenceRelation (X : Type ℓ') (equality : Predicate (X × X)) : Type (ℓ-max (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ')) (ℓ-suc ℓ'')) where
-  field
-    isSetX : isSet X
-    isSymmetric : ∃[ sm ∈ A ] (∀ x x' r → r ⊩[ equality ] (x , x') → (sm ⨾ r) ⊩[ equality ] (x' , x))
-    isTransitive : ∃[ ts ∈ A ] (∀ x x' x'' r s → r ⊩[ equality ] (x , x') → s ⊩[ equality ] (x' , x'') → (ts ⨾ r ⨾ s) ⊩[ equality ] (x , x''))
-
-opaque
-  isPropIsPartialEquivalenceRelation : ∀ X equality → isProp (isPartialEquivalenceRelation X equality)
-  isPropIsPartialEquivalenceRelation X equality x y i =
-    record { isSetX = isPropIsSet {A = X} (x .isSetX) (y .isSetX) i ; isSymmetric = squash₁ (x .isSymmetric) (y .isSymmetric) i ; isTransitive = squash₁ (x .isTransitive) (y .isTransitive) i } where
-      open isPartialEquivalenceRelation
+open Predicate renaming (isSetX to isSetPredicateBase)
+open PredicateProperties
+open Morphism
 
 record PartialEquivalenceRelation (X : Type ℓ') : Type (ℓ-max (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ')) (ℓ-suc ℓ'')) where
   field
+    isSetX : isSet X
     equality : Predicate (X × X)
-    isPerEquality : isPartialEquivalenceRelation X equality
-  open isPartialEquivalenceRelation isPerEquality public
-
-open PartialEquivalenceRelation
-
-unquoteDecl PartialEquivalenceRelationIsoΣ = declareRecordIsoΣ PartialEquivalenceRelationIsoΣ (quote PartialEquivalenceRelation)
-
-PartialEquivalenceRelationΣ : (X : Type ℓ') → Type (ℓ-max (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ')) (ℓ-suc ℓ''))
-PartialEquivalenceRelationΣ X = Σ[ equality ∈ Predicate (X × X) ] isPartialEquivalenceRelation X equality
-
-
-module _ (X : Type ℓ') where opaque
-  open Iso
-  PartialEquivalenceRelationΣ≡ : (perA perB : PartialEquivalenceRelationΣ X) → perA .fst ≡ perB .fst → perA ≡ perB
-  PartialEquivalenceRelationΣ≡ perA perB predicateEq = Σ≡Prop (λ x → isPropIsPartialEquivalenceRelation X x) predicateEq 
-
-  PartialEquivalenceRelationΣ≃ : (perA perB : PartialEquivalenceRelationΣ X) → (perA .fst ≡ perB .fst) ≃ (perA ≡ perB)
-  PartialEquivalenceRelationΣ≃ perA perB = Σ≡PropEquiv λ x → isPropIsPartialEquivalenceRelation X x
-
-  PartialEquivalenceRelationIso : (perA perB : PartialEquivalenceRelation X) → Iso (Iso.fun PartialEquivalenceRelationIsoΣ perA ≡ Iso.fun PartialEquivalenceRelationIsoΣ perB) (perA ≡ perB)
-  Iso.fun (PartialEquivalenceRelationIso perA perB) p i = Iso.inv PartialEquivalenceRelationIsoΣ (p i)
-  inv (PartialEquivalenceRelationIso perA perB) = cong (λ x → Iso.fun PartialEquivalenceRelationIsoΣ x)
-  rightInv (PartialEquivalenceRelationIso perA perB) b = refl
-  leftInv (PartialEquivalenceRelationIso perA perB) a = refl
-
-  -- Main SIP
-  PartialEquivalenceRelation≃ : (perA perB : PartialEquivalenceRelation X) → (perA .equality ≡ perB .equality) ≃ (perA ≡ perB)
-  PartialEquivalenceRelation≃ perA perB =
-    perA .equality ≡ perB .equality
-      ≃⟨ idEquiv (perA .equality ≡ perB .equality) ⟩
-    Iso.fun PartialEquivalenceRelationIsoΣ perA .fst ≡ Iso.fun PartialEquivalenceRelationIsoΣ perB .fst
-      ≃⟨ PartialEquivalenceRelationΣ≃ (Iso.fun PartialEquivalenceRelationIsoΣ perA) (Iso.fun PartialEquivalenceRelationIsoΣ perB) ⟩
-    Iso.fun PartialEquivalenceRelationIsoΣ perA ≡ Iso.fun PartialEquivalenceRelationIsoΣ perB
-      ≃⟨ isoToEquiv (PartialEquivalenceRelationIso perA perB) ⟩
-    perA ≡ perB
-      ■
+    isSymmetric : ∃[ s ∈ A ] (∀ x y r → r ⊩ ∣ equality ∣ (x , y) → (s ⨾ r) ⊩ ∣ equality ∣ (y , x))
+  field
+    isTransitive : ∃[ t ∈ A ] (∀ x y z a b → a ⊩ ∣ equality ∣ (x , y) → b ⊩ ∣ equality ∣ (y , z) → (t ⨾ (pair ⨾ a ⨾ b)) ⊩ ∣ equality ∣ (x , z))
+

src/Realizability/Tripos/Logic/Semantics.agda

@@ -27,18 +27,16 @@ open CombinatoryAlgebra ca
 private λ*ComputationRule = `λ*ComputationRule as fefermanStructure
 private λ* = `λ* as fefermanStructure
 
-open import Realizability.Tripos.Prealgebra.Predicate.Base ca renaming (Predicate to Predicate')
-open import Realizability.Tripos.Prealgebra.Predicate.Properties ca
-open import Realizability.Tripos.Prealgebra.Meets.Identity ca
-open import Realizability.Tripos.Prealgebra.Joins.Identity ca
-open import Realizability.Tripos.Prealgebra.Implication ca
+open import Realizability.Tripos.Prealgebra.Predicate.Base {ℓ' = ℓ'} {ℓ'' = ℓ''} ca
+open import Realizability.Tripos.Prealgebra.Predicate.Properties {ℓ' = ℓ'} {ℓ'' = ℓ''} ca
+open import Realizability.Tripos.Prealgebra.Meets.Identity {ℓ' = ℓ'} {ℓ'' = ℓ''} ca
+open import Realizability.Tripos.Prealgebra.Joins.Identity {ℓ' = ℓ'} {ℓ'' = ℓ''} ca
+open import Realizability.Tripos.Prealgebra.Implication {ℓ' = ℓ'} {ℓ'' = ℓ''} ca
 open import Realizability.Tripos.Logic.Syntax {ℓ = ℓ'}
 open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a)
-open Predicate'
+open Predicate
 open PredicateProperties hiding (_≤_ ; isTrans≤)
-open Morphism {ℓ' = ℓ'} {ℓ'' = ℓ''}
-private
-  Predicate = Predicate' {ℓ' = ℓ'} {ℓ'' = ℓ''}
+open Morphism
 RelationInterpretation : ∀ {n : ℕ} → (Vec Sort n) → Type _
 RelationInterpretation {n} relSym = (∀ i →  Predicate ⟨ ⟦ lookup i relSym ⟧ˢ ⟩)
 
@@ -315,8 +313,8 @@ module Soundness
       (ϕ⊨ψ >>=
         λ { (a , a⊩ϕ≤ψ) →
           ∣ a , (λ γ b b⊩ϕsubsγ → a⊩ϕ≤ψ (⟦ subs ⟧ᴮ γ) b b⊩ϕsubsγ) ∣₁ }) where
-      open PredProps {ℓ'' = ℓ''} ⟨ ⟦ Γ ⟧ᶜ ⟩ renaming (_≤_ to _≤Γ_)
-      open PredProps {ℓ'' = ℓ''} ⟨ ⟦ Δ ⟧ᶜ ⟩ renaming (_≤_ to _≤Δ_)
+      open PredProps ⟨ ⟦ Γ ⟧ᶜ ⟩ renaming (_≤_ to _≤Γ_)
+      open PredProps ⟨ ⟦ Δ ⟧ᶜ ⟩ renaming (_≤_ to _≤Δ_)
 
   `∧intro : ∀ {Γ} {ϕ ψ θ : Formula Γ} → ϕ ⊨ ψ → entails ϕ θ → entails ϕ (ψ `∧ θ)
   `∧intro {Γ} {ϕ} {ψ} {θ} ϕ⊨ψ ϕ⊨θ =

src/Realizability/Tripos/Prealgebra/Implication.agda

@@ -7,9 +7,9 @@ open import Cubical.HITs.PropositionalTruncation.Monad
 open import Cubical.Data.Fin
 open import Cubical.Data.Vec
 
-module Realizability.Tripos.Prealgebra.Implication {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
+module Realizability.Tripos.Prealgebra.Implication {ℓ ℓ' ℓ''} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
 
-open import Realizability.Tripos.Prealgebra.Predicate ca
+open import Realizability.Tripos.Prealgebra.Predicate {ℓ' = ℓ'} {ℓ'' = ℓ''} ca
 
 open CombinatoryAlgebra ca
 open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a)
@@ -18,10 +18,10 @@ private
   λ*ComputationRule = `λ*ComputationRule as fefermanStructure
   λ* = `λ* as fefermanStructure
 
-module _ {ℓ' ℓ''} (X : Type ℓ') (isSetX' : isSet X) where
-  PredicateX = Predicate {ℓ'' = ℓ''} X
+module _ (X : Type ℓ') (isSetX' : isSet X) where
+  PredicateX = Predicate  X
   open Predicate
-  open PredicateProperties {ℓ'' = ℓ''} X
+  open PredicateProperties  X
   -- ⇒ is Heyting implication
   a⊓b≤c→a≤b⇒c : ∀ a b c → (a ⊓ b ≤ c) → a ≤ (b ⇒ c)
   a⊓b≤c→a≤b⇒c a b c a⊓b≤c =

src/Realizability/Tripos/Prealgebra/Joins/Commutativity.agda

@@ -11,19 +11,17 @@ open import Cubical.HITs.PropositionalTruncation.Monad
 
 module Realizability.Tripos.Prealgebra.Joins.Commutativity {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
 
-open import Realizability.Tripos.Prealgebra.Predicate ca
-
 open CombinatoryAlgebra ca
 open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a)
 
 private λ*ComputationRule = `λ*ComputationRule as fefermanStructure
 private λ* = `λ* as fefermanStructure
 
 module _ {ℓ' ℓ''} (X : Type ℓ') (isSetX' : isSet X) where
-
-  private PredicateX = Predicate {ℓ'' = ℓ''} X
+  open import Realizability.Tripos.Prealgebra.Predicate {ℓ' = ℓ'} {ℓ'' = ℓ''} ca
+  private PredicateX = Predicate X
   open Predicate
-  open PredicateProperties {ℓ'' = ℓ''} X
+  open PredicateProperties  X
   open PreorderReasoning preorder≤
 
   -- ⊔ is commutative upto anti-symmetry

src/Realizability/Tripos/Prealgebra/Joins/Identity.agda

@@ -12,19 +12,19 @@ open import Cubical.Relation.Binary.Order.Preorder
 open import Realizability.CombinatoryAlgebra
 open import Realizability.ApplicativeStructure renaming (λ*-naturality to `λ*ComputationRule; λ*-chain to `λ*) hiding (λ*)
 
-module Realizability.Tripos.Prealgebra.Joins.Identity {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
-open import Realizability.Tripos.Prealgebra.Predicate ca
+module Realizability.Tripos.Prealgebra.Joins.Identity {ℓ ℓ' ℓ''} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
+open import Realizability.Tripos.Prealgebra.Predicate {ℓ' = ℓ'} {ℓ'' = ℓ''} ca
 open import Realizability.Tripos.Prealgebra.Joins.Commutativity ca
 open CombinatoryAlgebra ca
 open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a)
 
 private λ*ComputationRule = `λ*ComputationRule as fefermanStructure
 private λ* = `λ* as fefermanStructure
 
-module _ {ℓ' ℓ''} (X : Type ℓ') (isSetX' : isSet X) (isNonTrivial : s ≡ k → ⊥) where
-  private PredicateX = Predicate {ℓ'' = ℓ''} X
+module _ (X : Type ℓ') (isSetX' : isSet X) (isNonTrivial : s ≡ k → ⊥) where
+  private PredicateX = Predicate  X
   open Predicate
-  open PredicateProperties {ℓ'' = ℓ''} X
+  open PredicateProperties  X
   open PreorderReasoning preorder≤
 
 

src/Realizability/Tripos/Prealgebra/Meets/Commutativity.agda

@@ -9,21 +9,21 @@ open import Cubical.Relation.Binary.Order.Preorder
 open import Cubical.HITs.PropositionalTruncation
 open import Cubical.HITs.PropositionalTruncation.Monad
 
-module Realizability.Tripos.Prealgebra.Meets.Commutativity {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
+module Realizability.Tripos.Prealgebra.Meets.Commutativity {ℓ ℓ' ℓ''} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
 
-open import Realizability.Tripos.Prealgebra.Predicate ca
+open import Realizability.Tripos.Prealgebra.Predicate {ℓ' = ℓ'} {ℓ'' = ℓ''} ca
 
 open CombinatoryAlgebra ca
 open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a)
 
 private λ*ComputationRule = `λ*ComputationRule as fefermanStructure
 private λ* = `λ* as fefermanStructure
 
-module _ {ℓ' ℓ''} (X : Type ℓ') (isSetX' : isSet X) where
+module _ (X : Type ℓ') (isSetX' : isSet X) where
 
-  private PredicateX = Predicate {ℓ'' = ℓ''} X
+  private PredicateX = Predicate  X
   open Predicate
-  open PredicateProperties {ℓ'' = ℓ''} X
+  open PredicateProperties  X
   open PreorderReasoning preorder≤
 
   x⊓y≤y⊓x : ∀ x y → x ⊓ y ≤ y ⊓ x

src/Realizability/Tripos/Prealgebra/Meets/Identity.agda

@@ -11,19 +11,19 @@ open import Cubical.Relation.Binary.Order.Preorder
 open import Realizability.CombinatoryAlgebra
 open import Realizability.ApplicativeStructure renaming (λ*-naturality to `λ*ComputationRule; λ*-chain to `λ*) hiding (λ*)
 
-module Realizability.Tripos.Prealgebra.Meets.Identity {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
-open import Realizability.Tripos.Prealgebra.Predicate ca
-open import Realizability.Tripos.Prealgebra.Meets.Commutativity ca
+module Realizability.Tripos.Prealgebra.Meets.Identity {ℓ ℓ' ℓ''} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
+open import Realizability.Tripos.Prealgebra.Predicate {ℓ' = ℓ'} {ℓ'' = ℓ''} ca
+open import Realizability.Tripos.Prealgebra.Meets.Commutativity {ℓ' = ℓ'} {ℓ'' = ℓ''} ca
 open CombinatoryAlgebra ca
 open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a)
 
 private λ*ComputationRule = `λ*ComputationRule as fefermanStructure
 private λ* = `λ* as fefermanStructure
 
-module _ {ℓ' ℓ''} (X : Type ℓ') (isSetX' : isSet X) (isNonTrivial : s ≡ k → ⊥) where
-  private PredicateX = Predicate {ℓ'' = ℓ''} X
+module _ (X : Type ℓ') (isSetX' : isSet X) (isNonTrivial : s ≡ k → ⊥) where
+  private PredicateX = Predicate X
   open Predicate
-  open PredicateProperties {ℓ'' = ℓ''} X
+  open PredicateProperties X
   open PreorderReasoning preorder≤
 
   pre1 : PredicateX

src/Realizability/Tripos/Prealgebra/Predicate.agda

@@ -1,7 +1,7 @@
 open import Realizability.CombinatoryAlgebra
 open import Cubical.Foundations.Prelude
 
-module Realizability.Tripos.Prealgebra.Predicate {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
+module Realizability.Tripos.Prealgebra.Predicate {ℓ ℓ' ℓ''} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
 
-open import Realizability.Tripos.Prealgebra.Predicate.Base ca public
-open import Realizability.Tripos.Prealgebra.Predicate.Properties ca public
+open import Realizability.Tripos.Prealgebra.Predicate.Base {ℓ = ℓ} {ℓ' = ℓ'} {ℓ'' = ℓ''} ca public
+open import Realizability.Tripos.Prealgebra.Predicate.Properties {ℓ' = ℓ'} {ℓ'' = ℓ''} ca public

src/Realizability/Tripos/Prealgebra/Predicate/Base.agda

@@ -7,12 +7,12 @@ open import Cubical.Foundations.Isomorphism
 open import Cubical.Data.Sigma
 open import Cubical.Functions.FunExtEquiv
 
-module Realizability.Tripos.Prealgebra.Predicate.Base {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
+module Realizability.Tripos.Prealgebra.Predicate.Base {ℓ ℓ' ℓ''} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
 
 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
+record Predicate (X : Type ℓ') : Type (ℓ-max (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ')) (ℓ-suc ℓ'')) where
   field
     isSetX : isSet X
     ∣_∣ : X → A → Type (ℓ-max (ℓ-max ℓ ℓ') ℓ'')
@@ -24,40 +24,39 @@ infix 26 _⊩_
 _⊩_ : ∀ {ℓ'} → A → (A → Type ℓ') → Type ℓ'
 a ⊩ ϕ = ϕ a
 
-PredicateΣ : ∀ {ℓ' ℓ''} → (X : Type ℓ') → Type (ℓ-max (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ')) (ℓ-suc ℓ''))
-PredicateΣ {ℓ'} {ℓ''} X = Σ[ rel ∈ (X → A → hProp (ℓ-max (ℓ-max ℓ ℓ') ℓ'')) ] (isSet X)
+PredicateΣ : ∀ (X : Type ℓ') → Type (ℓ-max (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ')) (ℓ-suc ℓ''))
+PredicateΣ X = Σ[ rel ∈ (X → A → hProp (ℓ-max (ℓ-max ℓ ℓ') ℓ'')) ] (isSet X)
 
-isSetPredicateΣ : ∀ {ℓ' ℓ''} (X : Type ℓ') → isSet (PredicateΣ {ℓ'' = ℓ''} X)
+isSetPredicateΣ : ∀ (X : Type ℓ') → isSet (PredicateΣ X)
 isSetPredicateΣ X = isSetΣ (isSetΠ (λ x → isSetΠ λ a → isSetHProp)) λ _ → isProp→isSet isPropIsSet
 
-PredicateIsoΣ : ∀ {ℓ' ℓ''} (X : Type ℓ') → Iso (Predicate {ℓ'' = ℓ''} X) (PredicateΣ {ℓ'' = ℓ''} X)
-PredicateIsoΣ {ℓ'} {ℓ''} X =
+PredicateIsoΣ : ∀ (X : Type ℓ') → Iso (Predicate  X) (PredicateΣ  X)
+PredicateIsoΣ X =
   iso
     (λ p → (λ x a → (a ⊩ ∣ p ∣ x) , p .isPropValued x a) , p .isSetX)
     (λ p → record { isSetX = p .snd ; ∣_∣ = λ x a → p .fst x a .fst ; isPropValued = λ x a → p .fst x a .snd })
     (λ b → refl)
     λ a → refl
 
-Predicate≡PredicateΣ : ∀ {ℓ' ℓ''} (X : Type ℓ') → Predicate {ℓ'' = ℓ''} X ≡ PredicateΣ {ℓ'' = ℓ''} X
-Predicate≡PredicateΣ {ℓ'} {ℓ''} X = isoToPath (PredicateIsoΣ X)
+Predicate≡PredicateΣ : ∀ (X : Type ℓ') → Predicate  X ≡ PredicateΣ  X
+Predicate≡PredicateΣ X = isoToPath (PredicateIsoΣ X)
 
-isSetPredicate : ∀ {ℓ' ℓ''} (X : Type ℓ') → isSet (Predicate {ℓ'' = ℓ''} X)
-isSetPredicate {ℓ'} {ℓ''} X = subst (λ predicateType → isSet predicateType) (sym (Predicate≡PredicateΣ X)) (isSetPredicateΣ {ℓ'' = ℓ''} X)
+isSetPredicate : ∀  (X : Type ℓ') → isSet (Predicate  X)
+isSetPredicate X = subst (λ predicateType → isSet predicateType) (sym (Predicate≡PredicateΣ X)) (isSetPredicateΣ  X)
 
-PredicateΣ≡ : ∀ {ℓ' ℓ''} (X : Type ℓ') → (P Q : PredicateΣ {ℓ'' = ℓ''} X) → (P .fst ≡ Q .fst) → P ≡ Q
+PredicateΣ≡ : ∀  (X : Type ℓ') → (P Q : PredicateΣ  X) → (P .fst ≡ Q .fst) → P ≡ Q
 PredicateΣ≡ X P Q ∣P∣≡∣Q∣ = Σ≡Prop (λ _ → isPropIsSet) ∣P∣≡∣Q∣
 
 Predicate≡ :
-  ∀ {ℓ' ℓ''} (X : Type ℓ')
-  → (P Q : Predicate {ℓ'' = ℓ''} X)
+  ∀ (X : Type ℓ')
+  → (P Q : Predicate  X)
   → (∀ x a → a ⊩ ∣ P ∣ x → a ⊩ ∣ Q ∣ x)
   → (∀ x a → a ⊩ ∣ Q ∣ x → a ⊩ ∣ P ∣ x)
   -----------------------------------
   → P ≡ Q
-Predicate≡ {ℓ'} {ℓ''} X P Q P→Q Q→P i =
+Predicate≡ X P Q P→Q Q→P i =
   PredicateIsoΣ X .inv
     (PredicateΣ≡
-      {ℓ'' = ℓ''}
       X
       (PredicateIsoΣ X .fun P)
       (PredicateIsoΣ X .fun Q)