gallais

open import Data.List using (List); open List
open import Data.List.Properties
open import Data.Product
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Nullary.Product
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

private variable A : Set

gallais

open import Data.Nat.Base
open import Data.Vec
open import Data.Bool.Base using (Bool; false; true)
open import Data.Product

variable
  m n : ℕ
  b : Bool
  Γ Δ Ξ T I O : Vec Bool n

gallais

open import Size
open import Codata.Thunk

data BinaryTreePath (i : Size) : Set where
  here : BinaryTreePath i
  branchL : Thunk BinaryTreePath i → BinaryTreePath i
  branchR : Thunk BinaryTreePath i → BinaryTreePath i

zero : ∀ {i} → BinaryTreePath i
zero = branchL λ where .force → zero

gallais

module scope where

import Level as L
open import Data.Nat.Base
open import Data.Vec hiding (_>>=_)
open import Data.Fin.Base
open import Data.String
open import Data.Maybe as Maybe
open import Data.Product as Prod
open import Relation.Nullary

gallais

open import Level
open import Data.List.Base hiding (filter)
open import Data.List.Relation.Unary.All
open import Data.List.Relation.Ternary.Interleaving.Propositional
open import Function
open import Relation.Nullary
open import Relation.Unary

module _ {a} {A : Set a} where

gallais

open import Relation.Nullary
open import Agda.Builtin.Equality

data X : Set where
  a b c : X

firstA : (x y z : X) → X
firstA a y z = a
firstA x a z = a
firstA x y a = a

gallais

module Container

%default total

record Container where
  constructor MkContainer
  shape : Type
  position : shape -> Type

container : Container -> Type -> Type

gallais

open import Relation.Binary

module Reasoning {a ℓ₁ ℓ₂ ℓ₃} {A : Set a}
  {_≈_ : Rel A ℓ₁} (≈-trans : Transitive _≈_) (≈-sym   : Symmetric _≈_) (≈-refl : Reflexive _≈_)
  {_≤_ : Rel A ℓ₂} (≤-trans : Transitive _≤_) (≤-respˡ-≈ : _≤_ Respectsˡ _≈_) (≤-respʳ-≈ : _≤_ Respectsʳ _≈_) (≤-refl  : Reflexive _≤_)
  {_<_ : Rel A ℓ₃} (<-trans : Transitive _<_) (<-respˡ-≈ : _<_ Respectsˡ _≈_) (<-respʳ-≈ : _<_ Respectsʳ _≈_) (<⇒≤ : _<_ ⇒ _≤_)
  (<-≤-trans : ∀ {x y z} → x < y → y ≤ z → x < z)
  (≤-<-trans : ∀ {x y z} → x ≤ y → y < z → x < z)
  where

gallais

module bins where

open import Size
open import Codata.Stream
open import Codata.Thunk
open import Data.List.Base as List using (List; _∷_; [])
open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_; [_])
open import Function
open import Relation.Unary

gallais

open import Relation.Binary.PropositionalEquality
open import Relation.Binary.HeterogeneousEquality
open import Data.Maybe
open import Function

cong⁻¹ : ∀ {A B : Set} {a a'} (f : A → Maybe B) →
         (eq : a ≡ a') →
         from-just (f a) ≅ from-just (f a')
cong⁻¹ {a = a} f refl = refl