Implements Chu construction, defines setoids, constructs the function space on setoids. https://golem.ph.utexas.edu/category/2018/05/linear_logic_for_constructive.html

Synthesis.agda

{-# OPTIONS --prop --without-K --safe #-}

module Synthesis where

-- Utilities
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.Nat using (zero; suc; _+_) renaming (Nat to ℕ)

infixl 8 _∧_ _×_
infixl 7 _∨_ _⊎_

data ⊥ : Prop where
record ⊤ : Prop where
    constructor ⋆

record _∧_ {ℓ ℓ'} (P : Prop ℓ) (Q : Prop ℓ') : Prop (ℓ ⊔ ℓ') where
    constructor [_,_]
    field
        π₁ : P
        π₂ : Q

record _×_ {ℓ ℓ'} (P : Set ℓ) (Q : Set ℓ') : Set (ℓ ⊔ ℓ') where
    constructor _,_
    field
        proj₁ : P
        proj₂ : Q

open _∧_
open _×_

data _∨_ {ℓ ℓ'} (P : Prop ℓ) (Q : Prop ℓ') : Prop (ℓ ⊔ ℓ') where
    ι₁ : P -> P ∨ Q
    ι₂ : Q -> P ∨ Q

data _⊎_ {ℓ ℓ'} (P : Set ℓ) (Q : Set ℓ') : Set (ℓ ⊔ ℓ') where
    inj₁ : P -> P ⊎ Q
    inj₂ : Q -> P ⊎ Q

data Bool {ℓ} : Set ℓ where
    true : Bool
    false : Bool

data ∃ {ℓ ℓ'} (A : Set ℓ) (P : A -> Prop ℓ') : Prop (ℓ ⊔ ℓ') where
    ⟨_,_⟩ : (a : A) -> P a -> ∃ A P

syntax ∃ A (\ a -> P) = ∃⟨ a ∈ A ⟩ P

data ∥_∥ {ℓ} (A : Set ℓ) : Prop ℓ where
    tt : A -> ∥ A ∥


-- We start by defining propositions.
record PProp ℓ ℓ' : Set (lsuc (ℓ ⊔ ℓ')) where
    field
        Pos : Prop ℓ  -- Thesis
        Neg : Prop ℓ' -- Antithesis
        Chu : Pos -> Neg -> ⊥  -- Synthesis

open PProp

True : PProp lzero lzero
Pos True = ⊤
Neg True = ⊥
Chu True _ ()

False : PProp lzero lzero
Pos False = ⊥
Neg False = ⊤
Chu False () _

tight : ∀ {ℓ} (A : Prop ℓ) -> PProp ℓ ℓ
Pos (tight A) = A
Neg (tight {ℓ} A) = A -> ⊥
Chu (tight A) a ¬a = ¬a a

infixr 20 ¬_
¬_ : ∀ {ℓ ℓ'} -> PProp ℓ ℓ' -> PProp ℓ' ℓ
Pos (¬ P) = Neg P
Neg (¬ P) = Pos P
Chu (¬ P) p n = Chu P n p

-- We get double negation elimination for free!
_ : ∀ {ℓ ℓ'} {P : PProp ℓ ℓ'} -> P ≡ ¬ ¬ P
_ = refl

infixl 10 _&_ _⊕_ _≪⊗_ _⊗≫_ _⊗_
infixr 9 _≪-o_ _-o≫_ _⟶_
_&_ : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} -> PProp ℓ₁ ℓ₂ -> PProp ℓ₃ ℓ₄ -> PProp (ℓ₁ ⊔ ℓ₃) (ℓ₂ ⊔ ℓ₄)
Pos (A & B) = Pos A ∧ Pos B
Neg (A & B) = Neg A ∨ Neg B
Chu (A & B) [ a⁺ , b⁺ ] (ι₁ a⁻) = Chu A a⁺ a⁻
Chu (A & B) [ a⁺ , b⁺ ] (ι₂ b⁻) = Chu B b⁺ b⁻

_⊕_ : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} -> PProp ℓ₁ ℓ₂ -> PProp ℓ₃ ℓ₄ -> PProp (ℓ₁ ⊔ ℓ₃) (ℓ₂ ⊔ ℓ₄)
Pos (A ⊕ B) = Pos A ∨ Pos B
Neg (A ⊕ B) = Neg A ∧ Neg B
Chu (A ⊕ B) (ι₁ a⁺) [ a⁻ , b⁻ ] = Chu A a⁺ a⁻
Chu (A ⊕ B) (ι₂ b⁺) [ a⁻ , b⁻ ] = Chu B b⁺ b⁻

-- These are different, but we use Prop, so..
_≪⊗_ : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} -> PProp ℓ₁ ℓ₂ -> PProp ℓ₃ ℓ₄ -> PProp (ℓ₁ ⊔ ℓ₃) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄)
Pos (A ≪⊗ B) = Pos A ∧ Pos B
Neg (A ≪⊗ B) = (Pos A -> Neg B) ∧ (Pos B -> Neg A)
Chu (A ≪⊗ B) [ a⁺ , b⁺ ] [ f , g ] = Chu A a⁺ (g b⁺)

_⊗≫_ : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} -> PProp ℓ₁ ℓ₂ -> PProp ℓ₃ ℓ₄ -> PProp (ℓ₁ ⊔ ℓ₃) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄)
Pos (A ⊗≫ B) = Pos A ∧ Pos B
Neg (A ⊗≫ B) = (Pos A -> Neg B) ∧ (Pos B -> Neg A)
Chu (A ⊗≫ B) [ a⁺ , b⁺ ] [ f , g ] = Chu B b⁺ (f a⁺)

