fsestini

{-# OPTIONS --cubical #-}

open import Cubical.Core.Prelude
open import Data.List hiding ([_])
open import Cubical.Foundations.Isomorphism

data FreeMonoid (A : Set) : Set where
  [_] : A -> FreeMonoid A
  _●_ : FreeMonoid A -> FreeMonoid A -> FreeMonoid A
  ε   : FreeMonoid A

fsestini

{-# LANGUAGE TemplateHaskell, RankNTypes #-}

module DbCodeGen where

import Data.List (intercalate)
import Control.Lens

type Endo a = a -> a
fix :: Endo a -> a
fix f = f (fix f)

fsestini

module Fulcrum where

open import Data.Maybe using (Maybe ; nothing ; just)
open import Data.Nat
open import Data.Nat.Properties
open import Data.Vec
open import Relation.Nullary
open import Data.Product hiding (map)
open import Data.Fin hiding (_+_ ; _-_ ; _≤_ ; _<_)
open import Data.Sum using (_⊎_ ; [_,_]′ ; inj₁ ; inj₂)