{-# OPTIONS --cubical-compatible --safe #-} module Forcing.Base where open import Level open import Data.Sum open import Data.Product open import Relation.Unary record ForcingNotion : Set₁ where field L : Set _≼_ : L → L → Set ≼-refl : {x : L} → x ≼ x ≼-trans : {x y z : L} → x ≼ y → y ≼ z → x ≼ z Cov : L → Set _◁_ : {x : L} → (a : L) → (R : Cov x) → Set ◁⇒≼ : {x y : L} {R : Cov x} → y ◁ R → y ≼ x stable : {x y : L} → y ≼ x → (R : Cov x) → Σ[ S ∈ Cov y ] ({a : L} → a ◁ S → Σ[ b ∈ L ] (a ≼ b × b ◁ R)) record Filter (L… : ForcingNotion) : Set₁ where open ForcingNotion L… field F : Pred L 0ℓ upward-closed : {x y : L} → y ≼ x → F y → F x downward-directed₁ : Σ[ x ∈ L ] F x downward-directed₂ : {a b : L} → F a → F b → Σ[ x ∈ L ] x ≼ a × x ≼ b × F x split : {x : L} {R : Cov x} → F x → Σ[ y ∈ L ] F y × y ◁ R