Trebor-Huang

{-# OPTIONS --cubical #-}
module HitPuzzle where
open import Cubical.Foundations.Everything
open import Cubical.Data.Empty
open import Cubical.Data.Sum
open import Cubical.Data.Sigma
open import Cubical.Data.Maybe
open import Cubical.Data.Nat

data Perm : Type → Type₁ where

Trebor-Huang

{-# OPTIONS --postfix-projections #-}
open import Agda.Primitive
open import Data.Product
module Polynomial where

variable
  X I O : Set

record Poly : Set₁ where
  -- A polynomial is an expression

Trebor-Huang

structure Pprop : Type where
  pos : Prop
  neg : Prop
  syn : pos → neg → False := by intros; assumption
namespace Pprop

instance : CoeSort Pprop Prop := ⟨Pprop.pos⟩
instance : Coe Bool Pprop where
  coe
  | true => {pos := True, neg := False}

Trebor-Huang

{-# OPTIONS --cubical -Wignore #-}
module lccc where
open import Cubical.Foundations.Prelude

data Obj : Type
data Hom : Obj → Obj → Type

variable
  A B C D X Y : Obj
  f g h u v e : Hom A B

Trebor-Huang

from functools import lru_cache

class Map:
    def __init__(self, f, iterable):
        self.data = (f, iterable)

    def __iter__(self):
        for i in self.data[1]:
            yield self.data[0](i)

Trebor-Huang

module _ where
open import Data.Nat using (ℕ; suc; _+_)
open import Data.Fin using (Fin) renaming (zero to 𝕫; suc to 𝕤_)
open import Data.Vec using (Vec; []; [_]; _∷_; tail; map; allFin) renaming (lookup to _!_)
open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise; []; _∷_)
open import Data.Vec.Relation.Binary.Equality.Propositional using (_≋_; ≋⇒≡)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)

variable
  n m n' : ℕ

Trebor-Huang

{-# OPTIONS --cubical --no-import-sorts --postfix-projections -W ignore #-}
module freeCCC where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Data.Unit using (Unit; isPropUnit; isSetUnit)
open import Cubical.Data.Bool using (Bool; true; false; if_then_else_; isSetBool)
open import Cubical.Data.Sum using (_⊎_; inr; inl)
open import Cubical.Data.Sigma using (Σ; _×_; ΣPathP)

Trebor-Huang

{-# OPTIONS --prop #-}
module Logic where

id : ∀ {ℓ} {A : Set ℓ} -> A -> A
id x = x

data 𝕋 : Set where
    𝒩𝒶𝓉 : 𝕋
    𝒫𝓇ℴ𝓅 : 𝕋
    _⟶_ : 𝕋 -> 𝕋 -> 𝕋

Trebor-Huang

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

module Synthesis where

-- Utilities
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.Nat using (zero; suc; _+_) renaming (Nat to ℕ)

infixl 8 _∧_ _×_

Trebor-Huang

Require Coq.Lists.List.

Module Type Sig.
  Parameter Atomic : Set.
  Parameter Atomic_dec : forall x y : Atomic, {x = y} + {x <> y}.
End Sig.

Module Propositional (UnderlyingAtomic : Sig).
Import UnderlyingAtomic.
Import Coq.Lists.List.