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

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

# 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

-- {-# 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

{-# 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

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 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"