Skip to content

Instantly share code, notes, and snippets.

@TOTBWF

TOTBWF/CartesianNbE.agda

Last active February 5, 2022 23:24
Show Gist options
  • Save TOTBWF/9faf5e00f9e85b5d569a5f34a7f55fb3 to your computer and use it in GitHub Desktop.
Save TOTBWF/9faf5e00f9e85b5d569a5f34a7f55fb3 to your computer and use it in GitHub Desktop.
Download ZIP
NbE for Cartesian Categories
Raw
CartesianNbE.agda
{-# OPTIONS --without-K --safe #-}
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.BinaryProducts
open import Categories.Object.Terminal
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 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)
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 ∎
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment