basic-calculus

Require Import Coq.Unicode.Utf8.
Require Coq.Program.Equality.
Require Coq.Lists.List.

Import IfNotations.
Import List.ListNotations.

Inductive sort := dom | void | unit | sum (A B: sort) | prod (A B: sort) | fn (A B: sort).

Module Var.

basic-calculus

Require Import Coq.Unicode.Utf8.
Require Import Coq.Classes.SetoidClass.
Require Import Coq.Arith.PeanoNat.
Require Coq.Vectors.Vector.
Require Coq.Vectors.Fin.

Import IfNotations.
Import Vector.VectorNotations.

Reserved Infix "∘" (at level 30).

basic-calculus

THE WRATH THAT MIGHT HAVE BEEN

At the rising of the sun,
From their hovels creep the working men
And crawling from the forest muck, crawling from its den
To the city - a sick thing wanders in

It is almost like a man
a rotten starving man

basic-calculus

The bungler in the grip of the demon held
To his crypt by strange means is compelled
And sleeping as a corpse in darkness rotting
He dreams forth the red eyed thing
So rises from the sleeper's breath
Comes the Night Ghost - who brings death!

The Night Ghost climbs, as a shadow leaping, overtop the manor wall
And through an open window goes, as a chilling fog
To the room of the sleeper he creeps

basic-calculus

A man walked into town
Bound up in a brown coat
When he talked you could see
Beneath his broad hat
A cigarillo glow
Red then black then red

His face all bandaged
The left arm just gone
And the man had a limp when he walked

basic-calculus

Require Import Coq.Unicode.Utf8.
Require Import Coq.Strings.String.
Require Import Coq.Arith.PeanoNat.
Require Coq.Vectors.Fin.
Require Coq.Lists.List.

Import IfNotations.
Import List.ListNotations.

Fixpoint inj {m n} (e: Fin.t m): Fin.t (m + n) :=

basic-calculus

Require Import Coq.Unicode.Utf8.
Require Import Coq.Classes.SetoidClass.
Require Import Coq.Program.Basics.

Import IfNotations.

Local Open Scope program_scope.

(* just weird all around *)

basic-calculus

Require Import Coq.Unicode.Utf8.
Require Coq.Vectors.Vector.
Require Coq.Lists.List.

Import IfNotations.
Import List.ListNotations.
Import Vector.VectorNotations.

Inductive sort := dom | fn (A B: sort).

basic-calculus

Require Import Coq.Unicode.Utf8.
Require Import Coq.Program.Basics.
Require Import Coq.Logic.FunctionalExtensionality.

Import IfNotations.

Open Scope program_scope.

(* a profunctor from set to set *)
Class Profunctor P := {

basic-calculus

Require Import Coq.Unicode.Utf8.
Require Import Coq.Strings.String.
Require Import Coq.Program.Equality.
Require Coq.Vectors.Vector.
Require Coq.Lists.List.

Import IfNotations.
Import Vector.VectorNotations.

Definition vand {n}: Vector.t _ n → bool := Vector.fold_left andb Datatypes.true.