jonsterling

(* an abstract signature for instantiations of the existential quantifier *)
module type EXISTS =
sig
  (* the predicate *)
  type 'a phi

  (* the existential type *)
  type t

  (* the introduction rule *)

jonsterling

discipline = __ (!`SELECT discipline FROM "/test/testDb/olympics" LIMIT 1`) year = __ (!`SELECT year FROM "/test/testDb/olympics" LIMIT 1`) country = {!`SELECT DISTINCT country FROM "/test/testDb/olympics"`} (!`SELECT country FROM "/test/testDb/olympics" LIMIT 1`) type = (!`SELECT DISTINCT type FROM "/test/testDb/olympics" LIMIT 1`) !`SELECT DISTINCT type FROM "/test/testDb/olympics" OFFSET 1` gender = [!`SELECT gender FROM "/test/testDb/olympics" LIMIT 1`] !`SELECT DISTINCT gender FROM "/test/testDb/olympics"`

jonsterling

ERROR:root:code for hash md5 was not found.
Traceback (most recent call last):
  File "/usr/local/Cellar/python/2.7.10_1/Frameworks/Python.framework/Versions/2.7/lib/python2.7/hashlib.py", line 147, in <module>
    globals()[__func_name] = __get_hash(__func_name)
  File "/usr/local/Cellar/python/2.7.10_1/Frameworks/Python.framework/Versions/2.7/lib/python2.7/hashlib.py", line 97, in __get_builtin_constructor
    raise ValueError('unsupported hash type ' + name)
ValueError: unsupported hash type md5
ERROR:root:code for hash sha1 was not found.
Traceback (most recent call last):
  File "/usr/local/Cellar/python/2.7.10_1/Frameworks/Python.framework/Versions/2.7/lib/python2.7/hashlib.py", line 147, in <module>

jonsterling

Theorem axiom-of-choice : [
  {A : U{i}} {B : A -> U{i}} {Q : (a : A) B a -> U{i}}
    (q : (a : A) ((b : B a) * Q a b)) -> (f : (a : A) B a) * ((a : A) Q a (f a))
] {
  auto;
  intro [lam(x. spread(q x; a.b.a))]; auto;
  reduce;
  elim <q> [a]; auto;
  hyp-subst <- #7 [h. Q a spread(h; a._.a)]; auto;
  elim <y>; reduce; assumption

jonsterling

signature EQ =
sig
  type t
  val eq : t * t -> bool
end

signature SHOW =
sig
  type t
  val toString : t -> string

jonsterling

From 9883e42e7f6f281e7ebada6d998d5a15789c6d6d Mon Sep 17 00:00:00 2001
From: Jonathan Sterling <[email protected]>
Date: Wed, 23 Sep 2015 10:28:12 -0700
Subject: [PATCH 1/1] Reformulate Injector in terms of profunctors

---
 bower.json             |  2 ++
 docs/Data/Injector.md  | 15 ++++++-----
 src/Data/Injector.purs | 72 ++++++++++++++++++++++++++++++++++++++++----------
 3 files changed, 69 insertions(+), 20 deletions(-)

jonsterling

||| Some handy notation:
Infix 2 "∈" := member.

||| First we define the option/maybe type constructor
Operator option : (0).
Postfix 10 "?" := option.
[A ?] =def= [A + unit].

Theorem option-wf : [{A:U{i}} A? ∈ U{i}] {
  unfold <option>; auto

jonsterling

signature OPERATIONS =
sig
  type 'a t
  val default : unit -> 'a t
  val enrich : ('b -> 'a option) -> 'b t * 'a t -> 'b t
end

structure UnitOperations : OPERATIONS =
struct
  type 'a t = unit

jonsterling

Theorem darin : [{X:U{i}} {Y:U{i}} {a:X}{b:Y}{c:X}{d:Y} =(<a,b>;<c,d>;X*Y) => =(a;c;X) * =(b;d;Y)] {
  auto;
  [ assert [=(a;spread(<a,b>; x._.x); X)];
      [reduce; auto, hyp-subst -> #8 [h.=(h;c;X)]; auto];

    assert [=(c;spread(<c,d>;x.y.x); X)];
      [reduce; auto, hyp-subst -> #9 [h.=(spread(<a,b>; x._.x); h; X)]; auto];

    eq-cd [h.X, X*Y]; auto

jonsterling

Theorem prod_obj_eq : [
  ∀(RawCatSig; RC.
  ∀(RawCatSig; RD.
  ∀(ap(obj; RC); CA. ∀(ap(obj; RC); CB.
  ∀(ap(obj; RD); DA. ∀(ap(obj; RD); DB.
  ∀(=(CA; CB; ap(obj; RC)); fst.
  ∀(=(DA; DB; ap(obj; RD)); snd.
    =(pair(CA; DA); pair(CB; DB); Σ(ap(obj; RC); _. ap(obj; RD)))))))))))
] {
  auto; isect-intro @1;