ncfavier

  [よ(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

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

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

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

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

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

-- Moved to https://agda.monade.li/PostcomposeNotFull.html

ncfavier

-- Moved to https://agda.monade.li/AdjunctionCommaIso.html

ncfavier

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)

ncfavier

{-# OPTIONS --cubical #-}
open import Cubical.Data.Int
open import Cubical.Data.Int.Divisibility
open import Cubical.Data.Nat
open import Cubical.Foundations.Everything
open import Data.List
open import Data.List.NonEmpty as List⁺

data Vertex : Type where
  a b c : Vertex