favonia

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

favonia

{-# OPTIONS --safe #-}

open import Agda.Primitive
open import Agda.Builtin.Sigma
open import Agda.Builtin.Equality

variable
  ℓ : Level
  A : Set ℓ

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

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

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

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

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

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

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