favonia

#include <stdio.h>
#include <ft2build.h>
#include FT_FREETYPE_H
#include <freetype/ftsnames.h>

int main (int argc, const char *argv[]) {
  if (argc != 2) return -1;

  FT_Library lib;
  memset(&lib, 0, sizeof lib);

favonia

import Control.Monad
import Data.List
import Data.Ord

type Cell a = (Integer,[a])
type Row a = [Cell a]

lcs :: Eq a => [a] -> [a] -> [a]
lcs [] _  = []
lcs _  [] = []

favonia

-- Released under CC0.

import System.IO
import Control.Applicative

type Code = [Cmd]
data Cmd = L | R | I | D | P | G | W Code deriving Show

data CodeZipper = CZ Code [(Code,Code)] deriving Show
data DataZipper = DZ [Int]  Int  [Int] deriving Show

favonia

{-# OPTIONS --type-in-type #-}

-- Burali-Forti's paradox in MLTT-ish without W-types

-- I was following Coquand's paper "An Analysis of Girard's Paradox"
-- and Hurkens's paper "A Simplification of Girard's Paradox".
-- Code is released under CC0.

-- Σ-types
record Σ (A : Set) (B : A → Set) : Set where

favonia

-- released under CC0 by favonia

import System.Environment

quotes :: [String -> String]
quotes = map q $ cycle [("「", "」"), ("『", "』")]
  where q (l,r) str = l ++ str ++ r

warn :: (String -> String) -> String -> String
warn q str = concat ["分享", q str, "難判定有無違法，盡量不要分享", q str, "，以免觸法。"]

favonia

Keybase proof

I hereby claim:

• I am favonia on github.
• I am favonia (https://keybase.io/favonia) on keybase.
• I have a public key ASCGlfRtcmUII_C0EtGiRXoRtwG21ECCnZ504VtZajdUJwo

To claim this, I am signing this object:

favonia

import bool
import s1
import isotoequiv

let not/equiv : equiv bool bool =
  iso→equiv _ _ (not, (not, (not∘not/id/pt, not∘not/id/pt)))

let not/path : path^1 type bool bool =
  ua _ _ not/equiv

favonia

import path

let cube/2loop
  (A : type) (a : A)
  (sq : [i j] A [∂[i j] → a])
  : [i j k] A [
    | ∂[i] → sq j k
    | ∂[j] → sq i k
    | ∂[k] → sq i j
    ]

favonia

import Data.Char
import Data.List
import Control.Applicative

up :: String -> String
up = map toUpper

convertWord :: String -> String
convertWord = intercalate "\\ls " . map pure . up

favonia

AGDA_FILES=$(wildcard *.agda)
TEX_FILES=${AGDA_FILES:.agda=.tex}
PDF_FILES=${AGDA_FILES:.agda=.pdf}
MONO_FONT=DejaVu Sans Mono # FreeMono is another choice
PYGMENTS_STYLE=tango

GRADED_XOPP_FILES=$(wildcard *-graded.xopp)
GRADED_PDF_FILES=${GRADED_XOPP_FILES:.xopp=.pdf}

.PHONY: all