text:
open import Relation.Binary.Core

module PLRTree.Insert.Complete {A : Set}
                     (_≤_ : A → A → Set)
                     (tot≤ : Total _≤_) where

open import Data.Empty
open import Data.Sum renaming (_⊎_ to _∨_)
open import PLRTree {A}
open import PLRTree.Compound {A}
open import PLRTree.Insert _≤_ tot≤
open import PLRTree.Insert.Properties _≤_ tot≤
open import PLRTree.Complete {A}
open import PLRTree.Complete.Properties {A}
open import PLRTree.Equality {A}
open import PLRTree.Equality.Properties {A}

lemma-≃-⊥ : {l : PLRTree}(x : A) → l ≃ insert x l → ⊥
lemma-≃-⊥ {leaf} _ ()
lemma-≃-⊥ {node perfect x' l' r'} x l≃lᵢ
    with tot≤ x x' | l' | r' | l≃lᵢ
... | inj₁ x≤x' | leaf | leaf | ()
... | inj₁ x≤x' | leaf | node _ _ _ _ | ()
... | inj₁ x≤x' | node _ _ _ _ | leaf | ()
... | inj₁ x≤x' | node _ _ _ _ | node _ _ _ _ | ()
... | inj₂ x'≤x | leaf | leaf | ()
... | inj₂ x'≤x | leaf | node _ _ _ _ | ()
... | inj₂ x'≤x | node _ _ _ _ | leaf | ()
... | inj₂ x'≤x | node _ _ _ _ | node _ _ _ _ | ()
lemma-≃-⊥ {node left _ _ _} _ ()
lemma-≃-⊥ {node right _ _ _} _ ()

lemma-⋗-⊥ : {l : PLRTree}(x : A) → l ⋗ insert x l → ⊥
lemma-⋗-⊥ {leaf} _ ()
lemma-⋗-⊥ {node perfect x' l' r'} x l⋗lᵢ
    with tot≤ x x' | l' | r' | l⋗lᵢ
... | inj₁ x≤x' | leaf | leaf | ()
... | inj₁ x≤x' | leaf | node _ _ _ _ | ()
... | inj₁ x≤x' | node _ _ _ _ | leaf | ()
... | inj₁ x≤x' | node _ _ _ _ | node _ _ _ _ | ()
... | inj₂ x'≤x | leaf | leaf | ()
... | inj₂ x'≤x | leaf | node _ _ _ _ | ()
... | inj₂ x'≤x | node _ _ _ _ | leaf | ()
... | inj₂ x'≤x | node _ _ _ _ | node _ _ _ _ | ()
lemma-⋗-⊥ {node left _ _ _} _ ()
lemma-⋗-⊥ {node right _ _ _} _ ()

lemma-⋙-⊥ : {l r : PLRTree}(x : A) → l ⋙ r → l ⋗ insert x r → ⊥
lemma-⋙-⊥ x (⋙p l⋗r) l⋗rᵢ = lemma-≃-⊥ x (lemma-⋗* l⋗r l⋗rᵢ)
lemma-⋙-⊥ x (⋙l {l' = l''} y' y'' l'≃r' l''⋘r'' l'⋗r'') l⋗rᵢ
    with tot≤ x y''
... | inj₁ x≤y''
    with insert y'' l'' | lemma-insert-compound y'' l'' | l⋗rᵢ
... | node perfect _ _ _ | compound | ()
... | node left _ _ _ | compound | ()
... | node right _ _ _ | compound | ()
lemma-⋙-⊥ x (⋙l {l' = l''} y' y'' l'≃r' l''⋘r'' l'⋗r'') l⋗rᵢ | inj₂ y''≤x
    with insert x l'' | lemma-insert-compound x l'' | l⋗rᵢ
... | node perfect _ _ _ | compound | ()
... | node left _ _ _ | compound | ()
... | node right _ _ _ | compound | ()
lemma-⋙-⊥ x (⋙r {r' = r''} y' y'' l'≃r' l''⋙r'' l'≃l'') l⋗rᵢ
    with tot≤ x y''
... | inj₁ x≤y''
    with insert y'' r'' | lemma-insert-compound y'' r'' | l⋗rᵢ
... | node perfect _ _ _ | compound | ⋗nd .y' .x _ l''≃r''ᵢ l'⋗l'' = lemma-⋗refl-⊥ (lemma-⋗-≃ l'⋗l'' (sym≃ l'≃l''))
... | node left _ _ _ | compound | ()
... | node right _ _ _ | compound | ()
lemma-⋙-⊥ x (⋙r {r' = r''} y' y'' l'≃r' l''⋙r'' l'≃l'') l⋗rᵢ | inj₂ y''≤x
    with insert x r'' | lemma-insert-compound x r'' | l⋗rᵢ
... | node perfect _ _ _ | compound | ⋗nd .y' .y'' _ l''≃r''ᵢ l'⋗l'' = lemma-⋗refl-⊥ (lemma-⋗-≃ l'⋗l'' (sym≃ l'≃l''))
... | node left _ _ _ | compound | ()
... | node right _ _ _ | compound | ()

lemma-insert-≃ : {l r : PLRTree}{x : A} → Compound l → l ≃ r → insert x l ⋘ r
lemma-insert-≃ {node perfect y l r} {node perfect y' l' r'} {x} compound (≃nd .y .y' l≃r l'≃r' l≃l')
    with tot≤ x y | l | r | l≃r | l' | l≃l'
... | inj₁ x≤y | leaf | leaf | ≃lf | leaf | ≃lf = r⋘ x y' (⋙p (⋗lf y)) l'≃r' (⋗lf y)
... | inj₁ x≤y | node perfect z₁ _ _ | node perfect z₂ _ _ | ≃nd .z₁ .z₂ l₁≃r₁ l₂≃r₂ l₁≃l₂ | node perfect z₃ _ _ | ≃nd .z₁ .z₃ _ l₃≃r₃ l₁≃l₃
                                           = l⋘ x y' (lemma-insert-≃ compound (≃nd z₁ z₂ l₁≃r₁ l₂≃r₂ l₁≃l₂)) l'≃r' (≃nd z₂ z₃ l₂≃r₂ l₃≃r₃ (trans≃ (sym≃ l₁≃l₂) l₁≃l₃))
... | inj₂ y≤x | leaf | leaf | ≃lf | leaf | ≃lf = r⋘ y y' (⋙p (⋗lf x)) l'≃r' (⋗lf x)
... | inj₂ y≤x |  node perfect z₁ _ _ | node perfect z₂ _ _ | ≃nd .z₁ .z₂ l₁≃r₁ l₂≃r₂ l₁≃l₂ | node perfect z₃ _ _ | ≃nd .z₁ .z₃ _ l₃≃r₃ l₁≃l₃
                                           = l⋘ y y' (lemma-insert-≃ compound (≃nd z₁ z₂ l₁≃r₁ l₂≃r₂ l₁≃l₂)) l'≃r' (≃nd z₂ z₃ l₂≃r₂ l₃≃r₃ (trans≃ (sym≃ l₁≃l₂) l₁≃l₃))

lemma-insert-⋗' : {l r : PLRTree}(x : A) → l ⋗ r → Compound r → l ⋙ (insert x r)
lemma-insert-⋗' x (⋗nd {l} {r} {l'} {r'} y y' l≃r l'≃r' l⋗l') compound
    with tot≤ x y' | l' | r' | l'≃r' | l | l⋗l'
... | inj₁ x≤y' | leaf | leaf | ≃lf | node perfect x₁ leaf leaf | ⋗lf .x₁ = ⋙r y x l≃r (⋙p (⋗lf y')) (≃nd x₁ y' ≃lf ≃lf ≃lf)
... | inj₁ x≤y' | node perfect x₃ l₃ r₃ | node perfect x₄ l₄ r₄ | ≃nd .x₃ .x₄ l₃≃r₃ l₄≃r₄ l₃≃l₄ | node perfect x₁ l₁ r₁ | ⋗nd .x₁ .x₃ l₁≃r₁ _ l₁⋗l₃
    with tot≤ y' x₃ | l₃ | r₃ | l₃≃r₃ | l₁ | l₁⋗l₃
... | inj₁ y'≤x₃ | leaf | leaf | ≃lf | node perfect x'₁ leaf leaf | ⋗lf .x'₁
    with l₄ | l₃≃l₄
... | leaf | ≃lf =
                let _l'ᵢ⋘r' = r⋘ y' x₄ (⋙p (⋗lf x₃)) l₄≃r₄ (⋗lf x₃) ;
                     _l⋗r' = lemma-⋗-≃ (⋗nd x₁ y' l₁≃r₁ ≃lf (⋗lf x'₁)) (≃nd y' x₄ ≃lf l₄≃r₄ ≃lf)
                in ⋙l y x l≃r _l'ᵢ⋘r' _l⋗r'
lemma-insert-⋗' x (⋗nd y y' l≃r _ _) compound | inj₁ x≤y' | node perfect x₃ _ _ | node perfect x₄ _ _ | ≃nd .x₃ .x₄ _ l₄≃r₄ l₃≃l₄ | node perfect x₁ _ _ | ⋗nd .x₁ .x₃ l₁≃r₁ _ _ | inj₁ y'≤x₃ | node perfect x'₅ _ _ | node perfect x'₆ _ _ | ≃nd .x'₅ .x'₆  l'₅≃r'₅ l'₆≃r'₆ l'₅≃l'₆ | node perfect x'₁ _ _ | ⋗nd .x'₁ .x'₅ l'₁≃r'₁ _ l'₁⋗l'₅
    with lemma-⋙-⋗ (lemma-insert-⋗' x₃  (⋗nd x'₁ x'₅ l'₁≃r'₁ l'₅≃r'₅ l'₁⋗l'₅) compound) (lemma-⋗-≃ (⋗nd x'₁ x'₅ l'₁≃r'₁ l'₅≃r'₅ l'₁⋗l'₅) (≃nd x'₅ x'₆ l'₅≃r'₅ l'₆≃r'₆ l'₅≃l'₆))
... | inj₁ _l₃ᵢ⋘r₃ =
                let _l₁⋗l₃ = ⋗nd x'₁ x'₅ l'₁≃r'₁ l'₅≃r'₅ l'₁⋗l'₅ ;
                     _l₃≃r₃ = ≃nd x'₅ x'₆ l'₅≃r'₅ l'₆≃r'₆ l'₅≃l'₆ ;
                     _l'ᵢ⋘r' = l⋘ y' x₄ _l₃ᵢ⋘r₃  l₄≃r₄ (trans≃ (sym≃ _l₃≃r₃) l₃≃l₄) ;
                     _l⋗r' = lemma-⋗-≃ (⋗nd x₁ x₃ l₁≃r₁ _l₃≃r₃ _l₁⋗l₃) (≃nd x₃ x₄ _l₃≃r₃ l₄≃r₄ l₃≃l₄)
                in ⋙l y x l≃r _l'ᵢ⋘r' _l⋗r'
... | inj₂ _l₃ᵢ≃r₃
    with lemma-≃-⊥ x₃ (trans≃ (≃nd x'₅ x'₆ l'₅≃r'₅ l'₆≃r'₆ l'₅≃l'₆ ) (sym≃ _l₃ᵢ≃r₃))
... | ()
lemma-insert-⋗' x (⋗nd y y' l≃r _ _) compound | inj₁ x≤y' | node perfect x₃ _ _ | node perfect x₄ l₄ _ | ≃nd .x₃ .x₄ _ l₄≃r₄ l₃≃l₄ | node perfect x₁ _ _ | ⋗nd .x₁ .x₃ l₁≃r₁ _ l₁⋗l₃ | inj₂ x₃≤y' | leaf | leaf | ≃lf | node perfect x'₁ leaf leaf | ⋗lf .x'₁
    with l₄ | l₃≃l₄
... | leaf | ≃lf =
                let _l'ᵢ⋘r' = r⋘ x₃ x₄ (⋙p (⋗lf y')) l₄≃r₄ (⋗lf y') ;
                     _l⋗r' = lemma-⋗-≃ (⋗nd x₁ x₃ l₁≃r₁ ≃lf (⋗lf x'₁)) (≃nd x₃ x₄ ≃lf l₄≃r₄ ≃lf)
                in ⋙l y x l≃r _l'ᵢ⋘r' _l⋗r'
lemma-insert-⋗' x (⋗nd y y' l≃r _ _) compound | inj₁ x≤y' | node perfect x₃ _ _ | node perfect x₄ _ _ | ≃nd .x₃ .x₄ l₃≃r₃ l₄≃r₄ l₃≃l₄ | node perfect x₁ _ _ | ⋗nd .x₁ .x₃ l₁≃r₁ _ l₁⋗l₃ | inj₂ x₃≤y' | node perfect x'₅ _ _ | node perfect x'₆ _ _ | ≃nd .x'₅ .x'₆ l'₅≃r'₅ l'₆≃r'₆ l'₅≃l'₆ | node perfect x'₁ _ _ | ⋗nd .x'₁ .x'₅ l'₁≃r'₁ _ l'₁⋗l'₅
    with lemma-⋙-⋗ (lemma-insert-⋗' y'  (⋗nd x'₁ x'₅ l'₁≃r'₁ l'₅≃r'₅ l'₁⋗l'₅) compound) (lemma-⋗-≃ (⋗nd x'₁ x'₅ l'₁≃r'₁ l'₅≃r'₅ l'₁⋗l'₅) (≃nd x'₅ x'₆ l'₅≃r'₅ l'₆≃r'₆ l'₅≃l'₆))
... | inj₁ _l₃ᵢ⋘r₃ =
                let _l₁⋗l₃ = ⋗nd x'₁ x'₅ l'₁≃r'₁ l'₅≃r'₅ l'₁⋗l'₅ ;
                     _l₃≃r₃ = ≃nd x'₅ x'₆ l'₅≃r'₅ l'₆≃r'₆ l'₅≃l'₆ ;
                     _l'ᵢ⋘r' = l⋘ x₃ x₄ _l₃ᵢ⋘r₃  l₄≃r₄ (trans≃ (sym≃ _l₃≃r₃) l₃≃l₄) ;
                     _l⋗r' = lemma-⋗-≃ (⋗nd x₁ x₃ l₁≃r₁ _l₃≃r₃ _l₁⋗l₃) (≃nd x₃ x₄ _l₃≃r₃ l₄≃r₄ l₃≃l₄)
                in ⋙l y x l≃r _l'ᵢ⋘r' _l⋗r'
... | inj₂ _l₃ᵢ≃r₃
    with lemma-≃-⊥ y' (trans≃ (≃nd x'₅ x'₆ l'₅≃r'₅ l'₆≃r'₆ l'₅≃l'₆ ) (sym≃ _l₃ᵢ≃r₃))
... | ()
lemma-insert-⋗' x (⋗nd y y' l≃r l'≃r' l⋗l') compound | inj₂ y'≤x | leaf | leaf | ≃lf | node perfect x₁ leaf leaf | ⋗lf .x₁ = ⋙r y y' l≃r (⋙p (⋗lf x)) (≃nd x₁ x ≃lf ≃lf ≃lf)
lemma-insert-⋗' x (⋗nd y y' l≃r _ _) compound | inj₂ y'≤x | node perfect x₃ l₃ r₃ | node perfect x₄ l₄ _ | ≃nd .x₃ .x₄ l₃≃r₃ l₄≃r₄ l₃≃l₄ | node perfect x₁ l₁ _ | ⋗nd .x₁ .x₃ l₁≃r₁ _ l₁⋗l₃
    with tot≤ x x₃ | l₃ | r₃ | l₃≃r₃ | l₁ | l₁⋗l₃
... | inj₁ x≤x₃ | leaf | leaf | ≃lf | node perfect x'₁ leaf leaf | ⋗lf .x'₁
    with l₄ | l₃≃l₄
... | leaf | ≃lf =
                let _l'ᵢ⋘r' = r⋘ x x₄ (⋙p (⋗lf x₃)) l₄≃r₄ (⋗lf x₃) ;
                     _l⋗r' = lemma-⋗-≃ (⋗nd x₁ x l₁≃r₁ ≃lf (⋗lf x'₁)) (≃nd x x₄ ≃lf l₄≃r₄ ≃lf)
                in ⋙l y y' l≃r _l'ᵢ⋘r' _l⋗r'
lemma-insert-⋗' x (⋗nd y y' l≃r _ _) compound | inj₂ y'≤x | node perfect x₃ _ _ | node perfect x₄ _ _ | ≃nd .x₃ .x₄ _ l₄≃r₄ l₃≃l₄ | node perfect x₁ _ _ | ⋗nd .x₁ .x₃ l₁≃r₁ _ _ | inj₁ x≤x₃ | node perfect x'₅ _ _ | node perfect x'₆ _ _ | ≃nd .x'₅ .x'₆  l'₅≃r'₅ l'₆≃r'₆ l'₅≃l'₆ | node perfect x'₁ _ _ | ⋗nd .x'₁ .x'₅ l'₁≃r'₁ _ l'₁⋗l'₅
    with lemma-⋙-⋗ (lemma-insert-⋗' x₃ (⋗nd x'₁ x'₅ l'₁≃r'₁ l'₅≃r'₅ l'₁⋗l'₅) compound) (lemma-⋗-≃ (⋗nd x'₁ x'₅ l'₁≃r'₁ l'₅≃r'₅ l'₁⋗l'₅) (≃nd x'₅ x'₆ l'₅≃r'₅ l'₆≃r'₆ l'₅≃l'₆))
... | inj₁ _l₃ᵢ⋘r₃ =
                let _l₁⋗l₃ = ⋗nd x'₁ x'₅ l'₁≃r'₁ l'₅≃r'₅ l'₁⋗l'₅ ;
                     _l₃≃r₃ = ≃nd x'₅ x'₆ l'₅≃r'₅ l'₆≃r'₆ l'₅≃l'₆ ;
                     _l'ᵢ⋘r' = l⋘ x x₄ _l₃ᵢ⋘r₃ l₄≃r₄ (trans≃ (sym≃ _l₃≃r₃) l₃≃l₄) ;
                     _l⋗r' = lemma-⋗-≃ (⋗nd x₁ x₃ l₁≃r₁ _l₃≃r₃ _l₁⋗l₃) (≃nd x₃ x₄ _l₃≃r₃ l₄≃r₄ l₃≃l₄)
                in ⋙l y y' l≃r _l'ᵢ⋘r' _l⋗r'
... | inj₂ _l₃ᵢ≃r₃
    with lemma-≃-⊥ x₃ (trans≃ (≃nd x'₅ x'₆ l'₅≃r'₅ l'₆≃r'₆ l'₅≃l'₆ ) (sym≃ _l₃ᵢ≃r₃))
... | ()
lemma-insert-⋗' x (⋗nd y y' l≃r _ _) compound | inj₂ y'≤x | node perfect x₃ _ _ | node perfect x₄ l₄ _ | ≃nd .x₃ .x₄ _ l₄≃r₄ l₃≃l₄ | node perfect x₁ _ _ | ⋗nd .x₁ .x₃ l₁≃r₁ _ _ | inj₂ x₃≤x | leaf | leaf | ≃lf | node perfect x'₁ leaf leaf | ⋗lf .x'₁
    with l₄ | l₃≃l₄
... | leaf | ≃lf =
                let _l'ᵢ⋘r' = r⋘ x₃ x₄ (⋙p (⋗lf x)) l₄≃r₄ (⋗lf x) ;
                     _l⋗r' = lemma-⋗-≃ (⋗nd x₁ x₃ l₁≃r₁ ≃lf (⋗lf x'₁)) (≃nd x₃ x₄ ≃lf l₄≃r₄ ≃lf)
                in ⋙l y y' l≃r _l'ᵢ⋘r' _l⋗r'
