daig

{-# LANGUAGE OverloadedStrings #-}
module App where
import Component
import Notes
import Reflex.Dom
import Data.Semigroup ((<>))

app :: MonadWidget t m => m ()
app = do
  add <- (BlankNote <$) <$> button "New Note"

daig

module Constrained where

-- | A constained function from @a@ to @b@, utilizing constraint @i@ and providing constraint @j@
--   C subsumes 'a -> b == C () () a b', 'Dict c = C () c a a', and 'c :- k == C c k a a'
newtype C i j a b = C {runC :: i => (j => a) -> b}

-- | Composition. Acts like function composition on the arrows, and 
(><) :: C j k a b -> C i j b c -> C i k a c
C f >< C g = C (\x -> g (f x))

daig

{-# language UndecidableInstances #-}
{-# language PostfixOperators #-}
module Fun where
import Prelude hiding ((.),($),(/))
import qualified Prelude as P
import Data.List
import Data.Bool
import Control.Exception
import qualified Data.Map as M
import qualified Data.Set as S

daig

-- {-# OPTIONS --cubical #-}
module cats where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
open import Level using (Level; _⊔_) renaming (zero to lzero; suc to lsuc)
-- open import Cubical.Core.Everything
-- open import Cubical.Foundations.Prelude

daig

# Supersripts and subscripts
<Multi_key> <asciicircum> <0> : "⁰"
<Multi_key> <asciicircum> <1> : "¹"
<Multi_key> <asciicircum> <2> : "²"
<Multi_key> <asciicircum> <3> : "³"
<Multi_key> <asciicircum> <4> : "⁴"
<Multi_key> <asciicircum> <5> : "⁵"
<Multi_key> <asciicircum> <6> : "⁶"
<Multi_key> <asciicircum> <7> : "⁷"
<Multi_key> <asciicircum> <8> : "⁸"

daig

Coherentism

I've been thinking a lot about primitives for epistemic justification. In particular Foundationalism vs Coherentism, their relationship to induction vs coinduction, with Productivity as the Coherentist analog to grounded arguments, ensuring that each step (of a potentially cyclic proof) does some useful and necessary work. Foundationalism is the standard for formal logic, and has gotten us quite far.

"According to the foundationalist option, the series of beliefs terminates with special justified beliefs called “basic beliefs”: these beliefs do not owe their justification to any other beliefs from which they are inferred."

daig

{- ghcid --command="cabal repl --repl-options=-XNoImplicitPrelude" -}
{-
function hdoc() {
	firefox $(cabal haddock --haddock-option="--hyperlinked-source" $1 | tail -n 1)
}
-}
:set -fno-code
:set -XMagicHash -XUnboxedTuples
:set -XPackageImports
:load ./src/Prelude.hs

daig

{-# OPTIONS --type-in-type #-}
module functors where
open import prelude

record Category {O : Set} (𝒞[_,_] : O → O → Set) : Set where
  constructor 𝒾:_▸:_𝒾▸:_▸𝒾:
  infixl 8 _▸_
  field
    𝒾 : ∀ {x} → 𝒞[ x , x ]
    _▸_ : ∀ {x y z} → 𝒞[ x , y ] → 𝒞[ y , z ] → 𝒞[ x , z ]

daig

% ----------------------------------------------------------------------
% Some useful commands when doing highlighting of Agda code in LaTeX.
% ----------------------------------------------------------------------

\ProvidesPackage{agda}

\RequirePackage{ifxetex, ifluatex, xifthen, xcolor, polytable, etoolbox,
                calc, environ, xparse, xkeyval}

% https://tex.stackexchange.com/questions/47576/combining-ifxetex-and-ifluatex-with-the-logical-or-operation

daig

\newcommand{\chumorph}[5]{
\color{mgrey}
\[
\begin{tikzcd}[ampersand replacement=\&]
\& \chuneu{#1} \& \\
\chupos{#4^+} \ar[rr, "\chupos{#2^+}"] \ar[rd, harpoon, bend right=38] \ar[dd, shift left=0.7, no head, "\chuneu{\overline{#4}}"] \& \& \chupos{#5^+} \ar[dd,phantom, shift left=1.5, "\times"] \ar[ld, harpoon', bend left=38] \\
 \& \chuneu{#3} \& \\
\chuneg{#4^-} \ar[uu, phantom, shift left=1.5, "\times"] \ar[ur, harpoon', bend left=38] \& \& \chuneg{#5^-} \ar[uu, no head, shift left=0.7, "\chuneu{\overline{#5}}"] \ar[lu, harpoon, bend right=38] \ar[ll, "\chuneg{#2^-}"]
\end{tikzcd}
\]