Skip to content

Instantly share code, notes, and snippets.

View ncfavier's full-sized avatar
🌷

NaΓ―m Camille Favier ncfavier

🌷
124 followers · 67 following
View GitHub Profile
@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
@ncfavier
ncfavier / Pullback.agda
Created January 14, 2025 23:49
Exercise 2.11 from the HoTT book
{-# OPTIONS --without-K #-}
open import Agda.Primitive renaming (Set to Type)
open import Data.Product
open import Data.Product.Properties
open import Function.Base
open import Relation.Binary.PropositionalEquality
open import Axiom.Extensionality.Propositional
module Pullback (funext : Extensionality _ _) where
@ncfavier
ncfavier / Probabilities.agda
Created January 6, 2025 20:06
open import 1Lab.Prelude
open import Data.Dec
open import Data.Fin
open import Data.Fin.Closure
module wip.Probabilities where
-- β€œI have two children, (at least) one of whom is a boy born on a Tuesday -
-- what is the probability that both children are boys?”
@ncfavier
ncfavier / JMeq.agda
Created December 28, 2024 17:25
{-# OPTIONS --without-K #-}
open import Agda.Primitive renaming (Set to Type)
open import Agda.Builtin.Equality
module JMeq where
data JMeq {β„“} {A : Type β„“} (a : A) : {B : Type β„“} β†’ B β†’ Type (lsuc β„“) where
refl : JMeq a a
JMeq-rec
: βˆ€ {β„“} {A B : Type β„“} (P : {A : Type β„“} β†’ A β†’ Type β„“) {x : A} {y : B}
@ncfavier
ncfavier / seminar20201020_TT-intro-06-family_model.agda
Created December 22, 2024 16:09
Pierce's law is unprovable in MLTT, based on https://bitbucket.org/akaposi/tipuselmelet/src/master/notes/seminar20201020_TT-intro-06-family_model.agda
-- A = 𝟘 β†’ πŸ™
-- Pierce's law does not hold in the family model: we have (A β‡’ βŠ₯) β‰… βŠ₯,
-- hence ((A β‡’ βŠ₯) β‡’ A) β‰… ⊀, hence (((A β‡’ βŠ₯) β‡’ A) β‡’ A) β‰… A, but there is
-- no term of type A.
notPierce : Tm β‹„ (((A β‡’ βŠ₯) β‡’ A) β‡’ A) β†’ 𝟘
notPierce (aβ‚€ , a₁) = a₁ tt tt _ (Ξ» aβ‚‚ _ β†’ aβ‚‚ tt)
@ncfavier
ncfavier / homogeneous.cooltt
Last active September 20, 2024 11:36
Homogeneous = heterogeneous dependent paths in cooltt 😎
import prelude
import coercion
-- De Morgan-style connections, adapted from https://github.com/RedPRL/redtt/blob/master/library/prelude/connection.red
-- Note that these are *strong* connections in the sense that p (i ∧ i) = p i, as
-- opposed to the weak connections defined in https://arxiv.org/abs/1911.05844.
def max
(A : type)
(p : 𝕀 β†’ A)
@ncfavier
ncfavier / PostcomposeNotFull.agda
Last active July 7, 2024 11:28
Moved to https://agda.monade.li/PostcomposeNotFull.html
-- Moved to https://agda.monade.li/PostcomposeNotFull.html
@ncfavier
ncfavier / AdjunctionComma.agda
Last active July 7, 2024 11:27
Moved to https://agda.monade.li/AdjunctionCommaIso.html
-- Moved to https://agda.monade.li/AdjunctionCommaIso.html
@ncfavier
ncfavier / Nat.agda
Created June 15, 2024 10:29
open import 1Lab.Prelude
open import Data.Nat
module wip.Nat where
module _
(N : Type)
(N-set : is-set N)
(z : N)
(s : N β†’ N)