open import Cat.Diagram.Limit.Finite
open import Cat.Displayed.Doctrine
open import Cat.Diagram.Pullback
open import Cat.Diagram.Terminal
open import Cat.Diagram.Product
open import Cat.Displayed.Base
open import Cat.Prelude hiding (_Κ»_)

import Cat.Displayed.Reasoning as Disp
import Cat.Reasoning as Cat

import Order.Reasoning

module Cat.Displayed.Doctrine.Logic

  {o β o' β'} {B : Precategory o β}
(fc : Finitely-complete B)
(P : Regular-hyperdoctrine B o' β')
where

open Regular-hyperdoctrine P
open Finitely-complete fc hiding (_ββ_)
open Binary-products B products
open Displayed β
open Cat B

private module P {x} = Order.Reasoning (β€-Poset {x})


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

infixl 15 _Κ»_
infixl 17 _β§_ _Γ_

private variable
Ξ Ξ Ξ : Cx
Ο Ο   : Ty


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  open is-pullback remβ : is-pullback B (Οβ {b = β¦ Ο β§α΅}) β¦ Ο β§Λ’ β¨ β¦ Ο β§Λ’ β Οβ , Οβ β© Οβ remβ .square = sym Οβββ¨β© remβ .universal {pβ' = pβ'} {pβ'} prf = β¨ pβ' , Οβ β pβ' β© remβ .pββuniversal = Οβββ¨β© remβ .pββuniversal {p = p} = β¨β©β _ Β·Β· apβ β¨_,_β© (pullr Οβββ¨β© β p) Οβββ¨β© Β·Β· sym (β¨β©β _) β eliml (sym (β¨β©-unique id (idr _) (idr _))) remβ .unique q r = β¨β©-unique _ q (sym (ap (Οβ β_) (sym r) β pulll Οβββ¨β©))  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 β§α΅ β© ]) [ β¦ Ο β§Λ’ ] β  sub-prop-β : β {Ξ¦} (Ο : Sub Ξ Ξ) (Ο : Sub Ξ Ξ¦) (Ο : Formula Ξ¦) β β¦ sub-prop Ο (sub-prop Ο Ο) β§α΅ β‘ β¦ Ο β§α΅ [ β¦ Ο β§Λ’ β β¦ Ο β§Λ’ ] sub-prop-β Ο Ο Ο = sub-prop-correct Ο (sub-prop Ο Ο) Β·Β· ap (_[ β¦ Ο β§Λ’ ]) (sub-prop-correct Ο Ο) Β·Β· subst-β _ _ private variable Ξ¦ Ξ¨ Ο Ο ΞΈ Ο' Ο' : Formula Ξ t tβ s sβ : Tm Ξ Ο wk : β {Ξ} (Ο : Formula Ξ) {Ο : Ty} β Formula (Ξ Κ» Ο) wk Ο = sub-prop (drop stop) Ο  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 _ _)  private entails : β {Ξ} β (Ο Ο : Formula Ξ) β Type β' entails = _β¨_  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. opaque unfolding _β¨_  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.β€β

  =-refl : entails Ο (t =α΅ t)
=-refl {t = t} =
cartesian.has-lift.universal _ _ _ $hom[ pulll (β¨β©β _ β apβ β¨_,_β© (idl _) (idl _)) ]$
cocartesian.has-lift.lifting β¨ id , id β© aye
β.β' cartesian.has-lift.lifting _ _
β.β' subst-! β¦ t β§α΅


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

_β’β¨_β©_ : β Ο β Ο β¨ Ο β Ο β¨ ΞΈ β Ο β¨ ΞΈ
_β’β¨_β©_ _ p q = cut p q

_ββ¨_β©_ : β Ο β Ο βα΅ Ο β Ο β¨ ΞΈ β Ο β¨ ΞΈ
_ββ¨_β©_ _ p q = cut (ββentails p) q

_βΛβ¨_β©_ : β Ο β Ο βα΅ Ο β Ο β¨ ΞΈ β Ο β¨ ΞΈ
_βΛβ¨_β©_ _ p q = cut (ββentailsβ» p) q

opaque
unfolding _β¨_

_β’β : (Ο : Formula Ξ) β Ο β¨ Ο
_β’β Ο = P.β€-refl {_} {β¦ Ο β§α΅}

`