Skip to content

Instantly share code, notes, and snippets.

View kyoDralliam's full-sized avatar

Kenji Maillard kyoDralliam

45 followers · 2 following
View GitHub Profile
@bobatkey
bobatkey / cont-cwf.agda
Last active December 4, 2024 11:35
Construction of the Containers / Polynomials CwF in Agda, showing that function extensionality is refuted
{-# OPTIONS --rewriting #-}
module cont-cwf where
open import Agda.Builtin.Sigma
open import Agda.Builtin.Unit
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Data.Empty
import Relation.Binary.PropositionalEquality as Eq