Skip to content

Instantly share code, notes, and snippets.

@TOTBWF

TOTBWF/CartesianNbE.agda

Last active February 5, 2022 23:24
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save TOTBWF/9faf5e00f9e85b5d569a5f34a7f55fb3 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save TOTBWF/9faf5e00f9e85b5d569a5f34a7f55fb3 to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. TOTBWF revised this gist Feb 3, 2022. 1 changed file with 2 additions and 1 deletion.
    3 changes: 2 additions & 1 deletion CartesianNbE.agda
    View file
    Original file line number Diff line number Diff line change
    @@ -66,7 +66,8 @@ embed _ _ [ f ↑] = f
    -- The way we handle neutral terms is somewhat subtle;
    -- For normal NbE we would keep a stack of eliminators
    -- blocked on a neutral. However, our neutral forms
    -- here are morphisms, so we can
    -- here are morphisms, so we can just compose onto it
    -- in do_fst/do_snd.

    data Sem (A : Type) : Type β†’ Set (o βŠ” β„“) where
    pair : βˆ€ {B C} β†’ Sem A B β†’ Sem A C β†’ Sem A (B Γ—β€² C)
  2. TOTBWF revised this gist Feb 3, 2022. 1 changed file with 162 additions and 191 deletions.
    353 changes: 162 additions & 191 deletions CartesianNbE.agda
    View file
    Original file line number Diff line number Diff line change
    @@ -1,198 +1,169 @@
    {-# OPTIONS --without-K --safe #-}
    module CartesianNbE where

    open import Categories.Category.Core
    open import Categories.Category.Cartesian

    module Categories.Tactic.Cartesian.Solver {o β„“ e} {π’ž : Category o β„“ e} (cartesian : Cartesian π’ž) where

    open import Level

    open import Categories.Category
    open import Categories.Category.Cartesian
    open import Categories.Category.BinaryProducts
    open import Categories.Object.Terminal

    open import Function using (_⟨_⟩_)

    import Data.Unit as Unit
    open import Data.Bool as Bool using (Bool; _∨_; if_then_else_)
    open import Data.Maybe as Maybe using (Maybe; just; nothing; maybe; fromMaybe)
    open import Data.List as List using (List; _∷_; [])
    open import Data.Product as Product using (Ξ£ ;_,_)

    open import Agda.Builtin.Reflection
    open import Reflection.Argument
    open import Reflection.Term using (getName; _β‹―βŸ…βˆ·βŸ†_)
    open import Reflection.TypeChecking.Monad.Syntax

    module _ {o β„“ e} {π’ž : Category o β„“ e} (cartesian : Cartesian π’ž) where

    open Category π’ž
    open Cartesian cartesian
    open BinaryProducts products
    open Terminal terminal
    open HomReasoning
    open Equiv


    --------------------------------------------------------------------------------
    -- Syntax

    data Ctx : Set o where
    βˆ™ : Ctx
    [_] : Obj β†’ Ctx
    _++_ : Ctx β†’ Ctx β†’ Ctx

    ctx : Ctx β†’ Obj
    ctx βˆ™ = ⊀
    ctx [ X ] = X
    ctx (Ξ“ ++ Ξ”) = ctx Ξ“ Γ— ctx Ξ”

    data Syn : Ctx β†’ Ctx β†’ Set (o βŠ” β„“) where
    idβ€² : βˆ€ {A} β†’ Syn A A
    _βˆ˜β€²_ : βˆ€ {A B C} β†’ Syn B C β†’ Syn A B β†’ Syn A C
    π₁′ : βˆ€ {A B} β†’ Syn (A ++ B) A
    Ο€β‚‚β€² : βˆ€ {A B} β†’ Syn (A ++ B) B
    ⟨_,_βŸ©β€² : βˆ€ {A B C} β†’ Syn C A β†’ Syn C B β†’ Syn C (A ++ B)
    !β€² : βˆ€ {A} β†’ Syn A βˆ™
    [_↑] : βˆ€ {A B} β†’ ctx A β‡’ ctx B β†’ Syn A B

    -- Read a piece of syntax back into a morphism.
    [_↓] : βˆ€ {A B} β†’ Syn A B β†’ ctx A β‡’ ctx B
    [ idβ€² ↓] = id
    [ f βˆ˜β€² g ↓] = [ f ↓] ∘ [ g ↓]
    [ π₁′ ↓] = π₁
    [ Ο€β‚‚β€² ↓] = Ο€β‚‚
    [ ⟨ f , g βŸ©β€² ↓] = ⟨ [ f ↓] , [ g ↓] ⟩
    [ !β€² ↓] = !
    [ [ f ↑] ↓] = f

    --------------------------------------------------------------------------------
    -- Semantics

    data Sem (Ξ“ : Ctx) : Ctx β†’ Set (o βŠ” β„“) where
    pair : βˆ€ {Ξ” Ξ¨} β†’ Sem Ξ“ Ξ” β†’ Sem Ξ“ Ξ¨ β†’ Sem Ξ“ (Ξ” ++ Ξ¨)
    tt : Sem Ξ“ βˆ™
    mor : βˆ€ {Ξ”} β†’ ctx Ξ“ β‡’ ctx Ξ” β†’ Sem Ξ“ Ξ”

    interp : βˆ€ {Ξ“ Ξ”} β†’ Sem Ξ“ Ξ” β†’ ctx Ξ“ β‡’ ctx Ξ”
    interp (pair e₁ eβ‚‚) = ⟨ interp e₁ , interp eβ‚‚ ⟩
    interp tt = !
    interp (mor f) = f

    do-fst : βˆ€ {Ξ“ Ξ” Ξ¨} β†’ Sem Ξ“ (Ξ” ++ Ξ¨) β†’ Sem Ξ“ Ξ”
    do-fst (pair e _) = e
    do-fst (mor f) = mor (π₁ ∘ f)

    do-snd : βˆ€ {Ξ“ Ξ” Ξ¨} β†’ Sem Ξ“ (Ξ” ++ Ξ¨) β†’ Sem Ξ“ Ξ¨
    do-snd (pair _ e) = e
    do-snd (mor f) = mor (Ο€β‚‚ ∘ f)

    eval : βˆ€ {Ξ“ Ξ” Ξ¨} β†’ Syn Ξ” Ξ¨ β†’ Sem Ξ“ Ξ” β†’ Sem Ξ“ Ξ¨
    eval idβ€² e = e
    eval (s₁ βˆ˜β€² sβ‚‚) e = eval s₁ (eval sβ‚‚ e)
    eval π₁′ e = do-fst e
    eval Ο€β‚‚β€² e = do-snd e
    eval ⟨ s₁ , sβ‚‚ βŸ©β€² e = pair (eval s₁ e) (eval sβ‚‚ e)
    eval !β€² e = tt
    eval [ f ↑] e = mor (f ∘ interp e)

    reflect : βˆ€ Ξ“ Ξ” β†’ Sem Ξ“ Ξ” β†’ Syn Ξ“ Ξ”
    reflect _ βˆ™ e = !β€²
    reflect _ [ x ] (mor f) = [ f ↑]
    reflect Ξ“ (Δ₁ ++ Ξ”β‚‚) e = ⟨ reflect Ξ“ Δ₁ (do-fst e) , reflect Ξ“ Ξ”β‚‚ (do-snd e) βŸ©β€²

    nf : βˆ€ {Ξ“ Ξ”} β†’ Syn Ξ“ Ξ” β†’ Syn Ξ“ Ξ”
    nf {Ξ“} {Ξ”} s = reflect Ξ“ Ξ” (eval s (mor id))

    interp-do-fst : βˆ€ {Ξ“ Ξ” Ξ¨} β†’ (e : Sem Ξ“ (Ξ” ++ Ξ¨)) β†’ interp (do-fst e) β‰ˆ π₁ ∘ interp e
    interp-do-fst (pair _ _) = ⟺ project₁
    interp-do-fst (mor _) = refl

    interp-do-snd : βˆ€ {Ξ“ Ξ” Ξ¨} β†’ (e : Sem Ξ“ (Ξ” ++ Ξ¨)) β†’ interp (do-snd e) β‰ˆ Ο€β‚‚ ∘ interp e
    interp-do-snd (pair _ _) = ⟺ projectβ‚‚
    interp-do-snd (mor _) = refl

    interp-eval : βˆ€ {Ξ“ Ξ” Ξ¨} β†’ (s : Syn Ξ” Ξ¨) β†’ (e : Sem Ξ“ Ξ”) β†’ interp {Ξ“ = Ξ”} (eval s (mor id)) ∘ interp e β‰ˆ interp (eval s e)
    interp-eval idβ€² e = identityΛ‘
    interp-eval (s₁ βˆ˜β€² sβ‚‚) e = begin
    (interp (eval s₁ (eval sβ‚‚ (mor id))) ∘ interp e)
    β‰ˆΛ˜βŸ¨ (interp-eval s₁ (eval sβ‚‚ (mor id)) ⟩∘⟨refl) ⟩
    (interp (eval s₁ (mor id)) ∘ interp (eval sβ‚‚ (mor id))) ∘ interp e
    β‰ˆβŸ¨ assoc ⟩
    interp (eval s₁ (mor id)) ∘ interp (eval sβ‚‚ (mor id)) ∘ interp e
    β‰ˆβŸ¨ (refl⟩∘⟨ interp-eval sβ‚‚ e) ⟩
    interp (eval s₁ (mor id)) ∘ interp (eval sβ‚‚ e)
    β‰ˆβŸ¨ interp-eval s₁ (eval sβ‚‚ e) ⟩
    interp (eval s₁ (eval sβ‚‚ e))
    ∎
    interp-eval π₁′ e = begin
    (π₁ ∘ id) ∘ interp e
    β‰ˆβŸ¨ ∘-resp-β‰ˆΛ‘ identityΚ³ ⟩
    π₁ ∘ interp e
    β‰ˆΛ˜βŸ¨ interp-do-fst e ⟩
    interp (do-fst e)
    ∎
    interp-eval Ο€β‚‚β€² e = begin
    (Ο€β‚‚ ∘ id) ∘ interp e
    β‰ˆβŸ¨ ∘-resp-β‰ˆΛ‘ identityΚ³ ⟩
    Ο€β‚‚ ∘ interp e
    β‰ˆΛ˜βŸ¨ interp-do-snd e ⟩
    interp (do-snd e)
    ∎
    interp-eval {Ξ“ = Ξ“} {Ξ” = Ξ”} {Ξ¨ = Ψ₁ ++ Ξ¨β‚‚} ⟨ s , s₁ βŸ©β€² e = begin
    ⟨ interp (eval s (mor id)) , interp {Ξ“ = Ξ”} {Ξ” = Ξ¨β‚‚} (eval s₁ (mor (id {A = ctx Ξ”}))) ⟩ ∘ interp e
    β‰ˆβŸ¨ ∘-distribΚ³-⟨⟩ ⟩
    ⟨ interp (eval s (mor id)) ∘ interp e , interp (eval s₁ (mor id)) ∘ interp e ⟩
    β‰ˆβŸ¨ ⟨⟩-congβ‚‚ (interp-eval s e) (interp-eval s₁ e) ⟩
    ⟨ interp (eval s e) , interp (eval s₁ e) ⟩
    ∎
    interp-eval !β€² e = ⟺ (!-unique _)
    interp-eval [ x ↑] e = ∘-resp-β‰ˆΛ‘ identityΚ³

    reflect-mor : βˆ€ Ξ“ Ξ” β†’ (f : ctx Ξ“ β‡’ ctx Ξ”) β†’ [ reflect Ξ“ Ξ” (mor f) ↓] β‰ˆ f
    reflect-mor _ βˆ™ f = !-unique f
    reflect-mor _ [ x ] f = refl
    reflect-mor Ξ“ (Δ₁ ++ Ξ”β‚‚) f = ⟨⟩-congβ‚‚ (reflect-mor Ξ“ Δ₁ (π₁ ∘ f)) (reflect-mor Ξ“ Ξ”β‚‚ (Ο€β‚‚ ∘ f)) β—‹ g-Ξ·


    reflect-interp (pair e₁ eβ‚‚) = ⟨⟩-congβ‚‚ (reflect-interp e₁) (reflect-interp eβ‚‚)
    reflect-interp tt = refl
    reflect-interp {Ξ“ = Ξ“} {Ξ” = Ξ”} (mor f) = reflect-mor Ξ“ Ξ” f

    sound : βˆ€ Ξ“ Ξ” β†’ (s : Syn Ξ“ Ξ”) β†’ [ nf s ↓] β‰ˆ [ s ↓]
    sound Ξ“ Ξ“ idβ€² = reflect-mor Ξ“ Ξ“ id
    sound Ξ“ Ξ” (s₁ βˆ˜β€² sβ‚‚) = begin
    [ reflect Ξ“ Ξ” (eval s₁ (eval sβ‚‚ (mor id))) ↓]
    β‰ˆβŸ¨ reflect-interp ((eval s₁ (eval sβ‚‚ (mor id)))) ⟩
    interp (eval s₁ (eval sβ‚‚ (mor id)))
    β‰ˆΛ˜βŸ¨ interp-eval s₁ ((eval sβ‚‚ (mor id))) ⟩
    (interp (eval s₁ (mor id)) ∘ interp (eval sβ‚‚ (mor id)))
    β‰ˆΛ˜βŸ¨ reflect-interp (eval s₁ (mor id)) ⟩∘⟨ reflect-interp (eval sβ‚‚ (mor id)) ⟩
    ([ reflect _ Ξ” (eval s₁ (mor id)) ↓] ∘ [ reflect Ξ“ _ (eval sβ‚‚ (mor id)) ↓])
    β‰ˆβŸ¨ sound _ _ s₁ ⟩∘⟨ sound _ _ sβ‚‚ ⟩
    [ s₁ ↓] ∘ [ sβ‚‚ ↓]
    ∎
    sound (Γ₁ ++ Ξ“β‚‚) Γ₁ π₁′ = begin
    [ reflect (Γ₁ ++ Ξ“β‚‚) Γ₁ (mor (π₁ ∘ id)) ↓]
    β‰ˆβŸ¨ reflect-mor (Γ₁ ++ Ξ“β‚‚) Γ₁ (π₁ ∘ id) ⟩
    π₁ ∘ id
    β‰ˆβŸ¨ identityΚ³ ⟩
    π₁
    ∎
    sound (Γ₁ ++ Ξ“β‚‚) Ξ“β‚‚ Ο€β‚‚β€² = begin
    [ reflect (Γ₁ ++ Ξ“β‚‚) Ξ“β‚‚ (mor (Ο€β‚‚ ∘ id)) ↓]
    β‰ˆβŸ¨ reflect-mor (Γ₁ ++ Ξ“β‚‚) Ξ“β‚‚ (Ο€β‚‚ ∘ id) ⟩
    Ο€β‚‚ ∘ id
    β‰ˆβŸ¨ identityΚ³ ⟩
    Ο€β‚‚
    ∎
    sound Ξ“ (Δ₁ ++ Ξ”β‚‚) ⟨ s , s₁ βŸ©β€² = ⟨⟩-congβ‚‚ (sound Ξ“ Δ₁ s) (sound Ξ“ Ξ”β‚‚ s₁)
    sound Ξ“ βˆ™ !β€² = refl
    sound Ξ“ βˆ™ [ f ↑] = !-unique f
    sound Ξ“ [ _ ] [ f ↑] = identityΚ³
    sound Ξ“ (Δ₁ ++ Ξ”β‚‚) [ f ↑] = begin
    ⟨ [ reflect Ξ“ Δ₁ (mor (π₁ ∘ f ∘ id)) ↓] , [ reflect Ξ“ Ξ”β‚‚ (mor (Ο€β‚‚ ∘ f ∘ id)) ↓] ⟩
    β‰ˆβŸ¨ ⟨⟩-congβ‚‚ (reflect-mor Ξ“ Δ₁ (π₁ ∘ f ∘ id)) (reflect-mor Ξ“ Ξ”β‚‚ (Ο€β‚‚ ∘ f ∘ id)) ⟩
    ⟨ π₁ ∘ f ∘ id , Ο€β‚‚ ∘ f ∘ id ⟩
    β‰ˆβŸ¨ g-Ξ· ⟩
    f ∘ id
    β‰ˆβŸ¨ identityΚ³ ⟩
    f
    ∎
    open Category π’ž
    open Cartesian cartesian
    open BinaryProducts products
    open Terminal terminal
    open HomReasoning
    open Equiv


    --------------------------------------------------------------------------------
    -- Syntax
    --
    -- The reified syntax of the language of cartesian categories.
    -- Note that we need to reflect objects as well as expressions; this allows
    -- us to perform typed NbE, allowing us to properly Ξ·-expand products.
    --
    -- We also make sure to avoid implicit parameters; these can cause
    -- some of the reflection machinery to act up.

    data Type : Set o where
    βŠ€β€² : Type
    _β€² : Obj β†’ Type
    _Γ—β€²_ : Type β†’ Type β†’ Type

    obj : Type β†’ Obj
    obj βŠ€β€² = ⊀
    obj (A β€²) = A
    obj (A Γ—β€² B) = obj A Γ— obj B

    data Syn : Type β†’ Type β†’ Set (o βŠ” β„“) where
    idβ€² : βˆ€ {A} β†’ Syn A A
    _βˆ˜β€²_ : βˆ€ {A B C} β†’ Syn B C β†’ Syn A B β†’ Syn A C
    π₁′ : βˆ€ {A B} β†’ Syn (A Γ—β€² B) A
    Ο€β‚‚β€² : βˆ€ {A B} β†’ Syn (A Γ—β€² B) B
    ⟨_,_βŸ©β€² : βˆ€ {A B C} β†’ Syn A B β†’ Syn A C β†’ Syn A (B Γ—β€² C)
    !β€² : βˆ€ {A} β†’ Syn A βŠ€β€²
    [_↑] : βˆ€ {A B} β†’ obj A β‡’ obj B β†’ Syn A B

    -- Read a piece of syntax back into a morphism.
    embed : βˆ€ A B β†’ Syn A B β†’ obj A β‡’ obj B
    embed _ _ idβ€² = id
    embed _ _ (f βˆ˜β€² g) = embed _ _ f ∘ embed _ _ g
    embed _ _ π₁′ = π₁
    embed _ _ Ο€β‚‚β€² = Ο€β‚‚
    embed _ _ ⟨ f , g βŸ©β€² = ⟨ embed _ _ f , embed _ _ g ⟩
    embed _ _ !β€² = !
    embed _ _ [ f ↑] = f

    --------------------------------------------------------------------------------
    -- Semantics
    --
    -- The idea here is similar to the Category tactic,
    -- but we need to use a slightly fancier presheaf.
    --
    -- The way we handle neutral terms is somewhat subtle;
    -- For normal NbE we would keep a stack of eliminators
    -- blocked on a neutral. However, our neutral forms
    -- here are morphisms, so we can

    data Sem (A : Type) : Type β†’ Set (o βŠ” β„“) where
    pair : βˆ€ {B C} β†’ Sem A B β†’ Sem A C β†’ Sem A (B Γ—β€² C)
    tt : Sem A βŠ€β€²
    mor : βˆ€ {B} β†’ obj A β‡’ obj B β†’ Sem A B


    do-fst : βˆ€ {A B C} β†’ Sem A (B Γ—β€² C) β†’ Sem A B
    do-fst (pair e _) = e
    do-fst (mor f) = mor (π₁ ∘ f)

    do-snd : βˆ€ {A B C} β†’ Sem A (B Γ—β€² C) β†’ Sem A C
    do-snd (pair _ e) = e
    do-snd (mor f) = mor (Ο€β‚‚ ∘ f)

    -- Reflect the semantics into a morphism in a type-directed manner.
    reflect : βˆ€ A B β†’ Sem A B β†’ obj A β‡’ obj B
    reflect _ βŠ€β€² e = !
    reflect _ (_ β€²) (mor f) = f
    reflect A (B Γ—β€² C) e = ⟨ reflect A B (do-fst e) , reflect A C (do-snd e) ⟩

    -- Evaluate a piece of syntax into a presheaf.
    eval : βˆ€ {A B C} β†’ Syn B C β†’ Sem A B β†’ Sem A C
    eval idβ€² e = e
    eval (s₁ βˆ˜β€² sβ‚‚) e = eval s₁ (eval sβ‚‚ e)
    eval π₁′ e = do-fst e
    eval Ο€β‚‚β€² e = do-snd e
    eval ⟨ s₁ , sβ‚‚ βŸ©β€² e = pair (eval s₁ e) (eval sβ‚‚ e)
    eval !β€² e = tt
    eval [ f ↑] e = mor (f ∘ reflect _ _ e)

    -- Normalize a piece of syntax.
    nf : βˆ€ A B β†’ Syn A B β†’ obj A β‡’ obj B
    nf A B s = reflect A B (eval s (mor id))

    -- Reflecting a morphism preserves equality.
    reflect-mor : βˆ€ A B β†’ (f : obj A β‡’ obj B) β†’ reflect A B (mor f) β‰ˆ f
    reflect-mor A βŠ€β€² f = !-unique f
    reflect-mor A (x β€²) f = refl
    reflect-mor A (B Γ—β€² C) f = begin
    reflect A (B Γ—β€² C) (mor f) β‰ˆβŸ¨ ⟨⟩-congβ‚‚ (reflect-mor A B (π₁ ∘ f)) (reflect-mor A C (Ο€β‚‚ ∘ f)) ⟩
    ⟨ π₁ ∘ f , Ο€β‚‚ ∘ f ⟩ β‰ˆβŸ¨ g-Ξ· ⟩
    f ∎

    reflect-eval : βˆ€ A B C β†’ (s : Syn B C) β†’ (e : Sem A B) β†’ reflect B C (eval s (mor id)) ∘ reflect A B e β‰ˆ reflect A C (eval s e)
    reflect-eval A B B idβ€² e = begin
    reflect B B (mor id) ∘ reflect A B e β‰ˆβŸ¨ (reflect-mor B B id ⟩∘⟨refl) ⟩
    id ∘ reflect A B e β‰ˆβŸ¨ identityΛ‘ ⟩
    reflect A B e ∎
    reflect-eval A B C (f βˆ˜β€² g) e = begin
    reflect B C (eval f (eval g (mor id))) ∘ reflect A B e β‰ˆΛ˜βŸ¨ reflect-eval B _ C f (eval g (mor id)) ⟩∘⟨refl ⟩
    (reflect _ C (eval f (mor id)) ∘ reflect B _ (eval g (mor id))) ∘ reflect A B e β‰ˆβŸ¨ assoc ⟩
    (reflect _ C (eval f (mor id)) ∘ reflect B _ (eval g (mor id)) ∘ reflect A B e) β‰ˆβŸ¨ refl⟩∘⟨ reflect-eval A B _ g e ⟩
    (reflect _ C (eval f (mor id)) ∘ reflect A _ (eval g e)) β‰ˆβŸ¨ reflect-eval A _ C f (eval g e) ⟩
    reflect A C (eval f (eval g e)) ∎
    reflect-eval A (B Γ—β€² C) B π₁′ e = begin
    (reflect (B Γ—β€² C) B (mor (π₁ ∘ id)) ∘ ⟨ reflect A B (do-fst e) , (reflect A C (do-snd e)) ⟩) β‰ˆβŸ¨ (reflect-mor (B Γ—β€² C) B (π₁ ∘ id)) ⟩∘⟨refl ⟩
    (π₁ ∘ id) ∘ ⟨ reflect A B (do-fst e) , reflect A C (do-snd e) ⟩ β‰ˆβŸ¨ (identityΚ³ ⟩∘⟨refl) ⟩
    π₁ ∘ ⟨ reflect A B (do-fst e) , reflect A C (do-snd e) ⟩ β‰ˆβŸ¨ project₁ ⟩
    reflect A B (do-fst e) ∎
    reflect-eval A (B Γ—β€² C) C Ο€β‚‚β€² e = begin
    (reflect (B Γ—β€² C) C (mor (Ο€β‚‚ ∘ id)) ∘ ⟨ reflect A B (do-fst e) , (reflect A C (do-snd e)) ⟩) β‰ˆβŸ¨ (reflect-mor (B Γ—β€² C) C (Ο€β‚‚ ∘ id)) ⟩∘⟨refl ⟩
    (Ο€β‚‚ ∘ id) ∘ ⟨ reflect A B (do-fst e) , reflect A C (do-snd e) ⟩ β‰ˆβŸ¨ (identityΚ³ ⟩∘⟨refl) ⟩
    Ο€β‚‚ ∘ ⟨ reflect A B (do-fst e) , reflect A C (do-snd e) ⟩ β‰ˆβŸ¨ projectβ‚‚ ⟩
    reflect A C (do-snd e) ∎
    reflect-eval A B (C Γ—β€² D) ⟨ f , g βŸ©β€² e = begin
    ⟨ reflect B C (eval f (mor id)) , reflect B D (eval g (mor id)) ⟩ ∘ reflect A B e β‰ˆβŸ¨ ∘-distribΚ³-⟨⟩ ⟩
    ⟨ reflect B C (eval f (mor id)) ∘ reflect A B e , reflect B D (eval g (mor id)) ∘ reflect A B e ⟩ β‰ˆβŸ¨ ⟨⟩-congβ‚‚ (reflect-eval A B C f e) (reflect-eval A B D g e) ⟩
    ⟨ reflect A C (eval f e) , reflect A D (eval g e) ⟩ ∎
    reflect-eval A B .βŠ€β€² !β€² e = ⟺ (!-unique (! ∘ reflect A B e))
    reflect-eval A B C [ f ↑] e = begin
    reflect B C (mor (f ∘ reflect B B (mor id))) ∘ reflect A B e β‰ˆβŸ¨ reflect-mor B C (f ∘ reflect B B (mor id)) ⟩∘⟨refl ⟩
    (f ∘ reflect B B (mor id)) ∘ reflect A B e β‰ˆβŸ¨ (refl⟩∘⟨ reflect-mor B B id) ⟩∘⟨refl ⟩
    (f ∘ id) ∘ reflect A B e β‰ˆβŸ¨ (identityΚ³ ⟩∘⟨ refl) ⟩
    f ∘ reflect A B e β‰ˆΛ˜βŸ¨ reflect-mor A C (f ∘ reflect A B e) ⟩
    reflect A C (mor (f ∘ reflect A B e)) ∎

    sound : βˆ€ A B β†’ (s : Syn A B) β†’ nf A B s β‰ˆ embed A B s
    sound A A idβ€² = reflect-mor A A id
    sound A C (_βˆ˜β€²_ {B = B} f g) = begin
    nf A C (f βˆ˜β€² g) β‰ˆΛ˜βŸ¨ reflect-eval A B C f (eval g (mor id)) ⟩
    nf B C f ∘ nf A B g β‰ˆβŸ¨ sound B C f ⟩∘⟨ sound A B g ⟩
    (embed B C f ∘ embed A B g) ∎
    sound (A Γ—β€² B) A π₁′ = begin
    nf (A Γ—β€² B) A π₁′ β‰ˆβŸ¨ reflect-mor (A Γ—β€² B) A (π₁ ∘ id) ⟩
    π₁ ∘ id β‰ˆβŸ¨ identityΚ³ ⟩
    π₁ ∎
    sound (A Γ—β€² B) B Ο€β‚‚β€² = begin
    nf (A Γ—β€² B) B Ο€β‚‚β€² β‰ˆβŸ¨ reflect-mor (A Γ—β€² B) B (Ο€β‚‚ ∘ id) ⟩
    Ο€β‚‚ ∘ id β‰ˆβŸ¨ identityΚ³ ⟩
    Ο€β‚‚ ∎
    sound A (B Γ—β€² C) ⟨ f , g βŸ©β€² = begin
    nf A (B Γ—β€² C) ⟨ f , g βŸ©β€² β‰ˆβŸ¨ ⟨⟩-congβ‚‚ (sound A B f) (sound A C g) ⟩
    ⟨ embed A B f , embed A C g ⟩ ∎
    sound A .βŠ€β€² !β€² = refl
    sound A B [ f ↑] = begin
    nf A B [ f ↑] β‰ˆβŸ¨ reflect-mor A B (f ∘ reflect A A (mor id)) ⟩
    f ∘ reflect A A (mor id) β‰ˆβŸ¨ (refl⟩∘⟨ reflect-mor A A id) ⟩
    f ∘ id β‰ˆβŸ¨ identityΚ³ ⟩
    f ∎
  3. TOTBWF created this gist Feb 3, 2022.
    198 changes: 198 additions & 0 deletions CartesianNbE.agda
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,198 @@
    {-# OPTIONS --without-K --safe #-}
    module CartesianNbE where

    open import Level

    open import Categories.Category
    open import Categories.Category.Cartesian
    open import Categories.Category.BinaryProducts
    open import Categories.Object.Terminal

    open import Function using (_⟨_⟩_)

    import Data.Unit as Unit
    open import Data.Bool as Bool using (Bool; _∨_; if_then_else_)
    open import Data.Maybe as Maybe using (Maybe; just; nothing; maybe; fromMaybe)
    open import Data.List as List using (List; _∷_; [])
    open import Data.Product as Product using (Ξ£ ;_,_)

    open import Agda.Builtin.Reflection
    open import Reflection.Argument
    open import Reflection.Term using (getName; _β‹―βŸ…βˆ·βŸ†_)
    open import Reflection.TypeChecking.Monad.Syntax

    module _ {o β„“ e} {π’ž : Category o β„“ e} (cartesian : Cartesian π’ž) where

    open Category π’ž
    open Cartesian cartesian
    open BinaryProducts products
    open Terminal terminal
    open HomReasoning
    open Equiv


    --------------------------------------------------------------------------------
    -- Syntax

    data Ctx : Set o where
    βˆ™ : Ctx
    [_] : Obj β†’ Ctx
    _++_ : Ctx β†’ Ctx β†’ Ctx

    ctx : Ctx β†’ Obj
    ctx βˆ™ = ⊀
    ctx [ X ] = X
    ctx (Ξ“ ++ Ξ”) = ctx Ξ“ Γ— ctx Ξ”

    data Syn : Ctx β†’ Ctx β†’ Set (o βŠ” β„“) where
    idβ€² : βˆ€ {A} β†’ Syn A A
    _βˆ˜β€²_ : βˆ€ {A B C} β†’ Syn B C β†’ Syn A B β†’ Syn A C
    π₁′ : βˆ€ {A B} β†’ Syn (A ++ B) A
    Ο€β‚‚β€² : βˆ€ {A B} β†’ Syn (A ++ B) B
    ⟨_,_βŸ©β€² : βˆ€ {A B C} β†’ Syn C A β†’ Syn C B β†’ Syn C (A ++ B)
    !β€² : βˆ€ {A} β†’ Syn A βˆ™
    [_↑] : βˆ€ {A B} β†’ ctx A β‡’ ctx B β†’ Syn A B

    -- Read a piece of syntax back into a morphism.
    [_↓] : βˆ€ {A B} β†’ Syn A B β†’ ctx A β‡’ ctx B
    [ idβ€² ↓] = id
    [ f βˆ˜β€² g ↓] = [ f ↓] ∘ [ g ↓]
    [ π₁′ ↓] = π₁
    [ Ο€β‚‚β€² ↓] = Ο€β‚‚
    [ ⟨ f , g βŸ©β€² ↓] = ⟨ [ f ↓] , [ g ↓] ⟩
    [ !β€² ↓] = !
    [ [ f ↑] ↓] = f

    --------------------------------------------------------------------------------
    -- Semantics

    data Sem (Ξ“ : Ctx) : Ctx β†’ Set (o βŠ” β„“) where
    pair : βˆ€ {Ξ” Ξ¨} β†’ Sem Ξ“ Ξ” β†’ Sem Ξ“ Ξ¨ β†’ Sem Ξ“ (Ξ” ++ Ξ¨)
    tt : Sem Ξ“ βˆ™
    mor : βˆ€ {Ξ”} β†’ ctx Ξ“ β‡’ ctx Ξ” β†’ Sem Ξ“ Ξ”

    interp : βˆ€ {Ξ“ Ξ”} β†’ Sem Ξ“ Ξ” β†’ ctx Ξ“ β‡’ ctx Ξ”
    interp (pair e₁ eβ‚‚) = ⟨ interp e₁ , interp eβ‚‚ ⟩
    interp tt = !
    interp (mor f) = f

    do-fst : βˆ€ {Ξ“ Ξ” Ξ¨} β†’ Sem Ξ“ (Ξ” ++ Ξ¨) β†’ Sem Ξ“ Ξ”
    do-fst (pair e _) = e
    do-fst (mor f) = mor (π₁ ∘ f)

    do-snd : βˆ€ {Ξ“ Ξ” Ξ¨} β†’ Sem Ξ“ (Ξ” ++ Ξ¨) β†’ Sem Ξ“ Ξ¨
    do-snd (pair _ e) = e
    do-snd (mor f) = mor (Ο€β‚‚ ∘ f)

    eval : βˆ€ {Ξ“ Ξ” Ξ¨} β†’ Syn Ξ” Ξ¨ β†’ Sem Ξ“ Ξ” β†’ Sem Ξ“ Ξ¨
    eval idβ€² e = e
    eval (s₁ βˆ˜β€² sβ‚‚) e = eval s₁ (eval sβ‚‚ e)
    eval π₁′ e = do-fst e
    eval Ο€β‚‚β€² e = do-snd e
    eval ⟨ s₁ , sβ‚‚ βŸ©β€² e = pair (eval s₁ e) (eval sβ‚‚ e)
    eval !β€² e = tt
    eval [ f ↑] e = mor (f ∘ interp e)

    reflect : βˆ€ Ξ“ Ξ” β†’ Sem Ξ“ Ξ” β†’ Syn Ξ“ Ξ”
    reflect _ βˆ™ e = !β€²
    reflect _ [ x ] (mor f) = [ f ↑]
    reflect Ξ“ (Δ₁ ++ Ξ”β‚‚) e = ⟨ reflect Ξ“ Δ₁ (do-fst e) , reflect Ξ“ Ξ”β‚‚ (do-snd e) βŸ©β€²

    nf : βˆ€ {Ξ“ Ξ”} β†’ Syn Ξ“ Ξ” β†’ Syn Ξ“ Ξ”
    nf {Ξ“} {Ξ”} s = reflect Ξ“ Ξ” (eval s (mor id))

    interp-do-fst : βˆ€ {Ξ“ Ξ” Ξ¨} β†’ (e : Sem Ξ“ (Ξ” ++ Ξ¨)) β†’ interp (do-fst e) β‰ˆ π₁ ∘ interp e
    interp-do-fst (pair _ _) = ⟺ project₁
    interp-do-fst (mor _) = refl

    interp-do-snd : βˆ€ {Ξ“ Ξ” Ξ¨} β†’ (e : Sem Ξ“ (Ξ” ++ Ξ¨)) β†’ interp (do-snd e) β‰ˆ Ο€β‚‚ ∘ interp e
    interp-do-snd (pair _ _) = ⟺ projectβ‚‚
    interp-do-snd (mor _) = refl

    interp-eval : βˆ€ {Ξ“ Ξ” Ξ¨} β†’ (s : Syn Ξ” Ξ¨) β†’ (e : Sem Ξ“ Ξ”) β†’ interp {Ξ“ = Ξ”} (eval s (mor id)) ∘ interp e β‰ˆ interp (eval s e)
    interp-eval idβ€² e = identityΛ‘
    interp-eval (s₁ βˆ˜β€² sβ‚‚) e = begin
    (interp (eval s₁ (eval sβ‚‚ (mor id))) ∘ interp e)
    β‰ˆΛ˜βŸ¨ (interp-eval s₁ (eval sβ‚‚ (mor id)) ⟩∘⟨refl) ⟩
    (interp (eval s₁ (mor id)) ∘ interp (eval sβ‚‚ (mor id))) ∘ interp e
    β‰ˆβŸ¨ assoc ⟩
    interp (eval s₁ (mor id)) ∘ interp (eval sβ‚‚ (mor id)) ∘ interp e
    β‰ˆβŸ¨ (refl⟩∘⟨ interp-eval sβ‚‚ e) ⟩
    interp (eval s₁ (mor id)) ∘ interp (eval sβ‚‚ e)
    β‰ˆβŸ¨ interp-eval s₁ (eval sβ‚‚ e) ⟩
    interp (eval s₁ (eval sβ‚‚ e))
    ∎
    interp-eval π₁′ e = begin
    (π₁ ∘ id) ∘ interp e
    β‰ˆβŸ¨ ∘-resp-β‰ˆΛ‘ identityΚ³ ⟩
    π₁ ∘ interp e
    β‰ˆΛ˜βŸ¨ interp-do-fst e ⟩
    interp (do-fst e)
    ∎
    interp-eval Ο€β‚‚β€² e = begin
    (Ο€β‚‚ ∘ id) ∘ interp e
    β‰ˆβŸ¨ ∘-resp-β‰ˆΛ‘ identityΚ³ ⟩
    Ο€β‚‚ ∘ interp e
    β‰ˆΛ˜βŸ¨ interp-do-snd e ⟩
    interp (do-snd e)
    ∎
    interp-eval {Ξ“ = Ξ“} {Ξ” = Ξ”} {Ξ¨ = Ψ₁ ++ Ξ¨β‚‚} ⟨ s , s₁ βŸ©β€² e = begin
    ⟨ interp (eval s (mor id)) , interp {Ξ“ = Ξ”} {Ξ” = Ξ¨β‚‚} (eval s₁ (mor (id {A = ctx Ξ”}))) ⟩ ∘ interp e
    β‰ˆβŸ¨ ∘-distribΚ³-⟨⟩ ⟩
    ⟨ interp (eval s (mor id)) ∘ interp e , interp (eval s₁ (mor id)) ∘ interp e ⟩
    β‰ˆβŸ¨ ⟨⟩-congβ‚‚ (interp-eval s e) (interp-eval s₁ e) ⟩
    ⟨ interp (eval s e) , interp (eval s₁ e) ⟩
    ∎
    interp-eval !β€² e = ⟺ (!-unique _)
    interp-eval [ x ↑] e = ∘-resp-β‰ˆΛ‘ identityΚ³

    reflect-mor : βˆ€ Ξ“ Ξ” β†’ (f : ctx Ξ“ β‡’ ctx Ξ”) β†’ [ reflect Ξ“ Ξ” (mor f) ↓] β‰ˆ f
    reflect-mor _ βˆ™ f = !-unique f
    reflect-mor _ [ x ] f = refl
    reflect-mor Ξ“ (Δ₁ ++ Ξ”β‚‚) f = ⟨⟩-congβ‚‚ (reflect-mor Ξ“ Δ₁ (π₁ ∘ f)) (reflect-mor Ξ“ Ξ”β‚‚ (Ο€β‚‚ ∘ f)) β—‹ g-Ξ·


    reflect-interp (pair e₁ eβ‚‚) = ⟨⟩-congβ‚‚ (reflect-interp e₁) (reflect-interp eβ‚‚)
    reflect-interp tt = refl
    reflect-interp {Ξ“ = Ξ“} {Ξ” = Ξ”} (mor f) = reflect-mor Ξ“ Ξ” f

    sound : βˆ€ Ξ“ Ξ” β†’ (s : Syn Ξ“ Ξ”) β†’ [ nf s ↓] β‰ˆ [ s ↓]
    sound Ξ“ Ξ“ idβ€² = reflect-mor Ξ“ Ξ“ id
    sound Ξ“ Ξ” (s₁ βˆ˜β€² sβ‚‚) = begin
    [ reflect Ξ“ Ξ” (eval s₁ (eval sβ‚‚ (mor id))) ↓]
    β‰ˆβŸ¨ reflect-interp ((eval s₁ (eval sβ‚‚ (mor id)))) ⟩
    interp (eval s₁ (eval sβ‚‚ (mor id)))
    β‰ˆΛ˜βŸ¨ interp-eval s₁ ((eval sβ‚‚ (mor id))) ⟩
    (interp (eval s₁ (mor id)) ∘ interp (eval sβ‚‚ (mor id)))
    β‰ˆΛ˜βŸ¨ reflect-interp (eval s₁ (mor id)) ⟩∘⟨ reflect-interp (eval sβ‚‚ (mor id)) ⟩
    ([ reflect _ Ξ” (eval s₁ (mor id)) ↓] ∘ [ reflect Ξ“ _ (eval sβ‚‚ (mor id)) ↓])
    β‰ˆβŸ¨ sound _ _ s₁ ⟩∘⟨ sound _ _ sβ‚‚ ⟩
    [ s₁ ↓] ∘ [ sβ‚‚ ↓]
    ∎
    sound (Γ₁ ++ Ξ“β‚‚) Γ₁ π₁′ = begin
    [ reflect (Γ₁ ++ Ξ“β‚‚) Γ₁ (mor (π₁ ∘ id)) ↓]
    β‰ˆβŸ¨ reflect-mor (Γ₁ ++ Ξ“β‚‚) Γ₁ (π₁ ∘ id) ⟩
    π₁ ∘ id
    β‰ˆβŸ¨ identityΚ³ ⟩
    π₁
    ∎
    sound (Γ₁ ++ Ξ“β‚‚) Ξ“β‚‚ Ο€β‚‚β€² = begin
    [ reflect (Γ₁ ++ Ξ“β‚‚) Ξ“β‚‚ (mor (Ο€β‚‚ ∘ id)) ↓]
    β‰ˆβŸ¨ reflect-mor (Γ₁ ++ Ξ“β‚‚) Ξ“β‚‚ (Ο€β‚‚ ∘ id) ⟩
    Ο€β‚‚ ∘ id
    β‰ˆβŸ¨ identityΚ³ ⟩
    Ο€β‚‚
    ∎
    sound Ξ“ (Δ₁ ++ Ξ”β‚‚) ⟨ s , s₁ βŸ©β€² = ⟨⟩-congβ‚‚ (sound Ξ“ Δ₁ s) (sound Ξ“ Ξ”β‚‚ s₁)
    sound Ξ“ βˆ™ !β€² = refl
    sound Ξ“ βˆ™ [ f ↑] = !-unique f
    sound Ξ“ [ _ ] [ f ↑] = identityΚ³
    sound Ξ“ (Δ₁ ++ Ξ”β‚‚) [ f ↑] = begin
    ⟨ [ reflect Ξ“ Δ₁ (mor (π₁ ∘ f ∘ id)) ↓] , [ reflect Ξ“ Ξ”β‚‚ (mor (Ο€β‚‚ ∘ f ∘ id)) ↓] ⟩
    β‰ˆβŸ¨ ⟨⟩-congβ‚‚ (reflect-mor Ξ“ Δ₁ (π₁ ∘ f ∘ id)) (reflect-mor Ξ“ Ξ”β‚‚ (Ο€β‚‚ ∘ f ∘ id)) ⟩
    ⟨ π₁ ∘ f ∘ id , Ο€β‚‚ ∘ f ∘ id ⟩
    β‰ˆβŸ¨ g-Ξ· ⟩
    f ∘ id
    β‰ˆβŸ¨ identityΚ³ ⟩
    f
    ∎