text:
open import Theory

module Categories.Category.Construction.Classifying {ℓ₁ ℓ₂ ℓ₃} (Th : Theory ℓ₁ ℓ₂ ℓ₃) where

open import Relation.Binary using (Rel)
open import Data.List using ([]; _∷_)
open import Data.Fin using () renaming (zero to fzero; suc to fsuc)
open import Level using (_⊔_)

open import Categories.Category

open import Syntax

open Theory.Theory Th
open Signature Sg
open Term Sg

private
  arr : Rel Type (ℓ₁ ⊔ ℓ₂)
  arr A B = A ∷ [] ⊢ B

  identityʳ : forall {A B} {e : A ∷ [] ⊢ B}
    -> A ∷ [] ⊢ e [ ext ! var ] ≡ e
  identityʳ {A} {e = e} = trans (cong/sub (trans (cong/ext !-unique refl) η-pair) refl) sub/id

  assoc : {A B C D : Type} {f : arr A B} {g : arr B C} {h : arr C D}
    -> A ∷ [] ⊢ h [ ext ! g ] [ ext ! f ] ≡ h [ ext ! (g [ ext ! f ]) ]
  assoc {f = f} {g = g} {h = h} = trans (sym sub/∙)
    (cong/sub (trans ext∙ (cong/ext (sym !-unique) refl)) refl)

Cl : Category ℓ₁ (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)
Cl = record
       { Obj = Type
       ; _⇒_ = arr
       ; _≈_ = λ e₁ e₂ → _ ∷ [] ⊢ e₁ ≡ e₂
       ; id = var
       ; _∘_ = λ e₁ e₂ → e₁ [ ext ! e₂ ]
       ; assoc = assoc
       ; sym-assoc = sym assoc
       ; identityˡ = λ {A} {B} {f} -> var/ext ! f
       ; identityʳ = identityʳ
       ; identity² = var/ext ! var
       ; equiv = record { refl = refl ; sym = sym ; trans = trans }
       ; ∘-resp-≈ = λ x x₁ → cong/sub (cong/ext refl x₁) x
       }

open import Categories.Category.BinaryProducts Cl

