bond15

{-# OPTIONS --copatterns #-}
module copattern where

record Bar : Set where
    field 
        x : List Unit
        y : Unit
        z : ℕ
open Bar

bond15

{-# OPTIONS  --copatterns #-}
module streams where

record Stream (A : Set) : Set where
    coinductive
    field
        hd : A
        tl : Stream A

open Stream

bond15

Inductive Nat : Type :=
  | z : Nat
  | suc : Nat -> Nat.

Print Nat_ind.


Fixpoint plus (n m : Nat): Nat :=
  match n with
  | z => m

bond15

{-# OPTIONS --cubical #-}
module cube where

open import Data.Nat 

open import Cubical.Foundations.Prelude 

data Int : Set where
    pos : (n : ℕ) -> Int
    neg : (n : ℕ) -> Int

bond15

module AOC where

open import Agda.Builtin.Sigma 
open import Relation.Binary.PropositionalEquality using (_≡_;refl)

infix 0 _≈_
record _≈_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A

bond15

{-# OPTIONS --type-in-type #-}
-- ^^ ignoring sizing
module Mon where
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

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

Rel :  Set -> Set 
Rel A  = REL A A 

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

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 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

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