Closed github-actions[bot] closed 10 months ago
https://api.github.com/pufferffish/agda-symmetries/blob/759f0a9c393787fc6cef1e2e97bb04702c866fa9/Cubical/Structures/Set/Mon/Desc.agda#L57
{-# OPTIONS --cubical --allow-unsolved-metas #-} module Cubical.Structures.Set.Mon.Desc where open import Cubical.Foundations.Everything open import Cubical.Data.Nat open import Cubical.Data.FinData as F public open import Cubical.Structures.Set.Sig open import Cubical.Structures.Set.Str public open import Cubical.Structures.Set.Tree open import Cubical.Structures.Set.Eq data MonSym : Type where e : MonSym ⊕ : MonSym MonAr : MonSym -> Type MonAr e = Fin 0 MonAr ⊕ = Fin 2 MonSig : Sig ℓ-zero ℓ-zero Sig.symbol MonSig = MonSym Sig.arity MonSig = MonAr data MonEq : Type where unitl unitr assocr : MonEq -- Vec n A ≃ Fin n -> A MonEqFree : MonEq -> Type MonEqFree unitl = Fin 1 MonEqFree unitr = Fin 1 MonEqFree assocr = Fin 3 MonEqLhs : (eq : MonEq) -> Tree MonSig (MonEqFree eq) MonEqLhs unitl = node ⊕ (F.rec (node e \()) (leaf zero)) MonEqLhs unitr = node ⊕ (F.rec (leaf zero) (node e \())) MonEqLhs assocr = node ⊕ (F.rec (node ⊕ (F.rec (leaf zero) (leaf (suc zero)))) (leaf (suc (suc zero)))) MonEqRhs : (eq : MonEq) -> Tree MonSig (MonEqFree eq) MonEqRhs unitl = leaf zero MonEqRhs unitr = leaf zero MonEqRhs assocr = node ⊕ (F.rec (leaf zero) (node ⊕ (F.rec (leaf (suc zero)) (leaf two)))) MonEqSig : EqSig ℓ-zero ℓ-zero name MonEqSig = MonEq free MonEqSig = MonEqFree MonEqs : EqThy MonSig MonEqSig lhs MonEqs = MonEqLhs rhs MonEqs = MonEqRhs MonSEq : seq MonSig MonEqSig MonSEq n = {!!} , {!!} -- TODO: Tr vs Tree MonStruct = Str ℓ-zero MonSig module Examples where ℕ-MonStr : MonStruct Str.carrier ℕ-MonStr = ℕ Str.ops ℕ-MonStr e f = 0 Str.ops ℕ-MonStr ⊕ f = f zero + f (suc zero) Str.isSetStr ℕ-MonStr = isSetℕ -- ℕ-MonStr-MonSeq : ℕ-MonStr ⊨ MonSEq -- TODO: struct vs Str -- ℕ-MonStr-MoNSEq = ?
https://api.github.com/pufferffish/agda-symmetries/blob/759f0a9c393787fc6cef1e2e97bb04702c866fa9/Cubical/Structures/Set/Mon/Desc.agda#L57