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:
-- Code supplement for CPP22 | |
-- (C) 2022 Patricia Johann, Enrico Ghiorzi | |
-- This information is free; you can redistribute and/or modify it under the terms of CC BY-SA 4.0. | |
-- The code was originally for the paper "(Deep) Induction Rules for GADTs", | |
-- then modified by Favonia, released also under CC BY-SA 4.0 | |
{-# OPTIONS --injective-type-constructors #-} | |
module _ where |
{-# OPTIONS --safe #-} | |
open import Agda.Primitive | |
open import Agda.Builtin.Sigma | |
open import Agda.Builtin.Equality | |
variable | |
ℓ : Level | |
A : Set ℓ |
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 |
import Data.Char | |
import Data.List | |
import Control.Applicative | |
up :: String -> String | |
up = map toUpper | |
convertWord :: String -> String | |
convertWord = intercalate "\\ls " . map pure . up |
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 | |
] |
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 |
I hereby claim:
To claim this, I am signing this object:
-- 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, ",以免觸法。"] |
{-# 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 |
-- 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 |