Prove List is free monoid on Set

[github-actions[bot]]

https://api.github.com/pufferffish/agda-symmetries/blob/9ff03831af62533f27f14967803064cc565afa9e/Cubical/Structures/Set/Mon/List.agda#L5

{-# OPTIONS --cubical #-}

module Cubical.Structures.Set.Mon.List where

-- TODO: Prove List is free monoid on Set

[pufferffish]

Blocked on #33

I'm trying to define Free for List but not sure how to deal with h-levels, so my original idea is that I would define something like List A is a Free on set is A is a set, then I'd use the isOfHLevelList lemmas from the base library to define it, but the current free definition doesn't really allow this:

      isFree : {X : Type n} {𝔜 : struct ns σ} (H : isOfHLevel h (𝔜 .carrier)) (ϕ : 𝔜 ⊨ ε)
            -> isEquiv (\(f : structHom {x = ns} < F X , α > 𝔜) -> f .fst ∘ η)

[pufferffish]

Or we try to prove this for a truncated list ∥ List A ∥₂, but this is kinda unsatisfying imo

[vikraman]

Truncation isn't necessary, assume that A is a set only where it is necessary, and use the fact that List A has the same h-level as A. We're trying to avoid equations in the List type.

[github-actions[bot]]

Closed in 0ff92bdb19aba58e89e9690583a23f811cdcca95