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

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

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