mstewartgallus

{-# OPTIONS --cubical --guarded #-}
module clocked where
open import Agda.Primitive
open import Agda.Builtin.Cubical.Path
open import Function.Base using (_∘_)
open import Relation.Nullary
open import Data.Unit
open import Data.Sum
open import Data.Product using (_×_; _,_)
open import Data.Bool using (Bool; true; false; if_then_else_)

mstewartgallus

I think you want something along the lines of the following for an internal logic of Rel.

One interesting thing is that I think you can extend things pretty simply with a kind of automatic differentation as Rel is pretty close to F₂-Vect/Ab₂.

So add h to the grammar and add rules.

Γ ⊢ h: B
h ∧ h ⟶ ∅

Then define

mstewartgallus

Trying to figure out an odd kind of anti-symmetric calculus. Just very awkward to work with substructural logic.

The trouble is that a double category sort of thing where the source object is the composition of several spans is really awkward to work with. Anti-symmetry is an attempt to approach things from the opposite perspective of apartness instead of equivalence and groupoids.

t ::= 𝔻 | 1 | t₀ ∧ t₁ | ⋆t

───    id
t ⊢ t

Γ, t₀, Δ, t₁, Σ, t₂, Π ⊢ t₃

mstewartgallus

Relational calculus with hopes to give semantics in a kind of "alternating multicategory".

I want to work with the exterior algebra ⋀ 𝔽₂[S] (or possibly formal power series ⋀ 𝔽₂[[S]] or algebraic power series ⋀ 𝔽₂(S)) as a nice way of working with set-set apartness relations and denotational semantics.

I want a kind of operad for my set of terms S that composes well with the exterior algebra ⋀ 𝔽₂[S]. I think I require some form of "super operads" but finite fields are already really confusing. Not really happy that enriching over super vector spaces seems to be required.

I suspect you basically want a kind of graded closed semi-additive category but maybe a little weaker.

Symmetry is a natural isomorphism.

mstewartgallus

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

Inductive U :=
| const (A: Type)

| id
(* | compose (τ0 τ1: U) *)

| empty

mstewartgallus

Set Primitive Projections.

Require Import Coq.Unicode.Utf8.

Reserved Infix "∈" (at level 90, right associativity).

Variant fiber {A B} (f: A → B): B → Type :=
  | fiber_intro x: fiber f (f x).
Arguments fiber_intro {A B f}.

mstewartgallus

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

Import List.ListNotations.

Reserved Notation "Γ ⊢ Δ ⇒ τ" (at level 90).
Reserved Notation "x ∈ Γ" (at level 90).
Reserved Infix "$" (at level 20, left associativity).

mstewartgallus

Global Set Primitive Projections.

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

Import List.ListNotations.

Variant zipper {A} := zip (Γ1: list A) (τ: A) (Γ2: list A).
Arguments zipper: clear implicits.

mstewartgallus

import {
    lazy, Suspense,
    createContext, useCallback, useContext, useEffect, useReducer, useTransition
} from "react";

const initialState = {
    poison: false,
    throwable: undefined
};

mstewartgallus

import { useId, useState, useCallback } from "react";

const Panel = ({children, heading}) => {
    const detailsId = useId();
    const headingTextId = useId();
    const headingId = useId();
    const contentId = useId();
    const [open, setOpen] = useState(false);

    const onToggle = useCallback(e => {