module M where
  open import Categories.Category.CartesianClosed.Canonical Cl

  CC : CartesianClosed
  CC = record
         { ⊤ = Unit
         ; _×_ = _*_
         ; ! = unit
         ; π₁ = fst var
         ; π₂ = snd var
         ; ⟨_,_⟩ = pair
         ; !-unique = eta/Unit
         ; π₁-comp = trans comm/fst (trans (cong/fst (var/ext ! (pair _ _))) (beta/*₁ _ _))
         ; π₂-comp = trans comm/snd (trans (cong/snd (var/ext ! (pair _ _))) (beta/*₂ _ _))
         ; ⟨,⟩-unique = ⟨,⟩-unique
         ; _^_ = λ A B → B => A
         ; eval = app (fst var) (snd var)
         ; curry = λ e → abs (e [ ext ! (pair (var [ weaken ]) var) ])
         ; eval-comp = eval-comp
         ; curry-resp-≈ = λ x → cong/abs (cong/sub refl x)
         ; curry-unique = λ x → curry-unique x
         }
    where
      ⟨,⟩-unique : forall {A B C} {h : C ∷ [] ⊢ A * B} {i : C ∷ [] ⊢ A} {j : C ∷ [] ⊢ B}
        -> C ∷ [] ⊢ fst var [ ext ! h ] ≡ i
        -> C ∷ [] ⊢ snd var [ ext ! h ] ≡ j
        -> C ∷ [] ⊢ pair i j ≡ h
      ⟨,⟩-unique x y = trans
        (cong/pair
          (sym (trans (cong/fst (sym (var/ext ! _))) (trans (sym comm/fst) x)))
          (sym (trans (cong/snd (sym (var/ext ! _))) (trans (sym comm/snd) y)))
        )
        (eta/* _)

      open import Categories.Object.Product.Morphisms Cl using ([_⇒_]_×_)
      open import Categories.Object.Product Cl using (Product)

      product : forall {A B} -> Product A B
      product {A} {B} = record
                          { A×B = A * B
                          ; π₁ = fst var
                          ; π₂ = snd var
                          ; ⟨_,_⟩ = pair
                          ; project₁ = trans comm/fst (trans (cong/fst (var/ext ! (pair _ _))) (beta/*₁ _ _))
                          ; project₂ = trans comm/snd (trans (cong/snd (var/ext ! (pair _ _))) (beta/*₂ _ _))
                          ; unique = ⟨,⟩-unique
                          }

      eval-comp : forall {B A C} {f : arr (C * A) B}
        -> C * A ∷ [] ⊢
             app (fst var) (snd var)
               [ ext ! ([ product ⇒ product ] (abs (f [ ext ! (pair (var [ weaken ]) var)])) × var) ]
           ≡
             f
      eval-comp = trans comm/app (trans (cong/app (trans comm/fst (cong/fst (var/ext _ _))) (trans comm/snd (cong/snd (var/ext _ _)))) (trans (cong/app (trans (beta/*₁ _ _) comm/abs) (beta/*₂ _ _)) (trans (beta/=> _ _) (trans (sym sub/∙) (trans (cong/sub (trans ext∙ (cong/ext (trans (cong/∙ (trans ext∙ (cong/ext (sym !-unique) comm/fst)) refl) (trans ext∙ (cong/ext (sym !-unique) (trans comm/fst (cong/fst (trans (sym sub/∙) (cong/sub weaken/ext refl))))))) (trans (var/ext _ _) (var/ext _ _)))) refl) (trans (sym sub/∙) (trans (cong/sub (trans ext∙ (trans (cong/ext (sym !-unique) (trans comm/pair (cong/pair (trans (sym sub/∙) (trans (cong/sub weaken/ext refl) (trans (var/ext _ _) (cong/fst sub/id)))) (var/ext _ _)))) (trans (cong/ext !-unique (eta/* _)) η-pair))) refl) sub/id)))))))

      open BinaryProducts (record { product = product })
      open Category Cl

      helper : forall {A B C} {f : A ⇒ B => C}
        -> B ∷ A ∷ [] ⊨ ext ! (var [ weaken ]) ≡ weaken
      helper = trans (cong/ext (!-unique {γ = weaken ∙ weaken}) refl) (trans (sym ext∙) (trans (cong/∙ η-pair refl) id∙ˡ))

      curry-unique : forall {A B C} {f : A ⇒ B => C} {g : A × B ⇒ C}
        -> app (fst var) (snd var) ∘ (f ⁂ Category.id Cl) ≈ g
        -> f ≈ abs (g [ ext ! (pair (var [ weaken ]) var) ])
      curry-unique {A} {B} {C} {f = f} {g = g} x =
        begin
          f
        ≈˘⟨ eta/=> _ ⟩
          abs (app (f [ weaken ]) var)
        ≈˘⟨ cong/abs (cong/app (cong/sub (helper {f = f}) refl) refl) ⟩
          abs (app (f [ ext ! (var [ weaken ]) ]) var)
        ≈˘⟨ cong/abs (cong/app (beta/*₁ _ _) (beta/*₂ _ _)) ⟩
          abs (app (fst (pair (f [ ext ! (var [ weaken ]) ]) var)) (snd (pair (f [ ext ! (var [ weaken ]) ]) var)))
        ≈˘⟨ cong/abs (cong/app (trans comm/fst (cong/fst (var/ext _ _))) (trans comm/snd (cong/snd (var/ext _ _)))) ⟩
          abs (app (fst var [ ext ! (pair (f [ ext ! (var [ weaken ]) ]) var) ]) (snd var [ ext ! (pair (f [ ext ! (var [ weaken ]) ]) var) ]))
        ≈˘⟨ cong/abs comm/app ⟩
          abs (app (fst var) (snd var) [ ext ! (pair (f [ ext ! (var [ weaken ]) ]) var) ])
        ≈˘⟨ cong/abs (cong/sub (cong/ext refl (cong/pair (cong/sub (cong/ext refl (trans comm/fst (trans (cong/fst (var/ext _ _)) (beta/*₁ _ _)))) refl) refl)) refl) ⟩
          abs (app (fst var) (snd var) [ ext ! (pair (f [ ext ! (fst var [ ext ! (pair (var [ weaken ]) var)]) ]) var) ])
        ≈˘⟨ cong/abs (cong/sub (cong/ext refl (cong/pair (cong/sub (trans ext∙ (cong/ext (sym !-unique) refl)) refl) (trans (cong/snd (var/ext _ _)) (beta/*₂ _ _)))) refl) ⟩
          abs (app (fst var) (snd var) [ ext ! (pair (f [ ext ! (fst var) ∙ ext ! (pair (var [ weaken ]) var) ]) (snd (var [ ext ! (pair (var [ weaken ]) var) ]))) ])
        ≈˘⟨ cong/abs (cong/sub (cong/ext refl (cong/pair (sym sub/∙) comm/snd)) refl) ⟩
          abs (app (fst var) (snd var) [ ext ! (pair (f [ ext ! (fst var) ] [ ext ! (pair (var [ weaken ]) var) ]) (snd var [ ext ! (pair (var [ weaken ]) var) ])) ])
        ≈˘⟨ cong/abs (cong/sub (cong/ext refl comm/pair) refl) ⟩
          abs (app (fst var) (snd var) [ ext ! (pair (f [ ext ! (fst var) ]) (snd var) [ ext ! (pair (var [ weaken ]) var) ]) ])
        ≈⟨ cong/abs (cong/sub (cong/ext !-unique (cong/sub refl (cong/pair refl (sym (var/ext _ _))))) refl) ⟩
          abs (app (fst var) (snd var) [ ext (! ∙ ext ! (pair (var [ weaken ]) var)) (pair (f [ ext ! (fst var) ]) (var [ ext ! (snd var) ]) [ ext ! (pair (var [ weaken ]) var) ]) ])
        ≈˘⟨ cong/abs (cong/sub ext∙ refl) ⟩
          abs (app (fst var) (snd var) [ ext ! (pair (f [ ext ! (fst var) ]) (var [ ext ! (snd var) ])) ∙ ext ! (pair (var [ weaken ]) var) ])
        ≡⟨⟩
          abs (app (fst var) (snd var) [ ext ! ⟨ f ∘ fst var , Category.id Cl ∘ snd var ⟩ ∙ ext ! (pair (var [ weaken ]) var) ])
        ≈⟨ cong/abs sub/∙ ⟩
          abs ((app (fst var) (snd var) ∘ ⟨ f ∘ fst var , Category.id Cl ∘ snd var ⟩) [ ext ! (pair (var [ weaken ]) var) ])
        ≡⟨⟩
          abs ((app (fst var) (snd var) ∘ (f ⁂ Category.id Cl)) [ ext ! (pair (var [ weaken ]) var) ])
        ≈⟨ cong/abs (cong/sub refl x) ⟩
          abs (g [ ext ! (pair (var [ weaken ]) var) ])
        ∎
        where
          open import Relation.Binary.Reasoning.Setoid TermSetoid

open import Categories.Category.CartesianClosed Cl
import Categories.Category.CartesianClosed.Canonical Cl as Can

CC : CartesianClosed
CC = Can.Equivalence.fromCanonical M.CC

open import Semantics Cl CC Sg
open Category Cl

private
  open import Data.Product using (_,_)

  open import Categories.Morphism Cl using (Iso; _≅_)
  open import Categories.Category.Cartesian using (Cartesian)
  open import Categories.Functor
  open import Categories.Functor.Properties using ([_]-resp-∘)
  open import Categories.Functor.Construction.Product using (Product)
  open import Categories.Functor.Construction.Exponential using (Exp)
  open import Categories.Functor.Bifunctor using (Bifunctor)

  open CartesianClosed CC
  open BinaryProducts (Cartesian.products cartesian)
  open I ⌊_⌋

  P : Bifunctor Cl Cl Cl
  P = Product Cl cartesian

  E : Bifunctor Cl op Cl
  E = Exp Cl CC

  from/⟦⟧T : forall (A : Type) -> ⟦ A ⟧T ⇒ A
  to/⟦⟧T : forall (A : Type) -> A ⇒ ⟦ A ⟧T

  from/⟦⟧T ⌊ x ⌋ = Category.id Cl
  from/⟦⟧T Unit = Category.id Cl
  from/⟦⟧T (A * A₁) = from/⟦⟧T A ⁂ from/⟦⟧T A₁
  from/⟦⟧T (A => A₁) = λg (from/⟦⟧T A₁ ∘ eval′ ∘ (Category.id Cl ⁂ to/⟦⟧T A))

  to/⟦⟧T ⌊ x ⌋ = Category.id Cl
  to/⟦⟧T Unit = Category.id Cl
  to/⟦⟧T (A * A₁) = to/⟦⟧T A ⁂ to/⟦⟧T A₁
  to/⟦⟧T (A => A₁) = λg (to/⟦⟧T A₁ ∘ eval′ ∘ (Category.id Cl ⁂ from/⟦⟧T A))

  to∘from : forall {A} -> ⟦ A ⟧T ∷ [] ⊢ to/⟦⟧T A [ ext ! (from/⟦⟧T A) ] ≡ var
  to∘from {⌊ x ⌋} = var/ext _ _
  to∘from {Unit} = var/ext _ _
  to∘from {A * A₁} = trans ([ P ]-resp-∘ (to∘from , to∘from)) (Functor.identity P)
  to∘from {A => A₁} = trans ([ E ]-resp-∘ (to∘from , to∘from)) (Functor.identity E)

  from∘to : forall {A} -> A ∷ [] ⊢ from/⟦⟧T A [ ext ! (to/⟦⟧T A) ] ≡ var
  from∘to {⌊ x ⌋} = var/ext _ _
  from∘to {Unit} = var/ext _ _
  from∘to {A * A₁} = trans ([ P ]-resp-∘ (from∘to , from∘to)) (Functor.identity P)
  from∘to {A => A₁} = trans ([ E ]-resp-∘ (from∘to , from∘to)) (Functor.identity E)

  Iso/⟦⟧T : forall {A : Type} -> ⟦ A ⟧T ≅ A
  Iso/⟦⟧T {A} = record
    { from = from/⟦⟧T A
    ; to = to/⟦⟧T A
    ; iso = record { isoˡ = to∘from ; isoʳ = from∘to }
    }

  ⟦_⟧F : (f : Func) -> ⟦ dom f ⟧T ⇒ ⟦ cod f ⟧T
  ⟦_⟧F f = _≅_.to Iso/⟦⟧T ∘ x ∘ _≅_.from Iso/⟦⟧T
    where
      x : dom f ⇒ cod f
      x = func f var

S : Structure
S = record { ⟦_⟧G = ⌊_⌋ ; ⟦_⟧F = λ f → ⟦ f ⟧F }

open Structure S

private
  γC : forall {Γ} -> ⟦ Γ ⟧C ∷ [] ⊨ Γ
  γC {[]} = !
  γC {A ∷ Γ} = ext (γC {Γ} ∙ ext ! π₁) (from/⟦⟧T A ∘ π₂)

  open HomReasoning
  open import Categories.Morphism.Reasoning Cl
  import Categories.Object.Product Cl as Prod

  open import Categories.Object.Terminal Cl using (Terminal)
  module T = Terminal (Cartesian.terminal cartesian)

  helper : forall {Γ} {A} {e : Γ ⊢ A} -> ⟦ e ⟧ ≈ to/⟦⟧T A ∘ (e [ γC ])
  helperS : forall {Γ Γ′} {γ : Γ ⊨ Γ′} -> _ ⊨ γC ∙ ext ! ⟦ γ ⟧S ≡ γ ∙ γC

  helper {e = func f e} =
    begin
      (to/⟦⟧T (cod f) ∘ func f var ∘ from/⟦⟧T (dom f)) ∘ ⟦ e ⟧
    ≈⟨ ∘-resp-≈ʳ (helper {e = e}) ⟩
      (to/⟦⟧T (cod f) ∘ func f var ∘ from/⟦⟧T (dom f)) ∘ to/⟦⟧T _ ∘ (e [ γC ])
    ≈⟨ assoc²' ⟩
      to/⟦⟧T (cod f) ∘ func f var ∘ from/⟦⟧T (dom f) ∘ to/⟦⟧T (dom f) ∘ (e [ γC ])
    ≈⟨ ∘-resp-≈ʳ (∘-resp-≈ʳ (cancelˡ from∘to)) ⟩
      to/⟦⟧T (cod f) ∘ func f var ∘ (e [ γC ])
    ≈⟨ ∘-resp-≈ʳ (comm/func _ _ _ _ _) ⟩
      to/⟦⟧T (cod f) ∘ func f (var ∘ (e [ γC ]))
    ≈⟨ ∘-resp-≈ʳ (cong/func identityˡ) ⟩
      to/⟦⟧T (cod f) ∘ func f (e [ γC ])
    ≈˘⟨ ∘-resp-≈ʳ (comm/func _ _ _ _ _) ⟩
      to/⟦⟧T (cod f) ∘ (func f e [ γC ])
    ∎
  helper {e = var} =
    begin
      π₂
    ≈⟨ insertˡ to∘from ⟩
      to/⟦⟧T _ ∘ (from/⟦⟧T _ ∘ π₂)
    ≈˘⟨ ∘-resp-≈ʳ (var/ext _ _) ⟩
      to/⟦⟧T _ ∘ (var [ ext _ (from/⟦⟧T _ ∘ π₂) ])
    ∎
  helper {e = unit} = T.!-unique _
  helper {e = pair e₁ e₂} =
    begin
      ⟨ ⟦ e₁ ⟧ , ⟦ e₂ ⟧ ⟩
    ≈⟨ ⟨⟩-cong₂ (helper {e = e₁}) (helper {e = e₂}) ⟩
      ⟨ to/⟦⟧T _ ∘ (e₁ [ γC ]) , to/⟦⟧T _ ∘ (e₂ [ γC ]) ⟩
    ≈˘⟨ ⁂∘⟨⟩ ⟩
      (to/⟦⟧T _ ⁂ to/⟦⟧T _) ∘ (pair (e₁ [ γC ]) (e₂ [ γC ]))
    ≈˘⟨ ∘-resp-≈ʳ comm/pair ⟩
      (to/⟦⟧T _ ⁂ to/⟦⟧T _) ∘ (pair e₁ e₂ [ γC ])
    ∎
  helper {e = fst {A = A} {B = B} e} = switch-fromtoˡ Iso/⟦⟧T (
    begin
      from/⟦⟧T _ ∘ π₁ ∘ ⟦ e ⟧
    ≈⟨ ∘-resp-≈ʳ (∘-resp-≈ʳ (helper {e = e})) ⟩
      from/⟦⟧T A ∘ π₁ ∘ to/⟦⟧T (A * B) ∘ (e [ γC ])
    ≈⟨ ∘-resp-≈ʳ (pullˡ π₁∘⁂) ⟩
      from/⟦⟧T A ∘ (to/⟦⟧T A ∘ π₁) ∘ (e [ γC ])
    ≈⟨ assoc²'' ⟩
      (from/⟦⟧T A ∘ to/⟦⟧T A) ∘ π₁ ∘ (e [ γC ])
    ≈⟨ elimˡ from∘to ⟩
      π₁ ∘ (e [ γC ])
    ≈⟨ comm/fst ⟩
      fst (var [ ext ! (e [ γC ]) ])
    ≈⟨ cong/fst (var/ext _ _) ⟩
      fst (e [ γC ])
    ≈˘⟨ comm/fst ⟩
      fst e [ γC ]
    ∎)
  helper {e = snd e} =
    begin
      π₂ ∘ ⟦ e ⟧
    ≈⟨ ∘-resp-≈ʳ (helper {e = e}) ⟩
      π₂ ∘ (to/⟦⟧T _ ∘ (e [ γC ]))
    ≈⟨ pullˡ π₂∘⁂ ⟩
      (to/⟦⟧T _ ∘ snd var) ∘ (e [ γC ])
    ≈⟨ pullʳ comm/snd ⟩
      to/⟦⟧T _ ∘ snd (var ∘ (e [ γC ]))
    ≈⟨ ∘-resp-≈ʳ (cong/snd identityˡ) ⟩
      to/⟦⟧T _ ∘ snd (e [ γC ])
    ≈˘⟨ ∘-resp-≈ʳ comm/snd ⟩
      to/⟦⟧T _ ∘ (snd e [ γC ])
    ∎
  helper {e = abs e} =
    begin
      λg ⟦ e ⟧
    ≈⟨ λ-cong (helper {e = e}) ⟩
      λg (to/⟦⟧T _ ∘ (e [ γC ]))
    ≈⟨ refl ⟩
      λg (to/⟦⟧T _ ∘ (e [ ext (γC ∙ ext ! π₁) (from/⟦⟧T _ ∘ π₂) ]))
    ≈˘⟨ λ-cong (∘-resp-≈ʳ (cong/sub (cong/ext id∙ʳ refl) refl)) ⟩
      λg (to/⟦⟧T _ ∘ (e [ ext ((γC ∙ ext ! π₁) ∙ _⊨_.id) (from/⟦⟧T _ ∘ π₂) ]))
    ≈˘⟨ λ-cong (∘-resp-≈ʳ (cong/sub ×id′-ext refl)) ⟩
      λg (to/⟦⟧T _ ∘ (e [ (γC ∙ ext ! π₁) ×id′ ∙ ext _⊨_.id (from/⟦⟧T _ ∘ π₂)]))
    ≈⟨ λ-cong (∘-resp-≈ʳ sub/∙) ⟩
      λg (to/⟦⟧T _ ∘ (e [ (γC ∙ ext ! π₁) ×id′ ] [ ext _⊨_.id (from/⟦⟧T _ ∘ π₂)]))
    ≈˘⟨ λ-cong (∘-resp-≈ʳ (cong/sub refl (cong/sub ×id′-∙ refl))) ⟩
      λg (to/⟦⟧T _ ∘ (e [ γC ×id′ ∙ ext ! π₁ ×id′ ] [ ext _⊨_.id (from/⟦⟧T _ ∘ π₂)]))
    ≈⟨ λ-cong (∘-resp-≈ʳ (cong/sub refl sub/∙)) ⟩
      λg (to/⟦⟧T _ ∘ (e [ ext (γC ∙ weaken) var ] [ ext (ext ! π₁ ∙ weaken) var ] [ ext _⊨_.id (from/⟦⟧T _ ∘ π₂)]))
    ≈˘⟨ λ-cong (∘-resp-≈ʳ (beta/=> _ _)) ⟩
      λg (to/⟦⟧T _ ∘ app (abs (e [ ext (γC ∙ weaken) var ] [ ext (ext ! π₁ ∙ weaken) var ])) (from/⟦⟧T _ ∘ π₂))
    ≈˘⟨ λ-cong (∘-resp-≈ʳ (cong/app comm/abs refl)) ⟩
      λg (to/⟦⟧T _ ∘ app (abs (e [ ext (γC ∙ weaken) var ]) ∘ π₁) (from/⟦⟧T _ ∘ π₂))
    ≈˘⟨ λ-cong (∘-resp-≈ʳ (cong/app (beta/*₁ _ _) (beta/*₂ _ _))) ⟩
      λg (to/⟦⟧T _ ∘ app (fst (abs (e [ ext (γC ∙ weaken) var ]) ⁂ from/⟦⟧T _)) (snd (abs (e [ ext (γC ∙ weaken) var ]) ⁂ from/⟦⟧T _)))
    ≈˘⟨ λ-cong (∘-resp-≈ʳ (trans comm/app (cong/app (trans comm/fst (cong/fst (var/ext _ _))) (trans comm/snd (cong/snd (var/ext _ _)))))) ⟩
      λg (to/⟦⟧T _ ∘ (app π₁ π₂) ∘ (abs (e [ ext (γC ∙ weaken) var ]) ⁂ from/⟦⟧T _))
    ≈˘⟨ λ-cong (∘-resp-≈ʳ (∘-resp-≈ˡ (cong/app (beta/*₁ _ _) (beta/*₂ _ _)))) ⟩
      λg (to/⟦⟧T _ ∘ (app (fst (pair π₁ π₂)) (snd (pair π₁ π₂))) ∘ (abs (e [ ext (γC ∙ weaken) var ]) ⁂ from/⟦⟧T _))
    ≈˘⟨ λ-cong (∘-resp-≈ʳ (∘-resp-≈ˡ (cong/app (trans comm/fst (cong/fst (var/ext _ _))) (trans comm/snd (cong/snd (var/ext _ _)))))) ⟩
      λg (to/⟦⟧T _ ∘ (app (fst var ∘ pair π₁ π₂) (snd var ∘ pair π₁ π₂)) ∘ (abs (e [ ext (γC ∙ weaken) var ]) ⁂ from/⟦⟧T _))
    ≈˘⟨ λ-cong (∘-resp-≈ʳ (∘-resp-≈ˡ comm/app)) ⟩
      λg (to/⟦⟧T _ ∘ (app (fst var) (snd var) ∘ (pair π₁ π₂)) ∘ (abs (e [ ext (γC ∙ weaken) var ]) ⁂ from/⟦⟧T _))
    ≈⟨ refl ⟩
      λg (to/⟦⟧T _ ∘ (eval ∘ Prod.repack product exp.product) ∘ (abs (e [ ext (γC ∙ weaken) var ]) ⁂ from/⟦⟧T _))
    ≈⟨ refl ⟩
      λg (to/⟦⟧T _ ∘ eval′ ∘ (abs (e [ ext (γC ∙ weaken) var ]) ⁂ from/⟦⟧T _))
    ≈˘⟨ λ-cong (∘-resp-≈ʳ (∘-resp-≈ʳ (⁂-cong₂ comm/abs refl))) ⟩
      λg (to/⟦⟧T _ ∘ eval′ ∘ ((abs e [ γC ]) ⁂ from/⟦⟧T _))
    ≈˘⟨ λ-cong (∘-resp-≈ʳ (∘-resp-≈ʳ (⁂-cong₂ identityˡ (Category.identityʳ Cl)))) ⟩
      λg (to/⟦⟧T _ ∘ eval′ ∘ (var ∘ (abs e [ γC ]) ⁂ from/⟦⟧T _ ∘ var))
    ≈˘⟨ λ-cong (∘-resp-≈ʳ (∘-resp-≈ʳ ⁂∘⁂)) ⟩
      λg (to/⟦⟧T _ ∘ eval′ ∘ (var ⁂ from/⟦⟧T _) ∘ ((abs e [ γC ]) ⁂ var))
    ≈˘⟨ λ-cong assoc²' ⟩
      λg ((to/⟦⟧T _ ∘ eval′ ∘ (var ⁂ from/⟦⟧T _)) ∘ ((abs e [ γC ]) ⁂ var))
    ≈˘⟨ exp.subst product product ⟩
      (λg (to/⟦⟧T _ ∘ eval′ ∘ (var ⁂ from/⟦⟧T _))) ∘ (abs e [ γC ])
    ≈⟨ refl ⟩
      to/⟦⟧T (_ => _) ∘ (abs e [ γC ])
    ∎
  helper {e = app e₁ e₂} =
    begin
      eval′ ∘ ⟨ ⟦ e₁ ⟧ , ⟦ e₂ ⟧ ⟩
    ≈⟨ refl ⟩
      (app (fst var) (snd var) ∘ _) ∘ ⟨ ⟦ e₁ ⟧ , ⟦ e₂ ⟧ ⟩
    ≈⟨ ∘-resp-≈ˡ (elimʳ η) ⟩
      app (fst var) (snd var) ∘ ⟨ ⟦ e₁ ⟧ , ⟦ e₂ ⟧ ⟩
    ≈⟨ ∘-resp-≈ʳ (⟨⟩-cong₂ (helper {e = e₁}) (helper {e = e₂})) ⟩
      app (fst var) (snd var) ∘ ⟨ to/⟦⟧T _ ∘ (e₁ [ γC ]) , to/⟦⟧T _ ∘ (e₂ [ γC ]) ⟩
    ≈⟨ comm/app ⟩
      app (fst var ∘ ⟨ to/⟦⟧T _ ∘ (e₁ [ γC ]) , to/⟦⟧T _ ∘ (e₂ [ γC ]) ⟩)
          (snd var ∘ ⟨ to/⟦⟧T _ ∘ (e₁ [ γC ]) , to/⟦⟧T _ ∘ (e₂ [ γC ]) ⟩)
    ≈⟨ cong/app comm/fst comm/snd ⟩
      app (fst (var ∘ ⟨ to/⟦⟧T _ ∘ (e₁ [ γC ]) , to/⟦⟧T _ ∘ (e₂ [ γC ]) ⟩))
          (snd (var ∘ ⟨ to/⟦⟧T _ ∘ (e₁ [ γC ]) , to/⟦⟧T _ ∘ (e₂ [ γC ]) ⟩))
    ≈⟨ cong/app (cong/fst (var/ext _ _)) (cong/snd (var/ext _ _)) ⟩
      app (fst ⟨ to/⟦⟧T _ ∘ (e₁ [ γC ]) , to/⟦⟧T _ ∘ (e₂ [ γC ]) ⟩)
          (snd ⟨ to/⟦⟧T _ ∘ (e₁ [ γC ]) , to/⟦⟧T _ ∘ (e₂ [ γC ]) ⟩)
    ≈⟨ cong/app (beta/*₁ _ _) (beta/*₂ _ _) ⟩
      app (to/⟦⟧T (_ => _) ∘ (e₁ [ γC ]))
          (to/⟦⟧T _ ∘ (e₂ [ γC ]))
    ≈⟨ refl ⟩
      app (λg (to/⟦⟧T _ ∘ eval′ ∘ (var ⁂ from/⟦⟧T _)) ∘ (e₁ [ γC ]))
          (to/⟦⟧T _ ∘ (e₂ [ γC ]))
    ≈⟨ refl ⟩
      app (curry ((to/⟦⟧T _ ∘ eval′ ∘ (var ⁂ from/⟦⟧T _)) ∘ Prod.repack product product) ∘ (e₁ [ γC ]))
          (to/⟦⟧T _ ∘ (e₂ [ γC ]))
    ≈⟨ refl ⟩
      app (abs (((to/⟦⟧T _ ∘ eval′ ∘ (var ⁂ from/⟦⟧T _)) ∘ Prod.repack product product) [ ext ! (pair (var [ weaken ]) var) ]) ∘ (e₁ [ γC ]))
          (to/⟦⟧T _ ∘ (e₂ [ γC ]))
    ≈⟨ cong/app (cong/sub refl (cong/abs (cong/sub refl (elimʳ η)))) refl ⟩
      app (abs ((to/⟦⟧T _ ∘ eval′ ∘ (var ⁂ from/⟦⟧T _)) [ ext ! (pair (var [ weaken ]) var) ]) ∘ (e₁ [ γC ]))
          (to/⟦⟧T _ ∘ (e₂ [ γC ]))
    ≈⟨ cong/app comm/abs refl ⟩
      app (abs ((to/⟦⟧T _ ∘ eval′ ∘ (var ⁂ from/⟦⟧T _)) [ ext ! (pair (var [ weaken ]) var) ] [ ext ! (e₁ [ γC ]) ×id′ ]))
          (to/⟦⟧T _ ∘ (e₂ [ γC ]))
    ≈⟨ beta/=> _ _ ⟩
      (to/⟦⟧T _ ∘ eval′ ∘ (var ⁂ from/⟦⟧T _)) [ ext ! (pair (var [ weaken ]) var) ] [ ext ! (e₁ [ γC ]) ×id′ ] [ ext _⊨_.id (to/⟦⟧T _ ∘ (e₂ [ γC ])) ]
    ≈⟨ refl ⟩
      (to/⟦⟧T _ ∘ (eval ∘ Prod.repack product product) ∘ (var ⁂ from/⟦⟧T _)) [ ext ! (pair (var [ weaken ]) var) ] [ ext ! (e₁ [ γC ]) ×id′ ] [ ext _⊨_.id (to/⟦⟧T _ ∘ (e₂ [ γC ])) ]
    ≈⟨ cong/sub refl (cong/sub refl (cong/sub refl (∘-resp-≈ʳ (∘-resp-≈ˡ (elimʳ η))))) ⟩
      (to/⟦⟧T _ ∘ (app (fst var) (snd var)) ∘ (var ⁂ from/⟦⟧T _)) [ ext ! (pair (var [ weaken ]) var) ] [ ext ! (e₁ [ γC ]) ×id′ ] [ ext _⊨_.id (to/⟦⟧T _ ∘ (e₂ [ γC ])) ]
    ≈˘⟨ sub/∙ ⟩
      (to/⟦⟧T _ ∘ (app (fst var) (snd var)) ∘ (var ⁂ from/⟦⟧T _)) [ ext ! (pair (var [ weaken ]) var) ] [ ext ! (e₁ [ γC ]) ×id′ ∙ ext _⊨_.id (to/⟦⟧T _ ∘ (e₂ [ γC ])) ]
    ≈⟨ cong/sub (×id′-ext) refl ⟩
      (to/⟦⟧T _ ∘ (app (fst var) (snd var)) ∘ (var ⁂ from/⟦⟧T _)) [ ext ! (pair (var [ weaken ]) var) ] [ ext (ext ! (e₁ [ γC ]) ∙ _⊨_.id) (to/⟦⟧T _ ∘ (e₂ [ γC ])) ]
    ≈⟨ cong/sub (cong/ext id∙ʳ refl) refl ⟩
      (to/⟦⟧T _ ∘ (app (fst var) (snd var)) ∘ (var ⁂ from/⟦⟧T _)) [ ext ! (pair (var [ weaken ]) var) ] [ ext (ext ! (e₁ [ γC ])) (to/⟦⟧T _ ∘ (e₂ [ γC ])) ]
    ≈˘⟨ sub/∙ ⟩
      (to/⟦⟧T _ ∘ (app (fst var) (snd var)) ∘ (var ⁂ from/⟦⟧T _)) [ ext ! (pair (var [ weaken ]) var) ∙ ext (ext ! (e₁ [ γC ])) (to/⟦⟧T _ ∘ (e₂ [ γC ])) ]
    ≈⟨ cong/sub (trans ext∙ (cong/ext (sym !-unique) refl)) refl ⟩
      (to/⟦⟧T _ ∘ (app (fst var) (snd var)) ∘ (var ⁂ from/⟦⟧T _)) ∘ (pair (var [ weaken ]) var [ ext (ext ! (e₁ [ γC ])) (to/⟦⟧T _ ∘ (e₂ [ γC ])) ])
    ≈⟨ ∘-resp-≈ʳ (trans comm/pair (cong/pair (trans (sym sub/∙) (cong/sub weaken/ext refl)) (var/ext _ _))) ⟩
      (to/⟦⟧T _ ∘ (app (fst var) (snd var)) ∘ (var ⁂ from/⟦⟧T _)) ∘ (pair (var [ (ext ! (e₁ [ γC ])) ]) (to/⟦⟧T _ ∘ (e₂ [ γC ])))
    ≈⟨ ∘-resp-≈ʳ (cong/pair (var/ext _ _) refl) ⟩
      (to/⟦⟧T _ ∘ (app (fst var) (snd var)) ∘ (var ⁂ from/⟦⟧T _)) ∘ (pair (e₁ [ γC ]) (to/⟦⟧T _ ∘ (e₂ [ γC ])))
    ≈⟨ pull-last ⁂∘⟨⟩ ⟩
      to/⟦⟧T _ ∘ (app (fst var) (snd var)) ∘ (pair (var ∘ (e₁ [ γC ])) (from/⟦⟧T _ ∘ to/⟦⟧T _ ∘ (e₂ [ γC ])))
    ≈⟨ ∘-resp-≈ʳ (cong/sub (cong/ext refl (cong/pair identityˡ (cancelˡ from∘to))) refl) ⟩
      to/⟦⟧T _ ∘ (app (fst var) (snd var)) ∘ (pair (e₁ [ γC ]) (e₂ [ γC ]))
    ≈⟨ ∘-resp-≈ʳ (trans comm/app (cong/app (trans comm/fst (trans (cong/fst (var/ext _ _)) (beta/*₁ _ _))) (trans comm/snd (trans (cong/snd (var/ext _ _)) (beta/*₂ _ _))))) ⟩
      to/⟦⟧T _ ∘ (app (e₁ [ γC ]) (e₂ [ γC ]))
    ≈˘⟨ ∘-resp-≈ʳ (comm/app) ⟩
      to/⟦⟧T _ ∘ (app e₁ e₂ [ γC ])
    ∎
      where
        curry : _ -> _
        curry e = abs (e [ ext ! (pair (var [ weaken ]) var) ])
  helper {e = e [ γ ]} =
    begin
      ⟦ e ⟧ ∘ ⟦ γ ⟧S
    ≈⟨ pushˡ (helper {e = e}) ⟩
      to/⟦⟧T _ ∘ (e [ γC ]) ∘ ⟦ γ ⟧S
    ≈⟨ refl ⟩
      to/⟦⟧T _ ∘ (e [ γC ] [ ext ! ⟦ γ ⟧S ])
    ≈˘⟨ ∘-resp-≈ʳ sub/∙ ⟩
      to/⟦⟧T _ ∘ (e [ γC ∙ ext ! ⟦ γ ⟧S ])
    ≈⟨ ∘-resp-≈ʳ (cong/sub (helperS {γ = γ}) refl) ⟩
      to/⟦⟧T _ ∘ (e [ γ ∙ γC ])
    ≈⟨ ∘-resp-≈ʳ sub/∙ ⟩
      to/⟦⟧T _ ∘ (e [ γ ] [ γC ])
    ∎

  helperS {γ = id} = trans (trans (cong/∙ refl (cong/ext !-unique refl)) (trans (cong/∙ refl η-pair) id∙ʳ)) (sym id∙ˡ)
  helperS {γ = γ ∙ γ₁} =
    S.begin
      γC ∙ ext ! (⟦ γ ⟧S ∘ ⟦ γ₁ ⟧S)
    S.≈˘⟨ cong/∙ refl (trans ext∙ (cong/ext (sym !-unique) refl)) ⟩
      γC ∙ (ext ! ⟦ γ ⟧S ∙ ext ! ⟦ γ₁ ⟧S)
    S.≈˘⟨ assoc∙ ⟩
      (γC ∙ ext ! ⟦ γ ⟧S) ∙ ext ! ⟦ γ₁ ⟧S
    S.≈⟨ cong/∙ (helperS {γ = γ}) refl ⟩
      (γ ∙ γC) ∙ ext ! ⟦ γ₁ ⟧S
    S.≈⟨ assoc∙ ⟩
      γ ∙ (γC ∙ ext ! ⟦ γ₁ ⟧S)
    S.≈⟨ cong/∙ refl (helperS {γ = γ₁}) ⟩
      γ ∙ (γ₁ ∙ γC)
    S.≈˘⟨ assoc∙ ⟩
      (γ ∙ γ₁) ∙ γC
    S.∎
    where import Relation.Binary.Reasoning.Setoid SubstSetoid as S
  helperS {γ = weaken} = sym weaken/ext
  helperS {γ = ext γ e} =
    S.begin
      γC {_ ∷ _} ∙ (ext ! ⟨ ⟦ γ ⟧S , ⟦ e ⟧ ⟩)
    S.≡⟨⟩
      ext (γC ∙ ext ! π₁) (from/⟦⟧T _ ∘ π₂) ∙ (ext ! ⟨ ⟦ γ ⟧S , ⟦ e ⟧ ⟩)
    S.≈⟨ ext∙ ⟩
      ext ((γC ∙ ext ! π₁) ∙ (ext ! ⟨ ⟦ γ ⟧S , ⟦ e ⟧ ⟩)) ((from/⟦⟧T _ ∘ π₂) ∘ ⟨ ⟦ γ ⟧S , ⟦ e ⟧ ⟩)
    S.≈⟨ cong/ext assoc∙ (pullʳ project₂) ⟩
      ext (γC ∙ (ext ! π₁ ∙ (ext ! ⟨ ⟦ γ ⟧S , ⟦ e ⟧ ⟩))) (from/⟦⟧T _ ∘ ⟦ e ⟧)
    S.≈⟨ cong/ext (cong/∙ refl (trans ext∙ (cong/ext (sym !-unique) refl))) refl ⟩
      ext (γC ∙ (ext ! (π₁ [ ext ! ⟨ ⟦ γ ⟧S , ⟦ e ⟧ ⟩ ]))) (from/⟦⟧T _ ∘ ⟦ e ⟧)
    S.≈⟨ cong/ext (cong/∙ refl (cong/ext refl project₁)) refl ⟩
      ext (γC ∙ ext ! ⟦ γ ⟧S) (from/⟦⟧T _ ∘ ⟦ e ⟧)
    S.≈⟨ cong/ext (helperS {γ = γ}) (sym (switch-tofromˡ Iso/⟦⟧T (sym (helper {e = e})))) ⟩
      ext (γ ∙ γC) (e [ γC ])
    S.≈˘⟨ ext∙ ⟩
      ext γ e ∙ γC
    S.∎
    where import Relation.Binary.Reasoning.Setoid SubstSetoid as S
  helperS {γ = !} = trans (sym !-unique) !-unique

  satisfyAxiom : forall {Γ} {A} {e₁ e₂ : Γ ⊢ A} -> Ax Γ A e₁ e₂ -> ⟦ e₁ ⟧ ≈ ⟦ e₂ ⟧
  satisfyAxiom {Γ} {A} {e₁} {e₂} x = trans (helper {e = e₁}) (trans (∘-resp-≈ʳ a) (sym (helper {e = e₂})))
    where
      a : (e₁ [ γC ]) ≈ (e₂ [ γC ])
      a = cong/sub refl (ax x)

M : Model Cl CC Th
M = S , satisfyAxiom

max_stars_repo_name: elpinal/exsub-ccc

max_issues_repo_name: elpinal/exsub-ccc

max_forks_repo_name: elpinal/exsub-ccc


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

open import HoTT
open import homotopy.Bouquet
open import homotopy.FinWedge
open import homotopy.SphereEndomorphism
open import groups.SphereEndomorphism
open import cw.CW
open import cw.FinCW
open import cw.WedgeOfCells
open import cw.FinBoundary
open import cohomology.Theory

module cw.cohomology.cochainequiv.HigherCoboundary (OT : OrdinaryTheory lzero)
  {n} (⊙fin-skel : ⊙FinSkeleton (S (S n))) where

open OrdinaryTheory OT
open import cohomology.SubFinBouquet OT
open import cohomology.RephraseSubFinCoboundary OT

private
  fin-skel = ⊙FinSkeleton.skel ⊙fin-skel
  I = AttachedFinSkeleton.numCells fin-skel
  ac = ⊙FinSkeleton-has-cells-with-choice 0 ⊙fin-skel lzero
  dec = ⊙FinSkeleton-has-cells-with-dec-eq ⊙fin-skel

  ⊙fin-skel₋₁ = ⊙fcw-init ⊙fin-skel
  fin-skel₋₁ = ⊙FinSkeleton.skel ⊙fin-skel₋₁
  I₋₁ = AttachedFinSkeleton.numCells fin-skel₋₁
  ac₋₁ = ⊙FinSkeleton-has-cells-with-choice 0 ⊙fin-skel₋₁ lzero
  dec₋₁ = ⊙FinSkeleton-has-cells-with-dec-eq ⊙fin-skel₋₁

open import cw.cohomology.WedgeOfCells OT
open import cw.cohomology.reconstructed.HigherCoboundary OT ⊙⦉ ⊙fin-skel ⦊
open import cw.cohomology.cochainequiv.HigherCoboundaryAbstractDefs OT ⊙fin-skel

abstract
  rephrase-cw-co∂-last-in-degree : ∀ g
    → GroupIso.f (CXₙ/Xₙ₋₁-diag-β ⊙⦉ ⊙fin-skel ⦊ ac) (GroupHom.f cw-co∂-last (GroupIso.g (CXₙ/Xₙ₋₁-diag-β ⊙⦉ ⊙fin-skel₋₁ ⦊ ac₋₁) g))
    ∼ λ <I → Group.sum (C2 0) (λ <I₋₁ → Group.exp (C2 0) (g <I₋₁) (fdegree-last fin-skel <I <I₋₁))
  rephrase-cw-co∂-last-in-degree g <I =
    GroupIso.f (C-FinBouquet-diag (S (S n)) I)
      (CEl-fmap (ℕ-to-ℤ (S (S n))) (⊙–> (Bouquet-⊙equiv-Xₙ/Xₙ₋₁ ⦉ fin-skel ⦊))
        (GroupHom.f cw-co∂-last
          (CEl-fmap (ℕ-to-ℤ (S n)) (⊙<– (Bouquet-⊙equiv-Xₙ/Xₙ₋₁ ⦉ fin-skel₋₁ ⦊))
            (GroupIso.g (C-FinBouquet-diag (S n) I₋₁)
              g)))) <I
      =⟨ ap
          (λ g →
            GroupIso.f (C-FinBouquet-diag (S (S n)) I)
              (CEl-fmap (ℕ-to-ℤ (S (S n))) (⊙–> (Bouquet-⊙equiv-Xₙ/Xₙ₋₁ ⦉ fin-skel ⦊)) g) <I) $
          cw-co∂-last-β
            (CEl-fmap (ℕ-to-ℤ (S n)) (⊙<– (Bouquet-⊙equiv-Xₙ/Xₙ₋₁ ⦉ fin-skel₋₁ ⦊))
              (GroupIso.g (C-FinBouquet-diag (S n) I₋₁)
                g)) ⟩
    GroupIso.f (C-FinBouquet-diag (S (S n)) I)
      (CEl-fmap (ℕ-to-ℤ (S (S n))) (⊙–> (Bouquet-⊙equiv-Xₙ/Xₙ₋₁ ⦉ fin-skel ⦊))
        (CEl-fmap (ℕ-to-ℤ (S (S n))) ⊙cw-∂-before-Susp
          (<– (CEl-Susp (ℕ-to-ℤ (S n)) (⊙Xₙ/Xₙ₋₁ ⦉ fin-skel₋₁ ⦊))
            (CEl-fmap (ℕ-to-ℤ (S n)) (⊙<– (Bouquet-⊙equiv-Xₙ/Xₙ₋₁ ⦉ fin-skel₋₁ ⦊))
              (GroupIso.g (C-FinBouquet-diag (S n) I₋₁)
                g))))) <I
      =⟨ ap
          (λ g →
            GroupIso.f (C-FinBouquet-diag (S (S n)) I)
              (CEl-fmap (ℕ-to-ℤ (S (S n))) (⊙–> (Bouquet-⊙equiv-Xₙ/Xₙ₋₁ ⦉ fin-skel ⦊))
                (CEl-fmap (ℕ-to-ℤ (S (S n))) ⊙cw-∂-before-Susp g)) <I) $
          C-Susp-fmap' (ℕ-to-ℤ (S n)) (⊙<– (Bouquet-⊙equiv-Xₙ/Xₙ₋₁ ⦉ fin-skel₋₁ ⦊)) □$ᴳ
            (GroupIso.g (C-FinBouquet-diag (S n) I₋₁)
              g) ⟩
    GroupIso.f (C-FinBouquet-diag (S (S n)) I)
      (CEl-fmap (ℕ-to-ℤ (S (S n))) (⊙–> (Bouquet-⊙equiv-Xₙ/Xₙ₋₁ ⦉ fin-skel ⦊))
        (CEl-fmap (ℕ-to-ℤ (S (S n))) ⊙cw-∂-before-Susp
          (CEl-fmap (ℕ-to-ℤ (S (S n))) (⊙Susp-fmap (⊙<– (Bouquet-⊙equiv-Xₙ/Xₙ₋₁ ⦉ fin-skel₋₁ ⦊)))
            (<– (CEl-Susp (ℕ-to-ℤ (S n)) (⊙FinBouquet _ (S n)))
              (GroupIso.g (C-FinBouquet-diag (S n) I₋₁)
                g))))) <I
      =⟨ ap (λ g → GroupIso.f (C-FinBouquet-diag (S (S n)) I) g <I) $
            ∘-CEl-fmap (ℕ-to-ℤ (S (S n))) (⊙–> (Bouquet-⊙equiv-Xₙ/Xₙ₋₁ ⦉ fin-skel ⦊)) ⊙cw-∂-before-Susp
              (CEl-fmap (ℕ-to-ℤ (S (S n))) (⊙Susp-fmap (⊙<– (Bouquet-⊙equiv-Xₙ/Xₙ₋₁ ⦉ fin-skel₋₁ ⦊)))
                (<– (CEl-Susp (ℕ-to-ℤ (S n)) (⊙FinBouquet _ (S n)))
                  (GroupIso.g (C-FinBouquet-diag (S n) I₋₁)
                    g)))
          ∙ ∘-CEl-fmap (ℕ-to-ℤ (S (S n)))
              (⊙cw-∂-before-Susp ⊙∘ ⊙–> (Bouquet-⊙equiv-Xₙ/Xₙ₋₁ ⦉ fin-skel ⦊))
              (⊙Susp-fmap (⊙<– (Bouquet-⊙equiv-Xₙ/Xₙ₋₁ ⦉ fin-skel₋₁ ⦊)))
              (<– (CEl-Susp (ℕ-to-ℤ (S n)) (⊙FinBouquet _ (S n)))
                (GroupIso.g (C-FinBouquet-diag (S n) I₋₁)
                  g))
          ∙ ap (λ f → CEl-fmap (ℕ-to-ℤ (S (S n))) f
              (<– (CEl-Susp (ℕ-to-ℤ (S n)) (⊙FinBouquet _ (S n)))
                (GroupIso.g (C-FinBouquet-diag (S n) I₋₁)
                  g)))
              (! ⊙function₀'-β) ⟩
    GroupIso.f (C-FinBouquet-diag (S (S n)) I)
      (CEl-fmap (ℕ-to-ℤ (S (S n))) ⊙function₀'
        (<– (CEl-Susp (ℕ-to-ℤ (S n)) (⊙FinBouquet _ (S n)))
          (GroupIso.g (C-FinBouquet-diag (S n) I₋₁)
            g))) <I
      =⟨ rephrase-in-degree' (S n) {I = I} {J = I₋₁} ⊙function₀' g <I ⟩
    Group.sum (C2 0)
      (λ <I₋₁ → Group.exp (C2 0) (g <I₋₁)
        (⊙SphereS-endo-degree (S n)
          (⊙Susp-fmap (⊙fwproj <I₋₁) ⊙∘ ⊙function₀' ⊙∘ ⊙fwin <I)))
      =⟨ ap (Group.sum (C2 0))
          (λ= λ <I₋₁ → ap (Group.exp (C2 0) (g <I₋₁)) $
            ⊙SphereS-endo-degree-base-indep (S n)
              {f = (  ⊙Susp-fmap (⊙fwproj <I₋₁)
                   ⊙∘ ⊙function₀'
                   ⊙∘ ⊙fwin <I)}
              {g = (Susp-fmap (function₁' <I <I₋₁) , idp)}
              (mega-reduction <I <I₋₁)) ⟩
    Group.sum (C2 0)
      (λ <I₋₁ → Group.exp (C2 0) (g <I₋₁)
        (⊙SphereS-endo-degree (S n)
          (Susp-fmap (function₁' <I <I₋₁) , idp)))
      =⟨ ap (Group.sum (C2 0))
          (λ= λ <I₋₁ → ap (Group.exp (C2 0) (g <I₋₁)) $
            ⊙SphereS-endo-degree-Susp' n (function₁' <I <I₋₁)) ⟩
    Group.sum (C2 0)
      (λ <I₋₁ → Group.exp (C2 0) (g <I₋₁)
        (Trunc-⊙SphereS-endo-degree n
          (Trunc-⊙SphereS-endo-in n
            [ function₁' <I <I₋₁ ])))
      =⟨ ap (Group.sum (C2 0))
          (λ= λ <I₋₁ → ap
            (λ f → Group.exp (C2 0) (g <I₋₁)
              (Trunc-⊙SphereS-endo-degree n
                (Trunc-⊙SphereS-endo-in n
                  [ f ])))
            (function₁'-β <I <I₋₁)) ⟩
    Group.sum (C2 0)
      (λ <I₋₁ → Group.exp (C2 0) (g <I₋₁)
        (Trunc-⊙SphereS-endo-degree n
          (Trunc-⊙SphereS-endo-in n
            [ function₁ <I <I₋₁ ])))
      =∎

ext: agda

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module UnSized.Parrot where

open import Data.Product
open import Data.String.Base

open import UnSizedIO.IOObject

open import UnSizedIO.Base hiding (main)
open import UnSizedIO.Console hiding (main)

open import NativeIO

open import UnSized.SimpleCell hiding (program; main)

--ParrotC : Set
--ParrotC = ConsoleObject (cellI String)

-- but reusing cellC from SimpleCell, as interface is ident!

-- class Parrot implements Cell {
--   Cell cell;
--   Parrot (Cell c) { cell = c; }
--   public String get() {
--     return "(" + cell.get() + ") is what parrot got";
--   }
--   public void put (String s) {
--     cell.put("parrot puts (" + s + ")");
--   }
-- }

-- parrotP is constructor for the consoleObject for interface (cellI String)
{-# NON_TERMINATING #-}
parrotP : (c : CellC) → CellC
(method (parrotP c) get) =
  exec1 (putStrLn "printing works")  >>
  method c get >>= λ { (s , c') →
  return ("(" ++ s ++ ") is what parrot got" , parrotP c')  }
(method (parrotP c) (put s)) =
  method c (put ("parrot puts (" ++ s ++ ")"))

--   public static void main (String[] args) {
--     Parrot c = new Parrot(new SimpleCell("Start"));
--     System.out.println(c.get());
--     c.put(args[1]);
--     System.out.println(c.get());
--   }
-- }

program : String → IOConsole Unit
program arg =
  let c₀ = parrotP (cellP "Start") in
  method c₀ get       >>= λ{ (s , c₁) →
  exec1 (putStrLn s)         >>
  method c₁ (put arg) >>= λ{ (_ , c₂) →
  method c₂ get       >>= λ{ (s' , c₃) →
  exec1 (putStrLn s')        }}}

main : NativeIO Unit
main = translateIOConsole (program "hello")

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
module ExtendedLam where

data Bool
  : Set
  where

  false
    : Bool
  true
    : Bool

f
  : Bool
  → Bool
  → Bool
f
  = λ
  { x false
    → true
  ; y true
    → y
  }

max_stars_repo_name: msuperdock/agda-unused

max_issues_repo_name: msuperdock/agda-unused

max_forks_repo_name: msuperdock/agda-unused


text:
{-

This file contains:
- The quotient of finite sets by decidable equivalence relation is still finite, by using equivalence class.

-}
{-# OPTIONS --safe #-}

module Cubical.Data.FinSet.Quotients where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv renaming (_∙ₑ_ to _⋆_)
open import Cubical.Foundations.Equiv.Properties
open import Cubical.Foundations.Univalence

open import Cubical.HITs.PropositionalTruncation as Prop
open import Cubical.HITs.SetQuotients as SetQuot
open import Cubical.HITs.SetQuotients.EqClass

open import Cubical.Data.Nat
open import Cubical.Data.Bool
open import Cubical.Data.Sigma

open import Cubical.Data.SumFin
open import Cubical.Data.FinSet.Base
open import Cubical.Data.FinSet.Properties
open import Cubical.Data.FinSet.DecidablePredicate
open import Cubical.Data.FinSet.Constructors
open import Cubical.Data.FinSet.Cardinality

open import Cubical.Relation.Nullary
open import Cubical.Relation.Nullary.DecidablePropositions
open import Cubical.Relation.Binary

private
  variable
    ℓ ℓ' ℓ'' : Level

LiftDecProp : {ℓ ℓ' : Level}{P : Type ℓ} → (p : isDecProp P) → P ≃ Bool→Type* {ℓ'} (p .fst)
LiftDecProp p = p .snd ⋆ BoolProp≃BoolProp*

open Iso

module _
  (X : Type ℓ) where

  ℙEff : Type ℓ
  ℙEff = X → Bool

  isSetℙEff : isSet ℙEff
  isSetℙEff = isSetΠ (λ _ → isSetBool)

  ℙEff→ℙDec : ℙEff → ℙDec {ℓ' = ℓ'} X
  ℙEff→ℙDec f .fst x = Bool→Type* (f x) , isPropBool→Type*
  ℙEff→ℙDec f .snd x = DecBool→Type*

  Iso-ℙEff-ℙDec : Iso ℙEff (ℙDec {ℓ' = ℓ'} X)
  Iso-ℙEff-ℙDec .fun = ℙEff→ℙDec
  Iso-ℙEff-ℙDec .inv (P , dec) x = Dec→Bool (dec x)
  Iso-ℙEff-ℙDec {ℓ' = ℓ'} .leftInv f i x = Bool≡BoolDec* {ℓ = ℓ'} {a = f x} (~ i)
  Iso-ℙEff-ℙDec .rightInv (P , dec) i .fst x .fst = ua (Dec≃DecBool* (P x .snd) (dec x)) (~ i)
  Iso-ℙEff-ℙDec .rightInv (P , dec) i .fst x .snd =
    isProp→PathP {B = λ i → isProp (Iso-ℙEff-ℙDec .rightInv (P , dec) i .fst x .fst)}
      (λ i → isPropIsProp)
      (Iso-ℙEff-ℙDec .fun (Iso-ℙEff-ℙDec .inv (P , dec)) .fst x .snd) (P x .snd) i
  Iso-ℙEff-ℙDec .rightInv (P , dec) i .snd x =
    isProp→PathP {B = λ i → Dec (Iso-ℙEff-ℙDec .rightInv (P , dec) i .fst x .fst)}
      (λ i → isPropDec (Iso-ℙEff-ℙDec .rightInv (P , dec) i .fst x .snd))
      (Iso-ℙEff-ℙDec .fun (Iso-ℙEff-ℙDec .inv (P , dec)) .snd x) (dec x) i

  ℙEff≃ℙDec : ℙEff ≃ (ℙDec {ℓ' = ℓ'} X)
  ℙEff≃ℙDec = isoToEquiv Iso-ℙEff-ℙDec

module _
  (X : Type ℓ)(p : isFinOrd X) where

  private
    e = p .snd

  isFinOrdℙEff : isFinOrd (ℙEff X)
  isFinOrdℙEff = _ , preCompEquiv (invEquiv e) ⋆ SumFinℙ≃ _

module _
  (X : FinSet ℓ) where

  isFinSetℙEff : isFinSet (ℙEff (X .fst))
  isFinSetℙEff = 2 ^ (card X) ,
    Prop.elim (λ _ → isPropPropTrunc {A = _ ≃ Fin _})
      (λ p → ∣ isFinOrdℙEff (X .fst) (_ , p) .snd ∣)
      (X .snd .snd)

module _
  (X : FinSet ℓ)
  (R : X .fst → X .fst → Type ℓ')
  (dec : (x x' : X .fst) → isDecProp (R x x')) where

  isEqClassEff : ℙEff (X .fst) → Type ℓ
  isEqClassEff f = ∥ Σ[ x ∈ X .fst ] ((a : X .fst) → f a ≡ dec a x .fst) ∥

  isDecPropIsEqClassEff : {f : ℙEff (X .fst)} → isDecProp (isEqClassEff f)
  isDecPropIsEqClassEff = isDecProp∃ X (λ _ → _ , isDecProp∀ X (λ _ → _ , _ , Bool≡≃ _ _))

  isEqClassEff→isEqClass' : (f : ℙEff (X .fst))(x : X .fst)
    → ((a : X .fst) → f a ≡ dec a x .fst)
    → (a : X .fst) → Bool→Type* {ℓ = ℓ'} (f a) ≃ ∥ R a x ∥
  isEqClassEff→isEqClass' f x h a =
      pathToEquiv (cong Bool→Type* (h a))
    ⋆ invEquiv (LiftDecProp (dec a x))
    ⋆ invEquiv (propTruncIdempotent≃ (isDecProp→isProp (dec a x)))

  isEqClass→isEqClassEff' : (f : ℙEff (X .fst))(x : X .fst)
    → ((a : X .fst) → Bool→Type* {ℓ = ℓ'} (f a) ≃ ∥ R a x ∥)
    → (a : X .fst) → f a ≡ dec a x .fst
  isEqClass→isEqClassEff' f x h a =
    Bool→TypeInj* _ _
        (h a ⋆ propTruncIdempotent≃ (isDecProp→isProp (dec a x)) ⋆ LiftDecProp (dec a x))

  isEqClassEff→isEqClass : (f : ℙEff (X .fst)) → isEqClassEff f ≃ isEqClass {ℓ' = ℓ'} _ R (ℙEff→ℙDec  _ f .fst)
  isEqClassEff→isEqClass f =
    propBiimpl→Equiv isPropPropTrunc isPropPropTrunc
      (Prop.map (λ (x , p) → x , isEqClassEff→isEqClass' f x p))
      (Prop.map (λ (x , p) → x , isEqClass→isEqClassEff' f x p))

  _∥Eff_ : Type ℓ
  _∥Eff_ = Σ[ f ∈ ℙEff (X .fst) ] isEqClassEff f

  ∥Eff≃∥Dec : _∥Eff_ ≃ _∥Dec_ (X .fst) R (λ x x' → isDecProp→Dec (dec x x'))
  ∥Eff≃∥Dec = Σ-cong-equiv (ℙEff≃ℙDec (X .fst)) isEqClassEff→isEqClass

  isFinSet∥Eff : isFinSet _∥Eff_
  isFinSet∥Eff = isFinSetSub (_ , isFinSetℙEff X) (λ _ → _ , isDecPropIsEqClassEff)

open BinaryRelation

module _
  (X : FinSet ℓ)
  (R : X .fst → X .fst → Type ℓ')
  (h : isEquivRel R)
  (dec : (x x' : X .fst) → isDecProp (R x x')) where

  isFinSetQuot : isFinSet (X .fst / R)
  isFinSetQuot =
    EquivPresIsFinSet
      ( ∥Eff≃∥Dec X _ dec
      ⋆ ∥Dec≃∥ _ _ (λ x x' → isDecProp→Dec (dec x x'))
      ⋆ invEquiv (equivQuot {ℓ' = ℓ'} _ _ h))
      (isFinSet∥Eff X _ dec)

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Data.Product using (∃; _,_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)

+-identity : ∀ (m : ℕ) → m + zero ≡ m
+-identity zero = refl
+-identity (suc m) rewrite +-identity m = refl

+-suc : ∀ (m n : ℕ) → n + suc m ≡ suc (n + m)
+-suc m zero = refl
+-suc m (suc n) rewrite +-suc m n = refl

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm zero n rewrite +-identity n = refl
+-comm (suc m) n rewrite +-suc m n | +-comm m n = refl

mutual
  data even : ℕ → Set where
    zero : even zero
    suc : ∀ {n : ℕ} → odd n → even (suc n)
  data odd : ℕ → Set where
    suc : ∀ {n : ℕ} → even n → odd (suc n)

+-lemma : ∀ (m : ℕ) → suc (suc (m + (m + 0))) ≡ suc m + suc (m + 0)
+-lemma m rewrite +-identity m | +-suc m m = refl

mutual
  is-even : ∀ (n : ℕ) → even n → ∃(λ (m : ℕ) → n ≡ 2 * m)
  is-even zero zero =  zero , refl
  is-even (suc n) (suc oddn) with is-odd n oddn
  ... | m , n≡1+2*m rewrite n≡1+2*m | +-lemma m = suc m , refl

  is-odd : ∀ (n : ℕ) → odd n → ∃(λ (m : ℕ) → n ≡ 1 + 2 * m)
  is-odd (suc n) (suc evenn) with is-even n evenn
  ... | m , n≡2*m rewrite n≡2*m = m , refl

+-lemma′ : ∀ (m : ℕ) → suc (suc (m + (m + 0))) ≡ suc m + suc (m + 0)
+-lemma′ m rewrite +-suc (m + 0) m = refl

is-even′ : ∀ (n : ℕ) → even n → ∃(λ (m : ℕ) → n ≡ 2 * m)
is-even′ zero zero =  zero , refl
is-even′ (suc n) (suc oddn) with is-odd n oddn
... | m , n≡1+2*m rewrite n≡1+2*m | +-identity m | +-suc m m = suc m , {!!}


text:
open import Relation.Binary.Core

module Mergesort.Everything {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_) where

open import Mergesort.Impl1.Correctness.Order _≤_ tot≤
open import Mergesort.Impl1.Correctness.Permutation _≤_ tot≤

open import Mergesort.Impl2.Correctness.Order _≤_ tot≤
open import Mergesort.Impl2.Correctness.Permutation _≤_ tot≤

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
import Data.Bool
import Relation.Nullary.Negation
import Relation.Nullary.Decidable


text:
------------------------------------------------------------------------
-- Library parsers which do not require the complicated setup used in
-- RecursiveDescent.Inductive.Lib
------------------------------------------------------------------------

-- This module also provides more examples of parsers for which the
-- indices cannot be inferred.

module RecursiveDescent.Inductive.SimpleLib where

open import RecursiveDescent.Inductive
open import RecursiveDescent.Index

open import Data.Nat
open import Data.Vec hiding (_⊛_; _>>=_)
open import Data.Vec1 using (Vec₁; []; _∷_)
open import Data.List using (List; []; _∷_)
open import Relation.Nullary
open import Data.Product.Record hiding (_×_)
open import Data.Product using (_×_) renaming (_,_ to pair)
open import Data.Bool
open import Data.Function
open import Data.Maybe
open import Data.Unit
open import Data.Bool.Properties as Bool
open import Algebra
private
  module BCS = CommutativeSemiring Bool.commutativeSemiring-∨-∧
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------
-- Applicative functor parsers

-- We could get these for free with better library support.

infixl 50 _⊛_ _⊛!_ _<⊛_ _⊛>_ _<$>_ _<$_ _⊗_ _⊗!_

_⊛_ : forall {tok nt i₁ i₂ r₁ r₂} ->
      Parser tok nt i₁ (r₁ -> r₂) ->
      Parser tok nt i₂ r₁ ->
      Parser tok nt _  r₂
p₁ ⊛ p₂ = p₁ >>= \f -> p₂ >>= \x -> return (f x)

-- A variant: If the second parser does not accept the empty string,
-- then neither does the combination. (This is immediate for the first
-- parser, but for the second one a small lemma is needed, hence this
-- variant.)

_⊛!_ : forall {tok nt i₁ c₂ r₁ r₂} ->
       Parser tok nt i₁ (r₁ -> r₂) ->
       Parser tok nt (false , c₂) r₁ ->
       Parser tok nt (false , _)  r₂
_⊛!_ {i₁ = i₁} p₁ p₂ = cast (BCS.*-comm (proj₁ i₁) false) refl
                            (p₁ ⊛ p₂)

_<$>_ : forall {tok nt i r₁ r₂} ->
        (r₁ -> r₂) ->
        Parser tok nt i r₁ ->
        Parser tok nt _ r₂
f <$> x = return f ⊛ x

_<⊛_ : forall {tok nt i₁ i₂ r₁ r₂} ->
       Parser tok nt i₁ r₁ ->
       Parser tok nt i₂ r₂ ->
       Parser tok nt _ r₁
x <⊛ y = const <$> x ⊛ y

_⊛>_ : forall {tok nt i₁ i₂ r₁ r₂} ->
       Parser tok nt i₁ r₁ ->
       Parser tok nt i₂ r₂ ->
       Parser tok nt _ r₂
x ⊛> y = flip const <$> x ⊛ y

_<$_ : forall {tok nt i r₁ r₂} ->
       r₁ ->
       Parser tok nt i r₂ ->
       Parser tok nt _ r₁
x <$ y = const x <$> y

_⊗_ : forall {tok nt i₁ i₂ r₁ r₂} ->
      Parser tok nt i₁ r₁ -> Parser tok nt i₂ r₂ ->
      Parser tok nt _ (r₁ × r₂)
p₁ ⊗ p₂ = pair <$> p₁ ⊛ p₂

_⊗!_ : forall {tok nt i₁ c₂ r₁ r₂} ->
      Parser tok nt i₁ r₁ -> Parser tok nt (false , c₂) r₂ ->
      Parser tok nt (false , _) (r₁ × r₂)
p₁ ⊗! p₂ = pair <$> p₁ ⊛! p₂

------------------------------------------------------------------------
-- Parsing sequences

-- Note that the resulting index here cannot be inferred...

private

  exactly'-corners : Corners -> ℕ -> Corners
  exactly'-corners c zero    = _
  exactly'-corners c (suc n) = _

  exactly' : forall {tok nt c r} n ->
             Parser tok nt (false , c) r ->
             Parser tok nt (false , exactly'-corners c n)
                           (Vec r (suc n))
  exactly' zero    p = [_] <$> p
  exactly' (suc n) p = _∷_ <$> p ⊛ exactly' n p

-- ...so we might as well generalise the function a little.
-- exactly n p parses n occurrences of p.

exactly-index : Index -> ℕ -> Index
exactly-index i zero    = _
exactly-index i (suc n) = _

exactly : forall {tok nt i r} n ->
          Parser tok nt i r ->
          Parser tok nt (exactly-index i n) (Vec r n)
exactly zero    p = return []
exactly (suc n) p = _∷_ <$> p ⊛ exactly n p

-- A function with a similar type:

sequence : forall {tok nt i r n} ->
           Vec₁ (Parser tok nt i r) n ->
           Parser tok nt (exactly-index i n) (Vec r n)
sequence []       = return []
sequence (p ∷ ps) = _∷_ <$> p ⊛ sequence ps

-- p between ps parses p repeatedly, between the elements of ps:
--   ∙ between (x ∷ y ∷ z ∷ []) ≈ x ∙ y ∙ z.

between-corners : Corners -> ℕ -> Corners
between-corners c′ zero    = _
between-corners c′ (suc n) = _

_between_ : forall {tok nt i r c′ r′ n} ->
            Parser tok nt i r ->
            Vec₁ (Parser tok nt (false , c′) r′) (suc n) ->
            Parser tok nt (false , between-corners c′ n) (Vec r n)
p between (x ∷ [])     = [] <$ x
p between (x ∷ y ∷ xs) = _∷_ <$> (x ⊛> p) ⊛ (p between (y ∷ xs))

------------------------------------------------------------------------
-- N-ary variants of _∣_

-- choice ps parses one of the elements in ps.

choice-corners : Corners -> ℕ -> Corners
choice-corners c zero    = _
choice-corners c (suc n) = _

choice : forall {tok nt c r n} ->
         Vec₁ (Parser tok nt (false , c) r) n ->
         Parser tok nt (false , choice-corners c n) r
choice []       = fail
choice (p ∷ ps) = p ∣ choice ps

-- choiceMap f xs ≈ choice (map f xs), but avoids use of Vec₁ and
-- fromList.

choiceMap-corners : forall {a} -> (a -> Corners) -> List a -> Corners
choiceMap-corners c []       = _
choiceMap-corners c (x ∷ xs) = _

choiceMap : forall {tok nt r a} {c : a -> Corners} ->
            ((x : a) -> Parser tok nt (false , c x) r) ->
            (xs : List a) ->
            Parser tok nt (false , choiceMap-corners c xs) r
choiceMap f []       = fail
choiceMap f (x ∷ xs) = f x ∣ choiceMap f xs

------------------------------------------------------------------------
-- sat and friends

sat : forall {tok nt r} ->
      (tok -> Maybe r) -> Parser tok nt (0I ·I 1I) r
sat {tok} {nt} {r} p = symbol !>>= \c -> ok (p c)
  where
  okIndex : Maybe r -> Index
  okIndex nothing  = _
  okIndex (just _) = _

  ok : (x : Maybe r) -> Parser tok nt (okIndex x) r
  ok nothing  = fail
  ok (just x) = return x

sat' : forall {tok nt} -> (tok -> Bool) -> Parser tok nt _ ⊤
sat' p = sat (boolToMaybe ∘ p)

any : forall {tok nt} -> Parser tok nt _ tok
any = sat just

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
------------------------------------------------------------------------------
-- The Collatz function: A function without a termination proof
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOTC.Program.Collatz.Collatz where

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.UnaryNumbers
open import FOTC.Program.Collatz.Data.Nat

------------------------------------------------------------------------------
-- The Collatz function.
postulate
  collatz         : D → D
  collatz-0       : collatz 0' ≡ 1'
  collatz-1       : collatz 1' ≡ 1'
  collatz-even    : ∀ {n} → Even (succ₁ (succ₁ n)) →
                    collatz (succ₁ (succ₁ n)) ≡
                      collatz (div (succ₁ (succ₁ n)) 2')
  collatz-noteven : ∀ {n} → NotEven (succ₁ (succ₁ n)) →
                    collatz (succ₁ (succ₁ n)) ≡
                      collatz (3' * (succ₁ (succ₁ n)) + 1')
{-# ATP axioms collatz-0 collatz-1 collatz-even collatz-noteven #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
open import Signature
import Program

module Observations (Σ : Sig) (V : Set) (P : Program.Program Σ V) where

open import Terms Σ
open import Program Σ V
open import Rewrite Σ V P
open import Relation.Nullary
open import Relation.Unary
open import Data.Product as Prod renaming (Σ to ⨿)

NonTrivial : T V → Pred (Subst V V) _
NonTrivial t σ = ∃ λ v → (v ∈ fv t) × ¬ isVar (σ v)

{- |
We can make an observation according to the following rule.

t ↓ s   fv(s) ≠ ∅    ∃ k, σ. s ~[σ]~ Pₕ(k)
--------------------------------------------
              t ----> t[σ]
-}
data _↦_ (t : T V) : T V → Set where
  obs-step : {s : T V} → t ↓ s → ¬ Empty (fv s) →
             (cl : dom P) {σ : Subst V V} → mgu s (geth P cl) σ →
             t ↦ app σ t

GroundTerm : Pred (T V) _
GroundTerm t = Empty (fv t)

--------
-- FLAW: This does not allow us to distinguish between inductive
-- and coinductive definitions on the clause level.
-- The following definitions are _global_ for a derivation!
-------

data IndDerivable (t : T V) : Set where
  ground : GroundTerm t → Valid t → IndDerivable t
  der-step : (s : T V) → t ↦ s → IndDerivable s → IndDerivable t

record CoindDerivable (t : T V) : Set where
  coinductive
  field
    term-SN : SN t
    der-obs : ⨿ (T V) λ s → t ↦ s × CoindDerivable s
open CoindDerivable

record _↥[_]_ (t : T V) (σ : Subst∞ V V) (s : T∞ V) : Set where
  coinductive
  field
    conv-match : app∞ σ (χ t) ~ s
    conv-step : ⨿ (T V) λ t₁ → t ↦ t₁ × t₁ ↥[ ? ] s

coind-converges-to : (t : T V) → CoindDerivable t → T∞ V
out (coind-converges-to t p) with der-obs p
... | (._ , obs-step t↓s _ cl {σ} _ , q) = {!!}

coind-converges : (t : T V) → CoindDerivable t →
                  ∃₂ λ s σ → Empty (fv∞ s) × t ↥[ σ ] s
coind-converges = {!!}

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text: module Categories.Functor.Coalgebras where

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
-- Andreas, 2015-11-19 Issue 1692
-- With-abstract also in types of variables mentioned in with-expressions
-- unless they are also mentioned in the types of the with-expressions.

-- {-# OPTIONS -v tc.with:40 #-}

open import Common.Equality

postulate
  A : Set
  a : A

test : (dummy : A) (f : ∀ x → a ≡ x) (b : A) → b ≡ a
test dummy f b rewrite f b = f b

-- WAS:
-- The `a` is not with-abstracted in the type of `f`, as `f` occurs
-- in the rewrite expression `f b : a ≡ b`.

-- NOW: with abstracts also in type of f, changing it to (f : ∀ x → b ≡ x)

test-with : (f : ∀ x → a ≡ x) (b : A) → b ≡ a
test-with f b with a | f b
test-with f b | .b | refl = f b

-- WAS:

-- Manually, we can construct what `magic with` DID not do:
-- abstract `a` also in the type of `f`, even though `f` is part of the
-- rewrite expression.
bla : (f : ∀ x → a ≡ x) (b : A) → b ≡ a
bla f b = aux b a (f b) f
  where
    aux : (b w : A) (p : w ≡ b) (f : ∀ x → w ≡ x) → b ≡ w
    aux b .b refl f = f b

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module STLC4 where

open import Data.Nat
open import Data.Nat.Properties using (≤-antisym; ≤-trans; ≰⇒>; ≤-step)
-- open import Data.List
open import Data.Empty using (⊥-elim)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; cong₂; subst)
open import Relation.Nullary.Decidable using (map)
open import Relation.Nullary
open import Data.Product

-- de Bruijn indexed lambda calculus
infix  5 ƛ_
infixl 7 _∙_
infix  9 var_

data Term : Set where
  var_  : (x : ℕ) → Term
  ƛ_    : Term → Term
  _∙_   :  Term → Term → Term

shift : (n i : ℕ) → Term → Term
shift free i (var x) with x ≥? free
shift free i (var x) | yes p = var (x + i) -- free
shift free i (var x) | no ¬p = var x -- bound
shift free i (ƛ M)   = ƛ shift (suc free) i M
shift free i (M ∙ N) = shift free i M ∙ shift free i N

infixl 10 _[_/_]
_[_/_] : Term → Term → ℕ → Term
(var x) [ N / i ] with compare x i
((var x) [ N / .(suc (x + k)) ])  | less .x k = var x
((var x) [ N / .x ])              | equal .x = shift 0 x N
((var .(suc (i + k))) [ N / i ])  | greater .i k = var (i + k)
(ƛ M)   [ N / i ] = ƛ (M [ N / suc i ])
(L ∙ M) [ N / i ] = L [ N / i ] ∙ M [ N / i ]

-- substitute the 0th var in M for N
infixl 10 _[_]
_[_] : Term → Term → Term
M [ N ] = M [ N / 0 ]

-- β reduction
infix 3 _β→_
data _β→_ : Term → Term → Set where

  β-ƛ-∙ : ∀ {M N} → ((ƛ M) ∙ N) β→ (M [ N ])

  β-ƛ : ∀ {M N} → M β→ N → ƛ M β→ ƛ N

  β-∙-l : ∀ {L M N} → M β→ N → M ∙ L β→ N ∙ L

  β-∙-r : ∀ {L M N} → M β→ N → L ∙ M β→ L ∙ N

module TransRefl where
  -- the reflexive and transitive closure of _β→_
  infix  2 _β→*_
  infixr 2 _→*_
  data _β→*_ : Term → Term → Set where

    ∎ : ∀ {M} → M β→* M

    _→*_
      : ∀ {L M N}
      → L β→ M
      → M β→* N
      --------------
      → L β→* N

  infixl 3 _<β>_
  _<β>_ : ∀ {M N O} → M β→* N → N β→* O → M β→* O
  _<β>_ {M} {.M} {O} ∎            N→O = N→O
  _<β>_ {M} {N}  {O} (L→M →* M→N) N→O = L→M →* M→N <β> N→O

  infixr 2 _→⟨⟩_
  _→⟨⟩_
    : ∀ {M}
    → ∀ N
    → N β→* M
    --------------
    → N β→* M
  M →⟨⟩ Q = Q

  infixr 2 _→⟨_⟩_
  _→⟨_⟩_
    : ∀ {M N}
    → ∀ L
    → L β→ M
    → M β→* N
    --------------
    → L β→* N
  L →⟨ P ⟩ Q = P →* Q

  infixr 2 _→*⟨_⟩_
  _→*⟨_⟩_
    : ∀ {M N}
    → ∀ L
    → L β→* M
    → M β→* N
    --------------
    → L β→* N
  L →*⟨ P ⟩ Q = P <β> Q

  infix 3 _→∎
  _→∎ : ∀ M → M β→* M
  M →∎ = ∎

  hop : ∀ {M N} → M β→ N → M β→* N
  hop {M} {N} M→N = M→N →* ∎

open TransRefl

-- the symmetric closure of _β→*_
module Eq where
  infix  1 _β≡_
  data _β≡_ : Term → Term → Set where
    β-sym : ∀ {M N}
        → M β→* N
        → N β→* M
        -------
        → M β≡ N

  infixr 2 _=*⟨_⟩_
  _=*⟨_⟩_
    : ∀ {M N}
    → ∀ L
    → L β≡ M
    → M β≡ N
    --------------
    → L β≡ N
  L =*⟨ β-sym A B ⟩ β-sym C D = β-sym (A <β> C) (D <β> B)

  infixr 2 _=*⟨⟩_
  _=*⟨⟩_
    : ∀ {N}
    → ∀ L
    → L β≡ N
    --------------
    → L β≡ N
  L =*⟨⟩ β-sym C D = β-sym C D

  infix 3 _=∎
  _=∎ : ∀ M → M β≡ M
  M =∎ = β-sym ∎ ∎

  forward : ∀ {M N} → M β≡ N → M β→* N
  forward (β-sym A _) = A

  backward : ∀ {M N} → M β≡ N → N β→* M
  backward (β-sym _ B) = B

module Example where

  test-1 : ƛ (ƛ var 1) ∙ var 0 β→* ƛ var 0
  test-1 =
          ƛ (ƛ var 1) ∙ var 0
      →⟨ β-ƛ β-ƛ-∙ ⟩
          ƛ var 0
      →∎

  test-0 : ƛ (ƛ var 0 ∙ var 1) ∙ (ƛ var 0 ∙ var 1) β→* ƛ var 0 ∙ var 0
  test-0 =
          ƛ (ƛ var 0 ∙ var 1) ∙ (ƛ var 0 ∙ var 1)
      →⟨ β-ƛ β-ƛ-∙ ⟩
          ƛ (var 0 ∙ var 1) [ ƛ var 0 ∙ var 1 ]
      →⟨⟩
          ƛ (var 0 ∙ var 1) [ ƛ var 0 ∙ var 1 / 0 ]
      →⟨⟩
          ƛ (var 0) [ ƛ var 0 ∙ var 1 / 0 ] ∙ (var 1) [ ƛ var 0 ∙ var 1 / 0 ]
      →⟨⟩
          ƛ shift 0 0 (ƛ var 0 ∙ var 1) ∙ var 0
      →⟨⟩
          ƛ (ƛ shift 1 0 (var 0 ∙ var 1)) ∙ var 0
      →⟨⟩
          ƛ (ƛ shift 1 0 (var 0) ∙ shift 1 0 (var 1)) ∙ var 0
      →⟨⟩
          ƛ ((ƛ var 0 ∙ var 1) ∙ var 0)
      →⟨ β-ƛ β-ƛ-∙ ⟩
          ƛ (var 0 ∙ var 1) [ var 0 / 0 ]
      →⟨⟩
          ƛ var 0 ∙ var 0
    →∎

  Z : Term
  Z = ƛ ƛ var 0

  SZ : Term
  SZ = ƛ ƛ var 1 ∙ var 0

  PLUS : Term
  PLUS = ƛ ƛ ƛ ƛ var 3 ∙ var 1 ∙ (var 2 ∙ var 1 ∙ var 0)

  test-2 : PLUS ∙ Z ∙ SZ β→* SZ
  test-2 =
      PLUS ∙ Z ∙ SZ
    →⟨ β-∙-l β-ƛ-∙ ⟩
      (ƛ ƛ ƛ var 3 ∙ var 1 ∙ (var 2 ∙ var 1 ∙ var 0)) [ ƛ ƛ var 0 / 0 ] ∙ SZ
    →⟨⟩
      (ƛ ((ƛ ƛ var 3 ∙ var 1 ∙ (var 2 ∙ var 1 ∙ var 0)) [ ƛ ƛ var 0 / 1 ])) ∙ SZ
    →⟨⟩
      (ƛ (ƛ (ƛ var 3 ∙ var 1 ∙ (var 2 ∙ var 1 ∙ var 0)) [ ƛ ƛ var 0 / 2 ])) ∙ SZ
    →⟨⟩
      (ƛ (ƛ (ƛ ((var 3 ∙ var 1 ∙ (var 2 ∙ var 1 ∙ var 0)) [ ƛ ƛ var 0 / 3 ])))) ∙ SZ
    →⟨⟩
      (ƛ (ƛ (ƛ (ƛ (ƛ var 0)) ∙ var 1 ∙ (var 2 ∙ var 1 ∙ var 0)))) ∙ SZ
    →⟨ β-∙-l (β-ƛ (β-ƛ (β-ƛ (β-∙-l β-ƛ-∙)))) ⟩
      (ƛ (ƛ (ƛ (ƛ var 0) [ var 1 / 0 ] ∙ (var 2 ∙ var 1 ∙ var 0)))) ∙ SZ
    →⟨⟩
      (ƛ (ƛ (ƛ (ƛ (var 0) [ var 1 / 1 ]) ∙ (var 2 ∙ var 1 ∙ var 0)))) ∙ SZ
    →⟨⟩
      (ƛ (ƛ (ƛ (ƛ var 0) ∙ (var 2 ∙ var 1 ∙ var 0)))) ∙ SZ
    →⟨ β-∙-l (β-ƛ (β-ƛ (β-ƛ β-ƛ-∙))) ⟩
      (ƛ (ƛ (ƛ (var 0) [ var 2 ∙ var 1 ∙ var 0 / 0 ]))) ∙ SZ
    →⟨⟩
      (ƛ (ƛ (ƛ (var 2 ∙ var 1 ∙ var 0)))) ∙ SZ
    →⟨ β-ƛ-∙ ⟩
      (ƛ (ƛ (var 2 ∙ var 1 ∙ var 0))) [ SZ / 0 ]
    →⟨⟩
      ƛ (ƛ (var 2 ∙ var 1 ∙ var 0) [ SZ / 2 ])
    →⟨⟩
      ƛ (ƛ shift 0 2 SZ ∙ var 1 ∙ var 0)
    →⟨⟩
      ƛ (ƛ (ƛ ƛ var 1 ∙ var 0) ∙ var 1 ∙ var 0)
    →⟨ β-ƛ (β-ƛ (β-∙-l β-ƛ-∙)) ⟩
      ƛ (ƛ (ƛ var 1 ∙ var 0) [ var 1 / 0 ] ∙ var 0)
    →⟨⟩
      ƛ (ƛ (ƛ ((var 1 ∙ var 0) [ var 1 / 1 ])) ∙ var 0)
    →⟨⟩
      ƛ (ƛ (ƛ ((var 1) [ var 1 / 1 ] ∙ (var 0) [ var 1 / 1 ])) ∙ var 0)
    →⟨⟩
      ƛ (ƛ (ƛ (shift 0 1 (var 1) ∙ var 0)) ∙ var 0)
    →⟨⟩
      ƛ (ƛ (ƛ (var 2 ∙ var 0)) ∙ var 0)
    →⟨ β-ƛ (β-ƛ β-ƛ-∙) ⟩
      ƛ (ƛ (var 2 ∙ var 0) [ var 0 / 0 ])
    →⟨⟩
      ƛ (ƛ (var 2) [ var 0 / 0 ] ∙ var 0)
    →⟨⟩
      ƛ (ƛ var 1 ∙ var 0)
    →∎

-- lemmas

cong-ƛ : {M N : Term} → M β→* N → ƛ M β→* ƛ N
cong-ƛ ∎            = ∎
cong-ƛ (M→N →* N→O) = β-ƛ M→N →* cong-ƛ N→O

cong-∙-l : {L M N : Term} → M β→* N → M ∙ L β→* N ∙ L
cong-∙-l ∎            = ∎
cong-∙-l (M→N →* N→O) = β-∙-l M→N →* cong-∙-l N→O

cong-∙-r : {L M N : Term} → M β→* N → L ∙ M β→* L ∙ N
cong-∙-r ∎            = ∎
cong-∙-r (M→N →* N→O) = β-∙-r M→N →* cong-∙-r N→O

-- shift-subst : ∀ freeM i n M N → (shift (suc (suc free)) i M) [ shift free i N / n ] β→* shift (suc free) i (M [ N / n ])
--
--      N  ---- shfit n   ---> N'
--      |                      |
--    M[_]          shfit n+2 [_]
--      |                      |
--    M[N] ---- shfit n+1 ---> N'
--
shift-subst : ∀ free i n M N → (shift (suc (suc free)) i M) [ shift free i N / n ] β→* shift (suc free) i (M [ N / n ])
shift-subst free i n (var x) N with compare x n
shift-subst free i .(suc (x + k)) (var x) N | less .x k with x ≥? suc free
shift-subst free i .(suc (x + k)) (var x) N | less .x k | yes p with suc (suc free) ≤? x
shift-subst free i .(suc (x + k)) (var x) N | less .x k | yes p | yes q = {!   !}
shift-subst free i .(suc (x + k)) (var x) N | less .x k | yes p | no ¬q = {!   !}
shift-subst free i .(suc (x + k)) (var x) N | less .x k | no ¬p = {!   !}
shift-subst free i n (var .n) N | equal .n = {!   !}
shift-subst free i n (var .(suc (n + k))) N | greater .n k = {!   !}
shift-subst free i n (ƛ M) N =
    ƛ (shift (suc (suc (suc free))) i M [ shift free i N / suc n ])
  →*⟨ cong-ƛ {! shift-subst (suc free) i (suc n) M N  !} ⟩
    {!   !}
  →*⟨ {!   !} ⟩
    ƛ (shift (suc (suc (suc free))) i M [ shift (suc free) i N / suc n ])
  →*⟨ cong-ƛ (shift-subst (suc free) i (suc n) M N) ⟩
    ƛ (shift (suc (suc free)) i (M [ N / suc n ]))
  →∎
shift-subst free i n (M ∙ L) N =
    shift (suc (suc free)) i M [ shift free i N / n ] ∙ shift (suc (suc free)) i L [ shift free i N / n ]
  →*⟨ cong-∙-l (shift-subst free i n M N) ⟩
    shift (suc free) i (M [ N / n ]) ∙ shift (suc (suc free)) i L [ shift free i N / n ]
  →*⟨ cong-∙-r (shift-subst free i n L N) ⟩
    shift (suc free) i (M [ N / n ]) ∙ shift (suc free) i (L [ N / n ])
  →∎

cong-shift-app0 : (free i : ℕ) → (M N : Term) → shift free i ((ƛ M) ∙ N) β→* shift free i (M [ N ])
cong-shift-app0 free i (var x) N = {!   !}
cong-shift-app0 free i (ƛ M) N =
    (ƛ (ƛ shift (suc (suc free)) i M)) ∙ shift free i N
  →*⟨ hop β-ƛ-∙ ⟩
    (ƛ shift (suc (suc free)) i M) [ shift free i N / 0 ]
  →⟨⟩
    ƛ (shift (suc (suc free)) i M) [ shift free i N / 1 ]
  →*⟨ cong-ƛ (shift-subst free i _ M N) ⟩
    ƛ shift (suc free) i (M [ N / 1 ])
  →∎
cong-shift-app0 free i (M ∙ L) N =
    (ƛ shift (suc free) i M ∙ shift (suc free) i L) ∙ shift free i N
  →*⟨ cong-∙-l {! cong-shift-app0 free i M L   !} ⟩
    {!   !} ∙ shift free i N
  →*⟨ {!   !} ⟩
    {!   !}
  →*⟨ {!   !} ⟩
    {!   !}
  →*⟨ {!   !} ⟩
    shift free i (M [ N ]) ∙ shift free i (L [ N ])
  →∎

-- cong-shift-app : (free i : ℕ) → (M N : Term) → shift free i ((ƛ M) ∙ N) β→* shift free i (M [ N ])
-- cong-shift-app free i (var x) (var y) = {!   !}
-- cong-shift-app free i (var x) (ƛ N)   = {!   !}
-- cong-shift-app free i (var x) (N ∙ O) = {!   !}
-- cong-shift-app free i (ƛ M)   (var y) = {!   !}
-- cong-shift-app free i (ƛ M)   (ƛ N)   = {!   !}
-- cong-shift-app free i (ƛ M)   (N ∙ O) = {!   !}
-- cong-shift-app free i (M ∙ L) (var y) = {!   !}
-- cong-shift-app free i (M ∙ L) (ƛ N)   = {!   !}
-- cong-shift-app free i (M ∙ L) (N ∙ O) = {!   !}

cong-shift : (free i : ℕ) → (M N : Term) → M β→ N → shift free i M β→* shift free i N
cong-shift free i (ƛ M) (ƛ N) (β-ƛ M→N) = cong-ƛ (cong-shift (suc free) i M N M→N)
cong-shift free i (.(ƛ M) ∙ N) .(M [ N / 0 ]) (β-ƛ-∙ {M}) = cong-shift-app0 free i M N
cong-shift free i (M ∙ L) .(N ∙ L) (β-∙-l {N = N} M→N) = cong-∙-l (cong-shift free i M N M→N)
cong-shift free i (M ∙ L) .(M ∙ N) (β-∙-r {N = N} M→N) = cong-∙-r (cong-shift free i L N M→N)

cong-[] : ∀ {i M N} (L : Term) → M β→ N → L [ M / i ] β→* L [ N / i ]
cong-[] {i} (var x) M→N with compare x i
cong-[] {.(suc (x + k))} (var x)              M→N | less .x k   = ∎
cong-[] {.x} {M} {N}     (var x)              M→N | equal .x    = cong-shift 0 x M N M→N
cong-[] {.m}             (var .(suc (m + k))) M→N | greater m k = ∎
cong-[] (ƛ L) M→N = cong-ƛ (cong-[] L M→N)
cong-[] {i} {M} {N} (L ∙ K) M→N =
    L [ M / i ] ∙ K [ M / i ]
  →*⟨ cong-∙-l (cong-[] L M→N) ⟩
    L [ N / i ] ∙ K [ M / i ]
  →*⟨ cong-∙-r (cong-[] K M→N) ⟩
    L [ N / i ] ∙ K [ N / i ]
  →∎

lemma : ∀ {M N O} → ƛ M β→ N → M [ O ] β→* N ∙ O
lemma {ƛ M}   (β-ƛ {N = ƛ N}   M→N) = {!   !}
lemma {M ∙ L} (β-ƛ {N = var x} M→N) = {!   !}
lemma {M ∙ L} (β-ƛ {N = ƛ N}   M→N) = {!   !}
lemma {M ∙ L} (β-ƛ {N = N ∙ K} M→N) = {!   !}

-- single-step
β→confluent : ∀ {M N O} → (M β→ N) → (M β→ O) → ∃ (λ P → (N β→* P) × (O β→* P))
β→confluent (β-ƛ-∙ {M} {N})         β-ƛ-∙               = M [ N ] , ∎ , ∎
β→confluent (β-ƛ-∙ {M} {N})         (β-∙-l {N = O} M→O) = {!   !}
  -- O ∙ N , lemma M→O , ∎
β→confluent (β-ƛ-∙ {M} {N})         (β-∙-r {N = O} M→O) = M [ O ] , cong-[] M M→O , hop β-ƛ-∙
β→confluent (β-ƛ   {M} {N}     M→N) (β-ƛ   {N = O} M→O) with β→confluent M→N M→O
β→confluent (β-ƛ   {M} {N}     M→N) (β-ƛ   {N = O} M→O) | P , N→P , O→P = ƛ P , cong-ƛ N→P , cong-ƛ O→P
β→confluent (β-∙-l {L} {N = N} M→N) (β-ƛ-∙ {M})         = N ∙ L , ∎ , lemma M→N
β→confluent (β-∙-l {L} {M} {N} M→N) (β-∙-l {N = O} M→O) with β→confluent M→N M→O
β→confluent (β-∙-l {L} {M} {N} M→N) (β-∙-l {N = O} M→O) | P , N→P , O→P = P ∙ L , cong-∙-l N→P , cong-∙-l O→P
β→confluent (β-∙-l {L} {M} {N} M→N) (β-∙-r {N = O} L→O) = N ∙ O , hop (β-∙-r L→O) , hop (β-∙-l M→N)
β→confluent (β-∙-r {M = M} {N} M→N) (β-ƛ-∙ {L})         = L [ N ] , (hop β-ƛ-∙) , cong-[] L M→N
β→confluent (β-∙-r {L} {M} {N} M→N) (β-∙-l {N = O} M→O) = O ∙ N , hop (β-∙-l M→O) , hop (β-∙-r M→N)
β→confluent (β-∙-r {M = M} {N} M→N) (β-∙-r {N = O} M→O) with β→confluent M→N M→O
β→confluent (β-∙-r {L} {M} {N} M→N) (β-∙-r {N = O} M→O) | P , N→P , O→P = (L ∙ P) , cong-∙-r N→P , cong-∙-r O→P

-- β→confluent : (M N O : Term) → (M β→ N) → (M β→ O) → ∃ (λ P → (N β→* P) × (O β→* P))
-- β→confluent .((ƛ _) ∙ _) ._           ._            β-ƛ-∙ β-ƛ-∙ = {!   !}
-- β→confluent .((ƛ _) ∙ _) ._           .(_ ∙ _)      β-ƛ-∙ (β-∙-l M→O) = {!   !}
-- β→confluent .((ƛ _) ∙ _) ._           .((ƛ _) ∙ _)  β-ƛ-∙ (β-∙-r M→O) = {!   !}
-- β→confluent .(ƛ _)       .(ƛ _)       .(ƛ _)        (β-ƛ M→N) (β-ƛ M→O) = {!   !}
-- β→confluent .((ƛ _) ∙ _) .(_ ∙ _)     ._            (β-∙-l M→N) β-ƛ-∙ = {!   !}
-- β→confluent .(_ ∙ _)     .(_ ∙ _)     .(_ ∙ _)      (β-∙-l M→N) (β-∙-l M→O) = {!   !}
-- β→confluent .(_ ∙ _)     .(_ ∙ _)     .(_ ∙ _)      (β-∙-l M→N) (β-∙-r M→O) = {!   !}
-- β→confluent .((ƛ _) ∙ _) .((ƛ _) ∙ _) ._            (β-∙-r M→N) β-ƛ-∙ = {!   !}
-- β→confluent .(_ ∙ _)     .(_ ∙ _)     .(_ ∙ _)      (β-∙-r M→N) (β-∙-l M→O) = {!   !}
-- β→confluent .(_ ∙ M)     .(_ ∙ N)     .(_ ∙ O)      (β-∙-r {M = M} {N} M→N) (β-∙-r {N = O} M→O) with β→confluent M N O M→N M→O
-- β→confluent .(_ ∙ M)     .(_ ∙ N)     .(_ ∙ O)      (β-∙-r {M = M} {N} M→N) (β-∙-r {N = O} M→O) | P , N→P , O→P = {!   !}

max_stars_repo_name: banacorn/bidirectional

max_issues_repo_name: banacorn/bidirectional

max_forks_repo_name: banacorn/bidirectional


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

module Definition.Typed.Consequences.Reduction where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.EqRelInstance
open import Definition.Typed.Consequences.Syntactic
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Fundamental.Reducibility

open import Tools.Product

-- Helper function where all reducible types can be reduced to WHNF.
whNorm′ : ∀ {A Γ l} ([A] : Γ ⊩⟨ l ⟩ A)
                → ∃ λ B → Whnf B × Γ ⊢ A :⇒*: B
whNorm′ (Uᵣ′ .⁰ 0<1 ⊢Γ) = U , Uₙ , idRed:*: (Uⱼ ⊢Γ)
whNorm′ (ℕᵣ D) = ℕ , ℕₙ , D
whNorm′ (Emptyᵣ D) = Empty , Emptyₙ , D
whNorm′ (Unitᵣ D) = Unit , Unitₙ , D
whNorm′ (ne′ K D neK K≡K) = K , ne neK , D
whNorm′ (Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) = Π F ▹ G , Πₙ , D
whNorm′ (Σᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) = Σ F ▹ G , Σₙ , D
whNorm′ (emb 0<1 [A]) = whNorm′ [A]

-- Well-formed types can all be reduced to WHNF.
whNorm : ∀ {A Γ} → Γ ⊢ A → ∃ λ B → Whnf B × Γ ⊢ A :⇒*: B
whNorm A = whNorm′ (reducible A)

-- Helper function where reducible all terms can be reduced to WHNF.
whNormTerm′ : ∀ {a A Γ l} ([A] : Γ ⊩⟨ l ⟩ A) → Γ ⊩⟨ l ⟩ a ∷ A / [A]
                → ∃ λ b → Whnf b × Γ ⊢ a :⇒*: b ∷ A
whNormTerm′ (Uᵣ x) (Uₜ A d typeA A≡A [t]) = A , typeWhnf typeA , d
whNormTerm′ (ℕᵣ x) (ℕₜ n d n≡n prop) =
  let natN = natural prop
  in  n , naturalWhnf natN , convRed:*: d (sym (subset* (red x)))
whNormTerm′ (Emptyᵣ x) (Emptyₜ n d n≡n prop) =
  let emptyN = empty prop
  in  n , ne emptyN , convRed:*: d (sym (subset* (red x)))
whNormTerm′ (Unitᵣ x) (Unitₜ n d prop) =
  n , prop , convRed:*: d (sym (subset* (red x)))
whNormTerm′ (ne (ne K D neK K≡K)) (neₜ k d (neNfₜ neK₁ ⊢k k≡k)) =
  k , ne neK₁ , convRed:*: d (sym (subset* (red D)))
whNormTerm′ (Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (Πₜ f d funcF f≡f [f] [f]₁) =
  f , functionWhnf funcF , convRed:*: d (sym (subset* (red D)))
whNormTerm′ (Σᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (Σₜ p d pProd p≡p [fst] [snd]) =
  p , productWhnf pProd , convRed:*: d (sym (subset* (red D)))
whNormTerm′ (emb 0<1 [A]) [a] = whNormTerm′ [A] [a]

-- Well-formed terms can all be reduced to WHNF.
whNormTerm : ∀ {a A Γ} → Γ ⊢ a ∷ A → ∃ λ b → Whnf b × Γ ⊢ a :⇒*: b ∷ A
whNormTerm {a} {A} ⊢a =
  let [A] , [a] = reducibleTerm ⊢a
  in  whNormTerm′ [A] [a]

redMany : ∀ {t u A Γ} → Γ ⊢ t ⇒ u ∷ A → Γ ⊢ t ⇒* u ∷ A
redMany d =
  let _ , _ , ⊢u = syntacticEqTerm (subsetTerm d)
  in  d ⇨ id ⊢u


text:
------------------------------------------------------------------------
-- Asymmetric choice
------------------------------------------------------------------------

module TotalParserCombinators.AsymmetricChoice where

open import Data.Bool
open import Data.Empty
open import Data.List
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Properties
open import Data.List.Relation.Binary.BagAndSetEquality
  using () renaming (_∼[_]_ to _List-∼[_]_)
open import Data.List.Relation.Unary.Any using (here)
open import Data.Product
import Data.Product.Function.Dependent.Propositional as Σ
open import Data.Unit
open import Function.Base
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence as Equiv
  using (module Equivalence; _⇔_)
open import Function.Inverse as Inv using (_↔_)
open import Function.Related as Related
open import Function.Related.TypeIsomorphisms
open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_)
open import Relation.Nullary

open import TotalParserCombinators.Congruence using (_∼[_]P_; _≅P_)
open import TotalParserCombinators.Derivative using (D)
open import TotalParserCombinators.Parser
import TotalParserCombinators.Pointwise as Pointwise
open import TotalParserCombinators.Semantics using (_∈_·_)
open import TotalParserCombinators.Semantics.Continuation as S
  using (_⊕_∈_·_)

------------------------------------------------------------------------
-- An initial bag operator

-- first-nonempty returns the left-most non-empty initial bag, if any.

first-nonempty : {R : Set} → List R → List R → List R
first-nonempty [] ys = ys
first-nonempty xs ys = xs

-- first-nonempty preserves equality.

first-nonempty-cong :
  ∀ {k R} {xs₁ xs₁′ xs₂ xs₂′ : List R} →
  xs₁ List-∼[ ⌊ k ⌋⇔ ] xs₁′ → xs₂ List-∼[ ⌊ k ⌋⇔ ] xs₂′ →
  first-nonempty xs₁ xs₂ List-∼[ ⌊ k ⌋⇔ ] first-nonempty xs₁′ xs₂′
first-nonempty-cong {xs₁ = []}    {[]}    eq₁ eq₂ = eq₂
first-nonempty-cong {xs₁ = _ ∷ _} {_ ∷ _} eq₁ eq₂ = eq₁
first-nonempty-cong {xs₁ = []} {_ ∷ _} eq₁ eq₂
  with Equivalence.from (⇒⇔ eq₁) ⟨$⟩ here P.refl
... | ()
first-nonempty-cong {xs₁ = _ ∷ _} {[]} eq₁ eq₂
  with Equivalence.to (⇒⇔ eq₁) ⟨$⟩ here P.refl
... | ()

-- first-nonempty is correct.

first-nonempty-left :
  ∀ {k R} {xs₁ xs₂ : List R} →
  (∃ λ y → y ∈ xs₁) → first-nonempty xs₁ xs₂ List-∼[ k ] xs₁
first-nonempty-left {xs₁ = []}    (_ , ())
first-nonempty-left {xs₁ = _ ∷ _} _        = _ ∎
  where open Related.EquationalReasoning

first-nonempty-right :
  ∀ {k R} {xs₁ xs₂ : List R} →
  (∄ λ y → y ∈ xs₁) → first-nonempty xs₁ xs₂ List-∼[ k ] xs₂
first-nonempty-right {xs₁ = x ∷ _} ∉x∷ = ⊥-elim $ ∉x∷ (x , here P.refl)
first-nonempty-right {xs₁ = []}    _   = _ ∎
  where open Related.EquationalReasoning

------------------------------------------------------------------------
-- Asymmetric choice

-- _◃_ is defined as a pointwise lifting of first-nonempty. Note that
-- _◃_ preserves parser and language equality, but not the
-- sub-/superparser and sub-/superlanguage relations.

private
  module AC {R} = Pointwise R R ⌊_⌋⇔ first-nonempty first-nonempty-cong

-- p₁ ◃ p₂ returns a result if either p₁ or p₂ does. For a given
-- string results are returned either from p₁ or from p₂, not both.

infixl 5 _◃_ _◃-cong_

_◃_ : ∀ {Tok R xs₁ xs₂} →
      Parser Tok R xs₁ → Parser Tok R xs₂ →
      Parser Tok R (first-nonempty xs₁ xs₂)
_◃_ = AC.lift

-- D distributes over _◃_.

D-◃ : ∀ {Tok R xs₁ xs₂ t}
      (p₁ : Parser Tok R xs₁) (p₂ : Parser Tok R xs₂) →
      D t (p₁ ◃ p₂) ≅P D t p₁ ◃ D t p₂
D-◃ = AC.D-lift

-- _◃_ preserves equality.

_◃-cong_ : ∀ {k Tok R xs₁ xs₁′ xs₂ xs₂′}
             {p₁  : Parser Tok R xs₁} {p₁′ : Parser Tok R xs₁′}
             {p₂  : Parser Tok R xs₂} {p₂′ : Parser Tok R xs₂′} →
           p₁ ∼[ ⌊ k ⌋⇔ ]P p₁′ → p₂ ∼[ ⌊ k ⌋⇔ ]P p₂′ →
           p₁ ◃ p₂ ∼[ ⌊ k ⌋⇔ ]P p₁′ ◃ p₂′
_◃-cong_ = AC.lift-cong

-- If p₁ accepts s, then p₁ ◃ p₂ behaves as p₁ when applied to s.

left : ∀ {Tok R xs₁ xs₂ x s}
       (p₁ : Parser Tok R xs₁) (p₂ : Parser Tok R xs₂) →
       (∃ λ y → y ∈ p₁ · s) → x ∈ p₁ ◃ p₂ · s ↔ x ∈ p₁ · s
left {x = x} =
  AC.lift-property
    (λ F _ H → ∃ F → H x ↔ F x)
    (λ F↔F′ _ H↔H′ →
       Σ.cong Inv.id (λ {x} → ↔⇒ (F↔F′ x))
         →-cong-⇔
       Related-cong (H↔H′ x) (F↔F′ x))
    (λ ∈xs₁ → first-nonempty-left ∈xs₁)

-- If p₁ does not accept s, then p₁ ◃ p₂ behaves as p₂ when applied to
-- s.

right : ∀ {Tok R xs₁ xs₂ x s}
        (p₁ : Parser Tok R xs₁) (p₂ : Parser Tok R xs₂) →
        (∄ λ y → y ∈ p₁ · s) → x ∈ p₁ ◃ p₂ · s ↔ x ∈ p₂ · s
right {x = x} =
  AC.lift-property
    (λ F G H → ∄ F → H x ↔ G x)
    (λ F↔F′ G↔G′ H↔H′ →
       ((Σ.cong Inv.id λ {x} → ↔⇒ (F↔F′ x)) →-cong-⇔ Equiv.id)
         →-cong-⇔
       Related-cong (H↔H′ x) (G↔G′ x))
    (λ ∉xs₁ → first-nonempty-right ∉xs₁)

-- In "Parsing with First-Class Derivatives" Brachthäuser, Rendel and
-- Ostermann state that "[...] and biased alternative cannot be
-- expressed as user defined combinators". Here I give a formal proof
-- of a variant of this statement (in the present setting): it is not
-- possible to construct an asymmetric choice operator that, in a
-- certain sense, is more like the prioritised choice of parsing
-- expression grammars (see Ford's "Parsing Expression Grammars: A
-- Recognition-Based Syntactic Foundation") without changing the
-- interface of the parser combinator library.

not-PEG-choice :
  ¬ ∃₂ λ (_◅-bag_ : {R : Set} → List R → List R → List R)
         (_◅_ : ∀ {Tok R xs₁ xs₂} →
               Parser Tok R xs₁ → Parser Tok R xs₂ →
               Parser Tok R (xs₁ ◅-bag xs₂)) →
      ∀ {Tok R xs₁ xs₂ s₁}
      (p₁ : Parser Tok R xs₁)
      (p₂ : Parser Tok R xs₂) →
      ((∃₂ λ y s₂ → y ⊕ s₂ ∈ p₁ · s₁) →
       ∀ {x s₂} → x ⊕ s₂ ∈ p₁ ◅ p₂ · s₁ ⇔ x ⊕ s₂ ∈ p₁ · s₁)
        ×
      (¬ (∃₂ λ y s₂ → y ⊕ s₂ ∈ p₁ · s₁) →
       ∀ {x s₂} → x ⊕ s₂ ∈ p₁ ◅ p₂ · s₁ ⇔ x ⊕ s₂ ∈ p₂ · s₁)
not-PEG-choice (_ , _◅_ , correct) = false∉p₁⊛·[-] false∈p₁⊛·[-]
  where
  p₁ p₂ : Parser ⊤ Bool _
  p₁ = const true <$> token
  p₂ = return false

  false∈p₂·[] : false ⊕ [] ∈ p₂ · []
  false∈p₂·[] = S.return

  ∄∈p₁·[] : ¬ ∃₂ (λ b s → b ⊕ s ∈ p₁ · [])
  ∄∈p₁·[] (_ , _ , S.<$> ())

  false∈p₁◅p₂·[] : false ⊕ [] ∈ p₁ ◅ p₂ · []
  false∈p₁◅p₂·[] =
    Equivalence.from (proj₂ (correct _ _) ∄∈p₁·[]) ⟨$⟩ false∈p₂·[]

  false∈p₁◅p₂·[-] : false ⊕ [ _ ] ∈ p₁ ◅ p₂ · [ _ ]
  false∈p₁◅p₂·[-] = S.extend false∈p₁◅p₂·[]

  true∈p₁·[-] : true ⊕ [] ∈ p₁ · [ _ ]
  true∈p₁·[-] = S.<$> S.token

  false∈p₁·[-] : false ⊕ [ _ ] ∈ p₁ · [ _ ]
  false∈p₁·[-] =
    Equivalence.to (proj₁ (correct _ _) (-, -, true∈p₁·[-])) ⟨$⟩
      false∈p₁◅p₂·[-]

  false∈p₁⊛·[-] :
    false ⊕ [] ∈ const <$> p₁ ⊛ (return _ ∣ token) · [ _ ]
  false∈p₁⊛·[-] = S.[ _ - _ ] S.<$> false∈p₁·[-] ⊛ S.∣-right _ S.token

  false∉p₁⊛·[-] :
    ¬ false ⊕ [] ∈ const <$> p₁ ⊛ (return _ ∣ token) · [ _ ]
  false∉p₁⊛·[-] = flip lemma P.refl
    where
    lemma :
      ∀ {b} →
      b ⊕ [] ∈ const <$> p₁ ⊛ (return _ ∣ token) · [ _ ] → b ≢ false
    lemma (S.[ _ - _ ] S.<$> (S.<$> S.token) ⊛ _) ()

max_stars_repo_name: nad/parser-combinators


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module provides alternative ways of providing instances of
-- structures in the Algebra.Module hierarchy.
------------------------------------------------------------------------

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

open import Relation.Binary using (Rel; Setoid; IsEquivalence)

module Algebra.Module.Structures.Biased where

open import Algebra.Bundles
open import Algebra.Core
open import Algebra.Module.Consequences
open import Algebra.Module.Structures
open import Function.Base using (flip)
open import Level using (Level; _⊔_)

private
  variable
    m ℓm r ℓr s ℓs : Level
    M : Set m

module _ (commutativeSemiring : CommutativeSemiring r ℓr) where
  open CommutativeSemiring commutativeSemiring renaming (Carrier to R)

  -- A left semimodule over a commutative semiring is already a semimodule.

  record IsSemimoduleFromLeft (≈ᴹ : Rel {m} M ℓm) (+ᴹ : Op₂ M) (0ᴹ : M)
                              (*ₗ : Opₗ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
    field
      isLeftSemimodule : IsLeftSemimodule semiring ≈ᴹ +ᴹ 0ᴹ *ₗ

    open IsLeftSemimodule isLeftSemimodule

    isBisemimodule : IsBisemimodule semiring semiring ≈ᴹ +ᴹ 0ᴹ *ₗ (flip *ₗ)
    isBisemimodule = record
      { +ᴹ-isCommutativeMonoid = +ᴹ-isCommutativeMonoid
      ; isPreleftSemimodule = isPreleftSemimodule
      ; isPrerightSemimodule = record
        { *ᵣ-cong = flip *ₗ-cong
        ; *ᵣ-zeroʳ = *ₗ-zeroˡ
        ; *ᵣ-distribˡ = *ₗ-distribʳ
        ; *ᵣ-identityʳ = *ₗ-identityˡ
        ; *ᵣ-assoc =
          *ₗ-assoc+comm⇒*ᵣ-assoc _≈_ ≈ᴹ-setoid *ₗ-congʳ *ₗ-assoc *-comm
        ; *ᵣ-zeroˡ = *ₗ-zeroʳ
        ; *ᵣ-distribʳ = *ₗ-distribˡ
        }
      ; *ₗ-*ᵣ-assoc =
        *ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc _≈_ ≈ᴹ-setoid *ₗ-congʳ *ₗ-assoc *-comm
      }

    isSemimodule : IsSemimodule commutativeSemiring ≈ᴹ +ᴹ 0ᴹ *ₗ (flip *ₗ)
    isSemimodule = record { isBisemimodule = isBisemimodule }

  -- Similarly, a right semimodule over a commutative semiring
  -- is already a semimodule.

  record IsSemimoduleFromRight (≈ᴹ : Rel {m} M ℓm) (+ᴹ : Op₂ M) (0ᴹ : M)
                               (*ᵣ : Opᵣ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
    field
      isRightSemimodule : IsRightSemimodule semiring ≈ᴹ +ᴹ 0ᴹ *ᵣ

    open IsRightSemimodule isRightSemimodule

    isBisemimodule : IsBisemimodule semiring semiring ≈ᴹ +ᴹ 0ᴹ (flip *ᵣ) *ᵣ
    isBisemimodule = record
      { +ᴹ-isCommutativeMonoid = +ᴹ-isCommutativeMonoid
      ; isPreleftSemimodule = record
        { *ₗ-cong = flip *ᵣ-cong
        ; *ₗ-zeroˡ = *ᵣ-zeroʳ
        ; *ₗ-distribʳ = *ᵣ-distribˡ
        ; *ₗ-identityˡ = *ᵣ-identityʳ
        ; *ₗ-assoc =
          *ᵣ-assoc+comm⇒*ₗ-assoc _≈_ ≈ᴹ-setoid *ᵣ-congˡ *ᵣ-assoc *-comm
        ; *ₗ-zeroʳ = *ᵣ-zeroˡ
        ; *ₗ-distribˡ = *ᵣ-distribʳ
        }
      ; isPrerightSemimodule = isPrerightSemimodule
      ; *ₗ-*ᵣ-assoc =
        *ᵣ-assoc+comm⇒*ₗ-*ᵣ-assoc _≈_ ≈ᴹ-setoid *ᵣ-congˡ *ᵣ-assoc *-comm
      }

    isSemimodule : IsSemimodule commutativeSemiring ≈ᴹ +ᴹ 0ᴹ (flip *ᵣ) *ᵣ
    isSemimodule = record { isBisemimodule = isBisemimodule }

module _ (commutativeRing : CommutativeRing r ℓr) where
  open CommutativeRing commutativeRing renaming (Carrier to R)

  -- A left module over a commutative ring is already a module.

  record IsModuleFromLeft (≈ᴹ : Rel {m} M ℓm)
                          (+ᴹ : Op₂ M) (0ᴹ : M) (-ᴹ : Op₁ M) (*ₗ : Opₗ R M)
                          : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
    field
      isLeftModule : IsLeftModule ring ≈ᴹ +ᴹ 0ᴹ -ᴹ *ₗ

    open IsLeftModule isLeftModule

    isModule : IsModule commutativeRing ≈ᴹ +ᴹ 0ᴹ -ᴹ *ₗ (flip *ₗ)
    isModule = record
      { isBimodule = record
        { isBisemimodule = IsSemimoduleFromLeft.isBisemimodule
          {commutativeSemiring = commutativeSemiring}
          (record { isLeftSemimodule = isLeftSemimodule })
        ; -ᴹ‿cong = -ᴹ‿cong
        ; -ᴹ‿inverse = -ᴹ‿inverse
        }
      }

  -- Similarly, a right module over a commutative ring is already a module.

  record IsModuleFromRight (≈ᴹ : Rel {m} M ℓm)
                           (+ᴹ : Op₂ M) (0ᴹ : M) (-ᴹ : Op₁ M) (*ᵣ : Opᵣ R M)
                           : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
    field
      isRightModule : IsRightModule ring ≈ᴹ +ᴹ 0ᴹ -ᴹ *ᵣ

    open IsRightModule isRightModule

    isModule : IsModule commutativeRing ≈ᴹ +ᴹ 0ᴹ -ᴹ (flip *ᵣ) *ᵣ
    isModule = record
      { isBimodule = record
        { isBisemimodule = IsSemimoduleFromRight.isBisemimodule
          {commutativeSemiring = commutativeSemiring}
          (record { isRightSemimodule = isRightSemimodule })
        ; -ᴹ‿cong = -ᴹ‿cong
        ; -ᴹ‿inverse = -ᴹ‿inverse
        }
      }


text:
{-

Freudenthal suspension theorem

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Homotopy.Freudenthal where

open import Cubical.Foundations.Everything
open import Cubical.Data.HomotopyGroup
open import Cubical.Data.Nat
open import Cubical.Data.Sigma
open import Cubical.HITs.Nullification
open import Cubical.HITs.Susp
open import Cubical.HITs.Truncation as Trunc renaming (rec to trRec)
open import Cubical.Homotopy.Connected
open import Cubical.Homotopy.WedgeConnectivity
open import Cubical.Homotopy.Loopspace

module _ {ℓ} (n : HLevel) {A : Pointed ℓ} (connA : isConnected (suc (suc n)) (typ A)) where

  σ : typ A → typ (Ω (∙Susp (typ A)))
  σ a = merid a ∙ merid (pt A) ⁻¹

  private
    2n+2 = suc n + suc n

    module WC (p : north ≡ north) =
      WedgeConnectivity (suc n) (suc n) A connA A connA
        (λ a b →
          ( (σ b ≡ p → hLevelTrunc 2n+2 (fiber (λ x → merid x ∙ merid a ⁻¹) p))
          , isOfHLevelΠ 2n+2 λ _ → isOfHLevelTrunc 2n+2
          ))
        (λ a r → ∣ a , (rCancel' (merid a) ∙ rCancel' (merid (pt A)) ⁻¹) ∙ r ∣)
        (λ b r → ∣ b , r ∣)
        (funExt λ r →
          cong′ (λ w → ∣ pt A , w ∣)
            (cong (_∙ r) (rCancel' (rCancel' (merid (pt A))))
              ∙ lUnit r ⁻¹))

    fwd : (p : north ≡ north) (a : typ A)
      → hLevelTrunc 2n+2 (fiber σ p)
      → hLevelTrunc 2n+2 (fiber (λ x → merid x ∙ merid a ⁻¹) p)
    fwd p a = Trunc.rec (isOfHLevelTrunc 2n+2) (uncurry (WC.extension p a))

    isEquivFwd : (p : north ≡ north) (a : typ A) → isEquiv (fwd p a)
    isEquivFwd p a .equiv-proof =
      elim.isEquivPrecompose (λ _ → pt A) (suc n)
        (λ a →
          ( (∀ t → isContr (fiber (fwd p a) t))
          , isProp→isOfHLevelSuc n (isPropΠ λ _ → isPropIsContr)
          ))

        (isConnectedPoint (suc n) connA (pt A))
        .equiv-proof
        (λ _ → Trunc.elim
          (λ _ → isProp→isOfHLevelSuc (n + suc n) isPropIsContr)
         (λ fib →
            subst (λ k → isContr (fiber k ∣ fib ∣))
              (cong (Trunc.rec (isOfHLevelTrunc 2n+2) ∘ uncurry)
                (funExt (WC.right p) ⁻¹))
              (subst isEquiv
                (funExt (Trunc.mapId) ⁻¹)
                (idIsEquiv _)
                .equiv-proof ∣ fib ∣)
             ))
        .fst .fst a

    interpolate : (a : typ A)
      → PathP (λ i → typ A → north ≡ merid a i) (λ x → merid x ∙ merid a ⁻¹) merid
    interpolate a i x j = compPath-filler (merid x) (merid a ⁻¹) (~ i) j

  Code : (y : Susp (typ A)) → north ≡ y → Type ℓ
  Code north p = hLevelTrunc 2n+2 (fiber σ p)
  Code south q = hLevelTrunc 2n+2 (fiber merid q)
  Code (merid a i) p =
    Glue
      (hLevelTrunc 2n+2 (fiber (interpolate a i) p))
      (λ
        { (i = i0) → _ , (fwd p a , isEquivFwd p a)
        ; (i = i1) → _ , idEquiv _
        })

  encode : (y : Susp (typ A)) (p : north ≡ y) → Code y p
  encode y = J Code ∣ pt A , rCancel' (merid (pt A)) ∣

  encodeMerid : (a : typ A) → encode south (merid a) ≡ ∣ a , refl ∣
  encodeMerid a =
    cong (transport (λ i → gluePath i))
      (funExt⁻ (WC.left refl a) _ ∙ cong ∣_∣ (cong (a ,_) (lem _ _)))
    ∙ transport (PathP≡Path gluePath _ _)
      (λ i → ∣ a , (λ j k → rCancel-filler' (merid a) i j k) ∣)
    where
    gluePath : I → Type _
    gluePath i = hLevelTrunc 2n+2 (fiber (interpolate a i) (λ j → merid a (i ∧ j)))

    lem : ∀ {ℓ} {A : Type ℓ} {x y z : A} (p : x ≡ y) (q : z ≡ y) → (p ∙ q ⁻¹) ∙ q ≡ p
    lem p q = assoc p (q ⁻¹) q ⁻¹ ∙ cong (p ∙_) (lCancel q) ∙ rUnit p ⁻¹

  contractCodeSouth : (p : north ≡ south) (c : Code south p) → encode south p ≡ c
  contractCodeSouth p =
    Trunc.elim
      (λ _ → isOfHLevelPath 2n+2 (isOfHLevelTrunc 2n+2) _ _)
      (uncurry λ a →
        J (λ p r → encode south p ≡ ∣ a , r ∣) (encodeMerid a))

  isConnectedMerid : isConnectedFun 2n+2 (merid {A = typ A})
  isConnectedMerid p = encode south p , contractCodeSouth p

  isConnectedσ : isConnectedFun 2n+2 σ
  isConnectedσ =
    transport (λ i → isConnectedFun 2n+2 (interpolate (pt A) (~ i))) isConnectedMerid

FreudenthalEquiv : ∀ {ℓ} (n : HLevel) (A : Pointed ℓ)
                → isConnected (2 + n) (typ A)
                → hLevelTrunc ((suc n) + (suc n)) (typ A)
                 ≃ hLevelTrunc ((suc n) + (suc n)) (typ (Ω (Susp (typ A) , north)))
FreudenthalEquiv n A iscon = connectedTruncEquiv _
                                                 (σ n {A = A} iscon)
                                                 (isConnectedσ _ iscon)
FreudenthalIso : ∀ {ℓ} (n : HLevel) (A : Pointed ℓ)
                → isConnected (2 + n) (typ A)
                → Iso (hLevelTrunc ((suc n) + (suc n)) (typ A))
                       (hLevelTrunc ((suc n) + (suc n)) (typ (Ω (Susp (typ A) , north))))
FreudenthalIso n A iscon = connectedTruncIso _ (σ n {A = A} iscon) (isConnectedσ _ iscon)

max_stars_repo_name: knrafto/cubical

max_issues_repo_name: knrafto/cubical

max_forks_repo_name: knrafto/cubical


text:
-- A formalised proof of the soundness and completeness of
-- a simply typed lambda-calculus with explicit substitutions
--
-- Catarina Coquand
--
-- Higher-Order and Symbolic Computation, 15, 57-90, 2002
--
-- http://dx.doi.org/10.1023/A:1019964114625

module Everything where

-- 1. Introduction
import Section1

-- 2. The proof editor
-- NOTE: Not relevant to this formalisation

-- 3. The calculus of proof trees
import Section3

-- 4. The semantic model
import Section4a
import Section4b

-- 5. Normal form
import Section5

-- 6. Application to terms
import Section6

-- 7. Correspondence between proof trees and terms
import Section7

-- 8. Correctness of conversion between terms
import Section8

-- 9. A decision algorithm for terms
import Section9

-- 10. Conclusions
import Section10

max_stars_repo_name: mietek/coquand

max_issues_repo_name: mietek/coquand

max_forks_repo_name: mietek/coquand


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Finding the maximum/minimum values in a list, specialised for Nat
------------------------------------------------------------------------

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

-- This specialised module is needed as `m < n` for Nat is not
-- implemented as `m ≤ n × m ≢ n`.

module Data.List.Extrema.Nat where

open import Data.Nat.Base using (ℕ; _≤_; _<_)
open import Data.Nat.Properties as ℕₚ using (≤∧≢⇒<; <⇒≤; <⇒≢)
open import Data.Sum.Base as Sum using (_⊎_)
open import Data.List.Base using (List)
import Data.List.Extrema
open import Data.List.Relation.Unary.Any as Any using (Any)
open import Data.List.Relation.Unary.All as All using (All)
open import Data.Product using (_×_; _,_; uncurry′)
open import Level using (Level)
open import Relation.Binary.PropositionalEquality using (_≢_)

private
  variable
    a : Level
    A : Set a

  <⇒<× : ∀ {x y} → x < y → x ≤ y × x ≢ y
  <⇒<× x<y = <⇒≤ x<y , <⇒≢ x<y

  <×⇒< : ∀ {x y} → x ≤ y × x ≢ y → x < y
  <×⇒< (x≤y , x≢y) = ≤∧≢⇒< x≤y x≢y

  module Extrema = Data.List.Extrema ℕₚ.≤-totalOrder

------------------------------------------------------------------------
-- Re-export the contents of Extrema

open Extrema public
  hiding
  ( f[argmin]<v⁺; v<f[argmin]⁺; argmin[xs]<argmin[ys]⁺
  ; f[argmax]<v⁺; v<f[argmax]⁺; argmax[xs]<argmax[ys]⁺
  ; min<v⁺; v<min⁺; min[xs]<min[ys]⁺
  ; max<v⁺; v<max⁺; max[xs]<max[ys]⁺
  )

------------------------------------------------------------------------
-- New versions of the proofs involving _<_

-- Argmin

f[argmin]<v⁺ : ∀ {f : A → ℕ} {v} ⊤ xs →
              (f ⊤ < v) ⊎ (Any (λ x → f x < v) xs) →
              f (argmin f ⊤ xs) < v
f[argmin]<v⁺ ⊤ xs arg =
  <×⇒< (Extrema.f[argmin]<v⁺ ⊤ xs (Sum.map <⇒<× (Any.map <⇒<×) arg))

v<f[argmin]⁺ : ∀ {f : A → ℕ} {v ⊤ xs} →
              v < f ⊤ → All (λ x → v < f x) xs →
              v < f (argmin f ⊤ xs)
v<f[argmin]⁺ {v} v<f⊤ v<fxs =
  <×⇒< (Extrema.v<f[argmin]⁺ (<⇒<× v<f⊤) (All.map <⇒<× v<fxs))

argmin[xs]<argmin[ys]⁺ : ∀ {f g : A → ℕ} ⊤₁ {⊤₂} xs {ys} →
                        (f ⊤₁ < g ⊤₂) ⊎ Any (λ x → f x < g ⊤₂) xs →
                        All (λ y → (f ⊤₁ < g y) ⊎ Any (λ x → f x < g y) xs) ys →
                        f (argmin f ⊤₁ xs) < g (argmin g ⊤₂ ys)
argmin[xs]<argmin[ys]⁺ ⊤₁ xs xs<⊤₂ xs<ys =
  v<f[argmin]⁺ (f[argmin]<v⁺ ⊤₁ _ xs<⊤₂) (All.map (f[argmin]<v⁺ ⊤₁ xs) xs<ys)

-- Argmax

v<f[argmax]⁺ : ∀ {f : A → ℕ} {v} ⊥ xs → (v < f ⊥) ⊎ (Any (λ x → v < f x) xs) →
              v < f (argmax f ⊥ xs)
v<f[argmax]⁺ ⊥ xs leq = <×⇒< (Extrema.v<f[argmax]⁺ ⊥ xs (Sum.map <⇒<× (Any.map <⇒<×) leq))

f[argmax]<v⁺ : ∀ {f : A → ℕ} {v ⊥ xs} → f ⊥ < v → All (λ x → f x < v) xs →
              f (argmax f ⊥ xs) < v
f[argmax]<v⁺ ⊥<v xs<v = <×⇒< (Extrema.f[argmax]<v⁺ (<⇒<× ⊥<v) (All.map <⇒<× xs<v))

argmax[xs]<argmax[ys]⁺ : ∀ {f g : A → ℕ} {⊥₁} ⊥₂ {xs} ys →
                         (f ⊥₁ < g ⊥₂) ⊎ Any (λ y → f ⊥₁ < g y) ys →
                         All (λ x → (f x < g ⊥₂) ⊎ Any (λ y → f x < g y) ys) xs →
                         f (argmax f ⊥₁ xs) < g (argmax g ⊥₂ ys)
argmax[xs]<argmax[ys]⁺ ⊥₂ ys ⊥₁<ys xs<ys =
  f[argmax]<v⁺ (v<f[argmax]⁺ ⊥₂ _ ⊥₁<ys) (All.map (v<f[argmax]⁺ ⊥₂ ys) xs<ys)

-- Min

min<v⁺ : ∀ {v} ⊤ xs → ⊤ < v ⊎ Any (_< v) xs → min ⊤ xs < v
min<v⁺ = f[argmin]<v⁺

v<min⁺ : ∀ {v ⊤ xs} → v < ⊤ → All (v <_) xs → v < min ⊤ xs
v<min⁺ = v<f[argmin]⁺

min[xs]<min[ys]⁺ : ∀ ⊤₁ {⊤₂} xs {ys} → (⊤₁ < ⊤₂) ⊎ Any (_< ⊤₂) xs →
                   All (λ y → (⊤₁ < y) ⊎ Any (λ x → x < y) xs) ys →
                   min ⊤₁ xs < min ⊤₂ ys
min[xs]<min[ys]⁺ = argmin[xs]<argmin[ys]⁺

-- Max

max<v⁺ : ∀ {v ⊥ xs} → ⊥ < v → All (_< v) xs → max ⊥ xs < v
max<v⁺ = f[argmax]<v⁺

v<max⁺ : ∀ {v} ⊥ xs → v < ⊥ ⊎ Any (v <_) xs → v < max ⊥ xs
v<max⁺ = v<f[argmax]⁺

max[xs]<max[ys]⁺ : ∀ {⊥₁} ⊥₂ {xs} ys → ⊥₁ < ⊥₂ ⊎ Any (⊥₁ <_) ys →
                   All (λ x → x < ⊥₂ ⊎ Any (x <_) ys) xs →
                   max ⊥₁ xs < max ⊥₂ ys
max[xs]<max[ys]⁺ = argmax[xs]<argmax[ys]⁺


text:
{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}

module Cubical.HITs.InfNat.Base where

open import Cubical.Core.Everything
open import Cubical.Data.Maybe
open import Cubical.Data.Nat

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism

data ℕ+∞ : Type₀ where
  zero : ℕ+∞
  suc : ℕ+∞ → ℕ+∞
  ∞ : ℕ+∞
  suc-inf : ∞ ≡ suc ∞

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module Data.Integer where

import Prelude
import Data.Nat as Nat
import Data.Bool

open Nat using (Nat; suc; zero)
         renaming ( _+_  to _+'_
                  ; _*_  to _*'_
                  ; _<_  to _<'_
                  ; _-_  to _-'_
                  ; _==_ to _=='_
                  ; div  to div'
                  ; mod  to mod'
                  ; gcd  to gcd'
                  ; lcm  to lcm'
                  )
open Data.Bool
open Prelude

data Int : Set where
  pos : Nat -> Int
  neg : Nat -> Int  -- neg n = -(n + 1)

infix 40 _==_ _<_ _>_ _≤_ _≥_
infixl 60 _+_ _-_
infixl 70 _*_
infix  90 -_

-_ : Int -> Int
- pos zero    = pos zero
- pos (suc n) = neg n
- neg n       = pos (suc n)

_+_ : Int -> Int -> Int
pos n + pos m = pos (n +' m)
neg n + neg m = neg (n +' m +' 1)
pos n + neg m =
  ! m <' n => pos (n -' m -' 1)
  ! otherwise neg (m -' n)
neg n + pos m = pos m + neg n

_-_ : Int -> Int -> Int
x - y = x + - y

!_! : Int -> Nat
! pos n ! = n
! neg n ! = suc n

_*_ : Int -> Int -> Int
pos 0 * _     = pos 0
_     * pos 0 = pos 0
pos n * pos m = pos (n *' m)
neg n * neg m = pos (suc n *' suc m)
pos n * neg m = neg (n *' suc m -' 1)
neg n * pos m = neg (suc n *' m -' 1)

div : Int -> Int -> Int
div _             (pos 0)       = pos 0
div (pos n)       (pos m)       = pos (div' n m)
div (neg n)       (neg m)       = pos (div' (suc n) (suc m))
div (pos 0)       (neg _)       = pos 0
div (pos (suc n)) (neg m)       = neg (div' n (suc m))
div (neg n)       (pos (suc m)) = div (pos (suc n)) (neg m)

mod : Int -> Int -> Int
mod _ (pos 0)       = pos 0
mod (pos n) (pos m) = pos (mod' n m)
mod (neg n) (pos m) = adjust (mod' (suc n) m)
  where
    adjust : Nat -> Int
    adjust 0 = pos 0
    adjust n = pos (m -' n)
mod n (neg m)       = adjust (mod n (pos (suc m)))
  where
    adjust : Int -> Int
    adjust (pos 0) = pos 0
    adjust (neg n) = neg n  -- impossible
    adjust x       = x + neg m

gcd : Int -> Int -> Int
gcd a b = pos (gcd' ! a ! ! b !)

lcm : Int -> Int -> Int
lcm a b = pos (lcm' ! a ! ! b !)

_==_ : Int -> Int -> Bool
pos n == pos m = n ==' m
neg n == neg m = n ==' m
pos _ == neg _ = false
neg _ == pos _ = false

_<_ : Int -> Int -> Bool
pos _ < neg _ = false
neg _ < pos _ = true
pos n < pos m = n <' m
neg n < neg m = m <' n

_≤_ : Int -> Int -> Bool
x ≤ y = x == y || x < y

_≥_ = flip _≤_
_>_ = flip _<_