lemma-insert-⋗' x (⋗nd y y' l≃r _ _) compound | inj₂ y'≤x | node perfect x₃ _ _ | node perfect x₄ _ _ | ≃nd .x₃ .x₄ _ l₄≃r₄ l₃≃l₄ | node perfect x₁ _ _ | ⋗nd .x₁ .x₃ l₁≃r₁ _ _ | inj₂ x₃≤x | node perfect x'₅ _ _ | node perfect x'₆ _ _ | ≃nd .x'₅ .x'₆ l'₅≃r'₅ l'₆≃r'₆ l'₅≃l'₆ | node perfect x'₁ _ _ | ⋗nd .x'₁ .x'₅ l'₁≃r'₁ _ l'₁⋗l'₅
    with  lemma-⋙-⋗ (lemma-insert-⋗' x (⋗nd x'₁ x'₅ l'₁≃r'₁ l'₅≃r'₅ l'₁⋗l'₅) compound) (lemma-⋗-≃ (⋗nd x'₁ x'₅ l'₁≃r'₁ l'₅≃r'₅ l'₁⋗l'₅) (≃nd x'₅ x'₆ l'₅≃r'₅ l'₆≃r'₆ l'₅≃l'₆))
... | inj₁ _l₃ᵢ⋘r₃ =
                let _l₁⋗l₃ = ⋗nd x'₁ x'₅ l'₁≃r'₁ l'₅≃r'₅ l'₁⋗l'₅ ;
                     _l₃≃r₃ = ≃nd x'₅ x'₆ l'₅≃r'₅ l'₆≃r'₆ l'₅≃l'₆ ;
                     _l'ᵢ⋘r' = l⋘ x₃ x₄ _l₃ᵢ⋘r₃  l₄≃r₄ (trans≃ (sym≃ _l₃≃r₃) l₃≃l₄) ;
                     _l⋗r' = lemma-⋗-≃ (⋗nd x₁ x₃ l₁≃r₁ _l₃≃r₃ _l₁⋗l₃) (≃nd x₃ x₄ _l₃≃r₃ l₄≃r₄ l₃≃l₄)
                in ⋙l y y' l≃r _l'ᵢ⋘r' _l⋗r'
... | inj₂ _l₃ᵢ≃r₃
    with lemma-≃-⊥ x (trans≃ (≃nd x'₅ x'₆ l'₅≃r'₅ l'₆≃r'₆ l'₅≃l'₆) (sym≃ _l₃ᵢ≃r₃))
... | ()

lemma-insert-⋗ : {l r : PLRTree}(x : A) → l ⋗ r → l ⋙ (insert x r) ∨ l ≃ (insert x r)
lemma-insert-⋗ x (⋗lf y) = inj₂ (≃nd y x ≃lf ≃lf ≃lf)
lemma-insert-⋗ x (⋗nd y y' l≃r l'≃r' l⋗l') = inj₁ (lemma-insert-⋗' x (⋗nd y y' l≃r l'≃r' l⋗l') compound)

mutual
  lemma-insert-⋘ : {l r : PLRTree}(x : A) → l ⋘ r → (insert x l) ⋘ r ∨ (insert x l) ⋗ r
  lemma-insert-⋘ x (x⋘ u v w)
      with tot≤ x u
  ... | inj₁ x≤u = inj₂ (⋗nd x w (≃nd v u ≃lf ≃lf ≃lf) ≃lf (⋗lf v))
  ... | inj₂ u≤x = inj₂ (⋗nd u w (≃nd v x ≃lf ≃lf ≃lf) ≃lf (⋗lf v))
  lemma-insert-⋘ x (l⋘ {l = l} y y' l⋘r l'≃r' r≃l')
      with tot≤ x y
  ... | inj₁ x≤y
      with insert y l | lemma-insert-compound y l | lemma-insert-⋘ y l⋘r
  ... | node left _ _ _ | compound | inj₁ lᵢ⋘r  = inj₁ (l⋘ x y' lᵢ⋘r l'≃r' r≃l')
  ... | node left _ _ _ | compound | inj₂ ()
  ... | node right _ _ _ | compound | inj₁ lᵢ⋙r  = inj₁ (l⋘ x y' lᵢ⋙r l'≃r' r≃l')
  ... | node right _ _ _ | compound | inj₂ ()
  ... | node perfect _ _ _ | compound | inj₂ lᵢ⋗r  = inj₁ (r⋘ x y' (⋙p lᵢ⋗r) l'≃r' (lemma-⋗-≃ lᵢ⋗r r≃l'))
  ... | node perfect _ _ _ | compound | inj₁ ()
  lemma-insert-⋘ x (l⋘ {l = l} y y' l⋘r l'≃r' r≃l') | inj₂ y≤x
      with insert x l | lemma-insert-compound x l | lemma-insert-⋘ x l⋘r
  ... | node left _ _ _ | compound | inj₁ lᵢ⋘r  = inj₁ (l⋘ y y' lᵢ⋘r l'≃r' r≃l')
  ... | node left _ _ _ | compound | inj₂ ()
  ... | node right _ _ _ | compound | inj₁ lᵢ⋘r  = inj₁ (l⋘ y y' lᵢ⋘r l'≃r' r≃l')
  ... | node right _ _ _ | compound | inj₂ ()
  ... | node perfect _ _ _ | compound | inj₂ lᵢ⋗r  = inj₁ (r⋘ y y' (⋙p lᵢ⋗r) l'≃r' (lemma-⋗-≃ lᵢ⋗r r≃l'))
  ... | node perfect _ _ _ | compound | inj₁ ()
  lemma-insert-⋘ x (r⋘ {r = r} y y' l⋙r l'≃r' l⋗l')
      with tot≤ x y
  ... | inj₁ x≤y
      with insert y r | lemma-insert-compound y r | lemma-insert-⋙ y l⋙r |  lemma-⋙-⊥ y l⋙r
  ... | node left _ _ _ | compound | inj₁ l⋙rᵢ | _ = inj₁ (r⋘ x y' l⋙rᵢ l'≃r' l⋗l')
  ... | node left _ _ _ | compound | inj₂ () | _
  ... | node right _ _ _ | compound | inj₁ l⋙rᵢ | _ = inj₁ (r⋘ x y' l⋙rᵢ l'≃r' l⋗l')
  ... | node right _ _ _ | compound | inj₂ () | _
  ... | node perfect _ _ _ | compound | inj₂ l≃rᵢ | _ = inj₂ (⋗nd x y' l≃rᵢ l'≃r' l⋗l')
  ... | node perfect _ _ _ | compound | inj₁ (⋙p l⋗rᵢ) | lemma-⋙-⊥'
      with lemma-⋙-⊥' l⋗rᵢ
  ... | ()
  lemma-insert-⋘ x (r⋘ {r = r} y y' l⋙r l'≃r' l⋗l') | inj₂ y'≤x
      with insert x r | lemma-insert-compound x r | lemma-insert-⋙ x l⋙r |  lemma-⋙-⊥ x l⋙r
  ... | node left _ _ _ | compound | inj₁ l⋙rᵢ | _ = inj₁ (r⋘ y y' l⋙rᵢ l'≃r' l⋗l')
  ... | node left _ _ _ | compound | inj₂ () | _
  ... | node right _ _ _ | compound | inj₁ l⋙rᵢ | _ = inj₁ (r⋘ y y' l⋙rᵢ l'≃r' l⋗l')
  ... | node right _ _ _ | compound | inj₂ () | _
  ... | node perfect _ _ _ | compound | inj₂ l≃rᵢ | _ = inj₂ (⋗nd y y' l≃rᵢ l'≃r' l⋗l')
  ... | node perfect _ _ _ | compound | inj₁ (⋙p l⋗rᵢ) | lemma-⋙-⊥'
      with lemma-⋙-⊥' l⋗rᵢ
  ... | ()

  lemma-insert-⋙ : {l r : PLRTree}(x : A) → l ⋙ r → l ⋙ (insert x r) ∨ l ≃ (insert x r)
  lemma-insert-⋙ x (⋙p l⋗r) = lemma-insert-⋗ x l⋗r
  lemma-insert-⋙ x (⋙l {l' = l'} y y' l≃r l'⋘r' l⋗r')
      with tot≤ x y'
  ... | inj₁ x≤y'
      with insert y' l' | lemma-insert-compound y' l' | lemma-insert-⋘ y' l'⋘r'
  ... | node left _ _ _ | compound | inj₁ l'ᵢ⋘r' = inj₁ (⋙l y x l≃r l'ᵢ⋘r' l⋗r')
  ... | node left _ _ _ | compound | inj₂ ()
  ... | node right _ _ _ | compound | inj₁ l'ᵢ⋙r' = inj₁ (⋙l y x l≃r l'ᵢ⋙r' l⋗r')
  ... | node right _ _ _ | compound | inj₂ ()
  ... | node perfect _ _ _ | compound | inj₂ l'ᵢ⋗r' = inj₁ (⋙r y x l≃r (⋙p l'ᵢ⋗r') (lemma-*⋗ l⋗r' l'ᵢ⋗r'))
  ... | node perfect _ _ _ | compound | inj₁ ()
  lemma-insert-⋙ x (⋙l {l' = l'} y y' l≃r l'⋘r' l⋗r') | inj₂ y'≤x
      with insert x l' | lemma-insert-compound x l' | lemma-insert-⋘ x l'⋘r'
  ... | node left _ _ _ | compound | inj₁ l'ᵢ⋘r' = inj₁ (⋙l y y' l≃r l'ᵢ⋘r' l⋗r')
  ... | node left _ _ _ | compound | inj₂ ()
  ... | node right _ _ _ | compound | inj₁ l'ᵢ⋘r' = inj₁ (⋙l y y' l≃r l'ᵢ⋘r' l⋗r')
  ... | node right _ _ _ | compound | inj₂ ()
  ... | node perfect _ _ _ | compound | inj₂ l'ᵢ⋗r' = inj₁ (⋙r y y' l≃r (⋙p l'ᵢ⋗r') (lemma-*⋗ l⋗r' l'ᵢ⋗r'))
  ... | node perfect _ _ _ | compound | inj₁ ()
  lemma-insert-⋙ x (⋙r {r' = r'} y y' l≃r l'⋙r' l≃l')
      with tot≤ x y'
  ... | inj₁ x≤y'
      with insert y' r' | lemma-insert-compound y' r' | lemma-insert-⋙ y' l'⋙r' |  lemma-⋙-⊥ y' l'⋙r'
  ... | node left _ _ _ | compound | inj₁ l'⋙r'ᵢ | _ = inj₁ (⋙r y x l≃r l'⋙r'ᵢ l≃l')
  ... | node left _ _ _ | compound | inj₂ () | _
  ... | node right _ _ _ | compound | inj₁ l'⋙r'ᵢ | _ = inj₁ (⋙r y x l≃r l'⋙r'ᵢ l≃l')
  ... | node right _ _ _ | compound | inj₂ () | _
  ... | node perfect _ _ _ | compound | inj₂ l'≃r'ᵢ | _ = inj₂ (≃nd y x l≃r l'≃r'ᵢ l≃l')
  ... | node perfect _ _ _ | compound | inj₁ (⋙p l'⋗r'ᵢ) | lemma-⋙-⊥'
      with lemma-⋙-⊥' l'⋗r'ᵢ
  ... | ()
  lemma-insert-⋙ x (⋙r {r' = r'} y y' l≃r l'⋙r' l≃l') | inj₂ y'≤x
      with insert x r' | lemma-insert-compound x r' | lemma-insert-⋙ x l'⋙r' |  lemma-⋙-⊥ x l'⋙r'
  ... | node left _ _ _ | compound | inj₁ l'⋙r'ᵢ | _ = inj₁ (⋙r y y' l≃r l'⋙r'ᵢ l≃l')
  ... | node left _ _ _ | compound | inj₂ () | _
  ... | node right _ _ _ | compound | inj₁ l'⋙r'ᵢ | _ = inj₁ (⋙r y y' l≃r l'⋙r'ᵢ l≃l')
  ... | node right _ _ _ | compound | inj₂ () | _
  ... | node perfect _ _ _ | compound | inj₂ l'≃r'ᵢ | _ = inj₂ (≃nd y y' l≃r l'≃r'ᵢ l≃l')
  ... | node perfect _ _ _ | compound | inj₁ (⋙p l'⋗r'ᵢ) | lemma-⋙-⊥'
      with lemma-⋙-⊥' l'⋗r'ᵢ
  ... | ()

lemma-insert-complete : {t : PLRTree}(x : A) → Complete t → Complete (insert x t)
lemma-insert-complete x leaf = perfect x leaf leaf ≃lf
lemma-insert-complete x (perfect {l} {r} y cl cr l≃r)
    with tot≤ x y | l | r | l≃r | lemma-insert-complete y cl | lemma-insert-complete x cl
... | inj₁ x≤y | leaf | leaf | ≃lf | _ | _ = right x (perfect y cr cr ≃lf) cr (⋙p (⋗lf y))
... | inj₁ x≤y | node perfect z' _ _ | node perfect z'' _ _ | ≃nd .z' .z'' l'≃r' l''≃r'' l'≃l'' | clᵢ | _ = left x clᵢ cr (lemma-insert-≃ compound (≃nd z' z'' l'≃r' l''≃r'' l'≃l''))
... | inj₂ y≤x | leaf | leaf | ≃lf | _ | _ = right y (perfect x cr cr ≃lf) cr (⋙p (⋗lf x))
... | inj₂ y≤x | node perfect z' _ _ | node perfect z'' _ _ | ≃nd .z' .z'' l'≃r' l''≃r'' l'≃l'' | _ | clᵢ = left y clᵢ cr (lemma-insert-≃ compound (≃nd z' z'' l'≃r' l''≃r'' l'≃l''))
lemma-insert-complete x (left {l} {r} y cl cr l⋘r)
    with tot≤ x y
... | inj₁ x≤y
    with insert y l | lemma-insert-complete y cl | lemma-insert-⋘ y l⋘r | lemma-insert-compound y l
... | node left _ _ _ | clᵢ | inj₁ lᵢ⋘r | compound = left x clᵢ cr lᵢ⋘r
... | node right _ _ _ | clᵢ | inj₁ lᵢ⋘r | compound = left x clᵢ cr lᵢ⋘r
... | node left _ _ _ | _ | inj₂ () | compound
... | node right _ _ _ | _ | inj₂ () | compound
... | node perfect _ _ _ | clᵢ | inj₂ lᵢ⋗r | compound = right x clᵢ cr (⋙p lᵢ⋗r)
... | node perfect x' l' r' | perfect .x' cl' cr' l'≃r' | inj₁ () | compound
lemma-insert-complete x (left {l} {r} y cl cr l⋘r) | inj₂ y≤x
    with insert x l |  lemma-insert-complete x cl | lemma-insert-⋘ x l⋘r | lemma-insert-compound x l
... | node left _ _ _ | clᵢ | inj₁ lᵢ⋘r | compound  = left y clᵢ cr lᵢ⋘r
... | node right _ _ _ | clᵢ | inj₁ lᵢ⋘r | compound  = left y clᵢ cr lᵢ⋘r
... | node left _ _ _ | _ | inj₂ () | compound
... | node right _ _ _ | _ | inj₂ () | compound
... | node perfect _ _ _ | clᵢ | inj₂ lᵢ⋗r | compound  = right y clᵢ cr (⋙p lᵢ⋗r)
... | node perfect x' l' r' | perfect .x' cl' cr' l'≃r' | inj₁ () | compound
lemma-insert-complete x (right {l} {r} y cl cr l⋙r)
    with tot≤ x y
... | inj₁ x≤y
    with insert y r | lemma-insert-complete y cr | lemma-insert-⋙ y l⋙r | lemma-insert-compound y r | lemma-⋙-⊥ y l⋙r
... | node left _ _ _ | crᵢ | inj₁ l⋙rᵢ | compound | _ = right x cl crᵢ l⋙rᵢ
... | node right _ _ _ | crᵢ | inj₁ l⋙rᵢ | compound | _ = right x cl crᵢ l⋙rᵢ
... | node left _ _ _ | _ | inj₂ () | compound | _
... | node right _ _ _ | _ | inj₂ () | compound | _
... | node perfect _ _ _ | crᵢ | inj₂ l≃rᵢ | compound | _ = perfect x cl crᵢ l≃rᵢ
... | node perfect x'' l'' r'' | perfect .x'' cl'' cr'' l''≃r'' | inj₁ (⋙p l⋗rᵢ) | compound |  lemma-⋙-⊥'
    with lemma-⋙-⊥' l⋗rᵢ
... | ()
lemma-insert-complete x (right {l} {r} y cl cr l⋙r) | inj₂ y≤x
    with insert x r |  lemma-insert-complete x cr | lemma-insert-⋙ x l⋙r | lemma-insert-compound x r | lemma-⋙-⊥ x l⋙r
... | node left _ _ _ | crᵢ | inj₁ l⋙rᵢ | compound | _ = right y cl crᵢ l⋙rᵢ
... | node right _ _ _ | crᵢ | inj₁ l⋙rᵢ | compound | _ = right y cl crᵢ l⋙rᵢ
... | node left _ _ _ | _ | inj₂ () | compound | _
... | node right _ _ _ | _ | inj₂ () | compound | _
... | node perfect _ _ _ | crᵢ | inj₂ l≃rᵢ | compound | _ = perfect y cl crᵢ l≃rᵢ
... | node perfect x'' l'' r'' | perfect .x'' cl'' cr'' l''≃r'' | inj₁ (⋙p l⋗rᵢ) | compound | lemma-⋙-⊥'
    with lemma-⋙-⊥' l⋗rᵢ
... | ()


text:
data Bool : Set where
  true false : Bool

postulate
  and : Bool → Bool → Bool

-- WAS: splitting on y removes the x@ as-pattern
test : Bool → Bool → Bool
test x@true y  = {!y!}
test x@false y = and x {!y!}  -- x will go out of scope if we split on y

-- Multiple as-patterns on the same pattern should be preserved in the
-- right order.
test₂ : Bool → Bool → Bool
test₂ x@y@true z = {!z!}
test₂ x@y z = {!!}

open import Agda.Builtin.String

-- As bindings on literals should also be preserved
test₃ : String → Bool → Bool
test₃ x@"foo" z = {!z!}
test₃ _ _ = {!!}

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --without-K --exact-split --allow-unsolved-metas #-}

module 12-univalence where

import 11-function-extensionality
open 11-function-extensionality public

-- Section 10.1 Type extensionality

equiv-eq : {i : Level} {A : UU i} {B : UU i} → Id A B → A ≃ B
equiv-eq {A = A} refl = equiv-id A

UNIVALENCE : {i : Level} (A B : UU i) → UU (lsuc i)
UNIVALENCE A B = is-equiv (equiv-eq {A = A} {B = B})

is-contr-total-equiv-UNIVALENCE : {i : Level} (A : UU i) →
  ((B : UU i) → UNIVALENCE A B) → is-contr (Σ (UU i) (λ X → A ≃ X))
is-contr-total-equiv-UNIVALENCE A UA =
  fundamental-theorem-id' A
    ( equiv-id A)
    ( λ B → equiv-eq {B = B})
    ( UA)

UNIVALENCE-is-contr-total-equiv : {i : Level} (A : UU i) →
  is-contr (Σ (UU i) (λ X → A ≃ X)) → (B : UU i) → UNIVALENCE A B
UNIVALENCE-is-contr-total-equiv A c =
  fundamental-theorem-id A
    ( equiv-id A)
    ( c)
    ( λ B → equiv-eq {B = B})

ev-id : {i j : Level} {A : UU i} (P : (B : UU i) → (A ≃ B) → UU j) →
  ((B : UU i) (e : A ≃ B) → P B e) → P A (equiv-id A)
ev-id {A = A} P f = f A (equiv-id A)

IND-EQUIV : {i j : Level} {A : UU i} → ((B : UU i) (e : A ≃ B) → UU j) → UU _
IND-EQUIV P = sec (ev-id P)

triangle-ev-id : {i j : Level} {A : UU i}
  (P : (Σ (UU i) (λ X → A ≃ X)) → UU j) →
  (ev-pt (Σ (UU i) (λ X → A ≃ X)) (pair A (equiv-id A)) P)
  ~ ((ev-id (λ X e → P (pair X e))) ∘ (ev-pair {A = UU i} {B = λ X → A ≃ X} {C = P}))
triangle-ev-id P f = refl

abstract
  IND-EQUIV-is-contr-total-equiv : {i j : Level} (A : UU i) →
    is-contr (Σ (UU i) (λ X → A ≃ X)) →
    (P : (Σ (UU i) (λ X → A ≃ X)) → UU j) → IND-EQUIV (λ B e → P (pair B e))
  IND-EQUIV-is-contr-total-equiv {i} {j} A c P =
    section-comp
      ( ev-pt (Σ (UU i) (λ X → A ≃ X)) (pair A (equiv-id A)) P)
      ( ev-id (λ X e → P (pair X e)))
      ( ev-pair {A = UU i} {B = λ X → A ≃ X} {C = P})
      ( triangle-ev-id P)
      ( sec-ev-pair (UU i) (λ X → A ≃ X) P)
      ( is-sing-is-contr (Σ (UU i) (λ X → A ≃ X))
        ( pair
          ( pair A (equiv-id A))
          ( λ t →
            ( inv (contraction c (pair A (equiv-id A)))) ∙
            ( contraction c t)))
        ( P)
        ( pair A (equiv-id A)))

abstract
  is-contr-total-equiv-IND-EQUIV : {i : Level} (A : UU i) →
    ( {j : Level} (P : (Σ (UU i) (λ X → A ≃ X)) → UU j) →
      IND-EQUIV (λ B e → P (pair B e))) →
    is-contr (Σ (UU i) (λ X → A ≃ X))
  is-contr-total-equiv-IND-EQUIV {i} A ind =
    is-contr-is-sing
      ( Σ (UU i) (λ X → A ≃ X))
      ( pair A (equiv-id A))
      ( λ P → section-comp'
        ( ev-pt (Σ (UU i) (λ X → A ≃ X)) (pair A (equiv-id A)) P)
        ( ev-id (λ X e → P (pair X e)))
        ( ev-pair {A = UU i} {B = λ X → A ≃ X} {C = P})
        ( triangle-ev-id P)
        ( sec-ev-pair (UU i) (λ X → A ≃ X) P)
        ( ind P))

-- The univalence axiom

postulate univalence : {i : Level} (A B : UU i) → UNIVALENCE A B

eq-equiv : {i : Level} (A B : UU i) → (A ≃ B) → Id A B
eq-equiv A B = inv-is-equiv (univalence A B)

abstract
  is-contr-total-equiv : {i : Level} (A : UU i) →
    is-contr (Σ (UU i) (λ X → A ≃ X))
  is-contr-total-equiv A = is-contr-total-equiv-UNIVALENCE A (univalence A)

inv-inv-equiv :
  {i j : Level} {A : UU i} {B : UU j} (e : A ≃ B) →
  Id (inv-equiv (inv-equiv e)) e
inv-inv-equiv (pair f (pair (pair g G) (pair h H))) = eq-htpy-equiv refl-htpy

is-equiv-inv-equiv :
  {i j : Level} {A : UU i} {B : UU j} → is-equiv (inv-equiv {A = A} {B = B})
is-equiv-inv-equiv =
  is-equiv-has-inverse
    ( inv-equiv)
    ( inv-inv-equiv)
    ( inv-inv-equiv)

equiv-inv-equiv :
  {i j : Level} {A : UU i} {B : UU j} → (A ≃ B) ≃ (B ≃ A)
equiv-inv-equiv = pair inv-equiv is-equiv-inv-equiv

is-contr-total-equiv' : {i : Level} (A : UU i) →
  is-contr (Σ (UU i) (λ X → X ≃ A))
is-contr-total-equiv' A =
  is-contr-equiv
    ( Σ (UU _) (λ X → A ≃ X))
    ( equiv-tot (λ X → equiv-inv-equiv))
    ( is-contr-total-equiv A)

abstract
  Ind-equiv : {i j : Level} (A : UU i) (P : (B : UU i) (e : A ≃ B) → UU j) →
    sec (ev-id P)
  Ind-equiv A P =
    IND-EQUIV-is-contr-total-equiv A
    ( is-contr-total-equiv A)
    ( λ t → P (pr1 t) (pr2 t))

ind-equiv : {i j : Level} (A : UU i) (P : (B : UU i) (e : A ≃ B) → UU j) →
  P A (equiv-id A) → {B : UU i} (e : A ≃ B) → P B e
ind-equiv A P p {B} = pr1 (Ind-equiv A P) p B

-- Subuniverses

is-subuniverse :
  {l1 l2 : Level} (P : UU l1 → UU l2) → UU ((lsuc l1) ⊔ l2)
is-subuniverse P = is-subtype P

subuniverse :
  (l1 l2 : Level) → UU ((lsuc l1) ⊔ (lsuc l2))
subuniverse l1 l2 = Σ (UU l1 → UU l2) is-subuniverse

{- By univalence, subuniverses are closed under equivalences. -}
in-subuniverse-equiv :
  {l1 l2 : Level} (P : UU l1 → UU l2) {X Y : UU l1} → X ≃ Y → P X → P Y
in-subuniverse-equiv P e = tr P (eq-equiv _ _ e)

in-subuniverse-equiv' :
  {l1 l2 : Level} (P : UU l1 → UU l2) {X Y : UU l1} → X ≃ Y → P Y → P X
in-subuniverse-equiv' P e = tr P (inv (eq-equiv _ _ e))

total-subuniverse :
  {l1 l2 : Level} (P : subuniverse l1 l2) → UU ((lsuc l1) ⊔ l2)
total-subuniverse {l1} P = Σ (UU l1) (pr1 P)

{- We also introduce the notion of 'global subuniverse'. The handling of
   universe levels is a bit more complicated here, since (l : Level) → A l are
   kinds but not types. -}

is-global-subuniverse :
  (α : Level → Level) (P : (l : Level) → subuniverse l (α l)) →
  (l1 l2 : Level) → UU _
is-global-subuniverse α P l1 l2 =
  (X : UU l1) (Y : UU l2) → X ≃ Y → (pr1 (P l1)) X → (pr1 (P l2)) Y

{- Next we characterize the identity type of a subuniverse. -}

Eq-total-subuniverse :
  {l1 l2 : Level} (P : subuniverse l1 l2) →
  (s t : total-subuniverse P) → UU l1
Eq-total-subuniverse (pair P H) (pair X p) t = X ≃ (pr1 t)

Eq-total-subuniverse-eq :
  {l1 l2 : Level} (P : subuniverse l1 l2) →
  (s t : total-subuniverse P) → Id s t → Eq-total-subuniverse P s t
Eq-total-subuniverse-eq (pair P H) (pair X p) .(pair X p) refl = equiv-id X

abstract
  is-contr-total-Eq-total-subuniverse :
    {l1 l2 : Level} (P : subuniverse l1 l2)
    (s : total-subuniverse P) →
    is-contr (Σ (total-subuniverse P) (λ t → Eq-total-subuniverse P s t))
  is-contr-total-Eq-total-subuniverse (pair P H) (pair X p) =
    is-contr-total-Eq-substructure (is-contr-total-equiv X) H X (equiv-id X) p

abstract
  is-equiv-Eq-total-subuniverse-eq :
    {l1 l2 : Level} (P : subuniverse l1 l2)
    (s t : total-subuniverse P) → is-equiv (Eq-total-subuniverse-eq P s t)
  is-equiv-Eq-total-subuniverse-eq (pair P H) (pair X p) =
    fundamental-theorem-id
      ( pair X p)
      ( equiv-id X)
      ( is-contr-total-Eq-total-subuniverse (pair P H) (pair X p))
      ( Eq-total-subuniverse-eq (pair P H) (pair X p))

eq-Eq-total-subuniverse :
  {l1 l2 : Level} (P : subuniverse l1 l2) →
  {s t : total-subuniverse P} → Eq-total-subuniverse P s t → Id s t
eq-Eq-total-subuniverse P {s} {t} =
  inv-is-equiv (is-equiv-Eq-total-subuniverse-eq P s t)

-- Section 12.2 Univalence implies function extensionality

is-equiv-postcomp-univalence :
  {l1 l2 : Level} {X Y : UU l1} (A : UU l2) (e : X ≃ Y) →
  is-equiv (postcomp A (map-equiv e))
is-equiv-postcomp-univalence {X = X} A =
  ind-equiv X
    ( λ Y e → is-equiv (postcomp A (map-equiv e)))
    ( is-equiv-id (A → X))

weak-funext-univalence :
  {l : Level} {A : UU l} {B : A → UU l} → WEAK-FUNEXT A B
weak-funext-univalence {A = A} {B} is-contr-B =
  is-contr-retract-of
    ( fib (postcomp A (pr1 {B = B})) id)
    ( pair
      ( λ f → pair (λ x → pair x (f x)) refl)
      ( pair
        ( λ h x → tr B (htpy-eq (pr2 h) x) (pr2 (pr1 h x)))
        ( refl-htpy)))
    ( is-contr-map-is-equiv
      ( is-equiv-postcomp-univalence A (equiv-pr1 is-contr-B))
      ( id))

funext-univalence :
  {l : Level} {A : UU l} {B : A → UU l} (f : (x : A) → B x) → FUNEXT f
funext-univalence {A = A} {B} f =
  FUNEXT-WEAK-FUNEXT (λ A B → weak-funext-univalence) A B f

-- Exercises

-- Exercise 10.1

tr-equiv-eq-ap : {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {x y : A}
  (p : Id x y) → (map-equiv (equiv-eq (ap B p))) ~ tr B p
tr-equiv-eq-ap refl = refl-htpy

-- Exercise 10.2

subuniverse-is-contr :
  {i : Level} → subuniverse i i
subuniverse-is-contr {i} = pair is-contr is-subtype-is-contr

unit' :
  (i : Level) → UU i
unit' i = pr1 (Raise i unit)

abstract
  is-contr-unit' :
    (i : Level) → is-contr (unit' i)
  is-contr-unit' i =
    is-contr-equiv' unit (pr2 (Raise i unit)) is-contr-unit

abstract
  center-UU-contr :
    (i : Level) → total-subuniverse (subuniverse-is-contr {i})
  center-UU-contr i =
    pair (unit' i) (is-contr-unit' i)

  contraction-UU-contr :
    {i : Level} (A : Σ (UU i) is-contr) →
    Id (center-UU-contr i) A
  contraction-UU-contr (pair A is-contr-A) =
    eq-Eq-total-subuniverse subuniverse-is-contr
      ( equiv-is-contr (is-contr-unit' _) is-contr-A)

abstract
  is-contr-UU-contr : (i : Level) → is-contr (Σ (UU i) is-contr)
  is-contr-UU-contr i =
    pair (center-UU-contr i) (contraction-UU-contr)

is-trunc-UU-trunc :
  (k : 𝕋) (i : Level) → is-trunc (succ-𝕋 k) (Σ (UU i) (is-trunc k))
is-trunc-UU-trunc k i X Y =
  is-trunc-is-equiv k
    ( Id (pr1 X) (pr1 Y))
    ( ap pr1)
    ( is-emb-pr1-is-subtype
      ( is-prop-is-trunc k) X Y)
    ( is-trunc-is-equiv k
      ( (pr1 X) ≃ (pr1 Y))
      ( equiv-eq)
      ( univalence (pr1 X) (pr1 Y))
      ( is-trunc-equiv-is-trunc k (pr2 X) (pr2 Y)))

ev-true-false :
  {l : Level} (A : UU l) → (f : bool → A) → A × A
ev-true-false A f = pair (f true) (f false)

map-universal-property-bool :
  {l : Level} {A : UU l} →
  A × A → (bool → A)
map-universal-property-bool (pair x y) true = x
map-universal-property-bool (pair x y) false = y

issec-map-universal-property-bool :
  {l : Level} {A : UU l} →
  ((ev-true-false A) ∘ map-universal-property-bool) ~ id
issec-map-universal-property-bool (pair x y) =
  eq-pair-triv (pair refl refl)

isretr-map-universal-property-bool' :
  {l : Level} {A : UU l} (f : bool → A) →
  (map-universal-property-bool (ev-true-false A f)) ~ f
isretr-map-universal-property-bool' f true = refl
isretr-map-universal-property-bool' f false = refl

isretr-map-universal-property-bool :
  {l : Level} {A : UU l} →
  (map-universal-property-bool ∘ (ev-true-false A)) ~ id
isretr-map-universal-property-bool f =
  eq-htpy (isretr-map-universal-property-bool' f)

universal-property-bool :
  {l : Level} (A : UU l) →
  is-equiv (λ (f : bool → A) → pair (f true) (f false))
universal-property-bool A =
  is-equiv-has-inverse
    map-universal-property-bool
    issec-map-universal-property-bool
    isretr-map-universal-property-bool

ev-true :
  {l : Level} {A : UU l} → (bool → A) → A
ev-true f = f true

triangle-ev-true :
  {l : Level} (A : UU l) →
  (ev-true) ~ (pr1 ∘ (ev-true-false A))
triangle-ev-true A = refl-htpy

aut-bool-bool :
  bool → (bool ≃ bool)
aut-bool-bool true = equiv-id bool
aut-bool-bool false = equiv-neg-𝟚

bool-aut-bool :
  (bool ≃ bool) → bool
bool-aut-bool e = map-equiv e true

decide-true-false :
  (b : bool) → coprod (Id b true) (Id b false)
decide-true-false true = inl refl
decide-true-false false = inr refl

eq-false :
  (b : bool) → (¬ (Id b true)) → (Id b false)
eq-false true p = ind-empty (p refl)
eq-false false p = refl

eq-true :
  (b : bool) → (¬ (Id b false)) → Id b true
eq-true true p = refl
eq-true false p = ind-empty (p refl)

Eq-𝟚-eq : (x y : bool) → Id x y → Eq-𝟚 x y
Eq-𝟚-eq x .x refl = reflexive-Eq-𝟚 x

eq-false-equiv' :
  (e : bool ≃ bool) → Id (map-equiv e true) true →
  is-decidable (Id (map-equiv e false) false) → Id (map-equiv e false) false
eq-false-equiv' e p (inl q) = q
eq-false-equiv' e p (inr x) =
  ind-empty
    ( Eq-𝟚-eq true false
      ( ap pr1
        ( is-prop-is-contr'
          ( is-contr-map-is-equiv (is-equiv-map-equiv e) true)
          ( pair true p)
          ( pair false (eq-true (map-equiv e false) x)))))

{-
eq-false-equiv :
  (e : bool ≃ bool) → Id (map-equiv e true) true → Id (map-equiv e false) false
eq-false-equiv e p =
  eq-false-equiv' e p (has-decidable-equality-𝟚 (map-equiv e false) false)
-}

{-
eq-true-equiv :
  (e : bool ≃ bool) →
  ¬ (Id (map-equiv e true) true) → Id (map-equiv e false) true
eq-true-equiv e f = {!!}

issec-bool-aut-bool' :
  ( e : bool ≃ bool) (d : is-decidable (Id (map-equiv e true) true)) →
  htpy-equiv (aut-bool-bool (bool-aut-bool e)) e
issec-bool-aut-bool' e (inl p) true =
  ( htpy-equiv-eq (ap aut-bool-bool p) true) ∙ (inv p)
issec-bool-aut-bool' e (inl p) false =
  ( htpy-equiv-eq (ap aut-bool-bool p) false) ∙
  ( inv (eq-false-equiv e p))
issec-bool-aut-bool' e (inr f) true =
  ( htpy-equiv-eq
    ( ap aut-bool-bool (eq-false (map-equiv e true) f)) true) ∙
  ( inv (eq-false (map-equiv e true) f))
issec-bool-aut-bool' e (inr f) false =
  ( htpy-equiv-eq (ap aut-bool-bool {!eq-true-equiv e ?!}) {!!}) ∙
  ( inv {!!})

issec-bool-aut-bool :
  (aut-bool-bool ∘ bool-aut-bool) ~ id
issec-bool-aut-bool e =
  eq-htpy-equiv
    ( issec-bool-aut-bool' e
      ( has-decidable-equality-𝟚 (map-equiv e true) true))
-}

max_stars_repo_name: hemangandhi/HoTT-Intro

max_issues_repo_name: hemangandhi/HoTT-Intro

max_forks_repo_name: hemangandhi/HoTT-Intro


text:
{-# OPTIONS --no-qualified-instances #-}

module NoQualifiedInstances-Import where

open import NoQualifiedInstances.Import.A as A

postulate
  f : {{A.I}} → A.I

test : A.I
test = f

max_forks_repo_name: shlevy/agda


text:
{-
This file contains:

- Elementary properties of homomorphisms
- H-level results for the properties of morphisms
- Special homomorphisms and operations (id, composition, inversion)
- Conversion functions between different notions of group morphisms

-}
{-# OPTIONS --safe #-}
module Cubical.Algebra.Group.MorphismProperties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure
open import Cubical.Functions.Embedding

open import Cubical.Data.Sigma

open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.DirProd
open import Cubical.Algebra.Group.Properties
open import Cubical.Algebra.Group.Morphisms

open import Cubical.HITs.PropositionalTruncation renaming (map to pMap)

private
  variable
    ℓ ℓ' ℓ'' ℓ''' : Level
    E F G H : Group ℓ

open Iso
open GroupStr
open IsGroupHom
open BijectionIso

-- Elementary properties of homomorphisms
module _ {A : Type ℓ} {B : Type ℓ'} (G : GroupStr A) (f : A → B) (H : GroupStr B)
  (pres : (x y : A) → f (G ._·_ x y) ≡ H ._·_ (f x) (f y))
  where

  private
    module G = GroupStr G
    module H = GroupStr H

  -- ϕ(1g) ≡ 1g
  hom1g : f G.1g ≡ H.1g
  hom1g =
    f G.1g                                  ≡⟨ sym (H.rid _) ⟩
    f G.1g H.· H.1g                         ≡⟨ (λ i → f G.1g H.· H.invr (f G.1g) (~ i)) ⟩
    f G.1g H.· (f G.1g H.· H.inv (f G.1g))  ≡⟨ H.assoc _ _ _ ⟩
    (f G.1g H.· f G.1g) H.· H.inv (f G.1g)  ≡⟨ sym (cong (λ x → x H.· _)
                                                (sym (cong f (G.lid _)) ∙ pres G.1g G.1g)) ⟩
    f G.1g H.· H.inv (f G.1g)               ≡⟨ H.invr _ ⟩
    H.1g ∎

  -- ϕ(- x) = - ϕ(x)
  homInv : ∀ g → f (G.inv g) ≡ H.inv (f g)
  homInv g =
    f (G.inv g)                            ≡⟨ sym (H.rid _) ⟩
    f (G.inv g) H.· H.1g                   ≡⟨ cong (_ H.·_) (sym (H.invr _)) ⟩
    f (G.inv g) H.· (f g H.· H.inv (f g))  ≡⟨ H.assoc _ _ _ ⟩
    (f (G.inv g) H.· f g) H.· H.inv (f g)  ≡⟨ cong (H._· _) (sym (pres _ g) ∙∙ cong f (G.invl g) ∙∙ hom1g) ⟩
    H.1g H.· H.inv (f g)                   ≡⟨ H.lid _ ⟩
    H.inv (f g) ∎

module _ {A : Type ℓ} {B : Type ℓ'} {G : GroupStr A} {f : A → B} {H : GroupStr B}
  (pres : (x y : A) → f (G ._·_ x y) ≡ H ._·_ (f x) (f y))
  where

  makeIsGroupHom : IsGroupHom G f H
  makeIsGroupHom .pres· = pres
  makeIsGroupHom .pres1 = hom1g G f H pres
  makeIsGroupHom .presinv = homInv G f H pres

isGroupHomInv : (f : GroupEquiv G H) → IsGroupHom (H .snd) (invEq (fst f)) (G .snd)
isGroupHomInv {G = G} {H = H} f = makeIsGroupHom λ h h' →
  isInj-f _ _
    (f' (g (h ⋆² h'))        ≡⟨ secEq (fst f) _ ⟩
     (h ⋆² h')               ≡⟨ sym (cong₂ _⋆²_ (secEq (fst f) h) (secEq (fst f) h')) ⟩
     (f' (g h) ⋆² f' (g h')) ≡⟨ sym (pres· (snd f) _ _) ⟩
     f' (g h ⋆¹ g h') ∎)
  where
  f' = fst (fst f)
  _⋆¹_ = _·_ (snd G)
  _⋆²_ = _·_ (snd H)
  g = invEq (fst f)

  isInj-f : (x y : ⟨ G ⟩) → f' x ≡ f' y → x ≡ y
  isInj-f x y = invEq (_ , isEquiv→isEmbedding (snd (fst f)) x y)

-- H-level results
isPropIsGroupHom : (G : Group ℓ) (H : Group ℓ') {f : ⟨ G ⟩ → ⟨ H ⟩}
                 → isProp (IsGroupHom (G .snd) f (H .snd))
isPropIsGroupHom G H =
  isOfHLevelRetractFromIso 1 IsGroupHomIsoΣ
    (isProp×
      (isPropΠ2 λ _ _ → GroupStr.is-set (snd H) _ _)
      (isProp×
        (GroupStr.is-set (snd H) _ _)
        (isPropΠ λ _ → GroupStr.is-set (snd H) _ _)))

isSetGroupHom : isSet (GroupHom G H)
isSetGroupHom {G = G} {H = H} =
  isSetΣ (isSetΠ λ _ → is-set (snd H)) λ _ → isProp→isSet (isPropIsGroupHom G H)

isPropIsInIm : (f : GroupHom G H) (x : ⟨ H ⟩) → isProp (isInIm f x)
isPropIsInIm f x = squash₁

isSetIm : (f : GroupHom G H) → isSet (Im f)
isSetIm {H = H} f = isSetΣ (is-set (snd H)) λ x → isProp→isSet (isPropIsInIm f x)

isPropIsInKer : (f : GroupHom G H) (x : ⟨ G ⟩) → isProp (isInKer f x)
isPropIsInKer {H = H} f x = is-set (snd H) _ _

isSetKer : (f : GroupHom G H) → isSet (Ker f)
isSetKer {G = G} f = isSetΣ (is-set (snd G)) λ x → isProp→isSet (isPropIsInKer f x)

isPropIsSurjective : (f : GroupHom G H) → isProp (isSurjective f)
isPropIsSurjective f = isPropΠ (λ x → isPropIsInIm f x)

isPropIsInjective : (f : GroupHom G H) → isProp (isInjective f)
isPropIsInjective {G = G} _ = isPropΠ2 (λ _ _ → is-set (snd G) _ _)

isPropIsMono : (f : GroupHom G H) → isProp (isMono f)
isPropIsMono {G = G} f = isPropImplicitΠ2 λ _ _ → isPropΠ (λ _ → is-set (snd G) _ _)

-- Logically equivalent versions of isInjective
isMono→isInjective : (f : GroupHom G H) → isMono f → isInjective f
isMono→isInjective f h x p = h (p ∙ sym (f .snd .pres1))

isInjective→isMono : (f : GroupHom G H) → isInjective f → isMono f
isInjective→isMono {G = G} {H = H} f h {x = x} {y = y} p =
  x                      ≡⟨ sym (G.rid _) ⟩
  x G.· G.1g             ≡⟨ cong (x G.·_) (sym (G.invl _)) ⟩
  x G.· (G.inv y G.· y)  ≡⟨ G.assoc _ _ _ ⟩
  (x G.· G.inv y) G.· y  ≡⟨ cong (G._· y) idHelper ⟩
  G.1g G.· y             ≡⟨ G.lid _ ⟩
  y ∎
    where
    module G = GroupStr (snd G)
    module H = GroupStr (snd H)

    idHelper : x G.· G.inv y ≡ G.1g
    idHelper = h _ (f .snd .pres· _ _ ∙
                    cong (λ a → f .fst x H.· a) (f .snd .presinv y) ∙
                    cong (H._· H.inv (f .fst y)) p ∙
                    H.invr _)

-- TODO: maybe it would be better to take this as the definition of isInjective?
isInjective→isContrKer : (f : GroupHom G H) → isInjective f → isContr (Ker f)
fst (isInjective→isContrKer {G = G} f hf) = 1g (snd G) , f .snd .pres1
snd (isInjective→isContrKer {G = G} f hf) k =
  Σ≡Prop (isPropIsInKer f) (sym (isInjective→isMono f hf (k .snd ∙ sym (f .snd .pres1))))

isContrKer→isInjective : (f : GroupHom G H) → isContr (Ker f) → isInjective f
isContrKer→isInjective {G = G} f ((a , b) , c) x y = cong fst (sym (c (x , y)) ∙ rem)
  where
  rem : (a , b) ≡ (1g (snd G) , pres1 (snd f))
  rem = c (1g (snd G) , pres1 (snd f))

-- Special homomorphisms and operations (id, composition...)
idGroupHom : GroupHom G G
idGroupHom .fst x = x
idGroupHom .snd = makeIsGroupHom λ _ _ → refl

isGroupHomComp : (f : GroupHom F G) → (g : GroupHom G H) → IsGroupHom (F .snd) (fst g ∘ fst f) (H .snd)
isGroupHomComp f g = makeIsGroupHom λ _ _ → cong (fst g) (f .snd .pres· _ _) ∙ (g .snd .pres· _ _)

compGroupHom : GroupHom F G → GroupHom G H → GroupHom F H
fst (compGroupHom f g) = fst g ∘ fst f
snd (compGroupHom f g) = isGroupHomComp f g

GroupHomDirProd : {A : Group ℓ} {B : Group ℓ'} {C : Group ℓ''} {D : Group ℓ'''}
                → GroupHom A C → GroupHom B D → GroupHom (DirProd A B) (DirProd C D)
fst (GroupHomDirProd mf1 mf2) = map-× (fst mf1) (fst mf2)
snd (GroupHomDirProd mf1 mf2) = makeIsGroupHom λ _ _ → ≡-× (mf1 .snd .pres· _ _) (mf2 .snd .pres· _ _)

GroupHom≡ : {f g : GroupHom G H} → (fst f ≡ fst g) → f ≡ g
fst (GroupHom≡ p i) = p i
snd (GroupHom≡ {G = G} {H = H} {f = f} {g = g} p i) = p-hom i
  where
  p-hom : PathP (λ i → IsGroupHom (G .snd) (p i) (H .snd)) (f .snd) (g .snd)
  p-hom = toPathP (isPropIsGroupHom G H _ _)

compGroupHomAssoc : (e : GroupHom E F) → (f : GroupHom F G) → (g : GroupHom G H)
                  → compGroupHom (compGroupHom e f) g ≡ compGroupHom e (compGroupHom f g)
compGroupHomAssoc e f g = GroupHom≡ refl

compGroupHomId : (f : GroupHom F G) → compGroupHom f idGroupHom ≡ f
compGroupHomId f = GroupHom≡ refl

-- The composition of surjective maps is surjective
compSurjective : ∀ {ℓ ℓ' ℓ''} {G : Group ℓ} {H : Group ℓ'} {L : Group ℓ''}
         → (G→H : GroupHom G H) (H→L : GroupHom H L)
         → isSurjective G→H → isSurjective H→L
         → isSurjective (compGroupHom G→H H→L)
compSurjective G→H H→L surj1 surj2 l =
  rec squash₁
    (λ {(h , p)
      → pMap (λ {(g , q) → g , (cong (fst H→L) q ∙ p)})
        (surj1 h)})
    (surj2 l)

-- GroupEquiv identity, composition and inversion
idGroupEquiv : GroupEquiv G G
fst (idGroupEquiv {G = G}) = idEquiv ⟨ G ⟩
snd idGroupEquiv = makeIsGroupHom λ _ _ → refl

compGroupEquiv : GroupEquiv F G → GroupEquiv G H → GroupEquiv F H
fst (compGroupEquiv f g) = compEquiv (fst f) (fst g)
snd (compGroupEquiv f g) = isGroupHomComp (_ , f .snd) (_ , g .snd)

invGroupEquiv : GroupEquiv G H → GroupEquiv H G
fst (invGroupEquiv f) = invEquiv (fst f)
snd (invGroupEquiv f) = isGroupHomInv f

GroupEquivDirProd : {A : Group ℓ} {B : Group ℓ'} {C : Group ℓ''} {D : Group ℓ'''}
                  → GroupEquiv A C → GroupEquiv B D
                  → GroupEquiv (DirProd A B) (DirProd C D)
fst (GroupEquivDirProd eq1 eq2) = ≃-× (fst eq1) (fst eq2)
snd (GroupEquivDirProd eq1 eq2) = GroupHomDirProd (_ , eq1 .snd) (_ , eq2 .snd) .snd

GroupEquiv≡ : {f g : GroupEquiv G H} → fst f ≡ fst g → f ≡ g
fst (GroupEquiv≡ p i) = p i
snd (GroupEquiv≡ {G = G} {H = H} {f} {g} p i) = p-hom i
  where
  p-hom : PathP (λ i → IsGroupHom (G .snd) (p i .fst) (H .snd)) (snd f) (snd g)
  p-hom = toPathP (isPropIsGroupHom G H _ _)

-- GroupIso identity, composition and inversion
idGroupIso : GroupIso G G
fst idGroupIso = idIso
snd idGroupIso = makeIsGroupHom λ _ _ → refl

compGroupIso : GroupIso G H → GroupIso H F → GroupIso G F
fst (compGroupIso iso1 iso2) = compIso (fst iso1) (fst iso2)
snd (compGroupIso iso1 iso2) = isGroupHomComp (_ , snd iso1) (_ , snd iso2)

invGroupIso : GroupIso G H → GroupIso H G
fst (invGroupIso iso1) = invIso (fst iso1)
snd (invGroupIso iso1) = isGroupHomInv (isoToEquiv (fst iso1) , snd iso1)

GroupIsoDirProd : {G : Group ℓ} {H : Group ℓ'} {A : Group ℓ''} {B : Group ℓ'''}
                → GroupIso G H → GroupIso A B → GroupIso (DirProd G A) (DirProd H B)
fun (fst (GroupIsoDirProd iso1 iso2)) prod =
  fun (fst iso1) (fst prod) , fun (fst iso2) (snd prod)
inv (fst (GroupIsoDirProd iso1 iso2)) prod =
  inv (fst iso1) (fst prod) , inv (fst iso2) (snd prod)
rightInv (fst (GroupIsoDirProd iso1 iso2)) a =
  ΣPathP (rightInv (fst iso1) (fst a) , (rightInv (fst iso2) (snd a)))
leftInv (fst (GroupIsoDirProd iso1 iso2)) a =
  ΣPathP (leftInv (fst iso1) (fst a) , (leftInv (fst iso2) (snd a)))
snd (GroupIsoDirProd iso1 iso2) = makeIsGroupHom λ a b →
  ΣPathP (pres· (snd iso1) (fst a) (fst b) , pres· (snd iso2) (snd a) (snd b))

GroupIso≡ : {f g : GroupIso G H} → f .fst ≡ g .fst → f ≡ g
fst (GroupIso≡ {G = G} {H = H} {f} {g} p i) = p i
snd (GroupIso≡ {G = G} {H = H} {f} {g} p i) = p-hom i
  where
  p-hom : PathP (λ i → IsGroupHom (G .snd) (p i .fun) (H .snd)) (snd f) (snd g)
  p-hom = toPathP (isPropIsGroupHom G H _ _)

-- Conversion functions between different notions of group morphisms
GroupEquiv→GroupHom : GroupEquiv G H → GroupHom G H
fst (GroupEquiv→GroupHom ((f , _) , _)) = f
snd (GroupEquiv→GroupHom (_ , isHom)) = isHom

GroupIso→GroupEquiv : GroupIso G H → GroupEquiv G H
fst (GroupIso→GroupEquiv i) = isoToEquiv (fst i)
snd (GroupIso→GroupEquiv i) = snd i

GroupEquiv→GroupIso : GroupEquiv G H → GroupIso G H
fst (GroupEquiv→GroupIso e) = equivToIso (fst e)
snd (GroupEquiv→GroupIso e) = snd e

GroupIso→GroupHom : GroupIso G H → GroupHom G H
GroupIso→GroupHom i = GroupEquiv→GroupHom (GroupIso→GroupEquiv i)

-- TODO: prove the converse
BijectionIso→GroupIso : BijectionIso G H → GroupIso G H
BijectionIso→GroupIso {G = G} {H = H} i = grIso
  where
  f = fst (fun i)

  helper : (b : _) → isProp (Σ[ a ∈ ⟨ G ⟩ ] f a ≡ b)
  helper _ (a , ha) (b , hb) =
    Σ≡Prop (λ _ → is-set (snd H) _ _)
           (isInjective→isMono (fun i) (inj i) (ha ∙ sym hb) )

  grIso : GroupIso G H
  fun (fst grIso) = f
  inv (fst grIso) b = rec (helper b) (λ a → a) (surj i b) .fst
  rightInv (fst grIso) b = rec (helper b) (λ a → a) (surj i b) .snd
  leftInv (fst grIso) b j = rec (helper (f b)) (λ a → a)
                                 (isPropPropTrunc (surj i (f b)) ∣ b , refl ∣₁ j) .fst
  snd grIso = snd (fun i)

BijectionIsoToGroupEquiv : BijectionIso G H → GroupEquiv G H
BijectionIsoToGroupEquiv i = GroupIso→GroupEquiv (BijectionIso→GroupIso i)

max_stars_repo_name: gmagaf/cubical

max_issues_repo_name: gmagaf/cubical

max_forks_repo_name: gmagaf/cubical


text:
-----------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of the setoid sublist relation
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

open import Relation.Binary using (Setoid; _⇒_; _Preserves_⟶_)

module Data.List.Relation.Binary.Sublist.Setoid.Properties
  {c ℓ} (S : Setoid c ℓ) where

open import Data.List.Base hiding (_∷ʳ_)
import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
import Data.List.Relation.Binary.Sublist.Setoid as SetoidSublist
import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties
  as HeteroProperties
import Data.List.Membership.Setoid as SetoidMembership
open import Data.List.Relation.Unary.Any using (Any)
open import Data.Nat using (_≤_; _≥_; z≤n; s≤s)
import Data.Nat.Properties as ℕₚ
import Data.Maybe.Relation.Unary.All as Maybe
open import Function
open import Function.Bijection   using (_⤖_)
open import Function.Equivalence using (_⇔_)

open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Unary using (Pred; Decidable; Irrelevant)
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Negation using (¬?)

open Setoid S using (_≈_) renaming (Carrier to A)
open SetoidEquality S using (_≋_; ≋-refl)
open SetoidSublist S hiding (map)
open SetoidMembership S using (_∈_)

------------------------------------------------------------------------
-- Injectivity of constructors
------------------------------------------------------------------------

module _ {xs ys : List A} where

  ∷-injectiveˡ : ∀ {x y} {px qx : x ≈ y} {pxs qxs : xs ⊆ ys} →
                 ((x ∷ xs) ⊆ (y ∷ ys) ∋ px ∷ pxs) ≡ (qx ∷ qxs) → px ≡ qx
  ∷-injectiveˡ refl = refl

  ∷-injectiveʳ : ∀ {x y} {px qx : x ≈ y} {pxs qxs : xs ⊆ ys} →
                 ((x ∷ xs) ⊆ (y ∷ ys) ∋ px ∷ pxs) ≡ (qx ∷ qxs) → pxs ≡ qxs
  ∷-injectiveʳ refl = refl

  ∷ʳ-injective : ∀ {y} {pxs qxs : xs ⊆ ys} → y ∷ʳ pxs ≡ y ∷ʳ qxs → pxs ≡ qxs
  ∷ʳ-injective refl = refl

------------------------------------------------------------------------
-- Various functions' outputs are sublists
------------------------------------------------------------------------

tail-⊆ : ∀ xs → Maybe.All (_⊆ xs) (tail xs)
tail-⊆ xs = HeteroProperties.tail-Sublist ⊆-refl

take-⊆ : ∀ n xs → take n xs ⊆ xs
take-⊆ n xs = HeteroProperties.take-Sublist n ⊆-refl

drop-⊆ : ∀ n xs → drop n xs ⊆ xs
drop-⊆ n xs = HeteroProperties.drop-Sublist n ⊆-refl

module _ {p} {P : Pred A p} (P? : Decidable P) where

  takeWhile-⊆ : ∀ xs → takeWhile P? xs ⊆ xs
  takeWhile-⊆ xs = HeteroProperties.takeWhile-Sublist P? ⊆-refl

  dropWhile-⊆ : ∀ xs → dropWhile P? xs ⊆ xs
  dropWhile-⊆ xs = HeteroProperties.dropWhile-Sublist P? ⊆-refl

  filter-⊆ : ∀ xs → filter P? xs ⊆ xs
  filter-⊆ xs = HeteroProperties.filter-Sublist P? ⊆-refl

module _ {p} {P : Pred A p} (P? : Decidable P) where

  takeWhile⊆filter : ∀ xs → takeWhile P? xs ⊆ filter P? xs
  takeWhile⊆filter xs = HeteroProperties.takeWhile-filter P? {xs} ≋-refl

  filter⊆dropWhile : ∀ xs → filter P? xs ⊆ dropWhile (¬? ∘ P?) xs
  filter⊆dropWhile xs = HeteroProperties.filter-dropWhile P? {xs} ≋-refl

------------------------------------------------------------------------
-- Various list functions are increasing wrt _⊆_
------------------------------------------------------------------------
-- We write f⁺ for the proof that `xs ⊆ ys → f xs ⊆ f ys`
-- and f⁻ for the one that `f xs ⊆ f ys → xs ⊆ ys`.

module _ {as bs : List A} where

  ∷ˡ⁻ : ∀ {a} → a ∷ as ⊆ bs → as ⊆ bs
  ∷ˡ⁻ = HeteroProperties.∷ˡ⁻

  ∷ʳ⁻ : ∀ {a b} → ¬ (a ≈ b) → a ∷ as ⊆ b ∷ bs → a ∷ as ⊆ bs
  ∷ʳ⁻ = HeteroProperties.∷ʳ⁻

  ∷⁻ : ∀ {a b} → a ∷ as ⊆ b ∷ bs → as ⊆ bs
  ∷⁻ = HeteroProperties.∷⁻

------------------------------------------------------------------------
-- map

module _ {b ℓ} (R : Setoid b ℓ) where

  open Setoid R using () renaming (Carrier to B; _≈_ to _≈′_)
  open SetoidSublist R using () renaming (_⊆_ to _⊆′_)

  map⁺ : ∀ {as bs} {f : A → B} → f Preserves _≈_ ⟶ _≈′_ →
         as ⊆ bs → map f as ⊆′ map f bs
  map⁺ {f = f} f-resp as⊆bs =
    HeteroProperties.map⁺ f f (SetoidSublist.map S f-resp as⊆bs)

------------------------------------------------------------------------
-- _++_

module _ {as bs : List A} where

  ++⁺ˡ : ∀ cs → as ⊆ bs → as ⊆ cs ++ bs
  ++⁺ˡ = HeteroProperties.++ˡ

  ++⁺ʳ : ∀ cs → as ⊆ bs → as ⊆ bs ++ cs
  ++⁺ʳ = HeteroProperties.++ʳ

  ++⁺ : ∀ {cs ds} → as ⊆ bs → cs ⊆ ds → as ++ cs ⊆ bs ++ ds
  ++⁺ = HeteroProperties.++⁺

  ++⁻ : ∀ {cs ds} → length as ≡ length bs → as ++ cs ⊆ bs ++ ds → cs ⊆ ds
  ++⁻ = HeteroProperties.++⁻

------------------------------------------------------------------------
-- take

module _  where

  take⁺ : ∀ {m n} {xs} → m ≤ n → take m xs ⊆ take n xs
  take⁺ m≤n = HeteroProperties.take⁺ m≤n ≋-refl

------------------------------------------------------------------------
-- drop

module _ {m n} {xs ys : List A} where

  drop⁺ : m ≥ n → xs ⊆ ys → drop m xs ⊆ drop n ys
  drop⁺ = HeteroProperties.drop⁺

module _ {m n} {xs : List A} where

  drop⁺-≥ : m ≥ n → drop m xs ⊆ drop n xs
  drop⁺-≥ m≥n = drop⁺ m≥n ⊆-refl

module _ {xs ys : List A} where

  drop⁺-⊆ : ∀ n → xs ⊆ ys → drop n xs ⊆ drop n ys
  drop⁺-⊆ n xs⊆ys = drop⁺ {n} ℕₚ.≤-refl xs⊆ys

------------------------------------------------------------------------
-- takeWhile / dropWhile

module _ {p q} {P : Pred A p} {Q : Pred A q}
         (P? : Decidable P) (Q? : Decidable Q) where

  takeWhile⁺ : ∀ {xs} → (∀ {a b} → a ≈ b → P a → Q b) →
               takeWhile P? xs ⊆ takeWhile Q? xs
  takeWhile⁺ {xs} P⇒Q = HeteroProperties.⊆-takeWhile-Sublist P? Q? {xs} P⇒Q ≋-refl

  dropWhile⁺ : ∀ {xs} → (∀ {a b} → a ≈ b → Q b → P a) →
               dropWhile P? xs ⊆ dropWhile Q? xs
  dropWhile⁺ {xs} P⇒Q = HeteroProperties.⊇-dropWhile-Sublist P? Q? {xs} P⇒Q ≋-refl

------------------------------------------------------------------------
-- filter

module _ {p q} {P : Pred A p} {Q : Pred A q}
         (P? : Decidable P) (Q? : Decidable Q) where

  filter⁺ : ∀ {as bs} → (∀ {a b} → a ≈ b → P a → Q b) →
            as ⊆ bs → filter P? as ⊆ filter Q? bs
  filter⁺ = HeteroProperties.⊆-filter-Sublist P? Q?

------------------------------------------------------------------------
-- reverse

module _ {as bs : List A} where

  reverseAcc⁺ : ∀ {cs ds} → as ⊆ bs → cs ⊆ ds →
                reverseAcc cs as ⊆ reverseAcc ds bs
  reverseAcc⁺ = HeteroProperties.reverseAcc⁺

  reverse⁺ : as ⊆ bs → reverse as ⊆ reverse bs
  reverse⁺ = HeteroProperties.reverse⁺

  reverse⁻ : reverse as ⊆ reverse bs → as ⊆ bs
  reverse⁻ = HeteroProperties.reverse⁻

------------------------------------------------------------------------
-- Inversion lemmas
------------------------------------------------------------------------

module _ {a b} {A : Set a} {B : Set b} {a as b bs} where

  ∷⁻¹ : a ≈ b → as ⊆ bs ⇔ a ∷ as ⊆ b ∷ bs
  ∷⁻¹ = HeteroProperties.∷⁻¹

  ∷ʳ⁻¹ : ¬ (a ≈ b) → a ∷ as ⊆ bs ⇔ a ∷ as ⊆ b ∷ bs
  ∷ʳ⁻¹ = HeteroProperties.∷ʳ⁻¹

------------------------------------------------------------------------
-- Other
------------------------------------------------------------------------

module _ where

  length-mono-≤ : ∀ {as bs} → as ⊆ bs → length as ≤ length bs
  length-mono-≤ = HeteroProperties.length-mono-≤

------------------------------------------------------------------------
-- Conversion to and from list equality

  to-≋ : ∀ {as bs} → length as ≡ length bs → as ⊆ bs → as ≋ bs
  to-≋ = HeteroProperties.toPointwise

------------------------------------------------------------------------
-- Irrelevant special case

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

  []⊆-irrelevant : Irrelevant ([] ⊆_)
  []⊆-irrelevant = HeteroProperties.Sublist-[]-irrelevant

------------------------------------------------------------------------
-- (to/from)∈ is a bijection

module _ {x xs} where

  to∈-injective : ∀ {p q : [ x ] ⊆ xs} → to∈ p ≡ to∈ q → p ≡ q
  to∈-injective = HeteroProperties.toAny-injective

  from∈-injective : ∀ {p q : x ∈ xs} → from∈ p ≡ from∈ q → p ≡ q
  from∈-injective = HeteroProperties.fromAny-injective

  to∈∘from∈≗id : ∀ (p : x ∈ xs) → to∈ (from∈ p) ≡ p
  to∈∘from∈≗id = HeteroProperties.toAny∘fromAny≗id

  [x]⊆xs⤖x∈xs : ([ x ] ⊆ xs) ⤖ (x ∈ xs)
  [x]⊆xs⤖x∈xs = HeteroProperties.Sublist-[x]-bijection


text:
module Fail.TupleTerm where

open import Haskell.Prelude

pair2trip : a → b × c → a × b × c
pair2trip x xs = x ∷ xs

{-# COMPILE AGDA2HS pair2trip #-}


text:
open import Level using () renaming (_⊔_ to _⊔ˡ_)

open import Relation.Binary.Morphism.Structures using (IsRelHomomorphism)
open import Algebra.Bundles using (RawMonoid; RawGroup; RawRing)

open import Algebra.Morphism.Structures using (IsMonoidHomomorphism; IsMonoidMonomorphism)

module AKS.Algebra.Morphism.Structures where

module GroupMorphisms {c₁ c₂ ℓ₁ ℓ₂} (G₁ : RawGroup c₁ ℓ₁) (G₂ : RawGroup c₂ ℓ₂) where
  open RawGroup G₁ using () renaming (Carrier to C₁; _∙_ to _+₁_; _⁻¹ to -₁_; ε to ε₁; _≈_ to _≈₁_; rawMonoid to +₁-rawMonoid)
  open RawGroup G₂ using () renaming (Carrier to C₂; _∙_ to _+₂_; _⁻¹ to -₂_; ε to ε₂; _≈_ to _≈₂_; rawMonoid to +₂-rawMonoid)
  open import Algebra.Morphism.Definitions C₁ C₂ _≈₂_ using (Homomorphic₂; Homomorphic₁; Homomorphic₀)
  open import Function.Definitions _≈₁_ _≈₂_ using (Injective)

  record IsGroupHomomorphism (⟦_⟧ : C₁ → C₂) : Set (c₁ ⊔ˡ ℓ₁ ⊔ˡ ℓ₂) where
    field
      isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧
      +-homo  : Homomorphic₂ ⟦_⟧ _+₁_ _+₂_
      -‿homo  : Homomorphic₁ ⟦_⟧ -₁_ -₂_
      ε-homo  : Homomorphic₀ ⟦_⟧ ε₁ ε₂

    open IsRelHomomorphism isRelHomomorphism public renaming (cong to ⟦⟧-cong)

    +-isMonoidHomomorphism : IsMonoidHomomorphism +₁-rawMonoid +₂-rawMonoid ⟦_⟧
    +-isMonoidHomomorphism = record
      { isMagmaHomomorphism = record
         { isRelHomomorphism = isRelHomomorphism
         ; homo = +-homo
         }
      ; ε-homo = ε-homo
      }

  record IsGroupMonomorphism (⟦_⟧ : C₁ → C₂) : Set (c₁ ⊔ˡ ℓ₁ ⊔ˡ ℓ₂) where
    field
      isGroupHomomorphism : IsGroupHomomorphism ⟦_⟧
      injective : Injective ⟦_⟧

    open IsGroupHomomorphism isGroupHomomorphism public

    +-isMonoidMonomorphism : IsMonoidMonomorphism +₁-rawMonoid +₂-rawMonoid ⟦_⟧
    +-isMonoidMonomorphism = record
      { isMonoidHomomorphism = +-isMonoidHomomorphism
      ; injective = injective
      }

open GroupMorphisms public

module RingMorphisms {c₁ c₂ ℓ₁ ℓ₂} (R₁ : RawRing c₁ ℓ₁) (R₂ : RawRing c₂ ℓ₂) where
  open RawRing R₁ using () renaming (Carrier to C₁; _+_ to _+₁_; _*_ to _*₁_; -_ to -₁_; 0# to 0#₁; 1# to 1#₁; _≈_ to _≈₁_)
  open RawRing R₂ using () renaming (Carrier to C₂; _+_ to _+₂_; _*_ to _*₂_; -_ to -₂_; 0# to 0#₂; 1# to 1#₂; _≈_ to _≈₂_)
  open import Algebra.Morphism.Definitions C₁ C₂ _≈₂_ using (Homomorphic₂; Homomorphic₁; Homomorphic₀)
  open import Function.Definitions _≈₁_ _≈₂_ using (Injective)

  +₁-rawGroup : RawGroup c₁ ℓ₁
  +₁-rawGroup = record { Carrier = C₁ ; _≈_ = _≈₁_ ; _∙_ = _+₁_ ; _⁻¹ = -₁_ ; ε = 0#₁ }

  +₂-rawGroup : RawGroup c₂ ℓ₂
  +₂-rawGroup = record { Carrier = C₂ ; _≈_ = _≈₂_ ; _∙_ = _+₂_ ; _⁻¹ = -₂_ ; ε = 0#₂ }

  *₁-rawMonoid : RawMonoid c₁ ℓ₁
  *₁-rawMonoid = record { Carrier = C₁ ; _≈_ = _≈₁_ ; _∙_ = _*₁_ ; ε = 1#₁ }

  *₂-rawMonoid : RawMonoid c₂ ℓ₂
  *₂-rawMonoid = record { Carrier = C₂ ; _≈_ = _≈₂_ ; _∙_ = _*₂_ ; ε = 1#₂ }

  record IsRingHomomorphism (⟦_⟧ : C₁ → C₂) : Set (c₁ ⊔ˡ ℓ₁ ⊔ˡ ℓ₂) where
    field
      isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧
      +-homo  : Homomorphic₂ ⟦_⟧ _+₁_ _+₂_
      *-homo  : Homomorphic₂ ⟦_⟧ _*₁_ _*₂_
      -‿homo  : Homomorphic₁ ⟦_⟧ -₁_ -₂_
      0#-homo : Homomorphic₀ ⟦_⟧ 0#₁ 0#₂
      1#-homo : Homomorphic₀ ⟦_⟧ 1#₁ 1#₂

    open IsRelHomomorphism isRelHomomorphism public renaming (cong to ⟦⟧-cong)

    +-isGroupHomomorphism : IsGroupHomomorphism +₁-rawGroup +₂-rawGroup ⟦_⟧
    +-isGroupHomomorphism = record
      { isRelHomomorphism = isRelHomomorphism
      ; +-homo = +-homo
      ; -‿homo = -‿homo
      ; ε-homo = 0#-homo
      }

    *-isMonoidHomomorphism : IsMonoidHomomorphism *₁-rawMonoid *₂-rawMonoid ⟦_⟧
    *-isMonoidHomomorphism = record
      { isMagmaHomomorphism = record
        { isRelHomomorphism = isRelHomomorphism
        ; homo = *-homo
        }
      ; ε-homo = 1#-homo
      }

  record IsRingMonomorphism (⟦_⟧ : C₁ → C₂) : Set (c₁ ⊔ˡ ℓ₁ ⊔ˡ ℓ₂) where
    field
      isRingHomomorphism : IsRingHomomorphism ⟦_⟧
      injective : Injective ⟦_⟧

    open IsRingHomomorphism isRingHomomorphism public

    +-isGroupMonomorphism : IsGroupMonomorphism +₁-rawGroup +₂-rawGroup ⟦_⟧
    +-isGroupMonomorphism = record
      { isGroupHomomorphism = +-isGroupHomomorphism
      ; injective = injective
      }

    *-isMonoidMonomorphism : IsMonoidMonomorphism *₁-rawMonoid *₂-rawMonoid ⟦_⟧
    *-isMonoidMonomorphism = record
      { isMonoidHomomorphism = *-isMonoidHomomorphism
      ; injective = injective
      }

open RingMorphisms public

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


text:
-- Andreas, 2016-07-19 issue #382, duplicate of #278
-- report and test case by Nisse, 2011-01-30

module Issue382 {A : Set} where

data _≡_ (x : A) : A → Set where
  refl : x ≡ x

abstract

  id : A → A
  id x = y
    where y = x

  lemma : ∀ x → id x ≡ x
  lemma x = refl

-- should succeed


text:
-- Andreas, 2015-09-12, issue reported by F Mazzoli
-- {-# OPTIONS -v tc.meta.assign.proj:85 #-}

open import Common.Product
open import Common.Equality

module _ (A : Set) where

mutual
  X : A × A → A
  X = _

  test : (x y : A × A) → X (proj₁ x , proj₁ y) ≡ proj₁ x
  test x y = refl

-- In order to solve X, record variables x and y
-- have to be expanded.

-- Previously, this happend only if projections were
-- direct argument to the meta-variable.
-- Now, we also accept them inside record constructors.

verify : ∀{p} → X p ≡ proj₁ p
verify = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
import      Lvl
open import Type

module FormalLanguage.RegularExpression {ℓ} (Σ : Type{ℓ}) where

open import Data.Boolean
open import Data.Boolean.Stmt.Proofs
open import Data.List as List using (List)
open import FormalLanguage
open import FormalLanguage.Proofs
open import Functional
open import Logic
open import Logic.Propositional
open import Numeral.Natural
open import Relator.Equals

data RegExp : Type{ℓ} where
  ∅ : RegExp     -- Empty language (Consisting of no words).
  ε : RegExp     -- Empty word language (Consisting of a single empty word).
  • : Σ → RegExp -- Singleton language (Consisting of a single one letter word).
  _++_ : RegExp → RegExp → RegExp -- Concatenation language (Consisting of the words concatenated pairwise).
  _‖_  : RegExp → RegExp → RegExp -- Union language (Consisting of the words in both languages).
  _*   : RegExp → RegExp          -- Infinite concatenations language (Consisting of the words concatenated with themselves any number of times).

-- Non-empty infinite concatenations language.
_+ : RegExp → RegExp
e + = e ++ (e *)

-- Optional expression language
_?? : RegExp → RegExp
e ?? = ε ‖ e

-- Finitely repeated expression language
exactly : ℕ → RegExp → RegExp
exactly 𝟎      e = ε
exactly (𝐒(n)) e = e ++ (exactly n e)

-- Minimum repetitions of an expression language
at-least : ℕ → RegExp → RegExp
at-least 𝟎      e = e *
at-least (𝐒(n)) e = e ++ (at-least n e)

-- Maximum repetitions of an expression language
at-most : ℕ → RegExp → RegExp
at-most 𝟎      e = ε
at-most (𝐒(n)) e = ε ‖ (e ++ (at-most n e))

-- Relation for whether a pattern/expression matches a word (whether the word is in the language that the pattern/expression describes).
data _matches_ : RegExp → List(Σ) → Stmt{ℓ} where
  empty-word : ε matches List.∅
  concatenation : ∀{r₁ r₂}{l₁ l₂} → (r₁ matches l₁) → (r₂ matches l₂) → ((r₁ ++ r₂) matches (l₁ List.++ l₂))
  disjunctionₗ : ∀{rₗ rᵣ}{l} → (rₗ matches l) → ((rₗ ‖ rᵣ) matches l)
  disjunctionᵣ : ∀{rₗ rᵣ}{l} → (rᵣ matches l) → ((rₗ ‖ rᵣ) matches l)
  iteration : ∀{r}{l₁ l₂} → (r matches l₁) → ((r *) matches l₂) → ((r *) matches (l₁ List.++ l₂))
  literal : ∀{a} → ((• a) matches List.singleton(a))

-- optional-empty : ∀{e} → ((e ??) matches List.∅)
pattern optional-empty = disjunctionₗ empty-word

optional-self : ∀{e}{l} → (e matches l) → ((e ??) matches l)
optional-self = disjunctionᵣ

empty-none : ∀{l} → ¬(∅ matches l)
empty-none ()

module _ ⦃ _ : ComputablyDecidable(_≡_) ⦄ where
  language : RegExp → Language(Σ)
  language ∅        = Oper.∅
  language ε        = Oper.ε
  language (• x)    = Oper.single x
  language (x ++ y) = language(x) Oper.𝁼 language(y)
  language (x ‖ y)  = language(x) Oper.∪ language(y)
  language (x *)    = language(x) Oper.*

  postulate matches-language : ∀{e}{l} → (e matches l) → (l Oper.∈ language(e))
  {-matches-language {ε} {List.∅} empty-word = [⊤]-intro
  matches-language {• a} {.a List.⊰ .List.∅} literal = {!!}
  matches-language {e₁ ++ e₂} {List.∅}     p = {!!}
  matches-language {e₁ ++ e₂} {x List.⊰ l} p = {!!}
  matches-language {e₁ ‖ e₂} {List.∅} (disjunctionₗ p) = IsTrue.[∨]-introₗ(matches-language {e₁} p)
  matches-language {e₁ ‖ e₂} {List.∅} (disjunctionᵣ p) = IsTrue.[∨]-introᵣ(matches-language {e₂} p)
    matches-language {e₁ ‖ e₂} {x List.⊰ l} (disjunctionₗ p) = [↔]-to-[←] ([∪]-containment {x = x List.⊰ l}{A = language(e₁)}{B = language(e₂)}) ([∨]-introₗ (matches-language {e₁} p))
    matches-language {e₁ ‖ e₂} {x List.⊰ l} (disjunctionᵣ p) = [↔]-to-[←] ([∪]-containment {x = x List.⊰ l}{A = language(e₁)}{B = language(e₂)}) ([∨]-introᵣ (matches-language {e₂} p))
  matches-language {e *} {List.∅}     p = {!!}
  matches-language {e *} {x List.⊰ l} p = {!!}
  -}

  postulate language-matches : ∀{e}{l} → (l Oper.∈ language(e)) → (e matches l)
  {-language-matches {∅}        {x List.⊰ l} p with () ← language-matches {∅} {l} p
  language-matches {ε}        {List.∅}     [⊤]-intro = empty-word
  language-matches {ε}        {x List.⊰ l} p with () ← [↔]-to-[→] ([ε]-containment {x = x List.⊰ l}) p
  language-matches {• a}      {x List.⊰ l} p with [≡]-intro ← [↔]-to-[→] (single-containment {x = x List.⊰ l}) p = literal
  language-matches {e₁ ++ e₂} {List.∅}     p = {!!}
  language-matches {e₁ ++ e₂} {x List.⊰ l} p = {!!}
  language-matches {e₁ ‖ e₂}  {l} p = [∨]-elim (disjunctionₗ ∘ language-matches) (disjunctionᵣ ∘ language-matches) ([↔]-to-[→] ([∪]-containment {x = l} {A = language(e₁)} {B = language(e₂)}) p)
  language-matches {e *}      {List.∅} [⊤]-intro = {![*]-containment!}
  language-matches {e *}      {x List.⊰ l} p = {!!}
  -}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
-- Currently primitive functions are not allowed in mutual blocks.
-- This might change.
module PrimitiveInMutual where

postulate String : Set
{-# BUILTIN STRING String #-}

mutual
  primitive primStringAppend : String -> String -> String

  _++_ : String -> String -> String
  x ++ y = primStringAppend x y

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Basic definitions for morphisms between algebraic structures
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

open import Relation.Binary.Core

module Algebra.Morphism.Definitions
  {a} (A : Set a)     -- The domain of the morphism
  {b} (B : Set b)     -- The codomain of the morphism
  {ℓ} (_≈_ : Rel B ℓ)  -- The equality relation over the codomain
  where

open import Algebra.Core
open import Function.Core

------------------------------------------------------------------------
-- Basic definitions

Homomorphic₀ : (A → B) → A → B → Set _
Homomorphic₀ ⟦_⟧ ∙ ∘ = ⟦ ∙ ⟧ ≈ ∘

Homomorphic₁ : (A → B) → Op₁ A → Op₁ B → Set _
Homomorphic₁ ⟦_⟧ ∙_ ∘_ = ∀ x → ⟦ ∙ x ⟧ ≈ (∘ ⟦ x ⟧)

Homomorphic₂ : (A → B) → Op₂ A → Op₂ B → Set _
Homomorphic₂ ⟦_⟧ _∙_ _∘_ = ∀ x y → ⟦ x ∙ y ⟧ ≈ (⟦ x ⟧ ∘ ⟦ y ⟧)

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 1.3

Morphism : Set _
Morphism = A → B

{-# WARNING_ON_USAGE Morphism
"Warning: Morphism was deprecated in v1.3.
Please use the standard function notation (e.g. A → B) instead."
#-}


text:
module 842Isomorphism where

-- Library

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; cong-app; sym) -- added last
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Nat.Properties using (+-comm; +-suc; +-identityʳ) -- added last

-- Function composition.

_∘_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
(g ∘ f) x = g (f x)

_∘′_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
g ∘′ f = λ x → g (f x)

postulate
  extensionality : ∀ {A B : Set} {f g : A → B}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    → f ≡ g

-- Another definition of addition.

_+′_ : ℕ → ℕ → ℕ -- split on n instead, get different code
m +′ zero = m
m +′ suc n = suc (m +′ n)

same-app : ∀ (m n : ℕ) → m +′ n ≡ m + n
same-app m zero = sym (+-identityʳ m)
same-app m (suc n) rewrite +-suc m n | same-app m n = refl

same : _+′_ ≡ _+_  -- this requires extensionality
same = extensionality λ x → extensionality λ x₁ → same-app x x₁

-- Isomorphism.

infix 0 _≃_
record _≃_ (A B : Set) : Set where
  constructor mk-≃  -- This has been added, not in PLFA
  field
    to   : A → B
    from : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
    to∘from : ∀ (y : B) → to (from y) ≡ y
open _≃_

-- Equivalent to the following:

data _≃′_ (A B : Set): Set where
  mk-≃′ : ∀ (to : A → B) →
          ∀ (from : B → A) →
          ∀ (from∘to : (∀ (x : A) → from (to x) ≡ x)) →
          ∀ (to∘from : (∀ (y : B) → to (from y) ≡ y)) →
          A ≃′ B

to′ : ∀ {A B : Set} → (A ≃′ B) → (A → B)
to′ (mk-≃′ f g g∘f f∘g) = f

from′ : ∀ {A B : Set} → (A ≃′ B) → (B → A)
from′ (mk-≃′ f g g∘f f∘g) = g

from∘to′ : ∀ {A B : Set} → (A≃B : A ≃′ B)
                         → (∀ (x : A)
                         → from′ A≃B (to′ A≃B x) ≡ x)
from∘to′ (mk-≃′ f g g∘f f∘g) = g∘f

to∘from′ : ∀ {A B : Set} → (A≃B : A ≃′ B)
                         → (∀ (y : B)
                         → to′ A≃B (from′ A≃B y) ≡ y)
to∘from′ (mk-≃′ f g g∘f f∘g) = f∘g

-- End of equivalent formulation (records are faster!)

-- Properties of isomorphism.

-- Reflexivity.

≃-refl : ∀ {A : Set}
    -----
  → A ≃ A

-- in empty hole, split on result, get copatterns (not in PLFA)

to ≃-refl x = x
from ≃-refl x = x
from∘to ≃-refl x = refl
to∘from ≃-refl x = refl

-- Symmetry.

≃-sym : ∀ {A B : Set}
  → A ≃ B
    -----
  → B ≃ A

to (≃-sym A≃B) = from A≃B
from (≃-sym A≃B) = to A≃B
from∘to (≃-sym A≃B) = to∘from A≃B
to∘from (≃-sym A≃B) = from∘to A≃B

-- Transitivity.

≃-trans : ∀ {A B C : Set}
  → A ≃ B
  → B ≃ C
    -----
  → A ≃ C

to (≃-trans A≃B B≃C) = to B≃C ∘ to A≃B
from (≃-trans A≃B B≃C) = from A≃B ∘ from B≃C
from∘to (≃-trans A≃B B≃C) x rewrite from∘to B≃C (to A≃B x) = from∘to A≃B x
to∘from (≃-trans A≃B B≃C) x rewrite to∘from A≃B (from B≃C x) = to∘from B≃C x

-- Isomorphism is an equivalence relation.
-- We can create syntax for equational reasoning.

module ≃-Reasoning where

  infix  1 ≃-begin_
  infixr 2 _≃⟨_⟩_
  infix  3 _≃-∎

  ≃-begin_ : ∀ {A B : Set}
    → A ≃ B
      -----
    → A ≃ B
  ≃-begin A≃B = A≃B

  _≃⟨_⟩_ : ∀ (A : Set) {B C : Set}
    → A ≃ B
    → B ≃ C
      -----
    → A ≃ C
  A ≃⟨ A≃B ⟩ B≃C = ≃-trans A≃B B≃C

  _≃-∎ : ∀ (A : Set)
      -----
    → A ≃ A
  A ≃-∎ = ≃-refl

open ≃-Reasoning

-- Embedding (weaker than isomorphism)

infix 0 _≲_
record _≲_ (A B : Set) : Set where
  field
    to      : A → B
    from    : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
open _≲_

≲-refl : ∀ {A : Set} → A ≲ A
to ≲-refl x = x
from ≲-refl x = x
from∘to ≲-refl x = refl

≲-trans : ∀ {A B C : Set} → A ≲ B → B ≲ C → A ≲ C
to (≲-trans A≲B B≲C) = to B≲C ∘ to A≲B
from (≲-trans A≲B B≲C) = from A≲B ∘ from B≲C
from∘to (≲-trans A≲B B≲C) x rewrite from∘to B≲C (to A≲B x) = from∘to A≲B x

≲-antisym : ∀ {A B : Set}
  → (A≲B : A ≲ B)
  → (B≲A : B ≲ A)
  → (to A≲B ≡ from B≲A)
  → (from A≲B ≡ to B≲A)
    -------------------
  → A ≃ B

to (≲-antisym A≲B B≲A to≡from from≡to) = to A≲B
from (≲-antisym A≲B B≲A to≡from from≡to) = from A≲B
from∘to (≲-antisym A≲B B≲A to≡from from≡to) x = from∘to A≲B x
to∘from (≲-antisym A≲B B≲A to≡from from≡to) y
  rewrite from≡to | to≡from = from∘to B≲A y

-- Tabular reasoning for embedding.

module ≲-Reasoning where

  infix  1 ≲-begin_
  infixr 2 _≲⟨_⟩_
  infix  3 _≲-∎

  ≲-begin_ : ∀ {A B : Set}
    → A ≲ B
      -----
    → A ≲ B
  ≲-begin A≲B = A≲B

  _≲⟨_⟩_ : ∀ (A : Set) {B C : Set}
    → A ≲ B
    → B ≲ C
      -----
    → A ≲ C
  A ≲⟨ A≲B ⟩ B≲C = ≲-trans A≲B B≲C

  _≲-∎ : ∀ (A : Set)
      -----
    → A ≲ A
  A ≲-∎ = ≲-refl

open ≲-Reasoning

-- PLFA exercise: Isomorphism implies embedding.

≃-implies-≲ : ∀ {A B : Set}
  → A ≃ B
    -----
  → A ≲ B

to (≃-implies-≲ a≃b) = to a≃b
from (≃-implies-≲ a≃b) = from a≃b
from∘to (≃-implies-≲ a≃b) = from∘to a≃b

-- PLFA exercise: propositional equivalence (weaker than embedding).

record _⇔_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A
open _⇔_ -- added

-- This is also an equivalence relation.

⇔-refl : ∀ {A : Set}
    -----
  → A ⇔ A

_⇔_.to ⇔-refl x = x
_⇔_.from ⇔-refl x = x

⇔-sym : ∀ {A B : Set}
  → A ⇔ B
    -----
  → B ⇔ A

_⇔_.to (⇔-sym A⇔B) = from A⇔B
_⇔_.from (⇔-sym A⇔B) = to A⇔B

⇔-trans : ∀ {A B C : Set}
  → A ⇔ B
  → B ⇔ C
    -----
  → A ⇔ C

to (⇔-trans A⇔B B⇔C) = to B⇔C ∘ to A⇔B
from (⇔-trans A⇔B B⇔C) = from A⇔B ∘ from B⇔C

-- 842 extended exercise: Canonical bitstrings.
-- Modified and extended from Bin-predicates exercise in PLFA Relations.

-- Copied from 842Naturals.

data Bin-ℕ : Set where
  bits : Bin-ℕ
  _x0 : Bin-ℕ → Bin-ℕ
  _x1 : Bin-ℕ → Bin-ℕ

dbl : ℕ → ℕ
dbl zero = zero
dbl (suc n) = suc (suc (dbl n))

-- Copy your versions of 'inc', 'tob', and 'fromb' over from earlier files.
-- You may choose to change the definitions here to make proofs easier.
-- But make sure to test them if you do!
-- You may also copy over any theorems that prove useful.

inc : Bin-ℕ → Bin-ℕ
inc n = {!!}

tob : ℕ → Bin-ℕ
tob n = {!!}

dblb : Bin-ℕ → Bin-ℕ
dblb n = {!!}

fromb : Bin-ℕ → ℕ
fromb n = {!!}

-- The reason that we couldn't prove ∀ {n : Bin-ℕ} → tob (fromb n) ≡ n
-- is because of the possibility of leading zeroes in a Bin-ℕ value.
-- 'bits x0 x0 x1' is such a value that gives a counterexample.
-- However, the theorem is true is true for n without leading zeroes.
-- We define a predicate to be able to state this in a theorem.
-- A value of type One n is evidence that n has a leading one.

data One : Bin-ℕ → Set where
  [bitsx1] : One (bits x1)
  _[x0] : ∀ {n : Bin-ℕ} → One n → One (n x0)
  _[x1] : ∀ {n : Bin-ℕ} → One n → One (n x1)

-- Here's a proof that 'bits x1 x0 x0' has a leading one.

_ : One (bits x1 x0 x0)
_ = [bitsx1] [x0] [x0]

-- There is no value of type One (bits x0 x0 x1).
-- But we can't state and prove this yet, because we don't know
-- how to express negation. That comes in the Connectives chapter.

-- A canonical binary representation is either zero or has a leading one.

data Can : Bin-ℕ → Set where
  [zero] : Can bits
  [pos]  : ∀ {n : Bin-ℕ} → One n → Can n

-- Some obvious examples:

_ : Can bits
_ = [zero]

_ : Can (bits x1 x0)
_ = [pos] ([bitsx1] [x0])

-- The Bin-predicates exercise in PLFA Relations gives three properties of canonicity.
-- The first is that the increment of a canonical number is canonical.

-- Most of the work is done in the following lemma.

-- 842 exercise: IncCanOne (2 points)
-- The increment of a canonical number has a leading one.

one-inc : ∀ {n : Bin-ℕ} → Can n → One (inc n)
one-inc cn = {!!}

-- The first canonicity property is now an easy corollary.

-- 842 exercise: OneInc (1 point)

can-inc : ∀ {n : Bin-ℕ} → Can n → Can (inc n)
can-inc cn = {!!}

-- The second canonicity property is that converting a unary number
-- to binary produces a canonical number.

-- 842 exercise: CanToB (1 point)

to-can : ∀ (n : ℕ) → Can (tob n)
to-can n = {!!}

-- The third canonicity property is that converting a canonical number
-- from binary and back to unary produces the same number.

-- This takes more work, and some helper lemmas from 842Induction.
-- You will need to discover which ones.

-- 842 exercise: OneDblbX0 (1 point)

-- This helper function relates binary double to the x0 constructor,
-- for numbers with a leading one.

dblb-x0 : ∀ {n : Bin-ℕ} → One n → dblb n ≡ n x0
dblb-x0 on = {!!}

-- We can now prove the third property for numbers with a leading one.

-- 842 exercise: OneToFrom (3 points)

one-to∘from : ∀ {n : Bin-ℕ} → One n → tob (fromb n) ≡ n
one-to∘from on = {!!}

-- The third property is now an easy corollary.

-- 842 exercise: CanToFrom (1 point)

can-to∘from : ∀ {n : Bin-ℕ} → Can n → tob (fromb n) ≡ n
can-to∘from cn = {!!}

-- 842 exercise: OneUnique (2 points)
-- Proofs of positivity are unique.

one-unique : ∀ {n : Bin-ℕ} → (x y : One n) → x ≡ y
one-unique x y = {!!}

-- 842 exercise: CanUnique (1 point)
-- Proofs of canonicity are unique.

can-unique : ∀ {n : Bin-ℕ} → (x y : Can n) → x ≡ y
can-unique x y = {!!}

-- Do we have an isomorphism between ℕ (unary) and canonical binary representations?
-- Can is not a set, but a family of sets, so it doesn't quite fit
-- into our framework for isomorphism.
-- But we can roll all the values into one set which is isomorphic to ℕ.

-- A CanR value wraps up a Bin-ℕ and proof it has a canonical representation.

data CanR : Set where
  wrap : ∀ (n : Bin-ℕ) → Can n → CanR

-- We can show that there is an isomorphism between ℕ and CanR.

-- 842 exercise: IsoNCanR (3 points)

iso-ℕ-CanR : ℕ ≃ CanR
iso-ℕ-CanR = {!!}

-- Can we get an isomorphism between ℕ and some binary encoding,
-- without the awkwardness of non-canonical values?
-- Yes: we use digits 1 and 2, instead of 0 and 1 (multiplier/base is still 2).
-- This is known as bijective binary numbering.
-- The counting sequence goes <empty>, 1, 2, 11, 12, 21, 22, 111...

data Bij-ℕ : Set where
  bits : Bij-ℕ
  _x1 : Bij-ℕ → Bij-ℕ
  _x2 : Bij-ℕ → Bij-ℕ

-- There is an isomorphism between ℕ and Bij-ℕ.
-- The proof largely follows the outline of what we did above,
-- and is left as an optional exercise.

-- See PLFA for remarks on standard library definitions similar to those here.

-- Unicode introduced in this chapter:

{-

  ∘  U+2218  RING OPERATOR (\o, \circ, \comp)
  λ  U+03BB  GREEK SMALL LETTER LAMBDA (\lambda, \Gl)
  ≃  U+2243  ASYMPTOTICALLY EQUAL TO (\~-)
  ≲  U+2272  LESS-THAN OR EQUIVALENT TO (\<~)
  ⇔  U+21D4  LEFT RIGHT DOUBLE ARROW (\<=>)

-}

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
module Pi.AuxLemmas where
open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Pi.Syntax
open import Pi.Opsem

Lemma₁ : ∀ {A B C D v v' κ κ'} {c : A ↔ B} {c' : C ↔ D}
           → ⟨ c ∣ v ∣ κ ⟩ ↦ ［ c' ∣ v' ∣ κ' ］
           → A ≡ C × B ≡ D
Lemma₁ ↦₁ = refl , refl
Lemma₁ ↦₂ = refl , refl

Lemma₂ : ∀ {A B v v' κ κ'} {c c' : A ↔ B}
           → ⟨ c ∣ v ∣ κ ⟩ ↦ ［ c' ∣ v' ∣ κ' ］
           → c ≡ c' × κ ≡ κ'
Lemma₂ ↦₁ = refl , refl
Lemma₂ ↦₂ = refl , refl

Lemma₃ : ∀ {A B v v' κ} {c : A ↔ B}
           → (r : ⟨ c ∣ v ∣ κ ⟩ ↦ ［ c ∣ v' ∣ κ ］)
           → base c ⊎ A ≡ B
Lemma₃ (↦₁ {b = b}) = inj₁ b
Lemma₃ ↦₂ = inj₂ refl

Lemma₄ : ∀ {A v v' κ} {c : A ↔ A}
           → (r : ⟨ c ∣ v ∣ κ ⟩ ↦ ［ c ∣ v' ∣ κ ］)
           → base c ⊎ c ≡ id↔
Lemma₄ {c = swap₊} ↦₁ = inj₁ tt
Lemma₄ {c = swap⋆} ↦₁ = inj₁ tt
Lemma₄ ↦₂ = inj₂ refl


text:
{-# OPTIONS --sized-types #-}
module SBList {A : Set}(_≤_ : A → A → Set) where

open import Bound.Total A
open import Bound.Total.Order _≤_
open import Data.List
open import Data.Product
open import Size

data SBList : {ι : Size} → Bound → Bound → Set where
  nil : {ι : Size}{b t : Bound}
                   → LeB b t
                   → SBList {↑ ι} b t
  cons : {ι : Size}{b t : Bound}
                   (x : A)
                   → LeB b (val x)
                   → LeB (val x) t
                   → SBList {ι} b t
                   → SBList {↑ ι} b t

bound : List A → SBList bot top
bound [] = nil lebx
bound (x ∷ xs) = cons x lebx lext (bound xs)

unbound : {b t : Bound} → SBList b t → List A
unbound (nil _) = []
unbound (cons x _ _ xs) = x ∷ unbound xs

unbound× : {ι : Size}{b t b' t' : Bound} → SBList {ι} b t × SBList {ι} b' t' → List A × List A
unbound×  (xs , ys) = (unbound xs , unbound ys)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module EqProof
  { A : Set }
  ( _==_ : A -> A -> Set )
  (refl  : {x : A} -> x == x)
  (trans : {x y z : A} -> x == y -> y == z -> x == z)
  where

  infix 2 eqProof>_
  infixl 2 _===_
  infix 3 _by_

  eqProof>_ : (x : A) -> x == x
  eqProof> x = refl

  _===_ : {x y z : A} -> x == y -> y == z -> x == z
  xy === yz = trans xy yz

  _by_ : {x : A}(y : A) -> x == y -> x == y
  y by eq = eq

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
{-# OPTIONS --without-K --rewriting #-}

open import HoTT
open import cohomology.Theory
open import homotopy.DisjointlyPointedSet

module cohomology.DisjointlyPointedSet {i} (OT : OrdinaryTheory i) where

  open OrdinaryTheory OT

  module _ (n : ℤ) (X : Ptd i)
    (X-is-set : is-set (de⊙ X)) (dec : is-separable X)
    (ac : has-choice 0 (de⊙ X) i) where

    private

      lemma : BigWedge {A = MinusPoint X} (λ _ → ⊙Bool) ≃ de⊙ X
      lemma = equiv to from to-from from-to where
        from : de⊙ X → BigWedge {A = MinusPoint X} (λ _ → ⊙Bool)
        from x with dec x
        from x | inl p  = bwbase
        from x | inr ¬p = bwin (x , ¬p) false

        module From = BigWedgeRec {A = MinusPoint X} {X = λ _ → ⊙Bool}
          (pt X) (λ{_ true → pt X; (x , _) false → x}) (λ _ → idp)
        to = From.f

        abstract
          from-to : ∀ x → from (to x) == x
          from-to = BigWedge-elim base* in* glue* where
            base* : from (pt X) == bwbase
            base* with dec (pt X)
            base* | inl _  = idp
            base* | inr ¬p = ⊥-rec (¬p idp)

            in* : (wp : MinusPoint X) (b : Bool)
              → from (to (bwin wp b)) == bwin wp b
            in* wp true with dec (pt X)
            in* wp true | inl _ = bwglue wp
            in* wp true | inr pt≠pt = ⊥-rec (pt≠pt idp)
            in* (x , pt≠x) false with dec x
            in* (x , pt≠x) false | inl pt=x = ⊥-rec (pt≠x pt=x)
            in* (x , pt≠x) false | inr pt≠'x =
              ap (λ ¬p → bwin (x , ¬p) false) $ prop-has-all-paths ¬-is-prop pt≠'x pt≠x

            glue* : (wp : MinusPoint X)
              → base* == in* wp true [ (λ x → from (to x) == x) ↓ bwglue wp ]
            glue* wp = ↓-∘=idf-from-square from to $ ap (ap from) (From.glue-β wp) ∙v⊡ square where
              square : Square base* idp (bwglue wp) (in* wp true)
              square with dec (pt X)
              square | inl _ = br-square (bwglue wp)
              square | inr ¬p = ⊥-rec (¬p idp)

          to-from : ∀ x → to (from x) == x
          to-from x with dec x
          to-from x | inl pt=x = pt=x
          to-from x | inr pt≠x = idp

    C-set : C n X ≃ᴳ Πᴳ (MinusPoint X) (λ _ → C n (⊙Lift ⊙Bool))
    C-set =
      C n X
        ≃ᴳ⟨ C-emap n (≃-to-⊙≃ lemma idp) ⟩
      C n (⊙BigWedge {A = MinusPoint X} (λ _ → ⊙Bool))
        ≃ᴳ⟨ C-emap n (⊙BigWedge-emap-r λ _ → ⊙lower-equiv) ⟩
      C n (⊙BigWedge {A = MinusPoint X} (λ _ → ⊙Lift ⊙Bool))
        ≃ᴳ⟨ C-additive-iso n (λ _ → ⊙Lift ⊙Bool)
              (MinusPoint-has-choice 0 (separable-has-disjoint-pt dec) ac) ⟩
      Πᴳ (MinusPoint X) (λ _ → C n (⊙Lift ⊙Bool))
        ≃ᴳ∎

  module _ {n : ℤ} (n≠0 : n ≠ 0) (X : Ptd i)
    (X-is-set : is-set (de⊙ X)) (dec : is-separable X)
    (ac : has-choice 0 (de⊙ X) i) where

    C-set-≠-is-trivial : is-trivialᴳ (C n X)
    C-set-≠-is-trivial = iso-preserves'-trivial
      (C-set n X X-is-set dec ac)
      (Πᴳ-is-trivial (MinusPoint X)
        (λ _ → C n (⊙Lift ⊙Bool))
        (λ _ → C-dimension n≠0))

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
-- Data: init commit

--{-# OPTIONS --show-implicit #-}
--{-# OPTIONS --rewriting #-}
module Oscar.Data0 where

data ⟦⟧ : Set where
  ∅ : ⟦⟧
  ! : ⟦⟧ → ⟦⟧

data ⟦_⟧ {a} (A : Set a) : Set a where
  ∅ : ⟦ A ⟧
  _∷_ : A → ⟦ A ⟧ → ⟦ A ⟧

data ⟦⟧[_] : ⟦⟧ → Set where
  ∅ : ∀ {n} → ⟦⟧[ ! n ]
  ! : ∀ {n} → ⟦⟧[ n ] → ⟦⟧[ ! n ]

data ⟦_⟧[_] {a} (A : ⟦⟧ → Set a) : ⟦⟧ → Set a where
  ∅ : ∀ {n} → ⟦ A ⟧[ ! n ]
  _∷_ : ∀ {n} → A n → ⟦ A ⟧[ n ] → ⟦ A ⟧[ ! n ]

data ⟦⟧[_≤↓_] (m : ⟦⟧) : ⟦⟧ → Set where
  ∅ : ⟦⟧[ m ≤↓ m ]
  ! : ∀ {n} → ⟦⟧[ m ≤↓ n ] → ⟦⟧[ m ≤↓ ! n ]

data ⟦_⟧[_≤↓_] {a} (A : ⟦⟧ → Set a) (m : ⟦⟧) : ⟦⟧ → Set a where
  ∅ : ⟦ A ⟧[ m ≤↓ m ]
  _∷_ : ∀ {n} → A n → ⟦ A ⟧[ m ≤↓ n ] → ⟦ A ⟧[ m ≤↓ ! n ]

data ⟦⟧[_↑≤_] (m : ⟦⟧) : ⟦⟧ → Set where
  ∅ : ⟦⟧[ m ↑≤ m ]
  ! : ∀ {n} → ⟦⟧[ ! m ↑≤ n ] → ⟦⟧[ m ↑≤ n ]

data ⟦_⟧[_↑≤_] {a} (A : ⟦⟧ → Set a) (m : ⟦⟧) : ⟦⟧ → Set a where
  ∅ : ⟦ A ⟧[ m ↑≤ m ]
  _∷_ : ∀ {n} → A m → ⟦ A ⟧[ ! m ↑≤ n ] → ⟦ A ⟧[ m ↑≤ n ]

data ⟦⟧[_↓≤↓_] : ⟦⟧ → ⟦⟧ → Set where
  ∅ : ∀ {n} → ⟦⟧[ ∅ ↓≤↓ n ]
  ! : ∀ {m n} → ⟦⟧[ m ↓≤↓ n ] → ⟦⟧[ ! m ↓≤↓ ! n ]

data ⟦_⟧[_↓≤↓_] {a} (A : ⟦⟧ → ⟦⟧ → Set a) : ⟦⟧ → ⟦⟧ → Set a where
  ∅ : ∀ {n} → ⟦ A ⟧[ ∅ ↓≤↓ n ]
  ! : ∀ {m n} → A m n → ⟦ A ⟧[ m ↓≤↓ n ] → ⟦ A ⟧[ ! m ↓≤↓ ! n ]

-- open import Oscar.Data.Unit
-- open import Oscar.Level
-- open import Data.Empty

-- 𝕋 : ∀ {a} {A : Set a} → A → Set
-- 𝕋 = λ _ → ⊤

-- postulate
--   ℓ : Level
--   Term : Set ℓ

-- -- module _ where -- second constructor is recursive

-- --   -- Nat
-- --   data ⟦⟧ : Set where
-- --     ∅ : ⟦⟧
-- --     ! : ⟦⟧ → ⟦⟧

-- --   -- List
-- --   data ⟦_⟧ {a} (A : Set a) : Set a where
-- --     ∅ : ⟦ A ⟧
-- --     _∷_ : A → ⟦ A ⟧ → ⟦ A ⟧

-- --   -- ⋆⋆ m, size: m
-- --   -- [ 0 ] = nothing
-- --   -- [ 1 ] = ∅0
-- --   -- [ 4 ] = ∅3 or !2∅3 or !1!2∅3 or !0!1!2∅3
-- --   data ⟦⟧[_] : ⟦⟧ → Set where
-- --     ∅ : ∀ {n} → ⟦⟧[ ! n ]
-- --     ! : ∀ {n} → ⟦⟧[ n ] → ⟦⟧[ ! n ]

-- --   data ⟦_⟧[_] {a} (A : ⟦⟧ → Set a) : ⟦⟧ → Set a where
-- --     ∅ : ∀ {n} → ⟦ A ⟧[ ! n ]
-- --     _∷_ : ∀ {n} → A n → ⟦ A ⟧[ n ] → ⟦ A ⟧[ ! n ]

-- --   -- 0 : ∅ (only)
-- --   -- 1 : ∅ or ! ∅
-- --   -- 2 : ∅ or ! ∅
-- --   -- 5 : ∅ or !
-- --   -- size: m + 1
-- --   -- ⋆⋆'' 0 = ∅0
-- --   -- ⋆⋆'' 4 = ∅(m=4) or !3∅4 or !2!3∅4 or !1!2!3∅4 or !0!1!2!3∅4
-- --   data ⋆⋆'' (m : ⟦⟧) : Set where
-- --     ∅ : ⋆⋆'' m
-- --     ! : ⋆⋆'' (! m) → ⋆⋆'' m

-- --   -- ⋆⋆'' ⊂ ⋆⋆

-- --   -- m ≤ n == n - 1 ⋱ m
-- --   -- m ↙ n
-- --   -- size = n - m
-- --   -- AList
-- --   -- 4≤↓2 = nothing
-- --   -- 2≤↓4 = !23!22∅22
-- --   data ⟦⟧[_≤↓_] (m : ⟦⟧) : ⟦⟧ → Set where
-- --     ∅ : ⟦⟧[ m ≤↓ m ]
-- --     ! : ∀ {n} → ⟦⟧[ m ≤↓ n ] → ⟦⟧[ m ≤↓ ! n ]
-- --     -- A n

-- --   （_⋱_］ : ⟦⟧ → ⟦⟧ → Set
-- --   （ n ⋱ m ］ = ⟦⟧[ m ≤↓ n ]

-- --   data ⟦_⟧[_≤↓_] {a} (A : ⟦⟧ → Set a) (m : ⟦⟧) : ⟦⟧ → Set where
-- --     ∅ : ⟦ A ⟧[ m ≤↓ m ]
-- --     ! : ∀ {n} → A n → ⟦ A ⟧[ m ≤↓ n ] → ⟦⟧[ m ≤↓ ! n ]

-- --   -- m ≤ n = m ⋰ n - 1
-- --   -- m ↗ n
-- --   -- size = n - m (+1?)
-- --   -- 2↑≤4 = !24!34∅44
-- --   data _↑≤_ (m : ⟦⟧) : ⟦⟧ → Set where
-- --     ∅ : m ↑≤ m
-- --     ! : ∀ {n} → ! m ↑≤ n → m ↑≤ n
-- --     -- A m

-- --   ［_⋰_） : ⟦⟧ → ⟦⟧ → Set
-- --   ［ m ⋰ n ） = m ↑≤ n

-- --   -- m ≤ n == n - 1 ⋱ n - m && m - 1 ⋱ 0
-- --   -- size = m (+1?)
-- --   -- Inj
-- --   -- 2↓≤↓4 = !13!02∅02
-- --   data _↓≤↓_ : ⟦⟧ → ⟦⟧ → Set where
-- --     ∅ : ∀ {n} → ∅ ↓≤↓ n
-- --     ! : ∀ {m n} → m ↓≤↓ n → ! m ↓≤↓ ! n -- A m n

-- --   -- Fin
-- --   -- P 0 = ∅0 or !0∅1 or !0!1∅2 or ...
-- --   -- P 3 = ∅3 or !3∅4 or !3!4∅5 or ... (infinite)
-- --   data P (n : ⋆) : Set where
-- --     ∅ : P n
-- --     ! : P (! n) → P n

-- --   {-
-- --     3 <= 5 = ! (4 <= 5) = ! ! (5 <= 5) = ! ! ∅
-- --     3≤5 witnesses
-- --     n=3,m=5
-- --       4   5
-- --   -}
-- --   -- m ≤ n == m ... n - 1 (this is the same as the two-indexed version)
-- --   data _≤_ (n : ⋆) : ⋆ → Set where
-- --     ∅ : n ≤ n
-- --     ! : ∀ {m} → ! n ≤ m → n ≤ m
-- --   -- or
-- --   -- m ≤ n == n - 1 ... m

-- --   three : ⋆
-- --   three = ! (! (! ∅))

-- --   five : ⋆
-- --   five = ! (! three)

-- --   foo : three ≤ five
-- --   foo = ! {n = {!!}} (! {n = {!!}} ∅)

-- -- --   {-
-- -- --     3 <= 5 = 3 <= ! 4 = ! (3 <= 4) = ! (! (3 <= 3)) = ! ! ∅
-- -- --     3 ≤ 5 witnesses
-- -- --     n=3,m=4
-- -- --     n=3,m=3
-- -- --
-- -- --   -}

-- -- --   data _≤_ (n : ⋆) : ⋆ → Set where
-- -- --     ∅ : n ≤ n
-- -- --     ! : ∀ {m} → n ≤ m → n ≤ ! m -- A m

-- -- --   {-
-- -- --     3 <= 5
-- -- --     m=2,n=4
-- -- --     m=1,n=3
-- -- --     m=0,n=2
-- -- --   -}
-- -- --   data _≤_ : ⋆ → ⋆ → Set where
-- -- --     ∅ : ∀ {n} → ∅ ≤ n
-- -- --     ! : ∀ {m n} → m ≤ n → ! m ≤ ! n

-- -- -- --   data # (n : ⋆) : Set where
-- -- -- --     ∅ : # n
-- -- -- --     ! : # (

-- -- -- --   data # : ⋆ → Set where
-- -- -- --     ∅ : # n
-- -- -- --     ! : ⋆

-- -- -- --   data ⋆[_] {a} (A : Set a) : Set a where
-- -- -- --     ∅ : ⋆[ A ]
-- -- -- --     _∷_ : A → ⋆[ A ] → ⋆[ A ]

-- -- -- --   data _≥_ (n : ⋆) : ⋆ → Set where
-- -- -- --     ∅ : n ≥ n
-- -- -- --     ! : ∀ {m} → n ≥ ¹⁺ m → n ≥ m

-- -- -- -- {-
-- -- -- --   data _≤_ (n : ⋆) : ⋆ → Set where
-- -- -- --     ∅ : n ≤ n
-- -- -- --     ! : ∀ {m} → n ≤ m → n ≤ ¹⁺ m
-- -- -- -- -}
-- -- -- --   data _≥_ : ⋆ → ⋆ → Set where
-- -- -- --     ∅ : ∀ {n} → n ≥ ∅
-- -- -- --     ! : ∀ {m n} → n ≥ m → ¹⁺ m ≤ ¹⁺ n

-- -- -- --   _≱_ : ⋆ → ⋆ → Set
-- -- -- --   n ≱ m = n ≥ m → ⊥

-- -- -- --   ε : ∀ {m} → m ≥ m
-- -- -- --   ε = ≥∅

-- -- -- --   ¹⁺≥ : ∀ {n m} → n ≥ m → ¹⁺ n ≥ m
-- -- -- --   ¹⁺≥ ≥∅ = ≥⁻¹ ≥∅
-- -- -- --   ¹⁺≥ (≥⁻¹ n≥m) = ≥⁻¹ (¹⁺≥ n≥m)

-- -- -- --   ∅≱¹⁺ : ∀ {n} → ∅ ≱ ¹⁺ n
-- -- -- --   ∅≱¹⁺ (≥⁻¹ ∅≥²⁺n) = ∅≱¹⁺ ∅≥²⁺n

-- -- -- --   _∙_ : ∀ {n m} → n ≥ m → ∀ {l} → m ≥ l → n ≥ l
-- -- -- --   ≥∅ ∙ ≥∅ = ≥∅
-- -- -- --   ≥∅ ∙ ≥⁻¹ x₁ = ⊥-elim ({!∅≱¹⁺ !})
-- -- -- --   ≥⁻¹ x ∙ ≥∅ = {!!}
-- -- -- --   _∙_ {n} {m} (≥⁻¹ x) {l} (≥⁻¹ x₁) = ≥⁻¹ (x ∙ ¹⁺≥ x₁)

-- -- -- --   stop≥ : ∀ {n} → n ≱ ¹⁺ n
-- -- -- --   stop≥ {∅} (≥⁻¹ x) = ∅≱¹⁺ x
-- -- -- --   stop≥ {¹⁺ n} (≥⁻¹ (≥⁻¹ x)) = {!stop≥ x!}

-- -- -- --   ¹⁺≥¹⁺ : ∀ {n m} → n ≥ m → ¹⁺ n ≥ ¹⁺ m
-- -- -- --   ¹⁺≥¹⁺ {∅} ≥∅ = ≥⁻¹ {¹⁺ ∅} {!!}
-- -- -- --   ¹⁺≥¹⁺ {¹⁺ n} ≥∅ = {!!}
-- -- -- --   ¹⁺≥¹⁺ (≥⁻¹ x) = {!!}

-- -- -- --   ⁻¹≥⁻¹ : ∀ {n m} → ¹⁺ n ≥ ¹⁺ m → n ≥ m
-- -- -- --   ⁻¹≥⁻¹ {n} {∅} (≥⁻¹ x) = {!!}
-- -- -- --   ⁻¹≥⁻¹ {∅} {¹⁺ m} (≥⁻¹ x) = ⊥-elim (∅≱¹⁺ (⁻¹≥⁻¹ x))
-- -- -- --   ⁻¹≥⁻¹ {¹⁺ n} {¹⁺ m} (≥⁻¹ x) = (⁻¹≥⁻¹ x) ∙ ¹⁺≥ {!!}

-- -- -- -- --   1>=1 : ¹⁺ ∅ ≥ ¹⁺ ∅
-- -- -- -- --   1>=1 = ¹⁺ {!!}

-- -- -- -- --   {- ⋮↓ -}
-- -- -- -- --   {- h  ｛ A ∣ 7 ≥ 4 ｝ = ｛ A 7 4 , A 7 5 , A 7 6 , A 7 7 ｝ -}
-- -- -- -- --   {- g  ｛ A ∣ 4 ≥ 2 ｝ = ｛ A 4 2 , A 4 3 , A 4 4 ｝ -}
-- -- -- -- --   {- h∘g｛ A ∣ 7 ≥ 2 ｝ = ｛ A 7 2 , A 7 3 , A 7 4 , A 7 5 , A 7 6 , A 7 7 ｝ -}
-- -- -- -- --   {- f  ｛ A ∣ 2 ≥ 0 ｝ = ｛ ｝ -}
-- -- -- -- --   {- g∘f｛ A ∣ 4 ≥ 0 ｝ = ｛ A 4 0 , A 4 1 , A 4 2 , A 4 3 , A 4 4 ｝ -}
-- -- -- -- --   data ⋆[_/_≥_] {a} (A : ⋆ → ⋆ → Set a) (m : ⋆) : ⋆ → Set a where
-- -- -- -- --     ∅ : ⋆[ A / m ≥ ∅ ]
-- -- -- -- --     _∷_ : ∀ {n} → A m n → ⋆[ A / m ≥ ¹⁺ n ] → ⋆[ A / m ≥ n ]

-- -- -- -- --   _≥'_ : ⋆ → ⋆ → Set
-- -- -- -- --   m ≥' n = ⋆[ (λ _ _ → ⊤) / m ≥ n ]

-- -- -- -- --   data _≤_ : ⋆ → ⋆ → Set where
-- -- -- -- --     ∅ : ∀ {n} → ∅ ≤ n
-- -- -- -- --     ¹⁺_ : ∀ {m n} → m ≤ n → ¹⁺ m ≤ ¹⁺ n

-- -- -- -- --   {- ⃔⋱ -}
-- -- -- -- --   {- ｛ A ∣ 4 ≤ 7 ｝ = ｛ A 3 6 , A 2 5 , A 1 4 , A 0 3 ｝ -}
-- -- -- -- --   {- ｛ A ∣ 2 ≤ 4 ｝ = ｛ A 1 3 , A 0 2 ｝ -}
-- -- -- -- --   data ⋆[_/_≤_] {a} (A : ⋆ → ⋆ → Set a) : ⋆ → ⋆ → Set a where
-- -- -- -- --     ∅ : ∀ {n} → ⋆[ A / ∅ ≤ n ]
-- -- -- -- --     _∷_ : ∀ {m n} → A m n → ⋆[ A / m ≤ n ] → ⋆[ A / ¹⁺ m ≤ ¹⁺ n ]

-- -- -- -- -- --   ---- indices on first and second constructors: 1 and 2
-- -- -- -- -- --   data ⋆[_,_] : ⋆ → ⋆ → Set where
-- -- -- -- -- --     ∅ : ∀ {n} → ⋆[ n , n ]
-- -- -- -- -- --     ! : ∀ {m n} → ⋆[ m , n ] → ⋆[ m , ! n ]

-- -- -- -- -- --   data ⋆[_,_] : ⋆ → ⋆ → Set where
-- -- -- -- -- --     ∅ : ∀ {m n} → ⋆[ m , n ]
-- -- -- -- -- --     ! : ∀ {m n} → ⋆[ m , n ] → ⋆[ ! m , ! n ]

-- -- -- -- -- --   -- ?
-- -- -- -- -- --   data _≛_ : ⋆ → ⋆ → Set where
-- -- -- -- -- --     ∅ : ∅ ≛ ∅
-- -- -- -- -- --     ! : ∀ {m} → ⋆[ m , m ] → ⋆[ ! m , ! m ]

-- -- -- -- -- --   data [_/_↦_] {a} (A : ⋆ → ⋆ → Set a) : ⋆ → ⋆ → Set a where
-- -- -- -- -- --     ∅ : ∀ {n} → [ A / ∅ ↦ n ]
-- -- -- -- -- --     ! : ∀ {m n} → A m n → [ A / ! m ↦ ! n ]

-- -- -- -- -- -- module _ where -- Two constructors, where the second constructor adds a payload and a recursive element

-- -- -- -- -- -- -- List
-- -- -- -- -- -- data [_] {a} (A : Set a) : Set a where
-- -- -- -- -- --   ∅ : [ A ]
-- -- -- -- -- --   _,_ : A → [ A ] → [ A ]

-- -- -- -- -- -- -- Fin
-- -- -- -- -- -- ⋆[_] = ⋆[ ∅ ,_]

-- -- -- -- -- -- record ⊤ : Set where

-- -- -- -- -- -- record ∃ {a} {A : Set a} {b} (B : A → Set b) : Set (a ⊔ b) where
-- -- -- -- -- --   field
-- -- -- -- -- --     ⟱ : A
-- -- -- -- -- --     ⟰ : B ⟱

-- -- -- -- -- -- syntax ∃ (λ x → f) = ∃[ x ] f

-- -- -- -- -- -- _×_ : ∀ {a} (A : Set a) {b} (B : Set b) → Set (a ⊔ b)
-- -- -- -- -- -- A × B = ∃ {A = A} (λ _ → B)

-- -- -- -- -- -- --
-- -- -- -- -- -- [_↦_] : ⋆ → ⋆ → Set
-- -- -- -- -- -- [_↦_] = [ (λ m n → ⋆[ ! m ] × {![ m ↦ n ]!}) /_↦_]

-- -- -- -- --   -- open import Agda.Builtin.Equality
-- -- -- -- --   -- open import Data.Empty


text:
{-# OPTIONS --universe-polymorphism #-}

module Issue464 where

open import Common.Level

data _×_ {a b}(A : Set a)(B : Set b) : Set (a ⊔ b) where
  _,_ : A → B → A × B

data ⊥ : Set where
record ⊤ : Set where

-----------------------------------

data nonSP : Set1 where
  ι : nonSP
  δ : (A : Set) -> nonSP -> nonSP

⟦_⟧ : nonSP -> (Set × ⊤) -> Set
⟦ ι ⟧ UT = ⊤
⟦ (δ A γ) ⟧ (U , T) = (U -> A) × ⟦ γ ⟧ (U , T)

data U (γ : nonSP) : Set where
  intro : ⟦ γ ⟧ (U γ , _) -> U γ
-- the positivity checker objects (as it should) if "(Set × ⊤)" is changed to "Set"
-- in the type of ⟦_⟧ and "(U γ , _)" is changed accordingly to "U γ".

bad : Set
bad = U (δ ⊥ ι) -- constructor in : (bad -> ⊥) -> bad

p : bad -> ⊥
p (intro (x , _)) = x (intro (x , _))

absurd : ⊥
absurd = p (intro (p , _))


text:
module PropositionalFormula where

open import HasNegation
open import IsPropositionalFormula
open import Formula
open import HasNeitherNor

record PropositionalFormula : Set
 where
  constructor ⟨_⟩
  field
    {formula} : Formula
    isPropositionalFormula : IsPropositionalFormula formula

open PropositionalFormula

instance HasNegationPropositionalFormula : HasNegation PropositionalFormula
HasNegation.~ HasNegationPropositionalFormula ⟨ φ ⟩ = ⟨ logical φ φ ⟩

instance HasNeitherNorPropositionalFormula : HasNeitherNor PropositionalFormula
HasNeitherNor._⊗_ HasNeitherNorPropositionalFormula ⟨ φ₁ ⟩ ⟨ φ₂ ⟩ = ⟨ logical φ₁ φ₂ ⟩

{-# DISPLAY IsPropositionalFormula.logical = _⊗_ #-}


text:
------------------------------------------------------------------------
-- List equality
------------------------------------------------------------------------

module Data.List.Equality where

open import Data.List
open import Relation.Nullary
open import Relation.Binary

module Equality (S : Setoid) where

  open Setoid S renaming (_≈_ to _≊_)

  infixr 5 _∷_
  infix  4 _≈_

  data _≈_ : List carrier → List carrier → Set where
    []  : [] ≈ []
    _∷_ : ∀ {x xs y ys} (x≈y : x ≊ y) (xs≈ys : xs ≈ ys) →
          x ∷ xs ≈ y ∷ ys

  setoid : Setoid
  setoid = record
    { carrier = List carrier
    ; _≈_     = _≈_
    ; isEquivalence = record
      { refl  = refl'
      ; sym   = sym'
      ; trans = trans'
      }
    }
    where
    refl' : Reflexive _≈_
    refl' {[]}     = []
    refl' {x ∷ xs} = refl ∷ refl' {xs}

    sym' : Symmetric _≈_
    sym' []            = []
    sym' (x≈y ∷ xs≈ys) = sym x≈y ∷ sym' xs≈ys

    trans' : Transitive _≈_
    trans' []            []            = []
    trans' (x≈y ∷ xs≈ys) (y≈z ∷ ys≈zs) =
      trans x≈y y≈z ∷ trans' xs≈ys ys≈zs

  open Setoid setoid public hiding (_≈_)

module DecidableEquality (D : DecSetoid) where

  open DecSetoid D hiding (_≈_)
  open Equality setoid renaming (setoid to List-setoid)

  decSetoid : DecSetoid
  decSetoid = record
    { isDecEquivalence = record
      { isEquivalence = Setoid.isEquivalence List-setoid
      ; _≟_           = dec
      }
    }
    where
    dec : Decidable _≈_
    dec []       []       = yes []
    dec (x ∷ xs) (y ∷ ys) with x ≟ y | dec xs ys
    ... | yes x≈y | yes xs≈ys = yes (x≈y ∷ xs≈ys)
    ... | no ¬x≈y | _         = no helper
      where
      helper : ¬ _≈_ (x ∷ xs) (y ∷ ys)
      helper (x≈y ∷ _) = ¬x≈y x≈y
    ... | _       | no ¬xs≈ys = no helper
      where
      helper : ¬ _≈_ (x ∷ xs) (y ∷ ys)
      helper (_ ∷ xs≈ys) = ¬xs≈ys xs≈ys
    dec []       (y ∷ ys) = no λ()
    dec (x ∷ xs) []       = no λ()

  open DecSetoid decSetoid public

module PropositionalEquality {A : Set} where

  open import Relation.Binary.PropositionalEquality as PropEq
    using (_≡_) renaming (refl to ≡-refl)
  open Equality (PropEq.setoid A) public

  ≈⇒≡ : _≈_ ⇒ _≡_
  ≈⇒≡ []               = ≡-refl
  ≈⇒≡ (≡-refl ∷ xs≈ys) with ≈⇒≡ xs≈ys
  ≈⇒≡ (≡-refl ∷ xs≈ys) | ≡-refl = ≡-refl

max_issues_repo_name: larrytheliquid/Lemmachine


text:
open import Everything

module Test.ProblemWithDerivation where

postulate
  A : Set
  B : Set
  _~A~_ : A → A → Set
  _~B~_ : B → B → Set
  s1 : A → B
  f1 : ∀ {x y} → x ~A~ y → s1 x ~B~ s1 y

module _ {𝔭} (𝔓 : Ø 𝔭) where

  open Substitunction 𝔓

  test-before : ∀ {m n ℓ} {f : Substitunction m n} (P : LeftExtensionṖroperty ℓ Substitunction Proposextensequality m) (let P₀ = π₀ (π₀ P)) → P₀ f → P₀ (ε ∙ f)
  test-before P pf = hmap _ P pf -- needs Oscar.Class.Hmap.Transleftidentity.Relprop'idFromTransleftidentity

  instance

    𝓢urjectivity1 : Smap.class _~A~_ _~B~_ s1 s1
    𝓢urjectivity1 .⋆ _ _ = f1

  test : ∀ {x y} → x ~A~ y → s1 x ~B~ s1 y
  test {x} {y} = smap

  test-after : ∀ {m n ℓ} {f : Substitunction m n} (P : LeftExtensionṖroperty ℓ Substitunction Proposextensequality m) (let P₀ = π₀ (π₀ P)) → P₀ f → P₀ (ε ∙ f)
  test-after P pf = hmap _ P pf


text:
module Examples where

open import Data.List hiding (reverse)
open import Data.List.All
open import Data.Nat

open import Typing
open import Syntax

ex1 : Expr [] TUnit
ex1 =
  letbind [] (new [] (delay send!))
  (letpair (left []) (here [])
  (letbind (rght (left []))
           (fork (wait (here [])))
  (close (there UUnit (here [])))))

ex1dual : Expr [] TUnit
ex1dual =
  letbind [] (new [] (delay send!))
  (letpair (left []) (here [])
  (letbind (left (rght []))
           (fork (close (here [])))
  (wait (there UUnit (here [])))))

-- sending and receiving
ex2 : Expr [] TUnit
ex2 =
  letbind [] (new [] (delay (Typing.send TInt (delay send!))))
  (letpair (left []) (here [])
  (letbind (left (rght []))
           (fork (letbind (rght []) (nat [] 42)
                 (letbind (left (left [])) (Expr.send (rght (left [])) (here []) (here []))
                 (letbind (left []) (close (here []))
                 (var (here []))))))
  (letbind (rght (left [])) (Expr.recv (here []))
  (letpair (left (rght [])) (here [])
  (letbind (left (left (rght []))) (wait (here (UInt ∷ [])))
  (var (here (UUnit ∷ []))))))))

-- higher order sending and receiving
ex3 : Expr [] TUnit
ex3 =
  letbind [] (new [] (delay (Typing.send (TChan send!) (delay send!))))
  (letbind (rght []) (new [] (delay send!))
  (letpair (left (rght [])) (here [])
  (letpair (rght (rght (left []))) (here [])
  (letbind (left (rght (left (left []))))
           (fork (letbind (left (left (rght []))) (Expr.send (left (rght [])) (here []) (here []))
                 (letbind (left (rght [])) (close (here []))
                 (wait (there UUnit (here []))))))
  (letbind (left (left [])) (Expr.recv (there UUnit (here [])))
  (letpair (left []) (here [])
  (letbind (left (rght [])) (wait (here []))
  (letbind (left (left [])) (close (there UUnit (here [])))
  (var (here []))))))))))

-- branching
ex4 : Expr [] TUnit
ex4 =
  letbind [] (new [] (delay (sintern (delay send!) (delay send?))))
  (letpair (left []) (here [])
  (letbind (left (rght []))
           (fork (letbind (left []) (select Left (here []))
                 (close (here []))))
  (branch (left (left [])) (there UUnit (here []))
          (wait (here []))
          (close (here [])))))

-- simple lambda: (λx.x)()
ex5 : Expr [] TUnit
ex5 = letbind [] (llambda [] [] (var (here [])))
      (letbind (rght []) (unit [])
      (app (rght (left [])) (here []) (here [])))

-- lambda app: (λfx.fx) (λx.x)()
ex6 : Expr [] TUnit
ex6 = letbind [] (llambda [] [] (llambda (left []) [] (app (rght (left [])) (here []) (here []))))
      (letbind (rght []) (llambda [] [] (var (here [])))
      (letbind (rght (rght [])) (unit [])
      (letbind (rght (left (left []))) (app (rght (left [])) (here []) (here []))
      (app (left (rght [])) (here []) (here [])))))

max_stars_repo_name: peterthiemann/definitional-session

max_issues_repo_name: peterthiemann/definitional-session

max_forks_repo_name: peterthiemann/definitional-session