TOTBWF

-- Regexes via Brzozowski derivatives
{-# OPTIONS --without-K --safe #-}
module Regex where

open import Function

open import Data.Char
open import Data.Char.Properties renaming (_≟_ to _≟ᶜ_)
open import Data.String using (toList)
open import Data.Bool

TOTBWF

-- A proof of the Knaster-Tarski Fixpoint Theorem
-- See https://en.wikipedia.org/wiki/Knaster%E2%80%93Tarski_theorem
module Fixpoint where

open import Level
open import Data.Product

open import Relation.Binary
open import Relation.Binary.Morphism

TOTBWF

module DayOne where

-- Lets build this up from scratch, for didactic purposes.
-- If we were doing this "for real" we ought to use agda-stdlib.

--------------------------------------------------------------------------------
-- Basic Definitions
--------------------------------------------------------------------------------

-- First, natural numbers and lists. Nothing too exciting here.

TOTBWF

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoImplicitPrelude #-}

TOTBWF

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
module IOHCC where

import Unsafe.Coerce

u = unsafeCoerce

TOTBWF

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE TemplateHaskell #-}
module ObfuscatedSKI where

import Unsafe.Coerce (unsafeCoerce)

--------------------------------------------------------------------------------
-- A Lambda to SKI Combinator Compiler, written entirely using SKI Combinators

TOTBWF

{-# OPTIONS --allow-exec #-}

-- Embed a file as a string inside of an agda program.
-- To use this, make sure to add '/bin/cat' to '~/.agda/executables'

module Static where

open import Function

open import Data.Unit

TOTBWF

{-# OPTIONS --without-K --safe #-}
module InitialAlgebra where

open import Level hiding (zero) renaming (suc to ℓ-suc)

open import Relation.Binary.PropositionalEquality.Core

open import Data.Nat.Base using (ℕ; zero; suc; _+_)
open import Data.List.Base using (List; []; _∷_)

TOTBWF

{-# OPTIONS --without-K --safe #-}
module Operads where

open import Level

open import Categories.Category.Core
open import Categories.Functor.Core

open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂; sym)
import Relation.Binary.PropositionalEquality as Eq

TOTBWF

{-# OPTIONS --without-K --safe #-}

open import Categories.Category.Core
open import Categories.Category.Cartesian

module Categories.Tactic.Cartesian.Solver {o ℓ e} {𝒞 : Category o ℓ e} (cartesian : Cartesian 𝒞) where

open import Level

open import Categories.Category.BinaryProducts