module ImprHIT.Background.Examples where

open import Cubical.Foundations.Prelude

data S¹ : Type₀ where --  ╭───╮ loop
  base : S¹           --  ╰─∘─╯
  loop : base ≡ base  --    base

data FreeSemigroup (A : Type₀) {h : isSet A} : Type₀ where
  η : A → FreeSemigroup A
  _⋆_ : FreeSemigroup A {h} → FreeSemigroup A → FreeSemigroup A
  associative : {a b c : FreeSemigroup A} → (a ⋆ b) ⋆ c ≡ a ⋆ (b ⋆ c)
  truncated : isSet (FreeSemigroup A)

data K (A : Type₀) : Type₀ where
  ∅   : K A
  ⟨_⟩ : A → K A
  _∪_ : K A → K A → K A
  identityₗ     : (x : K A) → ∅ ∪ x ≡ x
  identityᵣ     : (x : K A) → x ∪ ∅ ≡ x
  idempotence   : (x : A) → ⟨ x ⟩ ∪ ⟨ x ⟩ ≡ ⟨ x ⟩
  associativity : (x  y z : K A) → x ∪ (y ∪ z) ≡ (x ∪ y) ∪ z
  commutativity : (x y : K A) → x ∪ y ≡ y ∪ x
  truncated     : isSet (K A)