jonsterling

Require Import Coq.Unicode.Utf8.
Require Import List.

Global Obligation Tactic := compute; firstorder.

(* How do to topology in Coq if you are secretly an HOL fan.
   We will not use type classes or canonical structures because they
   count as "advanced" technology. But we will use notations.
 *)

jonsterling

Keybase proof

I hereby claim:

• I am jonsterling on github.
• I am jonsterling (https://keybase.io/jonsterling) on keybase.
• I have a public key whose fingerprint is 0D26 4B16 F650 0D8A CFB1 A781 2FC8 9E5C B6AC C521

To claim this, I am signing this object:

jonsterling

tp : type.

val : tp -> type.
el : tp -> type.
! : val A -> el A.

eq : {A:tp} el A -> el A -> type.

⇓ : el A -> val A -> type. %infix right 11 ⇓.
red : eq A M (! N)

jonsterling

record Container : Set where
  constructor _▹_
  field
    sh : Set
    po : sh → Set

⟦_⟧ : Container → Set → Set
⟦ sh ▹ po ⟧ A = Σ[ s ∶ sh ] (po s → A)

module _ {A : Set} {C : Container} (Q : A → Set) where

jonsterling

val : type.
exp : type.

set : val.
void : val.
unit : val.
& : exp -> exp -> val.   %infix right 10 &.
+ : exp -> exp -> val.   %infix right 10 +.

ax : val.

jonsterling

%solve 
ctx/snoc (ctx/snoc ctx/nil (! ↑ unit)) (@ ([x:tm] ! ↑ unit))
   >> judgement/type (@ ([x:tm] @ ([y:tm] ! ↑ unit))).
 OK
- :
   ctx/snoc (ctx/snoc ctx/nil (! ↑ unit)) (@ ([x:tm] ! ↑ unit))
      >> judgement/type (@ ([x:tm] @ ([y:tm] ! ↑ unit)))
   = >>/,
        ([x:tm] [x':otm (ctx/snoc ctx/nil (! ↑ unit))]
            [x1:weaken (ctx/snoc ctx/nil (! ↑ unit)) x x'] [y:tm]

jonsterling

ac

Goal:

◊ ≫
  ∩(U<0>; A.
  ∩(U<0>; B.
  ∩(∏(A; _.∏(B; _.U<0>)); Q.
 ∏(∏(A; a.prod(B; b.ap(ap(Q; a); b))); _.

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;

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

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