bond15

Require Import PeanoNat.
Require Import Coq.Logic.Eqdep_dec. 
Import EqNotations.
Require Import Coq.Logic.JMeq.


Infix "==" := JMeq (at level 70, no associativity).

Print JMeq.
Print eq.

bond15

module FinClosureEx where
open import Agda.Primitive
open import Data.Bool
open import Data.Fin
open import Data.List
open import Data.Nat
open import Data.Product
open import Function.Base

private

bond15

module Presentation where 

{-


Topics
    Agda
    Cubical Agda
        Interval / Paths
        Univalence

bond15

{-# OPTIONS --rewriting #-}

module cont-cwf where

open import Agda.Builtin.Sigma
open import Agda.Builtin.Unit
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Data.Empty
import Relation.Binary.PropositionalEquality as Eq

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
    

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

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