module Cat.Displayed.Doctrine.Logic

The internal logic of a regular hyperdoctrine🔗

Fix a regular hyperdoctrine over a finitely complete category We’ve claimed that the data of is enough to interpret regular logic relative to but that proof was deferred. This module actually finishes this claim, but because syntax is always fiddly, it’s quite long.

Terms🔗

The first thing we’ll do is strictify a bit. Instead of working directly with arbitrary morphisms, it’s slightly better — for the computational behaviour of substitution — to have a syntactic presentation of the terms of our logic. We start with the types, built inductively using _`×_, and with an injection from the objects of We also single out a class of objects which are built from repeated pairing onto the terminal object to be the contexts.

data Ty : Typeω where
  ↑    : Ob → Ty
  _`×_ : Ty → Ty → Ty

data Cx : Typeω where
  []  : Cx
  _ʻ_ : Cx → Ty → Cx

These two classes can be interpreted into objects in the base category. Throughout this entire module, we’ll write for the semantic interpretation of a syntactic object; In the formalisation, the brackets are always superscript with an indicator of what is being interpreted.

⟦_⟧ᵗ : Ty → Ob
⟦ ↑ x    ⟧ᵗ = x
⟦ t `× s ⟧ᵗ = ⟦ t ⟧ᵗ ⊗₀ ⟦ s ⟧ᵗ

⟦_⟧ᶜ : Cx → Ob
⟦ []    ⟧ᶜ = Terminal.top terminal
⟦ Γ ʻ x ⟧ᶜ = ⟦ Γ ⟧ᶜ ⊗₀ ⟦ x ⟧ᵗ

Next we have the syntax of variables: A variable encodes a projection which, because of the structure of our contexts, is always of the form Put syntactically, we can always access the latest variable, and we can also weaken variables by one.

data _∋_ : Cx → Ty → Typeω where
  stop : (Γ ʻ τ) ∋ τ
  pop  : Γ ∋ τ → (Γ ʻ σ) ∋ τ

Finally, we can define the class of terms: A term is a variable, or lies in the fragment dealing with Cartesian products, or comes from applying a function from the base category to an argument this is required if we want our logic to be applicable to more than variables and products!

data Tm : Cx → Ty → Typeω where
  var : Γ ∋ τ → Tm Γ τ

  _,_ : Tm Γ τ → Tm Γ σ → Tm Γ (τ `× σ)
  `π₁ : Tm Γ (τ `× σ) → Tm Γ τ
  `π₂ : Tm Γ (τ `× σ) → Tm Γ σ

  fun : Hom ⟦ τ ⟧ᵗ ⟦ σ ⟧ᵗ → Tm Γ τ → Tm Γ σ

-- Superscript n for "name", e for "expression"
⟦_⟧ⁿ : Γ ∋ τ → Hom ⟦ Γ ⟧ᶜ ⟦ τ ⟧ᵗ
⟦ stop ⟧ⁿ  = π₂
⟦ pop x ⟧ⁿ = ⟦ x ⟧ⁿ ∘ π₁

⟦_⟧ᵉ : Tm Γ τ → Hom ⟦ Γ ⟧ᶜ ⟦ τ ⟧ᵗ
⟦ var x ⟧ᵉ   = ⟦ x ⟧ⁿ
⟦ x , y ⟧ᵉ   = ⟨ ⟦ x ⟧ᵉ , ⟦ y ⟧ᵉ ⟩
⟦ `π₁ x ⟧ᵉ   = π₁ ∘ ⟦ x ⟧ᵉ
⟦ `π₂ x ⟧ᵉ   = π₂ ∘ ⟦ x ⟧ᵉ
⟦ fun f t ⟧ᵉ = f ∘ ⟦ t ⟧ᵉ

Renamings and substitutions🔗

Even after we have a good grasp on the morphisms in that we want to call terms, there are still two classes of maps, now between pairs of contexts, that we must single out. A renaming maps variables in to variables in there’s an identity renaming, and you can either choose to keep or drop variables from