-- .. they are the same, judgementally (!)
_ : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} {A : PProp ℓ₁ ℓ₂} {B : PProp ℓ₃ ℓ₄} -> A ≪⊗ B ≡ A ⊗≫ B
_ = refl

-- So we are justified to just commit to one of them.
_⊗_ = _⊗≫_
{-# DISPLAY _⊗≫_ = _⊗_ #-}

_≪-o_ : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} -> PProp ℓ₁ ℓ₂ -> PProp ℓ₃ ℓ₄ -> PProp (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) (ℓ₁ ⊔ ℓ₄)
Pos (A ≪-o B) = (Pos A -> Pos B) ∧ (Neg B -> Neg A)
Neg (A ≪-o B) = Pos A ∧ Neg B
Chu (A ≪-o B) [ imply , contrapose ] [ PosA , NegB ] = Chu A PosA (contrapose NegB)

_-o≫_ : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} -> PProp ℓ₁ ℓ₂ -> PProp ℓ₃ ℓ₄ -> PProp (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) (ℓ₁ ⊔ ℓ₄)
Pos (A -o≫ B) = (Pos A -> Pos B) ∧ (Neg B -> Neg A)
Neg (A -o≫ B) = Pos A ∧ Neg B
Chu (A -o≫ B) [ imply , contrapose ] [ PosA , NegB ] = Chu B (imply PosA) NegB

_ : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} {A : PProp ℓ₁ ℓ₂} {B : PProp ℓ₃ ℓ₄} -> A ≪-o B ≡ A -o≫ B
_ = refl

_⟶_ = _-o≫_
{-# DISPLAY _-o≫_ = _⟶_ #-}

Forall : ∀ {ℓ ℓ₁ ℓ₂} (A : Set ℓ) (P : A -> PProp ℓ₁ ℓ₂) -> PProp (ℓ ⊔ ℓ₁) (ℓ ⊔ ℓ₂)
Pos (Forall A P) = ∀(a : A) -> Pos (P a)
Neg (Forall A P) = ∃⟨ a ∈ A ⟩ Neg (P a)
Chu (Forall A P) func ⟨ a , witness ⟩ = Chu (P a) (func a) witness
syntax Forall A (\ a -> P) = ∀⟦ a ∈ A ⟧ P
infixr 6 Forall

Exists : ∀ {ℓ ℓ₁ ℓ₂} (A : Set ℓ) (P : A -> PProp ℓ₁ ℓ₂) -> PProp (ℓ ⊔ ℓ₁) (ℓ ⊔ ℓ₂)
Exists A P = ¬ (Forall A \ x -> ¬ (P x))
syntax Exists A (\ a -> P) = ∃⟦ a ∈ A ⟧ P
infixr 6 Exists

-- We have developed a decent set of connectives. Now for the connections between them.
Identity : ∀ {ℓ₁ ℓ₂} (P : PProp ℓ₁ ℓ₂)
    -> Pos (P ⟶ P)
Identity P = [ (\ z -> z) , (\ z -> z) ]

ModusPonens : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} (P : PProp ℓ₁ ℓ₂) (Q : PProp ℓ₃ ℓ₄)
    -> Pos P -> Pos (P ⟶ Q) -> Pos Q
