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

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

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

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

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

{-# 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 proofalg where 

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong)
open import Data.Product using (Σ ; Σ-syntax ; _,_ ; proj₁ ; proj₂)

postulate  Extensionality : {A : Set} {B : A → Set} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g

_∘_ : {X Y Z : Set} → (f : Y → Z) → (g : X → Y) → X → Z
f ∘ g = λ x → f(g x)

bond15

{-# OPTIONS --type-in-type #-}
{-# OPTIONS --no-import-sorts #-}
module Foo where
open import Agda.Primitive renaming (Set to Type)
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; cong₂)
open import Data.Product using (_×_; _,_) renaming (proj₁ to π₁; proj₂ to π₂)

postulate  Extensionality : {A : Type} {B : A → Type} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g

bond15

open import Data.Bool.Base
open import Data.List.Base
open import Data.Nat.Base
open import Data.Product
open import Data.Unit

open import Function

open import Reflection

bond15

{-# OPTIONS --guardedness #-}
module tutorial where

open import Poly
open import Data.Product
open import Dynamics
open Systems

postulate A B C D S T : Set