If we allow ourselves to map variables in to terms in we get the class of substitutions. Now, instead of keeping a variable as-is, we can instead use an arbitrary term:

data Ren : Cx → Cx → Typeω where
  stop : Ren Γ Γ
  drop : Ren Γ Δ → Ren (Γ ʻ τ) Δ
  keep : Ren Γ Δ → Ren (Γ ʻ τ) (Δ ʻ τ)

data Sub : Cx → Cx → Typeω where
  stop : Sub Γ Γ
  _,_  : Tm Γ τ  → Sub Γ Δ → Sub Γ (Δ ʻ τ)
  drop : Sub Γ Δ → Sub (Γ ʻ τ) Δ
-- Superscript r for "renaming", s for "substitution"
⟦_⟧ʳ : Ren Γ Δ → Hom ⟦ Γ ⟧ᶜ ⟦ Δ ⟧ᶜ
⟦ stop ⟧ʳ = id
⟦ drop r ⟧ʳ = ⟦ r ⟧ʳ ∘ π₁
⟦ keep r ⟧ʳ = ⟦ r ⟧ʳ ⊗₁ id

⟦_⟧ˢ : Sub Γ Δ → Hom ⟦ Γ ⟧ᶜ ⟦ Δ ⟧ᶜ
⟦ stop    ⟧ˢ = id
⟦ x , s   ⟧ˢ = ⟨ ⟦ s ⟧ˢ , ⟦ x ⟧ᵉ ⟩
⟦ drop ρ  ⟧ˢ = ⟦ ρ ⟧ˢ ∘ π₁

One substitution which deserves special attention is the “terminating” substitution, which maps from an arbitrary to the empty context.

!ˢ : ∀ {Γ} → Sub Γ []
!Ë¢ {[]}    = Sub.stop
!ˢ {Γ ʻ x} = Sub.drop !ˢ

Now comes the fiddly part of dealing with syntax: the endless recursive functions for the action of renamings and substitutions on everything, and all the correctness lemmas that guarantee we’re doing the right thing.

_∘ʳ_    : Ren Γ Δ → Ren Δ Θ → Ren Γ Θ
ren-var : Ren Γ Δ → Δ ∋ τ → Γ ∋ τ
ren-tm  : Ren Γ Δ → Tm Δ τ → Tm Γ τ
sub-var : Sub Γ Δ → Δ ∋ τ → Tm Γ τ
sub-tm  : Sub Γ Δ → Tm Δ τ → Tm Γ τ

ren-var-correct
  : (ρ : Ren Γ Δ) (v : Δ ∋ τ) → ⟦ ren-var ρ v ⟧ⁿ ≡ ⟦ v ⟧ⁿ ∘ ⟦ ρ ⟧ʳ
sub-var-correct
  : (ρ : Sub Γ Δ) (t : Δ ∋ τ) → ⟦ sub-var ρ t ⟧ᵉ ≡ ⟦ t ⟧ⁿ ∘ ⟦ ρ ⟧ˢ

ren-tm-correct
  : (ρ : Ren Γ Δ) (v : Tm Δ τ) → ⟦ ren-tm ρ v ⟧ᵉ ≡ ⟦ v ⟧ᵉ ∘ ⟦ ρ ⟧ʳ
sub-tm-correct
  : (ρ : Sub Γ Δ) (t : Tm Δ τ) → ⟦ sub-tm ρ t ⟧ᵉ ≡ ⟦ t ⟧ᵉ ∘ ⟦ ρ ⟧ˢ
For the sake of the reader’s sanity, we’ve chosen to display only the type signatures, and all the implementations are in this <details> block.
stop   ∘ʳ ρ     = ρ
drop σ ∘ʳ ρ     = drop (σ ∘ʳ ρ)

keep σ ∘ʳ stop   = keep σ
keep σ ∘ʳ drop ρ = drop (σ ∘ʳ ρ)
keep σ ∘ʳ keep ρ = keep (σ ∘ʳ ρ)