ModusPonens _ _ p [ impl , _ ] = impl p

Lift : ∀ {ℓ ℓ₁ ℓ₂ ℓ₃ ℓ₄} {A : Set ℓ} (P : A -> PProp ℓ₁ ℓ₂) (Q : A -> PProp ℓ₃ ℓ₄)
    -> Pos ((∀⟦ a ∈ A ⟧ P a ⟶ Q a) ⟶ (∀⟦ a ∈ A ⟧ P a) ⟶ (∀⟦ a ∈ A ⟧ Q a))
Lift P Q .π₁ f .π₁ g a = f a .π₁ (g a)
Lift P Q .π₁ f .π₂ ⟨ a , nq ⟩ = ⟨ a , f a .π₂ nq ⟩
Lift P Q .π₂ [ f , ⟨ a , nq ⟩ ] = ⟨ a , [ f a , nq ] ⟩

Uncurry : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ ℓ₆} (P : PProp ℓ₁ ℓ₂) (Q : PProp ℓ₃ ℓ₄) (R : PProp ℓ₅ ℓ₆)
    -> Pos ((P & Q ⟶ R) ⟶ (P ⟶ Q ⟶ R))
Uncurry P Q R .π₁ [ P∧Q⟶R , ¬R⟶¬P∨¬Q ] .π₁ p .π₁ q = P∧Q⟶R [ p , q ]
Uncurry P Q R .π₁ [ P∧Q⟶R , ¬R⟶¬P∨¬Q ] .π₁ p .π₂ nr with ¬R⟶¬P∨¬Q nr
... | ι₂ nq = nq
... | ι₁ np with Chu P p np
... | ()  -- This essentially relies on ⊥ being elementless, i.e. the Chu algebra being semi-cartesian
Uncurry P Q R .π₁ [ P∧Q⟶R , ¬R⟶¬P∨¬Q ] .π₂ [ q , nr ] with ¬R⟶¬P∨¬Q nr
... | ι₁ np = np
... | ι₂ nq with Chu Q q nq
... | ()
Uncurry P Q R .π₂ [ p , [ q , nr ] ] = [ [ p , q ] , nr ]

-- We start to develop setoids

Binary : ∀ {ℓ ℓ₁ ℓ₂} -> Set ℓ -> Set (ℓ ⊔ lsuc (ℓ₁ ⊔ ℓ₂))
Binary {ℓ} {ℓ₁} {ℓ₂} A = A -> A -> PProp ℓ₁ ℓ₂

Reflexivity : ∀ {ℓ ℓ₁ ℓ₂} {A : Set ℓ} -> Binary {ℓ} {ℓ₁} {ℓ₂} A -> PProp (ℓ ⊔ ℓ₁) (ℓ ⊔ ℓ₂)
Reflexivity {A = A} _≈_ = ∀⟦ a ∈ A ⟧ (a ≈ a)

Symmetry : ∀ {ℓ ℓ₁ ℓ₂} {A : Set ℓ} -> Binary {ℓ} {ℓ₁} {ℓ₂} A -> PProp (ℓ ⊔ ℓ₁ ⊔ ℓ₂) (ℓ ⊔ ℓ₁ ⊔ ℓ₂)
Symmetry {A = A} _≈_ = ∀⟦ a ∈ A ⟧ ∀⟦ b ∈ A ⟧ (a ≈ b ⟶ b ≈ a)

