bond15

Require Import Program.Tactics.

Lemma prf (n : nat)(p : n = 0) : bool.
Admitted.

Program Definition huh(n : nat) : bool :=
  match n with
  | O => prf n _.   (* Program adds the equation `n = 0` to the context of this match branch which is pickec up by the implicit *) 
  | S n => true
end.

bond15

module modal where

open import Data.Unit
open import Data.Nat
open import Data.Product
open import Data.String
open import Data.Bool

open import Agda.Builtin.String

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)