kontheocharis

import Data.Fin
import Data.Vect
import Data.Vect.Quantifiers

-- No telescopes, no indexing (parameters still possible), no displayed
-- algebras, just paramorphisms.

-- This is the type of descriptions/signatures for constructor data.
-- Each operation (constructor) is a sequence of arguments, either data or
-- recursive calls.

kontheocharis

%default total

-- A set is an index type, and a set for each index, inductively.
record Set where
  constructor MkSet
  i : Type
  f : i -> Set

-- Set `a` is contained in set `b` if there is an index in `b` at which we find
-- a set equal to `a`

kontheocharis

import Data.DPair
import Decidable.Equality

interface IsProp a where
  prop : (0 x : a) -> (0 y : a) -> x = y

0 IsPropD : {a : Type} -> (p : a -> Type) -> Type
IsPropD {a} p = (0 m : a) -> IsProp (p m)

-- POSTULATES

kontheocharis

-- Definition of a CWF with irrelevant binders in Agda, in the style of QTT.
----------------------------------------------------------------------------

-- The CWF formulation of quantitative type theory (Atkey 2018) is basically a
-- base CWF B, a resourced CWF-like thing E, and a functor U : E → B that
-- preserves everything.
--
-- It is really annoying to define this directly as two syntaxes and a functor
-- between them. Instead, we can define a base CWF B, and a displayed CWF E over B.
-- We can recover the usual functorial formulation by taking the total space of E.

kontheocharis

module FakeSOGAT where

open import Relation.Binary.PropositionalEquality

infixr 3 _⇒_
_⇒_ : ∀ {I : Set} → (A : I → Set) → (I → Set) → (I → Set)
(A ⇒ B) j = A j → B j

∀[_] : ∀ {I : Set} → (I → Set) → Set
∀[_] {I} P = {Γ : I} → P Γ

kontheocharis

{-# OPTIONS --rewriting --prop --backtracking-instance-search #-}

open import Agda.Primitive
open import Agda.Builtin.Equality
open import Agda.Builtin.String

-- Problem:
--
-- HOAS (i.e. shallow embedding) is nice to work with because we can re-use the
-- host's functions. However, it does not allow us to inspect the contextual

kontheocharis

[colors]
background = #00000000
foreground = #88ffffff
highlight = #33ffffff
error = ${xrdb:color1:#ff7070}

[barsetup]
background = ${colors.background}
foreground = ${colors.foreground}
line-size = 2

kontheocharis

#!/bin/bash

# Usage: newpp [NAME OF PRESET] [NAME OF NEW PROJECT]

PRESET_DIR=$HOME/.pandoc-presets

mkdir "$2"
cp -rT $PRESET_DIR/"$1" "$2"