Skip to content

Instantly share code, notes, and snippets.

View ncfavier's full-sized avatar
πŸͺ»

NaΓ―m Camille Favier ncfavier

πŸͺ»
134 followers · 67 following
View GitHub Profile
@ncfavier
ncfavier / with.agda
Created March 8, 2026 19:59
Slightly surprising ill-typed with-abstraction. Is it a bug?
postulate
X : Set
u : X
P : X β†’ Set
Q : P u β†’ Set
f : (p : P u) β†’ Q p
f p with u | p
... | a | b = ?
-- f.with : (p : P u) (w : X) (p' : P w) β†’ Q p'
@ncfavier
ncfavier / W.agda
Last active February 24, 2026 17:26
A puzzle about an "extensional" induction principle for W-types
{-# OPTIONS --without-K #-}
module W where
open import Data.Container.Core
open import Data.Container.Relation.Unary.All
open import Data.W
open import Data.Product
open import Relation.Binary.PropositionalEquality
-- Originally asked by Jasper Hugunin at https://stackoverflow.com/questions/79894235
@ncfavier
ncfavier / Russell.agda
Last active January 7, 2026 07:23
Two versions of Russell's paradox in type theory
{-# OPTIONS --type-in-type --with-K #-}
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Empty
{-
Russell's paradox can be encoded in MLTT + K + U:U, as formalised in
https://github.com/KonjacSource/Russell-paradox-in-TT.
@ncfavier
ncfavier / subposet-dot.hs
Created December 26, 2025 14:57
Restrict a dot graph to a subposet.
#!/usr/bin/env nix-shell
#!nix-shell --pure -i runghc -p "haskellPackages.ghcWithPackages (pkgs: with pkgs; [ graphviz topograph ])"
{-
A simple script that reads a dot graph from standard input, restricts
it to the *subposet* on the labels given as arguments (that is, computes
the transitive reduction of a subgraph of its transitive closure) and
prints the result to standard output.
Node and edge labels are destroyed, and the output graph uses input
labels as node IDs.
@ncfavier
ncfavier / alligators.agda
Last active September 15, 2025 21:54
{-# OPTIONS --no-import-sorts --erasure #-}
open import Agda.Primitive renaming (Set to Type)
open import Data.Nat
open import Data.Bool
open import Data.Product
open import Relation.Binary.PropositionalEquality
-- An element of `Remember a` is a witness that `a` exists at runtime.
data Remember {β„“} {@0 A : Type β„“} : (@0 a : A) β†’ Type β„“ where
instance remember : {a : A} β†’ Remember a
@ncfavier
ncfavier / TerminalLarge.agda
Created July 31, 2025 21:02
module TerminalLarge where
open import 1Lab.Prelude
module
_
{β„“}
(X : Type β„“)
(Y : Type) (f : Y β†’ X)
(f-term : (Z : Type) (g : Z β†’ X) β†’ is-contr (Ξ£[ h ∈ (Z β†’ Y) ] f ∘ h ≑ g))
where
@ncfavier
ncfavier / ResizingLoop.agda
Created July 19, 2025 09:53
{-# OPTIONS --allow-unsolved-metas #-}
open import 1Lab.Prelude hiding (_∈_; el!)
module ResizingLoop where
module _ (all-prop : βˆ€ {β„“} {A : Type β„“} β†’ is-prop A) where
el! : Type β†’ Ξ©
el! A = el A all-prop
@ncfavier
ncfavier / partiality-monads.md
Last active July 7, 2025 13:16
A conspiracy board about partiality monads and CPOs.

background

  • constructive HoTT with propositional resizing and HIITs
  • Ξ© := type of propositions = free DCPPO on 1
  • Ξ£ := Rosolini "dominance" (not constructively) / type of semidecidable propositions = conatural numbers quotiented by bisimilarity = (P : Ξ©) Γ— βˆƒ[ f : β„• β†’ 2 ] P = (βˆƒ[ i : β„• ] f i = 0)
  • SΟƒ := SierpiΕ„ski set = initial Οƒ-frame (higher inductive type [1])
  • S∨ := free countably-complete join-semilattice on 1 (higher inductive type [1])
  • SΟ‰ := free Ο‰-CPPO on 1 (higher inductive-inductive type [2])
  • 2 := booleans
  • any dominance P induces a mnd-container, hence a monad on sets which I call P-partiality
@ncfavier
ncfavier / bug.agda
Created April 27, 2025 01:19
module bug where
open import Agda.Builtin.Equality
open import Data.Bool
module Acc
(Level : Set)
(_<_ : Level β†’ Level β†’ Set) where
-- This definition somehow results in the arguments to U< being marked Nonvariant
record Acc (k : Level) : Set where
@ncfavier
ncfavier / representable-tiny.txt
Last active April 18, 2025 18:23
If C has finite products then representables are tiny ([γ‚ˆ(t), β€”] has an amazing right adjoint)
[γ‚ˆ(t), X] β‡’ Y
= βˆ€ d. (γ‚ˆ(t) Γ— γ‚ˆ(d) β‡’ X) β†’ Y(d)
= βˆ€ d. (γ‚ˆ(t Γ— c) β‡’ X) β†’ Y(d)
= βˆ€ d. X(t Γ— d) β†’ Y(d)
= βˆ€ d c. X(c) β†’ (t Γ— d β†’ c) β†’ Y(d)
= βˆ€ c. X(c) β†’ βˆ€ d. (t Γ— d β†’ c) β†’ Y(d)
= βˆ€ c. X(c) β†’ βˆ€ d. (γ‚ˆ(t) Γ— γ‚ˆ(d) β‡’ γ‚ˆ(c)) β†’ Y(d)
= βˆ€ c. X(c) β†’ ([γ‚ˆ(t), γ‚ˆ(c)] β‡’ Y)
= X β‡’ √Y