isSet for Grammars, Monoidal Category of grammars, finish Dyck Trace …

…Equivalence (#28) * HLevels for grammars, instances for epsilon, tensor * triangle and pentagon laws * define monoidal category of grammars * naturality proofs for some combinators * finish the Dyck Trace proof using coherence for monoidal categories * update to CI to use latest cubical-categorical-logic
maxsnew · Oct 28, 2024 · 0f878cc · 0f878cc
1 parent 4b67f97
commit 0f878cc
Show file tree

Hide file tree

Showing 15 changed files with 649 additions and 58 deletions.
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
@@ -135,9 +135,9 @@ jobs:
       - name: Download categorical-logic from github
         run : |
           cd ~
-          git clone https://github.com/maxsnew/cubical-categorical-logic --branch master
+          git clone https://github.com/maxsnew/cubical-categorical-logic --branch main
           cd cubical-categorical-logic
-          git checkout 295cc5defa414b861959f89f52325e098b9db6ec
+          git checkout 4e7b1c3a2ba7ed528b3cd9a4c3a5e7be3ff3449d
           cd ..
           echo "CATLOG_DIR=$PWD/cubical-categorical-logic" >> "$GITHUB_ENV"
 
@@ -146,7 +146,7 @@ jobs:
           mkdir ~/.agda
           touch ~/.agda/libraries
           echo "$CUBICAL_DIR/cubical.agda-lib" >> ~/.agda/libraries
-          echo "$CATLOG_DIR/cubical.agda-lib" >> ~/.agda/libraries
+          echo "$CATLOG_DIR/cubical-categorical-logic.agda-lib" >> ~/.agda/libraries
           echo "$GITHUB_WORKSPACE/code/cubical/grammar.agda-lib" >> ~/.agda/libraries
 
       ########################################################################

diff --git a/code/cubical/Examples/Indexed/Dyck.agda b/code/cubical/Examples/Indexed/Dyck.agda
@@ -10,11 +10,13 @@ open import Cubical.Foundations.Structure
 
 open import Cubical.Data.Bool as Bool hiding (_⊕_ ;_or_)
 import Cubical.Data.Equality as Eq
+import Cubical.Data.Equality.Conversion as Eq
 open import Cubical.Data.Nat as Nat
 open import Cubical.Data.List hiding (init; rec; map)
 open import Cubical.Data.Sigma
 open import Cubical.Data.Sum as Sum hiding (rec; map)
 open import Cubical.Data.FinSet
+open import Cubical.Data.Unit
 
 private
   variable
@@ -45,19 +47,42 @@ open import Grammar.String.Properties Alphabet
 open import Grammar.Equivalence Alphabet
 open import Grammar.Equalizer Alphabet
 open import Grammar.Inductive.Indexed Alphabet
+open import Grammar.Inductive.HLevels Alphabet
+open import Grammar.HLevels Alphabet
+open import Grammar.Coherence Alphabet
 open import Term Alphabet
 
 open StrongEquivalence
 
 data DyckTag : Type ℓ-zero where
   nil' balanced' : DyckTag
+
+isSetDyckTag : isSet DyckTag
+isSetDyckTag = isSetRetract enc dec retr isSetBool where
+  enc : DyckTag → Bool
+  enc nil' = false
+  enc balanced' = true
+  dec : Bool → DyckTag
+  dec false = nil'
+  dec true = balanced'
+  retr : (x : DyckTag) → dec (enc x) ≡ x
+  retr nil' = refl
+  retr balanced' = refl
+
 DyckTy : Unit → Functor Unit
 DyckTy _ = ⊕e DyckTag (λ
   { nil' → k ε
   ; balanced' → ⊗e (k (literal [)) (⊗e (Var _) (⊗e (k (literal ])) (Var _))) })
+
+
 IndDyck : Grammar ℓ-zero
 IndDyck = μ DyckTy _
 
+isSetGrammarDyck : isSetGrammar IndDyck
+isSetGrammarDyck = isSetGrammarμ DyckTy
+  (λ _ → isSetDyckTag , (λ { nil' → isSetGrammarε ; balanced' → isSetGrammarLiteral _ , (tt* , (isSetGrammarLiteral _ , tt*)) }))
+  tt
+
 NIL : ε ⊢ IndDyck
 NIL = roll ∘g ⊕ᴰ-in nil' ∘g liftG
 
@@ -127,6 +152,52 @@ data TraceTag (b : Bool) (n : ℕ) : Type where
   leftovers' : (b Eq.≡ false) → ∀ n-1 → (suc n-1 Eq.≡ n) → TraceTag b n
   unexpected' : b Eq.≡ false → n Eq.≡ zero → TraceTag b n
 
+isSetTraceTag : ∀ b n → isSet (TraceTag b n)
+isSetTraceTag b n = isSetRetract {B = TT} enc dec retr isSetTT where
+  isPropBoolEq : ∀ {b b' : Bool} → isProp (b Eq.≡ b')
+  isPropBoolEq {b}{b'} =
+    subst isProp Eq.PathPathEq (isSetBool _ _)
+
+  isPropℕEq : ∀ {b b' : ℕ} → isProp (b Eq.≡ b')
+  isPropℕEq {b}{b'} =
+    subst isProp Eq.PathPathEq (isSetℕ _ _)
+
+  TT : Type ℓ-zero
+  TT =
+    ((b Eq.≡ true) × (n Eq.≡ zero))
+    ⊎ (Eq.fiber suc n
+    ⊎ (Unit
+    ⊎ (((b Eq.≡ false) × Eq.fiber suc n)
+    ⊎ ((b Eq.≡ false) × (n Eq.≡ zero)))))
+  isSetTT : isSet TT
+  isSetTT =
+    isSet⊎ (isProp→isSet (isProp× isPropBoolEq isPropℕEq))
+    (isSet⊎ (isSetΣ isSetℕ (λ _ → isProp→isSet isPropℕEq))
+    (isSet⊎ isSetUnit
+    (isSet⊎ (isSet× (isProp→isSet isPropBoolEq)
+      (isSetΣ isSetℕ (λ _ → isProp→isSet isPropℕEq)))
+    (isProp→isSet (isProp× isPropBoolEq isPropℕEq)))))
+  enc : TraceTag b n → TT
+  enc (eof' x x₁) = inl (x , x₁)
+  enc (close' n-1 x) = inr (inl (n-1 , x))
+  enc open' = inr (inr (inl tt))
+  enc (leftovers' x n-1 x₁) = inr (inr (inr (inl (x , n-1 , x₁))))
+  enc (unexpected' x x₁) = inr (inr (inr (inr (x , x₁))))
+
+  dec : TT → TraceTag b n
+  dec (inl x) = eof' (x .fst) (x .snd)
+  dec (inr (inl x)) = close' (x .fst) (x .snd)
+  dec (inr (inr (inl x))) = open'
+  dec (inr (inr (inr (inl x)))) = leftovers' (x .fst) _ (x .snd .snd)
+  dec (inr (inr (inr (inr x)))) = unexpected' (x .fst) (x .snd)
+
+  retr : ∀ t → dec (enc t) ≡ t
+  retr (eof' x x₁) = refl
+  retr (close' n-1 x) = refl
+  retr open' = refl
+  retr (leftovers' x n-1 x₁) = refl
+  retr (unexpected' x x₁) = refl
+
 LP = [
 RP = ]
 
@@ -142,6 +213,16 @@ TraceTys b n = ⊕e (TraceTag b n) (λ
 Trace : Bool → ℕ → Grammar _
 Trace b = μ (TraceTys b)
 
+isSetGrammarTrace : ∀ b n → isSetGrammar (Trace b n)
+isSetGrammarTrace b = isSetGrammarμ (TraceTys b) λ n →
+  isSetTraceTag b n
+  , λ { (eof' x x₁) → isSetGrammarε
+      ; (close' n-1 x) → (isSetGrammarLiteral _) , tt*
+      ; open' → (isSetGrammarLiteral _) , tt*
+      ; (leftovers' x n-1 x₁) → isSetGrammarε
+      ; (unexpected' x x₁) → (isSetGrammarLiteral _) , isSetGrammar⊤
+      }
+
 EOF : ε ⊢ Trace true 0
 EOF = roll ∘g ⊕ᴰ-in (eof' Eq.refl Eq.refl) ∘g liftG
 
@@ -267,6 +348,12 @@ GenDyck : ℕ → Grammar _
 GenDyck 0         = IndDyck
 GenDyck (suc n-1) = IndDyck ⊗ literal RP ⊗ GenDyck n-1
 
+isSetGrammarGenDyck : ∀ n → isSetGrammar (GenDyck n)
+isSetGrammarGenDyck zero = isSetGrammarDyck
+isSetGrammarGenDyck (suc n) =
+  isSetGrammar⊗ isSetGrammarDyck
+    (isSetGrammar⊗ (isSetGrammarLiteral _) (isSetGrammarGenDyck n))
+
 -- We extend the balanced constructor and append to our unbalanced
 -- trees
 opaque
@@ -280,13 +367,6 @@ upgradeBuilder (suc n) = ⟜-intro (⟜-app ,⊗ id ∘g ⊗-assoc)
 
 opaque
   unfolding ⊗-intro genBALANCED
-  -- uB-lem' :
-  --   ∀ n (f : Trace true n ⊢ GenDyck n)
-  --       (f' : {!!} ⊢ {!!})
-  --      → (⟜-app ∘g id ,⊗ f) ∘g
-  --       (upgradeBuilder n ∘g ⟜-intro {!!}) ,⊗ id
-  --       ≡ (f ∘g {!!})
-  -- uB-lem' = {!!}
   upgradeNilBuilder :
     ∀ n (f : Trace true n ⊢ GenDyck n)
        → (⟜-app ∘g id ,⊗ f) ∘g
@@ -300,8 +380,7 @@ opaque
     ∙ cong ((⟜-app ,⊗ id) ∘g_) (cong (_∘g (id ,⊗ f)) (⊗-assoc⊗-intro {f' = id}{f'' = id}))
     ∙ ( (λ i → (⟜-β ⊗-unit-l i) ,⊗ id ∘g ⊗-assoc ∘g id ,⊗ f))
     ∙ cong (_∘g (id ,⊗ f)) (cong ((⊗-unit-l ,⊗ id) ∘g_) (sym (⊗-assoc⊗-intro {f' = id}{f'' = id})))
-    -- ∙ cong (_∘g id ,⊗ f) ⊗-unit-l⊗-assoc
-    ∙ {!!}
+    ∙ cong (_∘g id ,⊗ f) (⊗-unit-l⊗-assoc isSetGrammarDyck (isSetGrammar⊗ (isSetGrammarLiteral _) (isSetGrammarGenDyck n)))
     ∙ sym (⊗-unit-l⊗-intro _)
 
   upgradeBalancedBuilder :
@@ -336,7 +415,8 @@ opaque
       ∘g id ,⊗ ((id ,⊗ NIL) ,⊗ id)
       ∘g id ,⊗ (⊗-assoc ∘g id ,⊗ ⊗-unit-l⁻)  --
       ∘g id ,⊗ id ,⊗ id ,⊗ ⟜-app
-      ∘g lowerG ,⊗ lowerG ,⊗ lowerG ,⊗ (id ∘g lowerG) ,⊗ id ∘g ⊗-assoc⁻4⊗-intro {f = id}{f' = id}{f'' = id}{f''' = id}{f'''' = f} i)
+      ∘g lowerG ,⊗ lowerG ,⊗ lowerG ,⊗ (id ∘g lowerG) ,⊗ id ∘g ⊗-assoc⁻4⊗-intro {f = id}{f' = id}{f'' = id}{f''' = id}{f'''' = f} i
+      )
     ∙ (λ i → BALANCED
       ∘g id ,⊗ (⟜-app ,⊗ id)
       ∘g id ,⊗ ⊗-assoc⊗-intro {f = id}{f' = NIL}{f'' = id} (~ i)
@@ -368,7 +448,14 @@ opaque
     ∙ (λ i →
        BALANCED ,⊗ id
        ∘g (lowerG ,⊗ (⟜-app ∘g lowerG ,⊗ NIL ∘g ⊗-unit-r⁻) ,⊗ lowerG ,⊗ (⟜-app ∘g lowerG ,⊗ id)) ,⊗ id
-       ∘g ⊗-assoc⁻4⊗-assoc i
+       ∘g ⊗-assoc⁻4⊗-assoc
+          (isSetGrammarLift (isSetGrammarLiteral _))
+          (isSetGrammarLift (isSetGrammar⟜ isSetGrammarDyck))
+          (isSetGrammarLift (isSetGrammarLiteral _))
+          (isSetGrammarLift (isSetGrammar⟜ isSetGrammarDyck))
+          isSetGrammarDyck
+          (isSetGrammar⊗ (isSetGrammarLiteral _) (isSetGrammarGenDyck n))
+          i
        ∘g id ,⊗ f)
     ∙ (λ i → BALANCED ,⊗ id
         ∘g ⊗-assoc4⊗-intro {f = lowerG}{f' = ⟜-app ∘g lowerG ,⊗ NIL ∘g ⊗-unit-r⁻}{f'' = lowerG}{f''' = (⟜-app ∘g lowerG ,⊗ id)}{f'''' = id} (~ i)
@@ -379,7 +466,8 @@ opaque
         ∘g ⊗-assoc4
         ∘g lowerG ,⊗ (⟜-app ∘g lowerG ,⊗ NIL ∘g ⊗-unit-r⁻) ,⊗ lowerG ,⊗ ((⟜-app ∘g lowerG ,⊗ id) ,⊗ id)
         ∘g id ,⊗ id ,⊗ id ,⊗ ⊗-assoc
-        ∘g ⊗-assoc⁻4⊗-intro {f = id}{f' = id}{f'' = id}{f''' = id}{f'''' = f} i)
+        ∘g ⊗-assoc⁻4⊗-intro {f = id}{f' = id}{f'' = id}{f''' = id}{f'''' = f} i
+        )
     ∙ (λ i → BALANCED ,⊗ id
         ∘g ⊗-assoc4
         ∘g lowerG ,⊗ ((⟜-app ∘g (id ,⊗ NIL) ∘g ⊗-unit-r⁻⊗-intro {f = lowerG} (~ i)) ,⊗ lowerG ,⊗ ((⟜-app ∘g lowerG ,⊗ id) ,⊗ id ∘g ⊗-assoc ∘g id ,⊗ f))
@@ -469,14 +557,6 @@ buildTraceAlg _ = ⊕ᴰ-elim (λ
 buildTrace : IndDyck ⊢ TraceBuilder _
 buildTrace = rec DyckTy buildTraceAlg _
 
--- buildTraceβBalanced :
---   buildTrace ∘g roll ∘g ⊕ᴰ-in balanced'
---   ≡ &ᴰ-intro λ n → ⟜-intro
---     (({!\!}
---      ∘g ⊗-assoc⁻4
---     )
---     ∘g (lowerG ,⊗ (buildTrace ∘g lowerG) ,⊗ lowerG ,⊗ (buildTrace ∘g lowerG)) ,⊗ id)
-
 -- we then extend the builder to generalized trees, which *adds*
 -- closed parens to the trace.
 genBuildTrace : ∀ m → GenDyck m ⊢ &[ n ∈ _ ] (Trace true (m + n) ⟜ Trace true n)
@@ -578,7 +658,8 @@ pfAlg _ =
                 ∘g id ,⊗ (⟜-app ∘g &ᴰ-π (suc n) ,⊗ id)
                 ∘g id ,⊗ id ,⊗ CLOSE
                 ∘g id ,⊗ id ,⊗ id ,⊗ (⟜-app ∘g &ᴰ-π n ,⊗ id)
-                ∘g ⊗-assoc⁻4⊗-intro {f = lowerG}{f' = buildTrace ∘g eq-π lhs rhs ∘g lowerG}{f'' = lowerG}{f''' = buildTrace ∘g eq-π lhs rhs ∘g lowerG}{f'''' = id} i)
+                ∘g ⊗-assoc⁻4⊗-intro {f = lowerG}{f' = buildTrace ∘g eq-π lhs rhs ∘g lowerG}{f'' = lowerG}{f''' = buildTrace ∘g eq-π lhs rhs ∘g lowerG}{f'''' = id} i
+                )
             ∙ (λ i → genBALANCED n
                 ∘g id ,⊗ (⟜-β (genMkTree (suc n) ∘g ⟜-app) (~ i) ∘g (&ᴰ-π (suc n) ∘g (buildTrace ∘g eq-π lhs rhs)) ,⊗ id)
                 ∘g id ,⊗ id ,⊗ CLOSE

diff --git a/code/cubical/Grammar/Coherence.agda b/code/cubical/Grammar/Coherence.agda
@@ -0,0 +1,73 @@
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+
+module Grammar.Coherence (Alphabet : hSet ℓ-zero) where
+
+open import Cubical.Data.Sigma
+open import Cubical.Data.List
+open import Cubical.Categories.Category.Base
+open import Cubical.Categories.Monoidal
+open import Cubical.Categories.Monoidal.Combinators.Base as Combinators
+open import Cubical.Categories.Monoidal.Combinators.Equations as Combinators
+
+open import Grammar.Base Alphabet
+open import Grammar.Lift Alphabet
+open import Grammar.HLevels Alphabet
+open import Grammar.Epsilon Alphabet
+open import Grammar.LinearProduct Alphabet
+open import Term.Base Alphabet
+open import Term.Bilinear Alphabet
+open import Term.Category Alphabet
+
+private
+  variable
+    ℓg ℓh ℓk ℓl ℓ ℓ' : Level
+    g g' g'' g''' g'''' g''''' : Grammar ℓg
+    h h' h'' h''' h'''' h''''' : Grammar ℓh
+    f f' f'' f''' f'''' f''''' : g ⊢ h
+    k : Grammar ℓk
+    l : Grammar ℓl
+
+private
+  G = GRAMMAR ℓ-zero
+  module G = MonoidalCategory G
+
+opaque
+  ⊗-assoc⁻4⊗-assoc :
+    ∀ {g g' g'' g''' g'''' g''''' : Grammar ℓ-zero}
+    → isSetGrammar g
+    → isSetGrammar g'
+    → isSetGrammar g''
+    → isSetGrammar g'''
+    → isSetGrammar g''''
+    → isSetGrammar g'''''
+    → ⊗-assoc⁻4 {g = g}{g' = g'}{g'' = g''}{g''' = g'''}{g'''' = g''''}
+      ,⊗ id {g = g'''''}
+      ∘g ⊗-assoc
+      ≡ ⊗-assoc4 ∘g id ,⊗ id ,⊗ id ,⊗ ⊗-assoc ∘g ⊗-assoc⁻4
+  ⊗-assoc⁻4⊗-assoc isSetG isSetG' isSetG'' isSetG''' isSetG'''' isSetG''''' =
+    α4⁻¹α G (_ , isSetG) (_ , isSetG') (_ , isSetG'')
+            (_ , isSetG''') (_ , isSetG'''') (_ , isSetG''''')
+
+⊗-unit*-l⊗-assoc :
+  {g g' : Grammar ℓ-zero}
+  → isSetGrammar g
+  → isSetGrammar g'
+  → ⊗-unit*-l {ℓ = ℓ-zero} {g = g} ,⊗ id {g = g'} ∘g ⊗-assoc ≡ ⊗-unit*-l
+⊗-unit*-l⊗-assoc isSetG isSetG' =
+  Combinators.ηα G (_ , isSetG) (_ , isSetG')
+
+opaque
+  unfolding ⊗-intro
+  ⊗-unit-l⊗-assoc :
+    {g g' : Grammar ℓ-zero}
+    → isSetGrammar g
+    → isSetGrammar g'
+    → ⊗-unit-l {g = g} ,⊗ id {g = g'} ∘g ⊗-assoc ≡ ⊗-unit-l
+  ⊗-unit-l⊗-assoc isSetG isSetG' =
+    ⊗-unit-l ,⊗ id ∘g ⊗-assoc
+      ≡⟨ cong ((⊗-unit*-l {ℓ-zero} ,⊗ id) ∘g_) ⊗-assoc⊗-intro ⟩
+    (⊗-unit*-l {ℓ-zero} ,⊗ id) ∘g ⊗-assoc ∘g ⊗-intro (liftG {ℓ-zero}) id
+      ≡⟨ cong (_∘g ⊗-intro liftG id) (⊗-unit*-l⊗-assoc isSetG isSetG') ⟩
+    ⊗-unit-l
+    ∎
diff --git a/code/cubical/Grammar/Dependent/Properties.agda b/code/cubical/Grammar/Dependent/Properties.agda
@@ -9,6 +9,7 @@ open import Cubical.Data.FinSet
 open import Cubical.Foundations.Structure
 
 open import Grammar.Base Alphabet
+open import Grammar.HLevels Alphabet
 open import Grammar.LinearProduct Alphabet
 open import Grammar.LinearFunction Alphabet
 open import Grammar.Equivalence.Base Alphabet
@@ -79,3 +80,12 @@ module _
   unambiguous⊕ᴰ unambig⊕ a =
     unambiguous'→unambiguous
       (unambiguous'⊕ᴰ (unambiguous→unambiguous' unambig⊕) a)
+
+module _
+  {X : Type ℓS} {A : X → Grammar ℓh}
+  where
+  isSetGrammar&ᴰ : (∀ x → isSetGrammar (A x)) → isSetGrammar (&ᴰ A)
+  isSetGrammar&ᴰ isSetGrammarA w = isSetΠ λ x → isSetGrammarA x w
+
+  isSetGrammar⊕ᴰ : isSet X → (∀ x → isSetGrammar (A x)) → isSetGrammar (⊕ᴰ A)
+  isSetGrammar⊕ᴰ isSetX isSetGrammarA w = isSetΣ isSetX (λ x → isSetGrammarA x w)
diff --git a/code/cubical/Grammar/Epsilon.agda b/code/cubical/Grammar/Epsilon.agda
@@ -7,6 +7,7 @@ open import Cubical.Data.List
 
 open import Helper
 open import Grammar.Base Alphabet
+open import Grammar.HLevels Alphabet
 open import Grammar.Lift Alphabet
 open import Term.Base Alphabet
 open import Term.Nullary Alphabet
@@ -53,5 +54,18 @@ opaque
       (sym (++-unit-r _) ∙ cong (w1 ++_) (sym w2≡[]))
       (f w1 gp)
 
+  isLangε : isLang ε
+  isLangε _ _ _ = isSetString _ _ _ _
+
+  isSetGrammarε : isSetGrammar ε
+  isSetGrammarε = isLang→isSetGrammar isLangε
+
 ε* : ∀ {ℓ : Level} → Grammar ℓ
 ε* {ℓ = ℓ} = LiftG ℓ ε
+
+isLangε* : ∀ {ℓ} → isLang (ε* {ℓ})
+isLangε* = isLangLift isLangε
+
+isSetGrammarε* : ∀ {ℓ} → isSetGrammar (ε* {ℓ})
+isSetGrammarε* = isLang→isSetGrammar isLangε*
+