Generalize universe levels in Indexed Inductives, progress on Dyck pr…

…oofs (#22)

* start changing the linPi/Sigma to dependent &/oplus

* wip on indexed dyck strong equivalences

* start on indexed inductives

* Dyck strong eq: nil case done. wip balanced

* unambiguous epsilon lemma. balanced' still wip

* clean up some goals, identify lemma that would finish off the proof

* a generalized inductive hypothesis that should work

* generalized goal for the section proof as well

* Indexed PAlgebra definitions

* alternate definition of Dyck Traces and wip on unambiguity proof

* include ind', note about NO_POSITIVITY_CHECK and opaque

* dyck traces are equivalent to strings, distributivity for bigoplus

* wip on lifting indexed inductives

* update Indexed Dyck code to use lifts in algebras

---------

Co-authored-by: Steven Schaefer <[email protected]>

code/cubical/Examples/Dyck.agda

@@ -24,18 +24,22 @@ private
 data Bracket : Type where
   [ ] : Bracket
 
-BracketRep : Bracket ≃ Bool
-BracketRep = isoToEquiv (iso
-  (λ { [ → true ; ] → false })
-  (λ { false → ] ; true → [ })
-  (λ { false → refl ; true → refl })
-  λ { [ → refl ; ] → refl })
+opaque
+  BracketRep : Bracket ≃ Bool
+  BracketRep = isoToEquiv (iso
+    (λ { [ → true ; ] → false })
+    (λ { false → ] ; true → [ })
+    (λ { false → refl ; true → refl })
+    λ { [ → refl ; ] → refl })
+
+  isFinBracket : isFinSet Bracket
+  isFinBracket = EquivPresIsFinSet (invEquiv BracketRep) isFinSetBool
 
-isFinBracket : isFinSet Bracket
-isFinBracket = EquivPresIsFinSet (invEquiv BracketRep) isFinSetBool
+  isSetBracket : isSet Bracket
+  isSetBracket = isFinSet→isSet isFinBracket
 
 Alphabet : hSet _
-Alphabet = (Bracket , isFinSet→isSet isFinBracket)
+Alphabet = (Bracket , isSetBracket)
 
 open import Grammar Alphabet
 open import Grammar.Maybe Alphabet