Transitivity : ∀ {ℓ ℓ₁ ℓ₂} {A : Set ℓ} -> Binary {ℓ} {ℓ₁} {ℓ₂} A -> PProp (ℓ ⊔ ℓ₁ ⊔ ℓ₂) (ℓ ⊔ ℓ₁ ⊔ ℓ₂)
Transitivity {A = A} _≈_
    = ∀⟦ a ∈ A ⟧ ∀⟦ b ∈ A ⟧ ∀⟦ c ∈ A ⟧ (a ≈ b & b ≈ c ⟶ a ≈ c)

IsEquivalence : ∀ {ℓ ℓ₁ ℓ₂} {A : Set ℓ} -> Binary {ℓ} {ℓ₁} {ℓ₂} A -> PProp (ℓ ⊔ ℓ₁ ⊔ ℓ₂) (ℓ ⊔ ℓ₁ ⊔ ℓ₂)
IsEquivalence R = Reflexivity R ⊗ Symmetry R ⊗ Transitivity R

record PSet ℓ ℓ₁ ℓ₂ : Set (lsuc (ℓ ⊔ ℓ₁ ⊔ ℓ₂)) where
    field
        Carrier : Set ℓ
        _≈_ : Binary {ℓ} {ℓ₁} {ℓ₂} Carrier
        symm : Pos (Symmetry _≈_)
        trans : Pos (Transitivity _≈_)
    -- Everything comes dually, example:
    _ : Pos (Transitivity _≈_) ≡ ∀ (a b c : Carrier) ->  -- Transitivity at the surface
        (Pos (a ≈ b) ∧ Pos (b ≈ c) -> Pos (a ≈ c)) ∧  -- Transitive
        (Neg (a ≈ c) -> Neg (a ≈ b) ∨ Neg (b ≈ c))    -- Comparison
    _ = refl

    -- If something is in the domain of _≈_, then it is reflexive
    reflDom : ∀ {a b : Carrier} -> Pos (a ≈ b ⟶ a ≈ a)
    reflDom {a} {b} .π₁ r = trans a b a .π₁
        [ r ,
        symm _ _ .π₁ r ]
    reflDom {a} {b} .π₂ r with trans a b a .π₂ r
    ... | ι₁ x = x
    ... | ι₂ x = symm _ _ .π₂ x

open PSet renaming (_≈_ to eq)
_≈_ : ∀ {ℓ ℓ₁ ℓ₂} {P : PSet ℓ ℓ₁ ℓ₂} -> (x y : Carrier P) -> PProp ℓ₁ ℓ₂
_≈_ {P = P} x y = PSet._≈_ P x y

record ⟦_⟧ {ℓ ℓ₁ ℓ₂} (S : PSet ℓ ℓ₁ ℓ₂) : Set (ℓ ⊔ ℓ₁ ⊔ ℓ₂) where
    field
        element : Carrier S
        reflexive : Pos (eq S element element)

data Empty {ℓ} : Set ℓ where

∅ : ∀ {ℓ ℓ₁ ℓ₂} -> PSet ℓ ℓ₁ ℓ₂
Carrier ∅ = Empty
eq ∅ ()
symm ∅ ()
trans ∅ ()

∅-is-empty : ∀ {ℓ ℓ₁ ℓ₂} -> ⟦ ∅ {ℓ} {ℓ₁} {ℓ₂} ⟧ -> ⊥
∅-is-empty ()

