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

ncfavier

module Lan where

open import Categories.Kan
open import Data.Product
open import Level
open import Function renaming (id to funId)
open import Categories.Functor
open import Categories.Category.Instance.Sets
open Functor
open import Relation.Binary.PropositionalEquality