[new] inital commit

Probably some broken things in this move. Basically collected all the
auxiliary/utility source files from across multiple repos into this one
place. It's hopefully going to be the home for most of my stuff going
forwards.

agda/Algebra/Structures/PartialMonoid.agda

@@ -0,0 +1,69 @@
+{-# OPTIONS --safe --without-K #-}
+module Algebra.Structure.PartialMonoid where
+
+open import Level
+open import Algebra.Core
+open import Data.Product hiding (assocˡ; assocʳ)
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality using (subst; dcong₂; _≡_)
+
+record IsPartialMonoid
+  {a b c} {A : Set a}
+  (_≈_ : Rel A b) (_R_ : Rel A c)
+  (∙ : (x y : A) → x R y → A)
+  (ε : A)
+  : Set (a ⊔ b ⊔ c) where
+
+  private
+    ∙[_] : {x y : A} → x R y → A
+    ∙[_] {x} {y} xy = ∙ x y xy
+
+  field
+    isEquivalence : IsEquivalence _≈_
+    A-set : Irrelevant (_≡_ {A = A})
+    R-prop : Irrelevant _R_
+    ε-compatˡ : ∀ {x} → ε R x
+    ε-compatʳ : ∀ {x} → x R ε
+    identityˡ : ∀ {x} → ∙[ ε-compatˡ {x} ] ≈ x
+    identityʳ : ∀ {x} → ∙[ ε-compatʳ {x} ] ≈ x
+    assocˡ : ∀ {x y z} → (yz : y R z) → (p : x R (∙[ yz ])) → Σ[ xy ∈ x R y ] Σ[ q ∈ ∙[ xy ] R z ] (∙[ p ] ≈ ∙[ q ])
+    assocʳ : ∀ {x y z} → (xy : x R y) → (p : ∙[ xy ] R z) → Σ[ yz ∈ y R z ] Σ[ q ∈ x R ∙[ yz ] ] (∙[ p ] ≈ ∙[ q ])
+
+  assocL1 : ∀ {x y z} → (yz : y R z) → (p : x R (∙[ yz ])) → Σ[ xy ∈ x R y ] (∙[ xy ] R z)
+  assocL1 yz p = let (a , b , _) = assocˡ yz p in a , b
+
+  assocR1 : ∀ {x y z} → (xy : x R y) → (p : ∙[ xy ] R z) → Σ[ yz ∈ y R z ] (x R ∙[ yz ])
+  assocR1 yz p = let (a , b , _) = assocʳ yz p in a , b
+
+  identityˡ' : ∀ {x} (r : ε R x) → ∙[ r ] ≈ x
+  identityˡ' {x} r = subst (λ z → ∙[ z ] ≈ x) (R-prop ε-compatˡ r) identityˡ
+
+  identityʳ' : ∀ {x} (r : x R ε) → ∙[ r ] ≈ x
+  identityʳ' {x} r = subst (λ z → ∙[ z ] ≈ x) (R-prop ε-compatʳ r) identityʳ
+
+  assocˡ₁ : ∀ {x y z} → (yz : y R z) → (p : x R (∙[ yz ])) → x R y
+  assocˡ₁ yz p = let (a , b , _) = assocˡ yz p in a
+
+  assocˡ₃ : ∀ {x y z} → (yz : y R z) → (p : x R (∙[ yz ])) → (xy : x R y) → (q : ∙[ xy ] R z ) → (∙ x (∙ y z yz) p ≈ ∙ (∙ x y xy) z q)
+  assocˡ₃ {x} {y} {z} yx p xy q = subst (λ w → ∙ x (∙ y z yx) p ≈ ∙ (∙ x y (proj₁ w)) z (proj₂ w)) goal (proj₂ (proj₂ (assocˡ yx p)))
+    where
+      goal : (proj₁ (assocˡ yx p) , proj₁ (proj₂ (assocˡ yx p))) ≡ (xy , q)
+      goal = dcong₂ _,_ (R-prop _ xy) (R-prop _ q)
+
+  assocʳ₃ : ∀ {x y z} → (xy : x R y) → (p : ∙[ xy ] R z) → (yz : y R z) (q : x R ∙[ yz ]) → (∙[ p ] ≈ ∙[ q ])
+  assocʳ₃ {x} {y} {z} yx p xy q = subst (λ w → ∙ (∙ x y yx) z p ≈ ∙ x (∙ y z (proj₁ w)) (proj₂ w)) goal (proj₂ (proj₂ (assocʳ yx p)))
+    where
+      goal : (proj₁ (assocʳ yx p) , proj₁ (proj₂ (assocʳ yx p))) ≡ (xy , q)
+      goal = dcong₂ _,_ (R-prop _ xy) (R-prop _ q)
+
+
+record IsReflexivePartialMonoid
+  {a b c} {A : Set a}
+  (_≈_ : Rel A b) (_R_ : Rel A c)
+  (∙ : (x y : A) → x R y → A)
+  (ε : A)
+  : Set (a ⊔ b ⊔ c) where
+  field
+    isPMon : IsPartialMonoid _≈_ _R_ ∙ ε
+    reflexive : ∀ {x} → x R x
+  open IsPartialMonoid isPMon public

agda/Algebra/Structures/Propositional.agda

@@ -0,0 +1,141 @@
+open import Algebra
+open import Data.Product
+open import Relation.Binary hiding (Irrelevant)
+
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Relation.Binary.Structures
+open import Relation.Nullary
+open import Data.Empty
+open import Data.Sum
+
+module Algebra.Structures.Propositional where
+
+record IsPropStrictTotalOrder
+  { S : Set }
+  ( _≈_ : S → S → Set )
+  ( _<_ : S → S → Set )
+  : Set where
+  constructor MkDto
+  field
+    isSTO : IsStrictTotalOrder _≈_ _<_
+    ≈-prop : ∀ {x y} → Irrelevant (x ≈ y)
+    <-prop : ∀ {x y} → Irrelevant (x < y)
+  open IsStrictTotalOrder isSTO public
+
+record IsPropDecTotalOrder
+  { S : Set }
+  ( _≈_ : S → S → Set )
+  ( _≤_ : S → S → Set )
+  : Set where
+  constructor MkDto
+  field
+    isDTO : IsDecTotalOrder _≈_ _≤_
+    ≤-prop : ∀ {x y} → Irrelevant (x ≤ y)
+  open IsDecTotalOrder isDTO public
+
+record IsPropDecTightApartnessRelation
+  { S : Set }
+  ( _≈_ : S → S → Set )
+  (_#_ : S → S → Set )
+  : Set where
+  field
+    isEquivalence : IsEquivalence _≈_
+    isAR : IsApartnessRelation _≈_ _#_
+    prop : ∀ {x y} → Irrelevant (x # y)
+    tight : Tight _≈_ _#_
+    dec : Decidable _#_
+  open IsApartnessRelation isAR public
+  open IsEquivalence isEquivalence renaming (sym to ≈-sym) public
+
+  eqOrApart : (x y : S) → x ≈ y ⊎ x # y
+  eqOrApart x y with dec x y
+  ... | yes x#y = inj₂ x#y
+  ... | no ¬x#y = inj₁ (proj₁ (tight x y) ¬x#y)
+
+
+module _ {X : Set}{_≈_ : X → X → Set}{_#_ : X → X → Set}
+         (isEq : IsEquivalence _≈_)(isAp : IsApartnessRelation _≈_ _#_)
+         (isProp : ∀ {x y} → Irrelevant (x # y))
+       where
+
+  open IsPropDecTightApartnessRelation
+
+  -- An apartness relation is tight and decidable iff it has the
+  -- eqOrApart property. Above we derived it from decidability +
+  -- tightness, here we go the other way.
+  eqOrApart→DecTight : ((x y : X) → x ≈ y ⊎ x # y) → IsPropDecTightApartnessRelation _≈_ _#_
+  isEquivalence (eqOrApart→DecTight p) = isEq
+  isAR (eqOrApart→DecTight p) = isAp
+  prop (eqOrApart→DecTight p) = isProp
+  proj₁ (tight (eqOrApart→DecTight p) x y) ¬x#y with p x y
+  ... | inj₁ x=y = x=y
+  ... | inj₂ x#y = ⊥-elim (¬x#y x#y)
+  proj₂ (tight (eqOrApart→DecTight p) x y) x=y = IsApartnessRelation.irrefl isAp x=y
+  dec (eqOrApart→DecTight p) x y with p x y
+  ... | inj₁ x=y = no (IsApartnessRelation.irrefl isAp x=y)
+  ... | inj₂ x#y = yes x#y
+
+denialApartness : {X : Set} {_≈_ : X → X → Set} → IsEquivalence _≈_ → Decidable _≈_ → IsPropDecTightApartnessRelation {X} _≈_ (λ x y → ¬ x ≈ y)
+denialApartness {X} {_≈_} isEq ≡-dec =
+  eqOrApart→DecTight isEq apartness (λ p q → refl) eqOrApart
+  where
+    apartness : IsApartnessRelation _≈_ (λ x y → x ≈ y → ⊥)
+    IsApartnessRelation.irrefl apartness x≡y ¬x≡y = ¬x≡y x≡y
+    IsApartnessRelation.sym apartness ¬x≡y y≡x = ¬x≡y (IsEquivalence.sym isEq y≡x )
+    IsApartnessRelation.cotrans apartness {x} {y} ¬x≡y z with ≡-dec x z | ≡-dec z y
+    ... | yes x≡z | yes z≡y = ⊥-elim (¬x≡y (IsEquivalence.trans isEq x≡z z≡y))
+    ... | yes x≡z | no ¬z≡y = inj₂ ¬z≡y
+    ... | no ¬x≡z | _ = inj₁ ¬x≡z
+    eqOrApart : (x y : X) → (x ≈ y) ⊎ (x ≈ y → ⊥)
+    eqOrApart x y with ≡-dec x y
+    ... | yes x=y = inj₁ x=y
+    ... | no ¬x=y = inj₂ ¬x=y
+
+-- NB: **Necessarily** strictly ordered when idempotent, non-strict when not.
+record IsOrderedCommutativeMonoid
+  { S : Set }
+  ( _≈_ : S → S → Set )
+  ( _≤_ : S → S → Set )
+  ( _∙_ : S → S → S )
+  ( ε : S )
+  : Set where
+  field
+    isICM : IsCommutativeMonoid _≈_ _∙_ ε
+    isPDTO : IsPropDecTotalOrder _≈_ _≤_
+  open IsPropDecTotalOrder isPDTO
+  open IsCommutativeMonoid isICM hiding (refl; sym; trans) public
+
+record IsOrderedIdempotentCommutativeMonoid
+  { S : Set }
+  ( _≈_ : S → S → Set )
+  ( _<_ : S → S → Set )
+  ( _∙_ : S → S → S )
+  ( ε : S )
+  : Set where
+  field
+    isICM : IsIdempotentCommutativeMonoid _≈_ _∙_ ε
+    isSTO : IsPropStrictTotalOrder _≈_ _<_
+
+    -- This is a sensible thing to ask, but is not true for sorted lists with lexicographic order.
+    -- ∙-preservesˡ-< : ∀ {a b} x → a < b → (x ∙ a) < (x ∙ b)
+
+    -- This is also too strong, but might be an interesting thing to think about.
+    -- ε-minimal : ∀ {a} → ε ≢ a → ε < a
+
+  open IsStrictTotalOrder
+  open IsIdempotentCommutativeMonoid hiding (refl; sym; trans) public
+
+record IsLeftRegularMonoidWithPropDecApartness
+  { S : Set }
+  ( _≈_ : S → S → Set )
+  ( _#_ : S → S → Set )
+  ( _∙_ : S → S → S )
+  ( ε : S )
+  : Set where
+  field
+    isICM : IsMonoid _≈_ _∙_ ε
+    leftregular : (x y : S) → ((x ∙ y) ∙ x) ≈ (x ∙ y)
+    isApartness : IsPropDecTightApartnessRelation _≈_ _#_
+
+  open IsPropDecTightApartnessRelation isApartness public
+  open IsMonoid isICM hiding (refl; sym; trans; reflexive; isPartialEquivalence) public

agda/Axiom/UniquenessOfIdentityProofs/Properties.agda

@@ -0,0 +1,140 @@
+module Axiom.UniquenessOfIdentityProofs.Properties where
+
+open import Axiom.UniquenessOfIdentityProofs
+open import Data.Product
+open import Data.Product.Properties
+open import Data.Sum
+open import Data.Sum.Properties
+open import Data.Unit
+open import Function
+open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Isomorphism
+open import Relation.Nullary
+
+UIP-⊤ : UIP ⊤
+UIP-⊤ {tt} {tt} refl refl = refl
+
+whisker : ∀ {ℓ} {A B : Set ℓ} (f : A -> B)  (g : B -> A)
+        → (α : ∀ x → f (g x) ≡ x) {x y : B} (p : x ≡ y)
+        → p ≡  trans (sym (α x)) (trans (cong f (cong g p)) (α y))
+whisker f g α {x = x} refl = sym (trans-symˡ (α x))
+
+UIP-Retract : ∀ {ℓ} {A B : Set ℓ} (f : A -> B)  (g : B -> A)
+            → (∀ x → f (g x) ≡  x) -> UIP A -> UIP B
+UIP-Retract f g α setA {x = x} {y} p q =
+  begin
+    p
+  ≡⟨ whisker f g α p ⟩
+    trans (sym (α x)) (trans (cong f (cong g p)) (α y))
+  ≡⟨ cong (λ z → trans (sym (α x)) (trans (cong f z) (α y))) (setA (cong g p) (cong g q)) ⟩
+    trans (sym (α x)) (trans (cong f (cong g q)) (α y))
+  ≡⟨ sym (whisker f g α q) ⟩
+    q
+  ∎ where open ≡-Reasoning
+
+-- Propositions have contractible identities
+prop-contr-≡ : ∀ {ℓ} {X : Set ℓ} → Irrelevant X
+             → {x y : X} → Σ[ c ∈ x ≡ y ] ((p : x ≡ y) → c ≡ p)
+prop-contr-≡ {ℓ} {X} propX {x} {y} =
+  (propX x y) ,
+  λ { refl → trans (canon (sym (propX y y))) (trans-symˡ (propX x x)) }
+  where
+    canon : {x y : X} → (p : x ≡ y) → propX x y ≡ trans p (propX y y)
+    canon refl = refl
+
+-- Propositions have UIP
+UIP-prop : ∀ {ℓ} {X : Set ℓ} → Irrelevant X → UIP X
+UIP-prop propX {x} {y} p q = trans (sym (proj₂ (prop-contr-≡ propX) p))
+                                   (proj₂ (prop-contr-≡ propX) q)
+
+-- In particular, if some type X has UIP, then so does its identity type
+-- (and so on, all the way up)
+UIP-≡ : ∀ {ℓ} {X : Set ℓ} → UIP X → (x y : X) → UIP (x ≡ y)
+UIP-≡ uipX x y = UIP-prop uipX
+
+
+
+-- UIP is closed under coproducts
+
+inj₁-lem : ∀ {ℓx ℓy} {X : Set ℓx} {Y : Set ℓy} {x y : X} (p : _≡_ {A = X ⊎ Y} (inj₁ x) (inj₁ y)) → p ≡ cong inj₁ (inj₁-injective p)
+inj₁-lem refl = refl
+
+inj₁-injective-injective : ∀ {ℓx ℓy} {X : Set ℓx} {Y : Set ℓy} {x y : X} (p q : _≡_ {A = X ⊎ Y} (inj₁ x) (inj₁ y)) → inj₁-injective p ≡ inj₁-injective q → p ≡ q
+inj₁-injective-injective p q u = trans (inj₁-lem p) (trans (cong (cong inj₁) u) (sym $ inj₁-lem q))
+
+inj₂-lem : ∀ {ℓx ℓy} {X : Set ℓx} {Y : Set ℓy} {x y : Y} (p : _≡_ {A = X ⊎ Y} (inj₂ x) (inj₂ y)) → p ≡ cong inj₂ (inj₂-injective p)
+inj₂-lem refl = refl
+
+inj₂-injective-injective : ∀ {ℓx ℓy} {X : Set ℓx} {Y : Set ℓy} {x y : Y} (p q : _≡_ {A = X ⊎ Y} (inj₂ x) (inj₂ y)) → inj₂-injective p ≡ inj₂-injective q → p ≡ q
+inj₂-injective-injective p q u = trans (inj₂-lem p) (trans (cong (cong inj₂) u) (sym $ inj₂-lem q))
+
+UIP-⊎ : ∀ {ℓx ℓy} {X : Set ℓx} {Y : Set ℓy} → UIP X → UIP Y → UIP (X ⊎ Y)
+UIP-⊎ uipX uipY {inj₁ x} {inj₁ y} p q = inj₁-injective-injective p q $ uipX (inj₁-injective p) (inj₁-injective q)
+UIP-⊎ uipX uipY {inj₂ x} {inj₂ y} p q = inj₂-injective-injective p q $ uipY (inj₂-injective p) (inj₂-injective q)
+
+
+-- UIP is closed under non-dependent pairs
+
+plumb : ∀ {ℓa ℓb ℓc ℓd} {A : Set ℓa} {B : Set ℓb} {C : A → A → Set ℓc} {D : B → B → Set ℓd}
+      → (f : (x y : A) → C x y) (g : (x y : B) → D x y)
+      → (p q : A × B) → C (proj₁ p) (proj₁ q) × D (proj₂ p) (proj₂ q)
+plumb f g (a1 , b1) (a2 , b2) = f a1 a2 , g b1 b2
+
+,-lem : ∀ {ℓx ℓy} {X : Set ℓx} {Y : Set ℓy} {x1 x2 : X} {y1 y2 : Y} (p : (x1 , y1) ≡ (x2 , y2))
+          → p ≡ cong₂ _,_ (proj₁ $ ,-injective p) (proj₂ $ ,-injective p)
+,-lem refl = refl
+
+repackage : ∀ {ℓx ℓy} {X : Set ℓx} {Y : Set ℓy} {x1 x2 : X} {y1 y2 : Y}
+          → (p q : (x1 , y1) ≡ (x2 , y2))
+          → proj₁ (,-injective p) ≡ proj₁ (,-injective q) × proj₂ (,-injective p) ≡ proj₂ (,-injective q)
+          → p ≡ q
+repackage p q (u , v) = trans (,-lem p) (trans (cong₂ (cong₂ _,_) u v) (sym $ ,-lem q))
+
+UIP-× : ∀ {ℓx ℓy} {X : Set ℓx} {Y : Set ℓy} → UIP X → UIP Y → UIP (X × Y)
+UIP-× uipX uipY {x1 , y1} {x2 , y2} p q = repackage p q $ plumb uipX uipY (,-injective p) (,-injective q)
+
+-- The full, general case:
+-- If both args of a sigma type are always sets, then the sigma type is a set.
+-- ie, UIP is closed under dependent pairs.
+
+cong-, : ∀ {ℓx ℓy} {X : Set ℓx} {Y : X → Set ℓy} {x1 x2 : X} {y1 : Y x1} {y2 : Y x2}
+       → (p : x1 ≡ x2)
+       → subst Y p y1 ≡ y2
+       → (x1 , y1) ≡ (x2 , y2)
+cong-, refl refl = refl
+
+
+cong₂-cong-, : ∀ {ℓx ℓy} {X : Set ℓx} {Y : X → Set ℓy} {x1 x2 : X} {y1 : Y x1} {y2 : Y x2}
+             → {p q : x1 ≡ x2} {p' : subst Y p y1 ≡ y2} {q' : subst Y q y1 ≡ y2}
+             → (eqL : p ≡ q)
+             → subst (λ z → subst Y z y1 ≡ y2) eqL p' ≡ q'
+             → cong-, p p' ≡ cong-, q q'
+cong₂-cong-, refl refl = refl
+
+
+,-lem' : ∀ {ℓx ℓy} {X : Set ℓx} {Y : X → Set ℓy} {x1 x2 : X} {y1 : Y x1} {y2 : Y x2}
+       → (uipX : UIP X) (uipY : ∀ x → UIP (Y x))
+       → (p : (x1 , y1) ≡ (x2 , y2))
+       → p ≡ cong-, (,-injectiveˡ p) (,-injectiveʳ-≡ uipX p (,-injectiveˡ p))
+,-lem' {Y = Y} {x1 = x1} {y1 = y1} uipX uipY refl rewrite UIP-≡ uipX x1 x1 (uipX refl refl) refl = refl
+
+repackage' : ∀ {ℓx ℓy} {X : Set ℓx} {Y : X → Set ℓy} {x1 x2 : X} {y1 : Y x1} {y2 : Y x2}
+           → (uipX : UIP X) (uipY : ∀ x → UIP (Y x))
+           → (p q : (x1 , y1) ≡ (x2 , y2))
+           → (u : ,-injectiveˡ p ≡ ,-injectiveˡ q)
+           → subst (λ z → subst Y z y1 ≡ y2) u (,-injectiveʳ-≡ uipX p (,-injectiveˡ p)) ≡ ,-injectiveʳ-≡ uipX q (,-injectiveˡ q)
+           → p ≡ q
+repackage' uipX uipY p q u v = trans (,-lem' uipX uipY p) (trans (cong₂-cong-, u v) (sym $ ,-lem' uipX uipY q))
+
+UIP-Σ :  ∀ {ℓx ℓy} {X : Set ℓx} {Y : X → Set ℓy} → UIP X
+       → (∀ x → UIP (Y x)) → UIP (Σ[ x ∈ X ] Y x)
+UIP-Σ {Y = Y} uipX uipY {x1 , y1} {x2 , y2} p q
+  = repackage' uipX uipY p q
+               (uipX (,-injectiveˡ p) (,-injectiveˡ q))
+               (uipY x2 (subst (λ z → subst (λ v → Y v) z y1 ≡ y2)
+                        (uipX (,-injectiveˡ p) (,-injectiveˡ q)) (,-injectiveʳ-≡ uipX p (,-injectiveˡ p))) (,-injectiveʳ-≡ uipX q (,-injectiveˡ q)))
+
+-- Lemma: UIP is preserved by isomorphism.
+UIP-≃ : ∀ {ℓ} {X : Set ℓ} {Y : Set ℓ} → UIP X → X ≃ Y → UIP Y
+UIP-≃ uipX iso = UIP-Retract (to iso) (from iso) (λ y → sym (to-from iso y)) uipX
+  where open _≃_

agda/Bug/mutual.agda

@@ -0,0 +1,33 @@
+{-# OPTIONS --safe #-}
+
+open import Function.Base using (_∘_)
+open import Data.Unit.Base using (⊤; tt)
+
+module bug where
+
+record WTy : Set
+
+TyFwd : WTy
+
+data WExpBase : WTy → Set
+
+record WTy where
+  -- inductive
+  constructor Is
+  field
+    inner : WExpBase TyFwd
+
+WExp : WExpBase TyFwd → Set
+WExp = WExpBase ∘ Is
+
+
+data WExpBase where
+  Ty    : WExpBase TyFwd
+  _-_  : WExpBase TyFwd → WExpBase TyFwd → WExpBase TyFwd
+
+TyFwd = Is Ty
+
+infixr 1 _-_
+
+foo : ∀ {a} → WExp a → ⊤
+foo Ty = tt