Naïm Camille Favier ncfavier

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

	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

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

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

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

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

	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)