dwarn

{-# OPTIONS --cubical --guardedness #-}

open import Cubical.Foundations.Everything
open import Cubical.Data.Sigma.Properties

-- We are given an indexed container.
module _
  (Ix : Type)
  (A : Ix → Type)
  (B : (i : Ix) → A i → Type)

dwarn

{- A simple, general version of Kraus' magic trick, to recover truncated data. -}
{-# OPTIONS --cubical #-}
module Magic where
open import Cubical.Foundations.Everything
open import Cubical.HITs.PropositionalTruncation

-- Let A be an arbitrary type (not necessarily homogeneous).
module _ {ℓ : Level} {A : Type ℓ} where

-- Define a family of contractible types over A using contractibility of singletons.

dwarn

import category_theory.closed.cartesian

noncomputable theory

open category_theory category_theory.limits tactic interactive interactive.types

def tidy_prod_helper {C} [category C] [has_binary_products C] {Γ X Y : C}
  (h : Π Δ, (Δ ⟶ Γ) → (Δ ⟶ X) → (Δ ⟶ Y)) : X ⨯ Γ ⟶ Y :=
h (X ⨯ Γ) limits.prod.snd limits.prod.fst

dwarn

import category_theory.closed.cartesian

noncomputable theory

open category_theory category_theory.limits tactic interactive interactive.types

lemma tidy_prod_helper {C} [category C] [has_binary_products C] {X Y Z : C}
  (h : Π Γ, (Γ ⟶ X) → (Γ ⟶ Y) → (Γ ⟶ Z)) : X ⨯ Y ⟶ Z :=
h (X ⨯ Y) limits.prod.fst limits.prod.snd

dwarn

import tactic.basic

/-- The states and moves of an infinite two-player game. -/
structure game :=
(angel_state devil_state : Type)
(angel_move : angel_state → set devil_state) 
(devil_move : devil_state → set angel_state) 
-- one could also define `angel_move : angel_state → Type`
-- and `next_state : Π {s}, angel_move s → devil_state`,
-- to allow the game to  distinguish moves leading to the same state.

dwarn

import order.ideal

/- Say a partial order `P` is directed complete, or a dcpo, if every directed subset in `P` has a 
supremum (we actually work with ideals instead of general directed subsets, but every directed
subset is cofinal with an ideal so it doesn't matter). A morphism `P → Q` of dcpo's is a monotone
function which preserves suprema of directed subsets. 

The main result of this file is that for any preorder `P`, `ideal P` is the free dcpo on `P`, in
the sense that any monotone funtcion `P → Q` where `Q` is a dcpo extends uniquely to a morphism 
`ideal P → Q` of dcpo's. -/

dwarn

import data.list.chain

section monoids

-- given a family of monoids, where both the monoids and the indexing set have decidable equality.
variables {ι : Type*} (G : Π i : ι, Type*) [Π i, monoid (G i)]
  [decidable_eq ι] [∀ i, decidable_eq (G i)]

-- The coproduct of our monoids.
@[derive decidable_eq]

dwarn

import order.filter.filter_product 
import category_theory.category.default -- for the `tidy` tactic
open filter filter.filter_product

noncomputable theory

/-- The ultrapower of a `Type`. -/
def upower (α : Type*) := filterprod α (@hyperfilter ℕ)

/-- We think of inhabitants of upower (α → β) as nonstandard functions internal