𝟚 : PSet lzero lzero lzero
Carrier 𝟚 = Bool
eq 𝟚 true true = True
eq 𝟚 false false = True
eq 𝟚 _ _ = False
symm 𝟚 true true = Identity True
symm 𝟚 false false = Identity True
symm 𝟚 true false = Identity False
symm 𝟚 false true = Identity False
trans 𝟚 true  true  true  = [ (\_ -> _) , (\())        ]
trans 𝟚 true  true  false = [ (\())     , (\_ -> ι₂ _) ]
trans 𝟚 true  false true  = [ (\())     , (\())        ]
trans 𝟚 true  false false = [ (\())     , (\_ -> ι₁ _) ]
trans 𝟚 false true  true  = [ (\())     , (\_ -> ι₁ _) ]
trans 𝟚 false true  false = [ (\())     , (\())        ]
trans 𝟚 false false true  = [ (\())     , (\_ -> ι₂ _) ]
trans 𝟚 false false false = [ (\_ -> _) , (\())        ]

-- PER function space
_⇒_ : ∀ {ℓ ℓ₁ ℓ₂ ℓ' ℓ₁' ℓ₂'} -> PSet ℓ ℓ₁ ℓ₂ -> PSet ℓ' ℓ₁' ℓ₂' -> PSet (ℓ ⊔ ℓ') (ℓ ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₁' ⊔ ℓ₂') (ℓ ⊔ ℓ₁ ⊔ ℓ₂')
Carrier (P ⇒ Q) = Carrier P -> Carrier Q
eq (P ⇒ Q) x y =
    ∀⟦ a ∈ Carrier P ⟧
    ∀⟦ b ∈ Carrier P ⟧
    (eq P a b ⟶ eq Q (x a) (y b))
symm (P ⇒ Q) x y = [ pos , neg ]
    where  -- We can definitely make some combinators to make this better
        pos : Pos (eq (P ⇒ Q) x y) -> Pos (eq (P ⇒ Q) y x)
        pos f _ _ .π₁ p =
            symm Q _ _ .π₁
                (f _ _ .π₁
                    (symm P _ _ .π₁ p))
        pos f _ _ .π₂ n =
            symm P _ _ .π₂
                (f _ _ .π₂
                    (symm Q _ _ .π₂ n))
        neg : Neg (eq (P ⇒ Q) y x) -> Neg (eq (P ⇒ Q) x y)
        neg ⟨ a , ⟨ b , [ eqP , neqQ ] ⟩ ⟩ =
            ⟨ b , ⟨ a , [ symm P _ _ .π₁ eqP , symm Q _ _ .π₂ neqQ ] ⟩ ⟩
trans (P ⇒ Q) a b c = [ pos , neg ]
    where
        {-
          a'  --a->   α
        ? ∥    ==>    ≀ f
          a'  --b->   β
          ∥    ==>    ≀ g
          c'  --c->   γ
        -}
        pos : Pos (eq (P ⇒ Q) a b) ∧ Pos (eq (P ⇒ Q) b c) -> Pos (eq (P ⇒ Q) a c)
        pos [ f , g ] a' c' .π₁ a'≈c' = trans Q _ (b a') _ .π₁ [
                f _ _ .π₁ (reflDom P .π₁ a'≈c') ,
                g _ _ .π₁ a'≈c'
            ]
        pos [ f , g ] a' c' .π₂ aa'#cc' with trans Q _ (b a') _ .π₂ aa'#cc'
        ... | ι₁ aa'#ba' = reflDom P .π₂ (f _ _ .π₂ aa'#ba')
        ... | ι₂ ba'#cc' = g _ _ .π₂ ba'#cc'
        neg : Neg (eq (P ⇒ Q) a c) -> Neg (eq (P ⇒ Q) a b) ∨ Neg (eq (P ⇒ Q) b c)
        neg ⟨ a' , ⟨ c' , [ a'≈c' , aa'#cc' ] ⟩ ⟩ with trans Q _ (b a') _ .π₂ aa'#cc'
        ... | ι₁ aa'#ba' = ι₁ ⟨ a' , ⟨ a' , [ reflDom P .π₁ a'≈c' , aa'#ba' ] ⟩ ⟩
        ... | ι₂ ba'#cc' = ι₂ ⟨ a' , ⟨ c' , [ a'≈c' , ba'#cc' ] ⟩ ⟩

This is more appropriately called bang.

https://github.com/zaklogician/linear-constructive/blob/master/src/Linear.agda
A relevant developemt