ren-var stop     v       = v
ren-var (drop σ) v       = pop (ren-var σ v)
ren-var (keep σ) stop    = stop
ren-var (keep σ) (pop v) = pop (ren-var σ v)

ren-tm ρ (var x)    = var (ren-var ρ x)
ren-tm ρ (t , s)    = ren-tm ρ t , ren-tm ρ s
ren-tm ρ (`π₁ t)    = `π₁ (ren-tm ρ t)
ren-tm ρ (`π₂ t)    = `π₂ (ren-tm ρ t)
ren-tm ρ (fun x t)  = fun x (ren-tm ρ t)

sub-var stop v          = var v
sub-var (x , ρ) stop    = x
sub-var (x , ρ) (pop v) = sub-var ρ v
sub-var (drop ρ) v      = ren-tm (drop stop) (sub-var ρ v)

sub-tm ρ (var x)    = sub-var ρ x
sub-tm ρ (t , s)    = sub-tm ρ t , sub-tm ρ s
sub-tm ρ (`π₁ tm)   = `π₁ (sub-tm ρ tm)
sub-tm ρ (`π₂ tm)   = `π₂ (sub-tm ρ tm)
sub-tm ρ (fun x tm) = fun x (sub-tm ρ tm)

ren-var-correct stop v = sym (idr _)
ren-var-correct (drop ρ) v = ap (_∘ π₁) (ren-var-correct ρ v) ∙ sym (assoc _ _ _)
ren-var-correct (keep ρ) stop    = sym (π₂∘⟨⟩ ∙ idl _)
ren-var-correct (keep ρ) (pop v) =
  pushl (ren-var-correct ρ v) ∙ sym (pullr π₁∘⟨⟩)

ren-tm-correct ρ (var x)   = ren-var-correct ρ x
ren-tm-correct ρ (v , v₁)  = sym (⟨⟩∘ _ ∙ sym (ap₂ ⟨_,_⟩ (ren-tm-correct ρ v) (ren-tm-correct ρ v₁)))
ren-tm-correct ρ (`π₁ v)   = pushr (ren-tm-correct ρ v)
ren-tm-correct ρ (`π₂ v)   = pushr (ren-tm-correct ρ v)
ren-tm-correct ρ (fun x v) = pushr (ren-tm-correct ρ v)

sub-var-correct stop    t       = sym (idr _)
sub-var-correct (x , ρ) stop    = sym π₂∘⟨⟩
sub-var-correct (x , ρ) (pop t) = sym (pullr π₁∘⟨⟩ ∙ sym (sub-var-correct ρ t))
sub-var-correct (drop ρ) v      =
  ren-tm-correct (drop stop) (sub-var ρ v)
    ∙ extendl (idr _ ∙ sub-var-correct ρ v)

sub-tm-correct ρ (var x) = sub-var-correct ρ x
sub-tm-correct ρ (t , s) =
  sym (⟨⟩∘ _ ∙ ap₂ ⟨_,_⟩ (sym (sub-tm-correct ρ t)) (sym (sub-tm-correct ρ s)))
sub-tm-correct ρ (`π₁ t) = ap (π₁ ∘_) (sub-tm-correct ρ t) ∙ assoc _ _ _
sub-tm-correct ρ (`π₂ t) = ap (π₂ ∘_) (sub-tm-correct ρ t) ∙ assoc _ _ _
sub-tm-correct ρ (fun x t) = ap (x ∘_) (sub-tm-correct ρ t) ∙ assoc _ _ _

Formulae🔗

Finally, we have a syntactic description of the objects in that concern regular logic: they are built from the following grammar. Each fibre has a top element and conjunction. We single out the existential quantification along the latest variable

Moreover, we can define equality of terms in terms of existential quantification, though not along a variable, so it gets its own constructor; and finally, if you have a predicate on a type and a term then you can from

data Formula : Cx → Typeω where
  `⊤   : Formula Γ
  _`∧_ : Formula Γ → Formula Γ → Formula Γ

  `∃   : Formula (Γ ʻ τ) → Formula Γ

  _=ᵖ_ : Tm Γ τ → Tm Γ τ → Formula Γ

  pred : ℙ.Ob[ ⟦ τ ⟧ᵗ ] → Tm Γ τ → Formula Γ

The formulas over become objects over in the way that was implied in the definition of hyperdoctrine: in particular, the inclusion of semantic predicates is interpreted into substitution, and the equality predicate is interpreted by the formula

⟦_⟧ᵖ : Formula Γ → ℙ.Ob[ ⟦ Γ ⟧ᶜ ]
⟦ x `∧ y    ⟧ᵖ = ⟦ x ⟧ᵖ & ⟦ y ⟧ᵖ
⟦ `⊤        ⟧ᵖ = aye
⟦ `∃ x      ⟧ᵖ = exists π₁ ⟦ x ⟧ᵖ
⟦ pred p tm ⟧ᵖ = p [ ⟦ tm ⟧ᵉ ]
⟦ t =ᵖ s    ⟧ᵖ = exists ⟨ id , id ⟩ aye [ ⟨ ⟦ t ⟧ᵉ , ⟦ s ⟧ᵉ ⟩ ]

Once again we have the strictified presentation of substitution, though this time it’s short enough to present inline:

sub-prop : Sub Γ Δ → Formula Δ → Formula Γ
sub-prop ρ (φ `∧ ψ)   = sub-prop ρ φ `∧ sub-prop ρ ψ
sub-prop ρ (t =ᵖ s)   = sub-tm ρ t =ᵖ sub-tm ρ s
sub-prop ρ `⊤         = `⊤
sub-prop ρ (`∃ φ)     = `∃ (sub-prop (var stop , Sub.drop ρ) φ)
sub-prop ρ (pred x t) = pred x (sub-tm ρ t)

Unfortunately, we also have to prove that this is sent by to the semantic substitution:

sub-prop-correct
  : (ρ : Sub Γ Δ) (φ : Formula Δ)
  → ⟦ sub-prop ρ φ ⟧ᵖ ≡ ⟦ φ ⟧ᵖ [ ⟦ ρ ⟧ˢ ]

sub-prop-correct ρ (φ `∧ ψ) = sym $
  (⟦ φ ⟧ᵖ & ⟦ ψ ⟧ᵖ) [ ⟦ ρ ⟧ˢ ]           ≡⟨ subst-& _ _ _ ⟩≡
  ⟦ φ ⟧ᵖ [ ⟦ ρ ⟧ˢ ] & ⟦ ψ ⟧ᵖ [ ⟦ ρ ⟧ˢ ]  ≡˘⟨ ap₂ _&_ (sub-prop-correct ρ φ) (sub-prop-correct ρ ψ) ⟩≡˘
  ⟦ sub-prop ρ (φ `∧ ψ) ⟧ᵖ               ∎

sub-prop-correct ρ `⊤       = sym (subst-aye _)

sub-prop-correct {Γ = Γ} ρ (`∃ {Γ = Δ} {τ = τ} φ) =
  exists π₁ ⟦ sub-prop (var stop , drop ρ) φ ⟧ᵖ   ≡⟨ ap (exists _) (sub-prop-correct _ φ) ⟩≡
  exists π₁ (⟦ φ ⟧ᵖ [ ⟨ ⟦ ρ ⟧ˢ ∘ π₁ , π₂ ⟩ ])     ≡⟨ beck-chevalley rem₁ ⟩≡
  (exists π₁ ⟦ φ ⟧ᵖ) [ ⟦ ρ ⟧ˢ ]                   ∎
  where

The most interesting case is the one above, for existential quantification, where we use Beck-Chevalley applied to the pullback square

to commute

sub-prop-correct ρ (pred P t) =
  ap₂ _[_] refl (sub-tm-correct ρ t) ∙ sym (subst-∘ _ _)

sub-prop-correct ρ (s =ᵖ t) =
  exists ⟨ id , id ⟩ aye [ ⟨ ⟦ sub-tm ρ s ⟧ᵉ , ⟦ sub-tm ρ t ⟧ᵉ ⟩ ]
    ≡⟨ ap₂ _[_] refl (ap₂ ⟨_,_⟩ (sub-tm-correct ρ s) (sub-tm-correct ρ t)) ⟩≡
  exists ⟨ id , id ⟩ aye [ ⟨ ⟦ s ⟧ᵉ ∘ ⟦ ρ ⟧ˢ , ⟦ t ⟧ᵉ ∘ ⟦ ρ ⟧ˢ ⟩ ]
    ≡⟨ ap₂ _[_] refl (sym (⟨⟩∘ _)) ⟩≡
  exists ⟨ id , id ⟩ aye [ ⟨ ⟦ s ⟧ᵉ , ⟦ t ⟧ᵉ ⟩ ∘ ⟦ ρ ⟧ˢ ]
    ≡⟨ sym (subst-∘ _ _) ⟩≡
  (exists ⟨ id , id ⟩ aye [ ⟨ ⟦ s ⟧ᵉ , ⟦ t ⟧ᵉ ⟩ ]) [ ⟦ ρ ⟧ˢ ]
    ∎

A sequent calculus🔗

We now turn to the problem of proving that our interpretation above satisfies the rules of regular logic. We will start by defining the entailment relation between syntactic formulae which is equivalent to entails iff thinks that the interpretation of implies that of

infix 10 _⊨_

opaque
  _⊨_ : ∀ {Γ} → (φ ψ : Formula Γ) → Type ℓ'
  _⊨_ φ ψ = ⟦ φ ⟧ᵖ ≤ ⟦ ψ ⟧ᵖ

  from-entails : φ ⊨ ψ → ⟦ φ ⟧ᵖ ≤ ⟦ ψ ⟧ᵖ
  from-entails p = p

  instance
    H-Level-⊨ : ∀ {n} → H-Level (φ ⊨ ψ) (suc n)
    H-Level-⊨ = prop-instance (has-is-thin _ _)

Having defined entailment, we can now build a deductive calculus on top of by constructing combinators corresponding to each proof rule. Most of the proofs are formalised straightforwardly, so we will restrict ourselves to pointing out which rule is being formalised.

The cut rule corresponds to transitivity of semantic entailment:

  cut : φ ⊨ ψ
      → ψ ⊨ θ
      → φ ⊨ θ
  cut p q = ≤-trans p q

The substitution rule follows from our previous correctness lemmas:

  sub-entail
    : (ρ : Sub Γ Δ) {φ ψ : Formula Δ}
    → φ ⊨ ψ
    → sub-prop ρ φ ⊨ sub-prop ρ ψ
  sub-entail ρ {φ} {ψ} α =
    ⟦ sub-prop ρ φ ⟧ᵖ  P.=⟨ sub-prop-correct ρ φ ⟩P.=
    ⟦ φ ⟧ᵖ [ ⟦ ρ ⟧ˢ ]  P.≤⟨ subst-≤ ⟦ ρ ⟧ˢ α ⟩P.≤
    ⟦ ψ ⟧ᵖ [ ⟦ ρ ⟧ˢ ]  P.=˘⟨ sub-prop-correct ρ ψ ⟩P.=˘
    ⟦ sub-prop ρ ψ ⟧ᵖ  P.≤∎

The three rules for conjunction follow at once from the definition of fibrewise meets:

  `∧-intro
    : Φ ⊨ φ
    → Φ ⊨ ψ
    → Φ ⊨ φ `∧ ψ
  `∧-intro α β = &-univ α β

  `∧-elimₗ
    : Φ ⊨ φ `∧ ψ
    → Φ ⊨ φ
  `∧-elimₗ α = ≤-trans α (fibrewise-meet.π₁ _ _)

  `∧-elimᵣ
    : Φ ⊨ φ `∧ ψ
    → Φ ⊨ ψ
  `∧-elimᵣ α = ≤-trans α (fibrewise-meet.π₂ _ _)

The rules for existentials are slightly fiddly, but they follow from the universal properties of co/cartesian lifts and Frobenius reciprocity:

  `∃-elim
    : Φ         ⊨ `∃ φ
    → wk Φ `∧ φ ⊨ wk ψ
    → Φ         ⊨ ψ

  `∃-intro
    : ∀ {Γ} {Φ ψ} {t : Tm Γ τ}
    → Φ ⊨ sub-prop (t , stop) ψ
    → Φ ⊨ `∃ ψ
The proofs here have a bit more “unfortunately, proof assistants” than the others, so we’ll keep them in <details> too.
  `∃-elim {Φ = Φ} {φ = φ} {ψ = ψ} Φ⊢exists φ⊢ψ =
    ⟦ Φ ⟧ᵖ                              P.≤⟨ &-univ Φ⊢exists P.≤-refl ⟩P.≤
    ⟦ `∃ φ ⟧ᵖ & ⟦ Φ ⟧ᵖ                  P.=⟨ frobenius π₁ ⟩P.=
    exists π₁ (⟦ φ ⟧ᵖ & ⟦ Φ ⟧ᵖ [ π₁ ])  P.=⟨ ap (exists π₁) &-comm ⟩P.=
    exists π₁ (⟦ Φ ⟧ᵖ [ π₁ ] & ⟦ φ ⟧ᵖ)  P.≤⟨ φ⊢ψ' ⟩P.≤
    ⟦ ψ ⟧ᵖ                              P.≤∎
    where
    φ⊢ψ' : exists π₁ (⟦ Φ ⟧ᵖ [ π₁ ] & ⟦ φ ⟧ᵖ) ≤ ⟦ ψ ⟧ᵖ
    φ⊢ψ' = ≤-exists π₁
      (transport (ap₂ _≤_
        (ap₂ _&_ (sub-prop-correct (drop stop) Φ ∙ ap₂ _[_] refl (idl _)) refl)
        (sub-prop-correct (drop stop) ψ ∙ ap₂ _[_] refl (idl _)))
        φ⊢ψ)

  `∃-intro {Γ = Γ} {Φ = Φ} {ψ = ψ} {t = t} α = hom[ cancell π₁∘⟨⟩ ] $
         cocartesian.has-lift.lifting π₁ ⟦ ψ ⟧ᵖ
    ℙ.∘' cartesian.has-lift.lifting ⟨ id , ⟦ t ⟧ᵉ ⟩ ⟦ ψ ⟧ᵖ
    ℙ.∘' p
    where
    p : ⟦ Φ ⟧ᵖ ≤ (⟦ ψ ⟧ᵖ [ ⟨ id , ⟦ t ⟧ᵉ ⟩ ])
    p =
      ⟦ Φ ⟧ᵖ                               P.≤⟨ α ⟩P.≤
      ⟦ sub-prop (t , stop) ψ ⟧ᵖ           P.=⟨ sub-prop-correct (t , stop) ψ ⟩P.=
      (⟦ ψ ⟧ᵖ [ ⟨ id , ⟦ t ⟧ᵉ ⟩ ])         P.≤∎

Local rewriting🔗

Since we’re working with a very strict presyntax of formulas, there are many distinct syntactic-formulae with identical semantics. This strictness affords us good computational properties at the cost of mathematical properties: our syntax isn’t initial in any sense. Moreover, since the details of the entailment relation are kept opaque to encourage use of the combinators above, it’s not immediate to the outside world that it respects semantic equality.

We’ll remedy this in the following way: we can define an inductive relation which includes semantic equality but also includes combinators for “zooming in” part of a formula, ignoring the parts that don’t change, so that we can deploy semantic equality at precisely the place where it matters. Then, we provide combinators witnessing that the entailment respects

data _≈ᵗ_ : Tm Γ τ → Tm Γ τ → Typeω where
  sem : ⟦ t ⟧ᵉ ≡ ⟦ s ⟧ᵉ → t ≈ᵗ s
  _,_ : t ≈ᵗ t₁ → s ≈ᵗ s₁ → (t , s) ≈ᵗ (t₁ , s₁)
  `π₁ : t ≈ᵗ t₁ → `π₁ t ≈ᵗ `π₁ t₁
  `π₂ : t ≈ᵗ t₁ → `π₂ t ≈ᵗ `π₂ t₁
  fun : ∀ {h : Hom ⟦ τ ⟧ᵗ ⟦ σ ⟧ᵗ} {t t₁ : Tm Γ τ}
      → t ≈ᵗ t₁
      → fun {τ = τ} {σ} h t ≈ᵗ fun h t₁

data _≈ᵖ_ : Formula Γ → Formula Γ → Typeω where
  sem  : ⟦ φ ⟧ᵖ ≡ ⟦ ψ ⟧ᵖ → φ ≈ᵖ ψ
  _`∧_ : φ ≈ᵖ φ' → ψ ≈ᵖ ψ' → (φ `∧ ψ) ≈ᵖ (φ' `∧ ψ')
  `∃   : φ ≈ᵖ ψ → `∃ φ ≈ᵖ `∃ ψ
  pred : ∀ {p} → t ≈ᵗ t₁ → pred p t ≈ᵖ pred p t₁
  _=ᵖ_ : ∀ {Γ τ} {t t₁ s s₁ : Tm Γ τ}
        → t ≈ᵗ t₁ → s ≈ᵗ s₁ → (t =ᵖ s) ≈ᵖ (t₁ =ᵖ s₁)

The data types above are simply presentations of semantic equality: iff. However, once again contains redundancy which is mathematically irrelevant but handy when working in a proof assistant.

to-semᵗ : t ≈ᵗ t₁ → ⟦ t ⟧ᵉ ≡ ⟦ t₁ ⟧ᵉ
to-semᵗ (sem p) = p
to-semᵗ (p , q) = ap₂ ⟨_,_⟩ (to-semᵗ p) (to-semᵗ q)
to-semᵗ (`π₁ p) = ap₂ _∘_ refl (to-semᵗ p)
to-semᵗ (`π₂ p) = ap₂ _∘_ refl (to-semᵗ p)
to-semᵗ (fun p) = ap₂ _∘_ refl (to-semᵗ p)

to-semᵖ : φ ≈ᵖ ψ → ⟦ φ ⟧ᵖ ≡ ⟦ ψ ⟧ᵖ
to-semᵖ (sem p)  = p
to-semᵖ (p `∧ q) = ap₂ _&_ (to-semᵖ p) (to-semᵖ q)
to-semᵖ (`∃ p)   = ap (exists π₁) (to-semᵖ p)
to-semᵖ (pred p) = ap₂ _[_] refl (to-semᵗ p)
to-semᵖ (_=ᵖ_ {Γ = Γ} {τ = τ} p q) = ap₂ equ (to-semᵗ p) (to-semᵗ q) where
  equ : ∀ (h h' : Hom ⟦ Γ ⟧ᶜ ⟦ τ ⟧ᵗ) → ℙ.Ob[ ⟦ Γ ⟧ᶜ ]
  equ h h' = exists ⟨ id , id ⟩ aye [ ⟨ h , h' ⟩ ]

We can then provide combinators for turning into or as appropriate.

opaque
  unfolding _⊨_

  ≈→entails : φ ≈ᵖ ψ → entails φ ψ
  ≈→entails p = transport (ap₂ _≤_ refl (to-semᵖ p)) P.≤-refl

  ≈→entails⁻ : φ ≈ᵖ ψ → entails ψ φ
  ≈→entails⁻ p = transport (ap₂ _≤_ refl (sym (to-semᵖ p))) P.≤-refl