lexa qexat

Notes

(Co)Cartesian Types

Definitions

A cartesian type is a generalized type product where one inhabitant, called origin is common to all the types involved (called axes). A cocartesian type is a generalized type sum with a common origin to all axes.

That is, A * ... * Z is a cartesian type if there exists one inhabitant i common to every axis — i_A = i_B = ... = i_Z.

jekyll: a hyper-declarative, statically-typed programming language around environment manipulation

# x is introduced to the environment
{ ..?e } → { x := 3 ; ..?e }
# y too ; ?e is not the same row variable as the one above
{ ..?e } → { y := 5 ; ..?e }
# matching the current context on one that contains an x and a y
# which allows us to add them to introduce y
{ x ; y ; ..?e } → { z := x + y ; ..?e }

	data Nat where
	O :: Nat
	S :: Nat -> Nat

	instance Eq Nat where
	(==) O O = True
	(==) O (S _) = False
	(==) (S _) O = False
	(==) (S n) (S m) = n == m

	let ( let+ ) = Option.bind

	module Expr = struct
	type app = A
	type fun' = F
	type name = N
	type 'variant reducible = A : app reducible

	type 'variant irreducible =
	\| F : fun' irreducible

	module type TYPE = sig
	type t
	end

	type 't module' = (module TYPE with type t = 't)
	type 'a first = 'b constraint 'a = 'b * _
	type 'a second = 'c constraint 'a = _ * 'c

	module Runtype = struct
	type 'a t =

	let get_char () =
	let attr = Unix.tcgetattr Unix.stdin in
	let () =
	Unix.tcsetattr
	Unix.stdin
	Unix.TCSADRAIN
	{ attr with Unix.c_icanon = false }
	in
	let res = input_byte stdin in
	Unix.tcsetattr Unix.stdin Unix.TCSADRAIN attr;

	module Option = struct
	include Option

	let or_else : type item. (unit -> item t) -> item t -> item t =
	fun rightf left ->
	match left with
	\| None -> rightf ()
	\| _ -> left
	;;

	tokens:
	INFINITY ≔ '∞'
	ZERO ≔ '0'
	ONE ≔ '1'
	NONZERO ≔ /[1-9][0-9]*/
	QUESTION_MARK ≔ '?'
	BANG ≔ '!'

	NAME ≔ /[A-Za-z_][A-Za-z0-9_']*/
	CONTAINS ≔ '∋'

	Require Import Utf8.

	(** [Eqw f x y] represents the equivalence x y up to an isomorphism f. *)
	Inductive Eqw {A B : Type} (f : A → B) : A → A → Prop :=
	\| Refl (x y : A) : f x = f y → Eqw f x y.

	(** Notation for convenience. Same level as equality. *)
	Notation "x = y 'up' 'to' f" := (Eqw f x y).

	(** Utilitary functions for the theorems below. *)

	Require Import String.

	Inductive Term : nat -> Type :=
	\| App : forall {n m : nat}, Term (S n) -> Term m -> Term (n + m)
	\| Fun : forall {n : nat}, Term 0 -> Term n -> Term (S n)
	\| Var : string -> Term 0.