From d02a8cf4094be165ffaf740589c0d10d103a9d7d Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 31 Oct 2025 07:49:58 +0000 Subject: [PATCH 1/7] add: adjoint properties for #2840 --- CHANGELOG.md | 14 ++++++++++++++ src/Function/Related/TypeIsomorphisms.agda | 6 ++++-- src/Relation/Unary.agda | 16 +++++++++++++++- src/Relation/Unary/Properties.agda | 17 +++++++++++++++++ 4 files changed, 50 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 6679049fd0..7cec4ce8d2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -221,6 +221,20 @@ Additions to existing modules contradiction′ : ¬ A → A → Whatever ``` +* In `Relation.Unary` + ```agda + ⟨_⟩⊢_ : (A → B) → Pred A ℓ → Pred B _ + [_]⊢_ : (A → B) → Pred A ℓ → Pred B _ + ``` + +* In `Relation.Unary.Properties` + ```agda + ⟨_⟩⊢ˡ : (f : A → B) → ⟨ f ⟩⊢ P ⊆ Q → P ⊆ f ⊢ Q + ⟨_⟩⊢ʳ : (f : A → B) → P ⊆ f ⊢ Q → ⟨ f ⟩⊢ P ⊆ Q + [_]⊢ˡ : (f : A → B) → Q ⊆ [ f ]⊢ P → f ⊢ Q ⊆ P + [_]⊢ʳ : (f : A → B) → f ⊢ Q ⊆ P → Q ⊆ [ f ]⊢ P + ``` + * In `System.Random`: ```agda randomIO : IO Bool diff --git a/src/Function/Related/TypeIsomorphisms.agda b/src/Function/Related/TypeIsomorphisms.agda index b1549ef14d..c635fe3da5 100644 --- a/src/Function/Related/TypeIsomorphisms.agda +++ b/src/Function/Related/TypeIsomorphisms.agda @@ -39,6 +39,8 @@ open import Relation.Binary.PropositionalEquality.Properties using (module ≡-Reasoning) open import Relation.Nullary.Negation.Core using (¬_) import Relation.Nullary.Indexed as I +open import Relation.Unary using (⟨_⟩⊢_) +open import Relation.Unary.Properties using (⟨_⟩⊢ˡ; ⟨_⟩⊢ʳ) private variable @@ -359,7 +361,7 @@ Related-cong {A = A} {B = B} {C = C} {D = D} A≈B C≈D = mk⇔ -- Relating a predicate to an existentially quantified one with the -- restriction that the quantified variable is equal to the given one -∃-≡ : ∀ (P : A → Set b) {x} → P x ↔ (∃[ y ] y ≡ x × P y) -∃-≡ P {x} = mk↔ₛ′ (λ Px → x , refl , Px) (λ where (_ , refl , Py) → Py) +∃-≡ : ∀ (P : A → Set b) {x} → P x ↔ (⟨ id ⟩⊢ P) x +∃-≡ P {x} = mk↔ₛ′ (⟨ id ⟩⊢ˡ id) (⟨ id ⟩⊢ʳ id) (λ where (_ , refl , _) → refl) (λ where _ → refl) diff --git a/src/Relation/Unary.agda b/src/Relation/Unary.agda index 86bb80f1bb..d8570699c0 100644 --- a/src/Relation/Unary.agda +++ b/src/Relation/Unary.agda @@ -261,11 +261,25 @@ P ⊥ Q = P ∩ Q ⊆ ∅ _⊥′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _ P ⊥′ Q = P ∩ Q ⊆′ ∅ --- Update. +-- Update/functorial change-of-base + +-- The notation captures the Martin-Löf tradition of only mentioning +-- updates to the ambient context when describing a context-indexed +-- family P e.g. (_, σ) ⊢ Tm τ is +-- "a term of type τ in the ambient context extended with a fresh σ". _⊢_ : (A → B) → Pred B ℓ → Pred A ℓ f ⊢ P = λ x → P (f x) +-- Change-of-base has left- and right- adjoints (Lawvere). +-- We borrow the 'diamond'/'box' notation from modal logic, cf. +-- `Relation.Unary.Closure.Base` +⟨_⟩⊢_ : (A → B) → Pred A ℓ → Pred B _ +⟨ f ⟩⊢ P = λ y → ∃ λ x → f x ≡ y × P x + +[_]⊢_ : (A → B) → Pred A ℓ → Pred B _ +[ f ]⊢ P = λ y → ∀ {x} → f x ≡ y → P x + ------------------------------------------------------------------------ -- Predicate combinators diff --git a/src/Relation/Unary/Properties.agda b/src/Relation/Unary/Properties.agda index 63a75e4cff..8d72616d2c 100644 --- a/src/Relation/Unary/Properties.agda +++ b/src/Relation/Unary/Properties.agda @@ -220,6 +220,23 @@ U-Universal = λ _ → _ ⊥⇒¬≬ : Binary._⇒_ {A = Pred A ℓ₁} {B = Pred A ℓ₂} _⊥_ (¬_ ∘₂ _≬_) ⊥⇒¬≬ P⊥Q = P⊥Q ∘ Product.proj₂ +------------------------------------------------------------------------ +-- Adjoint properties for change-of-base + +module _ {P : Pred A ℓ₁} {Q : Pred B ℓ₂} (f : A → B) where + + ⟨_⟩⊢ˡ : ⟨ f ⟩⊢ P ⊆ Q → P ⊆ f ⊢ Q + ⟨_⟩⊢ˡ ⟨f⟩⊢P⊆Q Px = ⟨f⟩⊢P⊆Q (_ , refl , Px) + + ⟨_⟩⊢ʳ : P ⊆ f ⊢ Q → ⟨ f ⟩⊢ P ⊆ Q + ⟨_⟩⊢ʳ P⊆f⊢Q (x , refl , Px) = P⊆f⊢Q Px + + [_]⊢ˡ : Q ⊆ [ f ]⊢ P → f ⊢ Q ⊆ P + [_]⊢ˡ Q⊆[f]⊢P Qfx = Q⊆[f]⊢P Qfx refl + + [_]⊢ʳ : f ⊢ Q ⊆ P → Q ⊆ [ f ]⊢ P + [_]⊢ʳ f⊢Q⊆P Qfx refl = f⊢Q⊆P Qfx + ------------------------------------------------------------------------ -- Decidability properties From 7a8d3cf55d66092461997070411bf9857bcd3e00 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 8 Nov 2025 07:03:04 +0000 Subject: [PATCH 2/7] add: functoriality proofs --- CHANGELOG.md | 11 ++++++---- src/Relation/Unary.agda | 5 ++++- src/Relation/Unary/Properties.agda | 32 +++++++++++++++++++++--------- 3 files changed, 34 insertions(+), 14 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 7cec4ce8d2..17de0197c8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -229,10 +229,13 @@ Additions to existing modules * In `Relation.Unary.Properties` ```agda - ⟨_⟩⊢ˡ : (f : A → B) → ⟨ f ⟩⊢ P ⊆ Q → P ⊆ f ⊢ Q - ⟨_⟩⊢ʳ : (f : A → B) → P ⊆ f ⊢ Q → ⟨ f ⟩⊢ P ⊆ Q - [_]⊢ˡ : (f : A → B) → Q ⊆ [ f ]⊢ P → f ⊢ Q ⊆ P - [_]⊢ʳ : (f : A → B) → f ⊢ Q ⊆ P → Q ⊆ [ f ]⊢ P + _map-⊢_ : P ⊆ Q → f ⊢ P ⊆ f ⊢ Q + map-⟨_⟩⊢_ : P ⊆ Q → ⟨ f ⟩⊢ P ⊆ ⟨ f ⟩⊢ Q + map-[_]⊢_ : P ⊆ Q → [ f ]⊢ P ⊆ [ f ]⊢ Q + ⟨_⟩⊢⁻_ : ⟨ f ⟩⊢ P ⊆ Q → P ⊆ f ⊢ Q + ⟨_⟩⊢⁺_ : P ⊆ f ⊢ Q → ⟨ f ⟩⊢ P ⊆ Q + [_]⊢⁻_ : Q ⊆ [ f ]⊢ P → f ⊢ Q ⊆ P + [_]⊢⁺_ : f ⊢ Q ⊆ P → Q ⊆ [ f ]⊢ P ``` * In `System.Random`: diff --git a/src/Relation/Unary.agda b/src/Relation/Unary.agda index d8570699c0..cd9be0ccdc 100644 --- a/src/Relation/Unary.agda +++ b/src/Relation/Unary.agda @@ -273,7 +273,10 @@ f ⊢ P = λ x → P (f x) -- Change-of-base has left- and right- adjoints (Lawvere). -- We borrow the 'diamond'/'box' notation from modal logic, cf. --- `Relation.Unary.Closure.Base` +-- `Relation.Unary.Closure.Base`, rather than Lawvere's ∃f, ∀f. +-- In some settings, the left adjoint is called 'image' or 'pushforward', +-- but the right adjoint doesn't seem to have a non-symbolic name. + ⟨_⟩⊢_ : (A → B) → Pred A ℓ → Pred B _ ⟨ f ⟩⊢ P = λ y → ∃ λ x → f x ≡ y × P x diff --git a/src/Relation/Unary/Properties.agda b/src/Relation/Unary/Properties.agda index 8d72616d2c..790582a9e5 100644 --- a/src/Relation/Unary/Properties.agda +++ b/src/Relation/Unary/Properties.agda @@ -221,21 +221,35 @@ U-Universal = λ _ → _ ⊥⇒¬≬ P⊥Q = P⊥Q ∘ Product.proj₂ ------------------------------------------------------------------------ --- Adjoint properties for change-of-base +-- Properties of adjoints to update: functoriality and adjointness + +module _ {P : Pred B ℓ₁} {Q : Pred B ℓ₂} where + + _map-⊢_ : (f : A → B) → P ⊆ Q → f ⊢ P ⊆ f ⊢ Q + f map-⊢ P⊆Q = P⊆Q + +module _ {P : Pred A ℓ₁} {Q : Pred A ℓ₂} (f : A → B) where + + map-⟨_⟩⊢_ : P ⊆ Q → ⟨ f ⟩⊢ P ⊆ ⟨ f ⟩⊢ Q + map-⟨_⟩⊢_ P⊆Q (_ , refl , Px) = (_ , refl , P⊆Q Px) + + map-[_]⊢_ : P ⊆ Q → [ f ]⊢ P ⊆ [ f ]⊢ Q + map-[_]⊢_ P⊆Q Px refl = P⊆Q (Px refl) module _ {P : Pred A ℓ₁} {Q : Pred B ℓ₂} (f : A → B) where - ⟨_⟩⊢ˡ : ⟨ f ⟩⊢ P ⊆ Q → P ⊆ f ⊢ Q - ⟨_⟩⊢ˡ ⟨f⟩⊢P⊆Q Px = ⟨f⟩⊢P⊆Q (_ , refl , Px) + ⟨_⟩⊢⁻_ : ⟨ f ⟩⊢ P ⊆ Q → P ⊆ f ⊢ Q + ⟨_⟩⊢⁻_ ⟨f⟩⊢P⊆Q Px = ⟨f⟩⊢P⊆Q (_ , refl , Px) + + ⟨_⟩⊢⁺_ : P ⊆ f ⊢ Q → ⟨ f ⟩⊢ P ⊆ Q + ⟨_⟩⊢⁺_ P⊆f⊢Q (_ , refl , Px) = P⊆f⊢Q Px - ⟨_⟩⊢ʳ : P ⊆ f ⊢ Q → ⟨ f ⟩⊢ P ⊆ Q - ⟨_⟩⊢ʳ P⊆f⊢Q (x , refl , Px) = P⊆f⊢Q Px + [_]⊢⁻_ : Q ⊆ [ f ]⊢ P → f ⊢ Q ⊆ P + [_]⊢⁻_ Q⊆[f]⊢P Qfx = Q⊆[f]⊢P Qfx refl - [_]⊢ˡ : Q ⊆ [ f ]⊢ P → f ⊢ Q ⊆ P - [_]⊢ˡ Q⊆[f]⊢P Qfx = Q⊆[f]⊢P Qfx refl + [_]⊢⁺_ : f ⊢ Q ⊆ P → Q ⊆ [ f ]⊢ P + [_]⊢⁺_ f⊢Q⊆P Qfx refl = f⊢Q⊆P Qfx - [_]⊢ʳ : f ⊢ Q ⊆ P → Q ⊆ [ f ]⊢ P - [_]⊢ʳ f⊢Q⊆P Qfx refl = f⊢Q⊆P Qfx ------------------------------------------------------------------------ -- Decidability properties From 3ca0b0613a9d7513fcc753d5ca846be17d981143 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 8 Nov 2025 07:14:28 +0000 Subject: [PATCH 3/7] tweak: keep original statement --- src/Function/Related/TypeIsomorphisms.agda | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/Function/Related/TypeIsomorphisms.agda b/src/Function/Related/TypeIsomorphisms.agda index c635fe3da5..14dc2bb7d5 100644 --- a/src/Function/Related/TypeIsomorphisms.agda +++ b/src/Function/Related/TypeIsomorphisms.agda @@ -39,8 +39,7 @@ open import Relation.Binary.PropositionalEquality.Properties using (module ≡-Reasoning) open import Relation.Nullary.Negation.Core using (¬_) import Relation.Nullary.Indexed as I -open import Relation.Unary using (⟨_⟩⊢_) -open import Relation.Unary.Properties using (⟨_⟩⊢ˡ; ⟨_⟩⊢ʳ) +open import Relation.Unary.Properties using (⟨_⟩⊢⁻_; ⟨_⟩⊢⁺_) private variable @@ -361,7 +360,7 @@ Related-cong {A = A} {B = B} {C = C} {D = D} A≈B C≈D = mk⇔ -- Relating a predicate to an existentially quantified one with the -- restriction that the quantified variable is equal to the given one -∃-≡ : ∀ (P : A → Set b) {x} → P x ↔ (⟨ id ⟩⊢ P) x -∃-≡ P {x} = mk↔ₛ′ (⟨ id ⟩⊢ˡ id) (⟨ id ⟩⊢ʳ id) +∃-≡ : ∀ (P : A → Set b) {x} → P x ↔ (∃[ y ] y ≡ x × P y) +∃-≡ P {x} = mk↔ₛ′ (⟨ id ⟩⊢⁻ id) (⟨ id ⟩⊢⁺ id) (λ where (_ , refl , _) → refl) (λ where _ → refl) From 8bf7322d78a9c573526ae27e93bf3b89c7832eed Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 8 Nov 2025 07:16:39 +0000 Subject: [PATCH 4/7] fix: whitespace --- src/Function/Related/TypeIsomorphisms.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Function/Related/TypeIsomorphisms.agda b/src/Function/Related/TypeIsomorphisms.agda index 14dc2bb7d5..1f7e0d7110 100644 --- a/src/Function/Related/TypeIsomorphisms.agda +++ b/src/Function/Related/TypeIsomorphisms.agda @@ -361,6 +361,6 @@ Related-cong {A = A} {B = B} {C = C} {D = D} A≈B C≈D = mk⇔ -- restriction that the quantified variable is equal to the given one ∃-≡ : ∀ (P : A → Set b) {x} → P x ↔ (∃[ y ] y ≡ x × P y) -∃-≡ P {x} = mk↔ₛ′ (⟨ id ⟩⊢⁻ id) (⟨ id ⟩⊢⁺ id) +∃-≡ P {x} = mk↔ₛ′ (⟨ id ⟩⊢⁻ id) (⟨ id ⟩⊢⁺ id) (λ where (_ , refl , _) → refl) (λ where _ → refl) From cbf3cc87868a0737d564596e69a44c651ae98570 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 8 Nov 2025 09:28:18 +0000 Subject: [PATCH 5/7] refactor: functoriality of the adjoints --- src/Relation/Unary/Properties.agda | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/Relation/Unary/Properties.agda b/src/Relation/Unary/Properties.agda index 790582a9e5..5d4de3109a 100644 --- a/src/Relation/Unary/Properties.agda +++ b/src/Relation/Unary/Properties.agda @@ -228,14 +228,6 @@ module _ {P : Pred B ℓ₁} {Q : Pred B ℓ₂} where _map-⊢_ : (f : A → B) → P ⊆ Q → f ⊢ P ⊆ f ⊢ Q f map-⊢ P⊆Q = P⊆Q -module _ {P : Pred A ℓ₁} {Q : Pred A ℓ₂} (f : A → B) where - - map-⟨_⟩⊢_ : P ⊆ Q → ⟨ f ⟩⊢ P ⊆ ⟨ f ⟩⊢ Q - map-⟨_⟩⊢_ P⊆Q (_ , refl , Px) = (_ , refl , P⊆Q Px) - - map-[_]⊢_ : P ⊆ Q → [ f ]⊢ P ⊆ [ f ]⊢ Q - map-[_]⊢_ P⊆Q Px refl = P⊆Q (Px refl) - module _ {P : Pred A ℓ₁} {Q : Pred B ℓ₂} (f : A → B) where ⟨_⟩⊢⁻_ : ⟨ f ⟩⊢ P ⊆ Q → P ⊆ f ⊢ Q @@ -250,6 +242,14 @@ module _ {P : Pred A ℓ₁} {Q : Pred B ℓ₂} (f : A → B) where [_]⊢⁺_ : f ⊢ Q ⊆ P → Q ⊆ [ f ]⊢ P [_]⊢⁺_ f⊢Q⊆P Qfx refl = f⊢Q⊆P Qfx +module _ {P : Pred A ℓ₁} {Q : Pred A ℓ₂} (f : A → B) where + + map-⟨_⟩⊢_ : P ⊆ Q → ⟨ f ⟩⊢ P ⊆ ⟨ f ⟩⊢ Q + map-⟨_⟩⊢_ P⊆Q = ⟨ f ⟩⊢⁺ ⊆-trans {j = Q} P⊆Q (⟨ f ⟩⊢⁻ ⊆-refl {x = ⟨ f ⟩⊢ Q}) + + map-[_]⊢_ : P ⊆ Q → [ f ]⊢ P ⊆ [ f ]⊢ Q + map-[_]⊢_ P⊆Q = [ f ]⊢⁺ ⊆-trans {j = P} ([ f ]⊢⁻ ⊆-refl {x = [ f ]⊢ P}) P⊆Q + ------------------------------------------------------------------------ -- Decidability properties From e32b4fc84add110401933a138e7540359b4b85ee Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 8 Nov 2025 09:36:41 +0000 Subject: [PATCH 6/7] refactor: functoriality of the adjoints, again --- src/Relation/Unary/Properties.agda | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/Relation/Unary/Properties.agda b/src/Relation/Unary/Properties.agda index 5d4de3109a..6714770562 100644 --- a/src/Relation/Unary/Properties.agda +++ b/src/Relation/Unary/Properties.agda @@ -245,10 +245,12 @@ module _ {P : Pred A ℓ₁} {Q : Pred B ℓ₂} (f : A → B) where module _ {P : Pred A ℓ₁} {Q : Pred A ℓ₂} (f : A → B) where map-⟨_⟩⊢_ : P ⊆ Q → ⟨ f ⟩⊢ P ⊆ ⟨ f ⟩⊢ Q - map-⟨_⟩⊢_ P⊆Q = ⟨ f ⟩⊢⁺ ⊆-trans {j = Q} P⊆Q (⟨ f ⟩⊢⁻ ⊆-refl {x = ⟨ f ⟩⊢ Q}) + map-⟨_⟩⊢_ P⊆Q = ⟨ f ⟩⊢⁺ ⊆-trans {k = f ⊢ ⟨f⟩⊢Q} P⊆Q (⟨ f ⟩⊢⁻ ⊆-refl {x = ⟨f⟩⊢Q}) + where ⟨f⟩⊢Q = ⟨ f ⟩⊢ Q map-[_]⊢_ : P ⊆ Q → [ f ]⊢ P ⊆ [ f ]⊢ Q - map-[_]⊢_ P⊆Q = [ f ]⊢⁺ ⊆-trans {j = P} ([ f ]⊢⁻ ⊆-refl {x = [ f ]⊢ P}) P⊆Q + map-[_]⊢_ P⊆Q = [ f ]⊢⁺ ⊆-trans {i = f ⊢ [f]⊢P} ([ f ]⊢⁻ ⊆-refl {x = [f]⊢P}) P⊆Q + where [f]⊢P = [ f ]⊢ P ------------------------------------------------------------------------ From 1dd33eef2e60765a714033fe61c00fdd302b5c79 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 11 Nov 2025 19:21:51 +0000 Subject: [PATCH 7/7] add: more commentary text --- src/Relation/Unary.agda | 19 ++++++++++++------- src/Relation/Unary/Properties.agda | 4 ++++ 2 files changed, 16 insertions(+), 7 deletions(-) diff --git a/src/Relation/Unary.agda b/src/Relation/Unary.agda index a29b1b526b..95d9792882 100644 --- a/src/Relation/Unary.agda +++ b/src/Relation/Unary.agda @@ -261,21 +261,26 @@ P ⊥ Q = P ∩ Q ⊆ ∅ _⊥′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _ P ⊥′ Q = P ∩ Q ⊆′ ∅ --- Update/functorial change-of-base - --- The notation captures the Martin-Löf tradition of only mentioning --- updates to the ambient context when describing a context-indexed --- family P e.g. (_, σ) ⊢ Tm τ is +-- Update/preimage/inverse image/functorial change-of-base +-- +-- The notation, which elsewhere might be rendered +-- * `f⁻¹ P`, for preimage/inverse image +-- * `f* P`, for change-of-base/pullback along `f` +-- captures the Martin-Löf tradition of only mentioning updates to +-- the ambient context when describing a context-indexed family P: +-- e.g. (_, σ) ⊢ Tm τ is -- "a term of type τ in the ambient context extended with a fresh σ". _⊢_ : (A → B) → Pred B ℓ → Pred A ℓ f ⊢ P = λ x → P (f x) -- Change-of-base has left- and right- adjoints (Lawvere). +-- -- We borrow the 'diamond'/'box' notation from modal logic, cf. -- `Relation.Unary.Closure.Base`, rather than Lawvere's ∃f, ∀f. --- In some settings, the left adjoint is called 'image' or 'pushforward', --- but the right adjoint doesn't seem to have a non-symbolic name. +-- In some settings (eg statistics/probability), the left adjoint +-- is called 'image' or 'pushforward', but the right adjoint +-- doesn't seem to have a non-symbolic name. -- Diamond diff --git a/src/Relation/Unary/Properties.agda b/src/Relation/Unary/Properties.agda index 6714770562..986a05da45 100644 --- a/src/Relation/Unary/Properties.agda +++ b/src/Relation/Unary/Properties.agda @@ -230,12 +230,16 @@ module _ {P : Pred B ℓ₁} {Q : Pred B ℓ₂} where module _ {P : Pred A ℓ₁} {Q : Pred B ℓ₂} (f : A → B) where +-- ⟨ f ⟩⊢_ is left adjoint to f ⊢_ for given f + ⟨_⟩⊢⁻_ : ⟨ f ⟩⊢ P ⊆ Q → P ⊆ f ⊢ Q ⟨_⟩⊢⁻_ ⟨f⟩⊢P⊆Q Px = ⟨f⟩⊢P⊆Q (_ , refl , Px) ⟨_⟩⊢⁺_ : P ⊆ f ⊢ Q → ⟨ f ⟩⊢ P ⊆ Q ⟨_⟩⊢⁺_ P⊆f⊢Q (_ , refl , Px) = P⊆f⊢Q Px +-- [ f ]⊢_ is right adjoint to f ⊢_ for given f + [_]⊢⁻_ : Q ⊆ [ f ]⊢ P → f ⊢ Q ⊆ P [_]⊢⁻_ Q⊆[f]⊢P Qfx = Q⊆[f]⊢P Qfx refl