bond15

{-# OPTIONS --with-K #-}
module EckmannHiltonWithK where
open import Agda.Primitive

data _≡_ {ℓ : Level} {A : Set ℓ} : A → A → Set ℓ where 
    refl : {a : A } → a ≡ a 

Ω : (A : Set₀) (a : A) → Set₀ 
Ω A a = a ≡ a

bond15

module SIPmonoid where

-- Uses Agdas reflection mechanism and generic programming 
-- to automatically generate definitions of..
-- structured equivalences
-- proofs that they are univalent
-- See https://github.com/agda/cubical/blob/master/Cubical/Papers/RepresentationIndependence.agda
-- and Internalizing Representation Independence with Univalence
-- for details

bond15

module Ex where 

data Unit : Set where 
    unit : Unit
data Bool : Set where 
    tt ff : Bool

nand : Bool → Bool → Bool 
nand tt tt = ff
nand _ _ = tt

bond15

{-# OPTIONS --type-in-type #-}
module WTypes where

data Nada : Set where

data Unit : Set where
  unit : Unit

data Pos₂ : Set where
    P₁ P₂ : Pos₂

bond15

{-# OPTIONS --cubical #-}
module CTTeq where
open import Cubical.Core.Everything

data Bool : Set where 
    tt ff : Bool

data FooBar : Set where 
    Foo Bar : FooBar

bond15

data Python : Set where
  def_⦅_⦆⦂_ : {A B : Set} → A → B → Python → Python
  for_in̂_⦂_ : {A B : Set} → A → B → Python → Python
  if_⦂_ : Python → Python → Python
  if_⦂_else⦂_ : Python → Python → Python → Python 
  _≕_ : {A B : Set} → A → B → Python
  return_ : {A : Set} → A → Python

foo : {A B C D E : Set} → A → B → C → D → E → Python
foo a b c d e = def a ⦅ b ⦆⦂ 

bond15

module PhoasEx where
data One : Set where
     one : One
        
data type : Set where
     Nat Unit : type
     _⇒_ : type -> type -> type
     
Value : type -> Set
Value Nat = ℕ

bond15

module TM where
open import Data.Integer

data V : Set where
    One Zero Empty : V

data HeadDir : Set where
    L R : HeadDir
 
-- An encoding of Polynomial Functors

bond15

{-# OPTIONS --type-in-type #-}
module Category where 
open import Base
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; trans; sym; cong; cong₂ ; cong-app; subst)

REL : Set -> Set  -> Set 
REL A B = A -> B -> Set 

Rel :  Set -> Set 

bond15

module Mon where

data Option a = None | Some a deriving Show


--class Functor f where
--    fmap :: (a -> b) -> f a -> f b

instance Functor Option where
    fmap f None = None