Skip to content

Instantly share code, notes, and snippets.

View pnlph's full-sized avatar
🐒
ἑρμηνΡύω

herminie pnlph

🐒
ἑρμηνΡύω
3 followers · 22 following
  • Leipzig
  • 07:55 (UTC +02:00)
View GitHub Profile
@pnlph
pnlph / lambda.agda
Created May 25, 2020 14:51
module test where
open import Data.Nat
open import Data.Product
foo : β„• β†’ β„•
foo = Ξ» where
zero β†’ 1
(suc x) β†’ 0
@pnlph
pnlph / 4648Μ£.agda
Created May 13, 2020 07:54
module 4648Μ£ where
open import Agda.Builtin.List using (List ; _∷_)
a∷as:ListA : βˆ€ {A : Set} β†’ βˆ€ {a : A} β†’ βˆ€ {as : List A} β†’ List A
a∷as:ListA {X} {x} {xs} = x ∷ xs
variable
I : Set
@pnlph
pnlph / #3135.agda
Last active May 10, 2020 16:11
module issue.#3135 where
-- latex \sqw
postulate
A : Set
β–‘ : Set
_β–‘ : Set β†’ Set
⟨_⟩ : Set β†’ Set
--G : Set
@pnlph
pnlph / compilers.agda
Last active May 7, 2020 15:55
module compilers where
module 1960s where
open import Agda.Builtin.Nat using (_+_ ; _*_)
open import Agda.Builtin.Equality using (_≑_ ; refl)
_ : 5 + 6 ≑ 11
_ = refl
module 1950s where
open import Agda.Builtin.Nat using (Nat)
@pnlph
pnlph / precedence.tex
Created May 6, 2020 13:46
\prec Precedes. Unicode U+227A: β‰Ί
\preceq Precedes or equals to. Unicode U+227C: β‰Ό
\precsim Precedes or equivalent to. Unicode U+227E: β‰Ύ
\precnsim Precedes and not equivalent to. Unicode U+22E8: ⋨
@pnlph
pnlph / l20.agda
Last active May 6, 2020 08:32
{-# OPTIONS --type-in-type #-}
{-
Computer Aided Formal Reasoning (G53CFR, G54CFR)
Thorsten Altenkirch
Lecture 20: Russell's paradox
In this lecture we show that it is inconsistent to have
Set:Set. Luckily, Agda is aware of this and indeed
Set=Setβ‚€ : Set₁ : Setβ‚‚ : ...
@pnlph
pnlph / sort.agda
Last active May 6, 2020 14:02
module sort where
-- Polymorphic types
-- Not the framework of pure type systems!
-- Reference https://jesper.sikanda.be/posts/agdas-new-sorts.html
------------------------------------------------------------
-- id₁ : id-sort₁ : SetΟ‰
-- with Level, Setω
------------------------------------------------------------
@pnlph
pnlph / _≀_Recursion.agda
Created April 7, 2020 13:14
_≀_ _β‰₯_ : β„• β†’ β„• β†’ 𝓀₀ Μ‡
0 ≀ y = πŸ™
succ x ≀ 0 = 𝟘
succ x ≀ succ y = x ≀ y
_≀'_ : β„• β†’ β„• β†’ 𝓀₀ Μ‡
_≀'_ = β„•-iteration (β„• β†’ 𝓀₀ Μ‡ ) (Ξ» y β†’ πŸ™) (Ξ» f β†’ β„•-recursion (𝓀₀ Μ‡ ) 𝟘 (Ξ» y P β†’ f y))
x β‰₯ y = y ≀ x
@pnlph
pnlph / HoTT-UF-Natural
Created April 7, 2020 11:09
β„•-induction : (A : β„• β†’ 𝓀 Μ‡ ) β†’ A 0 β†’ ((n : β„•) β†’ A n β†’ A (succ n)) β†’ (n : β„•) β†’ A n
β„•-induction A aβ‚€ f = h where h : (n : β„•) β†’ A n
h 0 = aβ‚€
h (succ n) = f n (h n)
β„•-recursion : (X : 𝓀 Μ‡ ) β†’ X β†’ (β„• β†’ X β†’ X) β†’ β„• β†’ X
β„•-recursion X = β„•-induction (Ξ» _ β†’ X)
β„•-iteration : (X : 𝓀 Μ‡ ) β†’ X β†’ (X β†’ X) β†’ β„• β†’ X
β„•-iteration X x f = β„•-recursion X x (Ξ» _ x β†’ f x)
@pnlph
pnlph / reflection-issue.agda
Last active March 19, 2020 14:52
module reflection-issue where
open import Data.Nat using (zero)
open import Data.Vec using (_∷_)
open import Agda.Builtin.Equality using (_≑_; refl)
open import Agda.Builtin.Reflection using (con)
open import Data.List using ([])
_ : quoteTerm zero ≑ con (quote zero) []
_ = refl