text:
module correct where
open import cfg
open import jarsec using (Parser ; parse ; run-parser ; partial-parse ; _>>=_ ; _>>_ ; _<*>_)

open import Data.Bool
open import Data.List hiding (lookup)
open import Data.Fin hiding (_+_)
open import Data.Char
open import Agda.Builtin.Char renaming ( primCharEquality to charEq )
open import Data.Nat
open import Relation.Binary.PropositionalEquality using (_≡_ ; _≢_ ; refl)
open import Relation.Unary
open import Data.Maybe hiding (Any ; All)
open import Data.Sum hiding (map)
open import Data.String hiding (length ; _++_) renaming (primStringToList to 𝕊→𝕃 ; primStringFromList to 𝕃→𝕊)
open import Data.Product hiding (map)
open import Agda.Builtin.Unit
open import Data.List.All
open import Level

postulate
  sym : ∀ {A : Set} {x y : A} → x ≡ y → y ≡ x
  head-from-≡ : ∀ {A : Set} {x y : A} {xs ys : List A} → (x List.∷ xs) ≡ (y ∷ ys) → x ≡ y
  tail-from-≡ : ∀ {A : Set} {x y : A} {xs ys : List A} → (x List.∷ xs) ≡ (y ∷ ys) → xs ≡ ys

  ++-runit : ∀ {A : Set} (m : List A) → m ++ [] ≡ m
  ++-assoc : ∀ {A : Set} (m n p : List A) → (m ++ n) ++ p ≡ m ++ (n ++ p)

  charEq-T : ∀ x c → (charEq x c) ≡ true → x ≡ c
  charEq-F : ∀ x c → (charEq x c) ≡ false → x ≢ c

correct : ∀ (cfg : Cfg 0) (cs : List Char)
  → let rs = jarsec.parse (interp cfg) cs in
    All (λ r → ((proj₁ r) ∈[ cfg ]) × (proj₁ r) ++ (proj₂ r) ≡ cs) rs

correct emp cs = []
correct eps cs = (eps , refl) ∷ []
correct (lit x) [] = []
correct (lit x) (c ∷ cs) with charEq x c | charEq-T x c | charEq-F x c
... | true | b | d rewrite b refl = (lit c , refl) ∷ []
... | false | b | d = []
correct (var ()) cs
correct (seq cfg₁ cfg₂) cs = {! correct-seq₁ (parse (interp cfg₁) cs) (correct cfg₁ cs)  !}
correct (seq cfg₁ cfg₂) cs with (parse (interp cfg₁) cs) | correct cfg₁ cs
correct (seq cfg₁ cfg₂) cs | [] | [] = []
correct (seq cfg₁ cfg₂) cs | r₁ ∷ rs₁ | a₁ ∷ all₁ with parse (interp cfg₂) (proj₂ r₁) | correct cfg₂ (proj₂ r₁)
correct (seq cfg₁ cfg₂) cs | r₁ ∷ rs₁ | a₁ ∷ all₁ | [] | [] = ?
correct (seq cfg₁ cfg₂) cs | r₁ ∷ rs₁ | a₁ ∷ all₁ | r₂ ∷ rs₂ | a₂ ∷ all₂

  = strengthen-to-seq r₁ a₁ r₂ a₂ ∷ correct-seq₁ cfg₁ cfg₂ cs r₁ rs₁ a₁ all₁ rs₂ all₂
  where
  Result : Set
  Result = List Char × List Char
  strengthen-to-seq :
    ∀ (r₁ : Result)
    → (a₁ : proj₁ r₁ ∈[ cfg₁ ] × proj₁ r₁ ++ proj₂ r₁ ≡ cs)
    → (r₂ : Result)
    → (a₂ : proj₁ r₂ ∈[ cfg₂ ] × proj₁ r₂ ++ proj₂ r₂ ≡ proj₂ r₁)
    → (proj₁ r₁ ++ proj₁ r₂) ∈[ seq cfg₁ cfg₂ ] × (proj₁ r₁ ++ proj₁ r₂) ++ proj₂ r₂ ≡ cs
  strengthen-to-seq r₁ a₁ r₂ a₂
    rewrite ++-assoc (proj₁ r₁)  (proj₁ r₂) (proj₂ r₂)
    | proj₂ a₂
    | proj₂ a₁
    = (seq (proj₁ a₁) (proj₁ a₂)) , refl

  -- correct-seq₁ :
  --   ∀ (rs₁ : List Result)
  --   → (all₁ : All (λ r → (proj₁ r ∈[ cfg₁ ]) × proj₁ r ++ proj₂ r ≡ cs) rs₁)
  --   → All (λ r → (proj₁ r ∈[ seq cfg₁ cfg₂ ]) × proj₁ r ++ proj₂ r ≡ cs)
  --     (parse (interp cfg₁ >>= (λ x → interp cfg₂ >>= (λ y →
  --       Parser.mk-parser (λ str → (x ++ y , str) ∷ [])))) cs)
  -- correct-seq₁ [] [] = {! []  !}
  -- correct-seq₁ (r₁ ∷ rs₁) (a₁ ∷ all₁) = {!   !}

  correct-seq₂ :
    ∀ (cfg₁ cfg₂ : Cfg 0) (cs : List Char)
    → (r₁ : Result)
    → (rs₁ : List Result)
    → (a₁ : Σ (proj₁ r₁ ∈[ cfg₁ ]) (λ x → proj₁ r₁ ++ proj₂ r₁ ≡ cs))
    → (all₁ : All (λ r → Σ (proj₁ r ∈[ cfg₁ ]) (λ x → proj₁ r ++ proj₂ r ≡ cs)) rs₁)
    → All (λ r → (proj₁ r ∈[ seq cfg₁ cfg₂ ]) × proj₁ r ++ proj₂ r ≡ cs)
      (concatMap
       (λ x →
          concatMap (λ x₁ → (proj₁ x ++ proj₁ x₁ , proj₂ x₁) ∷ [])
          (parse (interp cfg₂) (proj₂ x)))
       rs₁)
  correct-seq₂ cfg₁ cfg₂ cs r₁ [] a₁ [] = []
  correct-seq₂ cfg₁ cfg₂ cs r₁ (x ∷ rs₁) a₁ (px ∷ all₁) = ?

  correct-seq₁ :
    ∀ (cfg₁ cfg₂ : Cfg 0) (cs : List Char)
    → (r₁ : Result)
    → (rs₁ : List Result)
    → (a₁ : Σ (proj₁ r₁ ∈[ cfg₁ ]) (λ x → proj₁ r₁ ++ proj₂ r₁ ≡ cs))
    → (all₁ : All (λ r → Σ (proj₁ r ∈[ cfg₁ ]) (λ x → proj₁ r ++ proj₂ r ≡ cs)) rs₁)
    → (rs₂ : List Result)
    → (all₂ : All (λ r → Σ (proj₁ r ∈[ cfg₂ ]) (λ x → proj₁ r ++ proj₂ r ≡ proj₂ r₁)) rs₂)
    → All (λ r → proj₁ r ∈[ seq cfg₁ cfg₂ ] × proj₁ r ++ proj₂ r ≡ cs)
      (foldr _++_ []
        (Data.List.map (λ x → (proj₁ r₁ ++ proj₁ x , proj₂ x) ∷ []) rs₂)
        ++
        (concatMap (λ x →
          (concatMap (λ x₁ → (proj₁ x ++ proj₁ x₁ , proj₂ x₁) ∷ [])
            (parse (interp cfg₂) (proj₂ x))))
        rs₁))

  correct-seq₁ cfg₁ cfg₂ cs r₁ rs₁ a₁ all₁ [] [] = correct-seq₂ cfg₁ cfg₂ cs r₁ rs₁ a₁ all₁
  correct-seq₁ cfg₁ cfg₂ cs r₁ rs₁ a₁ all₁ (r₂ ∷ rs₂) (a₂ ∷ all₂)
    = ((seq (proj₁ a₁) (proj₁ a₂)) , fact) ∷ correct-seq₁ cfg₁ cfg₂ cs r₁ rs₁ a₁ all₁ rs₂ all₂
      where
      fact : (proj₁ r₁ ++ proj₁ r₂) ++ proj₂ r₂ ≡ cs
      fact rewrite ++-assoc (proj₁ r₁) (proj₁ r₂) (proj₂ r₂)
        | proj₂ a₂
        | proj₂ a₁
        = refl

correct (alt cfg₁ cfg₂) cs with (Parser.parse (interp (seq cfg₁ cfg₂)) cs)
... | rs =
  let all₁ = correct cfg₁ cs
      all₂ = correct cfg₂ cs

      weak-all₁ : All (λ r → proj₁ r ∈[ alt cfg₁ cfg₂ ] × proj₁ r ++ proj₂ r ≡ cs) (Parser.parse (interp cfg₁) cs)
      weak-all₁ = Data.List.All.map
        (λ r → ((weaken-to-alt {cfg₁ = cfg₁} {cfg₂ = cfg₂} (inj₁ (proj₁ r))) , (proj₂ r)))
        all₁

      weak-all₂ : All (λ r → proj₁ r ∈[ alt cfg₁ cfg₂ ] × proj₁ r ++ proj₂ r ≡ cs) (Parser.parse (interp cfg₂) cs)
      weak-all₂ = Data.List.All.map
        (λ r → (weaken-to-alt {cfg₁ = cfg₁} {cfg₂ = cfg₂} (inj₂ (proj₁ r))) , (proj₂ r))
        all₂

  in all++ weak-all₁ weak-all₂

  where
    all++ : ∀ {p} {A : Set} {P : Pred A p} {xs ys : List A}
      → All P xs → All P ys → All P (xs ++ ys)
    all++ [] [] = []
    all++ [] (py ∷ all₂) = py ∷ (all++ [] all₂)
    all++ (px ∷ all₁) all₂ = px ∷ (all++ all₁ all₂)

    weaken-to-alt : ∀ {r} {cfg₁ cfg₂ : Cfg 0}
      → (r ∈[ cfg₁ ]) ⊎ (r ∈[ cfg₂ ]) → r ∈[ alt cfg₁ cfg₂ ]
    weaken-to-alt (inj₁ e) = alt₁ e
    weaken-to-alt (inj₂ e) = alt₂ e

correct (many cfg) cs = ?

correct (fix cfg) cs = ?

max_stars_repo_name: jaywunder/jarsec-verified

max_issues_repo_name: jaywunder/jarsec-verified

max_forks_repo_name: jaywunder/jarsec-verified


text:
record R : Set where
  infix 0 _+_

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Mergesort

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

module Algorithms.List.Sort.Merge where

-- agda-stdlib
open import Level
open import Data.Bool using (true; false)
open import Data.List
import      Data.List.Properties as Listₚ
open import Data.Product as Prod
import      Data.Nat as ℕ
open import Data.Nat.Induction as Ind
open import Function.Base
open import Relation.Binary as B
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary
open import Relation.Unary as U
import      Relation.Unary.Properties as Uₚ
open import Induction.WellFounded

private
  variable
    a p r : Level

module Mergesort {A : Set a} {_≤_ : Rel A r} (_≤?_ : B.Decidable _≤_) where
  merge′ : A → A → List A → List A → List A
  merge′ x y xs ys with x ≤? y
  merge′ x y []        ys | true  because _ = x ∷ y ∷ ys
  merge′ x y (x₁ ∷ xs) ys | true  because _ = x ∷ merge′ x₁ y xs ys
  merge′ x y xs []        | false because _ = y ∷ x ∷ xs
  merge′ x y xs (y₁ ∷ ys) | false because _ = y ∷ merge′ x y₁ xs ys

  merge : List A → List A → List A
  merge []       ys       = ys
  merge (x ∷ xs) []       = x ∷ xs
  merge (x ∷ xs) (y ∷ ys) = merge′ x y xs ys

  _L<_ : Rel (List A) _
  _L<_ = ℕ._<_ on length

  L<-wf : WellFounded _L<_
  L<-wf = InverseImage.wellFounded length Ind.<-wellFounded

  split : List A → (List A × List A)
  split []           = [] , []
  split (x ∷ [])     = [ x ] , []
  split (x ∷ y ∷ xs) = Prod.map (x ∷_) (y ∷_) (split xs)
{-
  sort : List A → List A
  sort [] = []
  sort (x ∷ xs) = {!   !}
  sort xs = split xs
  ys , zs = merge (sort ys) (sort zs)
-}


text:
module slots.test where

open import slots.imports
open import slots.defs using (config ; game)
open import slots.bruteforce using (rtp)

c : config
c = record { n = 3 ; m = 4 }

g : game c
g = record { reels = reels ; winTable = winTable } where
  open config c
  reel : Reel
  reel = # 1 ∷ # 1 ∷ # 1 ∷ # 0 ∷ []
  reel′ : Reel
  reel′ = # 1 ∷ # 1 ∷ # 2 ∷ # 0 ∷ []
  reel″ : Reel
  reel″ = # 1 ∷ # 3 ∷ # 1 ∷ # 0 ∷ []

  reels : Reels
  reels =
    reel ∷
    reel′ ∷
    reel″ ∷
    []

  winTable : WinTable
  winTable =
    (0 ∷ 0 ∷ 0 ∷ []) ∷
    (0 ∷ 1 ∷ 2 ∷ []) ∷
    (0 ∷ 0 ∷ 0 ∷ []) ∷
    (0 ∷ 0 ∷ 0 ∷ []) ∷
    []

% : ℕ × ℕ
% = rtp g

%-prf : % ≡ (36 , 64)
%-prf = refl

max_stars_repo_name: semenov-vladyslav/slots-agda

max_issues_repo_name: semenov-vladyslav/slots-agda

max_forks_repo_name: semenov-vladyslav/slots-agda


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

module Categories.FreeObjects.Free where

open import Level
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
open import Relation.Binary using (IsEquivalence)
open import Categories.Functor renaming (id to idF)
open import Categories.Category
open import Categories.Adjoint
open import Categories.NaturalTransformation.Core

import Categories.Morphism.Reasoning as MR

private
  variable
    o ℓ e o' ℓ' e' : Level

record FreeObject {C : Category o ℓ e} {D : Category o' ℓ' e'} (U : Functor D C) (X : Category.Obj C) : Set (suc (e ⊔ e' ⊔ o ⊔ ℓ ⊔ o' ⊔ ℓ')) where

  private
    module C = Category C using (Obj; id; identityʳ; identityˡ; _⇒_; _∘_; equiv; module Equiv)
    module D = Category D using (Obj; _⇒_; _∘_; equiv)
    module U = Functor U using (₀; ₁)

  field
     FX : D.Obj
     η : C [ X , U.₀ FX ]
     _* : ∀ {A : D.Obj} → C [ X , U.₀ A ] → D [ FX , A ]
     *-lift : ∀ {A : D.Obj} (f : C [ X , U.₀ A ]) → C [ (U.₁ (f *) C.∘ η) ≈ f ]
     *-uniq : ∀ {A : D.Obj} (f : C [ X , U.₀ A ]) (g : D [ FX , A ]) → C [ (U.₁ g) C.∘ η ≈ f ] → D [ g ≈ f * ]

  *-cong : ∀ {A : D.Obj} {f g : C [ X , U.₀ A ]} → C [ f ≈ g ] → D [ f * ≈ g * ]
  *-cong {A} {f} {g} f≈g = *-uniq g (f *) (trans (*-lift f) f≈g)    where open C.Equiv

open FreeObject

module _  {C : Category o ℓ e} {D : Category o' ℓ' e'} (U : Functor D C) where

  private
    module C = Category C using (Obj; id; _⇒_; _∘_; identityʳ; identityˡ; assoc; equiv; module Equiv; module HomReasoning)
    module D = Category D using (Obj; id; _⇒_; _∘_; identityʳ; identityˡ; assoc; equiv; module Equiv; module HomReasoning)
    module U = Functor U using (₀; ₁; identity; homomorphism)

  -- free object construction is functorial
  FO⇒Functor : (F : ((X : C.Obj) → FreeObject U X)) → Functor C D
  FO⇒Functor F =
    record
      { F₀ = λ X → FX (F X)
      ; F₁ = λ {X} {Y} f → _* (F X) (η (F Y) C.∘ f)
      ; identity = λ {X} → sym (*-uniq (F X) (η (F X) C.∘ C.id) D.id (id-proof {X}))
      ; homomorphism = λ {X} {Y} {Z} {f} {g} →
          sym (*-uniq (F X) (η (F Z) C.∘ (g C.∘ f))
              ((_* (F Y) (η (F Z) C.∘ g)) D.∘ (_* (F X) (η (F Y) C.∘ f)))
              (⟺ (hom-proof {X} {Y} {Z} {f} {g}))
              )
      ; F-resp-≈ = λ {X} {Y} {f} {g} f≈g → sym (*-uniq (F X) (η (F Y) C.∘ f) (_* (F X) (η (F Y) C.∘ g)) (resp-proof  f≈g))
      }
      where
        open C.HomReasoning
        open D.Equiv

        id-proof : ∀ {X : C.Obj} → C [ U.₁ D.id C.∘ η (F X) ≈ η (F X) C.∘ C.id ]
        id-proof {X} = begin
           (U.₁ D.id) C.∘ FX.η         ≈⟨ U.identity ⟩∘⟨refl ⟩
           C.id C.∘ FX.η               ≈⟨ id-comm-sym ⟩
           FX.η C.∘ C.id               ∎
           where
            open MR C
            module FX = FreeObject (F X) using (η)

        hom-proof : ∀ {X : C.Obj} {Y : C.Obj} {Z : C.Obj} {f : C [ X , Y ]} {g : C [ Y , Z ]} →
            C [ (η (F Z) C.∘ (g C.∘ f)) ≈ (U.₁ (_* (F Y) (η (F Z) C.∘ g) D.∘ _* (F X) (η (F Y) C.∘ f) ) C.∘ η (F X)) ]
        hom-proof {X} {Y} {Z} {f} {g} =  begin
          FZ.η C.∘ (g C.∘ f)                                                     ≈˘⟨ pushˡ (FY.*-lift (FZ.η C.∘ g)) ⟩
          (U.₁((FZ.η C.∘ g) FY.*) C.∘ FY.η) C.∘ f                                ≈˘⟨ pushʳ (FX.*-lift (FY.η C.∘ f)) ⟩
          U.₁((FZ.η C.∘ g) FY.*) C.∘ (U.₁((FY.η C.∘ f) FX.*) C.∘ FX.η)           ≈˘⟨ pushˡ U.homomorphism ⟩
          U.₁ ((FZ.η C.∘ g) FY.* D.∘ (FY.η C.∘ f) FX.*) C.∘ FX.η                 ∎
          where
            open MR C
            open C.Equiv
            module FX =  FreeObject (F X) using (η; _*; *-lift)
            module FY =  FreeObject (F Y) using (η; _*; *-lift)
            module FZ =  FreeObject (F Z) using (η)

        resp-proof :{X Y : C.Obj} {f g : C [ X , Y ]} → C [ f ≈ g ] → C [ U.₁ ((F X *) (η (F Y) C.∘ g)) C.∘ η (F X) ≈ η (F Y) C.∘ f ]
        resp-proof {X} {Y} {f} {g} f≈g =  begin
            U.₁((FY.η C.∘ g) FX.*) C.∘ FX.η      ≈⟨ FX.*-lift (FY.η C.∘ g) ⟩
            (FY.η C.∘ g)                         ≈˘⟨ refl⟩∘⟨ f≈g ⟩
            (FY.η C.∘ f)                         ∎
            where
              module FX = FreeObject (F X) using (η; _*; *-lift)
              module FY = FreeObject (F Y) using (η; _*; *-lift)

  FO⇒unit : (F : ((X : C.Obj) → FreeObject U X)) → NaturalTransformation idF (U ∘F FO⇒Functor F)
  FO⇒unit F = ntHelper (record { η = λ X → η (F X) ; commute = λ {X} {Y} f → sym (*-lift (F X) (η (F Y) C.∘ f)) }) where open C.Equiv

  -- define a counit
  FO⇒counit : (F : ((X : C.Obj) → FreeObject U X)) → NaturalTransformation (FO⇒Functor F ∘F U) idF
  FO⇒counit F = ntHelper (record { η = λ X → _* (F (U.₀ X)) C.id ; commute = λ {X} {Y} f → counit-comm {X} {Y} f })
      where
      open D.Equiv
      module F = Functor (FO⇒Functor F) using (₀; ₁; identity; homomorphism)

      counit-comm : {X Y : D.Obj} (f : D [ X , Y ]) → D [ (_* (F (U.₀ Y)) C.id D.∘ F.₁ (U.₁ f)) ≈ (f D.∘ _* (F (U.₀ X)) C.id) ]
        -- proof idea: id* ∘ FU f ≈ (U f)* ≈ f ∘ id* using *-uniq two times

        -- left identity
      counit-comm-left : {X Y : D.Obj} (f : D [ X , Y ]) → C [ U.₁ ((_* (F (U.₀ Y)) C.id) D.∘ (F.₁ (U.₁ f)) ) C.∘ η (F (U.₀ X))  ≈ U.₁ f ]
      counit-comm-left {X} {Y} f =  begin
        U.₁(C.id FUY.* D.∘ F.₁(U.₁ f)) C.∘ FUX.η               ≈⟨ U.homomorphism ⟩∘⟨refl ⟩
        (U.₁ (C.id FUY.*) C.∘ U.₁ (F.₁(U.₁ f))) C.∘ FUX.η      ≈⟨ C.assoc ⟩
        U.₁ (C.id FUY.*) C.∘ (U.₁(F.₁(U.₁ f)) C.∘ FUX.η)       ≈⟨ refl⟩∘⟨ FUX.*-lift (FUY.η C.∘ U.₁ f) ⟩
        U.₁ (C.id FUY.*) C.∘ (FUY.η C.∘ U.₁ f)                 ≈˘⟨ C.assoc ⟩
        (U.₁ (C.id FUY.*) C.∘ FUY.η) C.∘ U.₁ f                 ≈⟨ FUY.*-lift C.id ⟩∘⟨refl ⟩
        C.id C.∘ U.₁ f                                         ≈⟨ C.identityˡ ⟩
        U.₁ f                                                  ∎
          where
            open C.HomReasoning
            module FUX = FreeObject (F (U.₀ X)) using (η; *-lift)
            module FUY = FreeObject (F (U.₀ Y)) using (η; _*; *-lift)

      -- right identity
      counit-comm-right : {X Y : D.Obj} (f : D [ X , Y ]) → C [ U.₁ (f D.∘ (_* (F (U.₀ X)) C.id)) C.∘ η (F (U.₀ X)) ≈ U.₁ f ]
      counit-comm-right {X} {Y} f =  begin
        U.₁ (f D.∘ (C.id FUX.*)) C.∘ FUX.η                ≈⟨ U.homomorphism ⟩∘⟨refl ⟩
        (U.₁ f C.∘ U.₁ (C.id FUX.*)) C.∘ FUX.η            ≈⟨ C.assoc ⟩
        U.₁ f C.∘ (U.₁ (C.id FUX.*) C.∘ FUX.η)            ≈⟨ refl⟩∘⟨ FUX.*-lift C.id ⟩
        U.₁ f C.∘ C.id                                    ≈⟨ C.identityʳ ⟩
        U.₁ f                                             ∎
        where
          open C.HomReasoning
          module FUX = FreeObject (F (U.₀ X)) using (η; _*; *-lift)

      counit-comm {X} {Y} f =  begin
        C.id FUY.* D.∘ F.₁ (U.₁ f)        ≈⟨ FUX.*-uniq (U.₁ f) (C.id FUY.* D.∘ F.₁ (U.₁ f)) (counit-comm-left {X} {Y} f) ⟩
        (U.₁ f) FUX.*                     ≈˘⟨ FUX.*-uniq (U.₁ f) (f D.∘ C.id FUX.*) (counit-comm-right {X} {Y} f) ⟩
        f D.∘ C.id FUX.*                  ∎
        where
          open D.HomReasoning
          module FUX = FreeObject (F (U.₀ X)) using (η; _*; *-lift; *-uniq)
          module FUY = FreeObject (F (U.₀ Y)) using (η; _*; *-lift)

  -- Free object functor is left adjoint to the forgetful functor
  FO⇒LAdj : (F : ((X : C.Obj) → FreeObject U X)) → (FO⇒Functor F) ⊣ U
  FO⇒LAdj F =  record
    { unit = FO⇒unit F
    ; counit = FO⇒counit F
    ; zig = zig
    ; zag = zag
    }
    where
      module F = Functor (FO⇒Functor F) using (₀; ₁; identity; homomorphism)

      zig-comm1 : {X : C.Obj} → C [ U.₁ D.id C.∘ η (F X) ≈ η (F X) ]
      zig-comm1 {X} =  elimˡ (U.identity)  where open MR C

      zig-helper1 : {X : C.Obj} → D [ _* (F X) (η (F X)) ≈ D.id ]
      zig-helper1 {X} =  sym (FX.*-uniq FX.η D.id (zig-comm1 {X}))
        where
          open D.Equiv
          module FX = FreeObject (F X) using (η; *-uniq)

      zig-comm2 : {X : C.Obj} → C [ U.₁ (_* (F (U.₀ (F.₀ X))) C.id D.∘ F.₁ (η (F X)) ) C.∘ η (F X) ≈ η (F X) ]
      zig-comm2 {X} = begin
        U.₁(C.id FUFX.* D.∘ F.₁ FX.η) C.∘ FX.η                   ≈⟨ U.homomorphism ⟩∘⟨refl ⟩
        (U.₁(C.id FUFX.*) C.∘ U.₁(F.₁ FX.η)) C.∘ FX.η            ≈⟨ C.assoc ⟩
        U.₁(C.id FUFX.*) C.∘ (U.₁(F.₁ FX.η) C.∘ FX.η)            ≈˘⟨ refl⟩∘⟨ NaturalTransformation.commute (FO⇒unit F) FX.η ⟩
        U.₁(C.id FUFX.*) C.∘ (FUFX.η C.∘ FX.η)                   ≈˘⟨ C.assoc ⟩
        (U.₁(C.id FUFX.*) C.∘ FUFX.η) C.∘ FX.η                   ≈⟨ FUFX.*-lift C.id ⟩∘⟨refl ⟩
        C.id C.∘ FX.η                                            ≈⟨ C.identityˡ ⟩
        FX.η                                                     ∎
        where
          open C.HomReasoning
          module FX = FreeObject (F X) using (η)
          module FUFX = FreeObject (F (U.₀ (F.₀ X)) ) using (η; _*; *-lift)

      zig-helper2 : {X : C.Obj} → D [ _* (F (U.₀ (F.₀ X))) C.id D.∘ F.₁ (η (F X)) ≈ _* (F X) (η (F X)) ]
      zig-helper2 {X} = FX.*-uniq FX.η (C.id FUFX.* D.∘ F.₁ FX.η) (zig-comm2 {X})
        where
          module FX = FreeObject (F X) using (η; *-uniq)
          module FUFX = FreeObject (F (U.₀ (F.₀ X))) using (η; _*)

      zig : {X : C.Obj} → D [ _* (F (U.₀ (F.₀ X))) C.id D.∘ F.₁ (η (F X)) ≈ D.id ]
      zig {X} = trans zig-helper2 zig-helper1 where open D.Equiv

      zag : {B : D.Obj} → C [ U.₁ (_* (F (U.₀ B)) C.id) C.∘ η (F (U.₀ B)) ≈ C.id ]
      zag {B} = FUB.*-lift C.id
        where module FUB = FreeObject (F (U.₀ B)) using (*-lift)

  -- left adjoints yield free objects
  LAdj⇒FO : (Free : Functor C D) → (Free ⊣ U) → (X : C.Obj) → FreeObject U X
  LAdj⇒FO Free Free⊣U X = record
      { FX = F.₀ X
      ; η = η₁ X
      ; _* =  λ {A : D.Obj} f → ε A D.∘ F.₁ f
      ; *-lift = *-lift'
      ; *-uniq = *-uniq'
      }
      where
        module F = Functor Free using (₀; ₁; identity; homomorphism; F-resp-≈)
        open Adjoint (Free⊣U) using (unit; counit; zig; zag)
        open NaturalTransformation unit renaming (η to η₁; sym-commute to η-sym-commute)
        open NaturalTransformation counit renaming (η to ε; commute to ε-commute)

        *-lift' : {A : D.Obj} (f : C [ X , U.₀ A ]) → C [ U.₁ (ε A D.∘ F.₁ f) C.∘ η₁ X ≈ f ]
        *-lift' {A} f =  begin
          U.₁ (ε A D.∘ F.₁ f) C.∘ η₁ X                ≈⟨ U.homomorphism ⟩∘⟨refl ⟩
          (U.₁ (ε A) C.∘ U.₁ (F.₁ f)) C.∘ η₁ X        ≈⟨ C.assoc ⟩
          U.₁ (ε A) C.∘ (U.₁ (F.₁ f) C.∘ η₁ X)        ≈⟨ refl⟩∘⟨ η-sym-commute f ⟩
          U.₁ (ε A) C.∘ (η₁ (U.₀ A) C.∘ f)            ≈˘⟨ C.assoc ⟩
          (U.₁ (ε A) C.∘ η₁ (U.₀ A)) C.∘ f            ≈⟨ zag ⟩∘⟨refl ⟩
          C.id C.∘ f                                  ≈⟨ C.identityˡ ⟩
          f                                           ∎
          where
            open C.HomReasoning

        *-uniq-sym : {A : D.Obj} (f : C [ X , U.₀ A ]) (g : D [ F.₀ X , A ]) → C [ U.₁ g C.∘ η₁ X ≈ f ] → D [ ε A D.∘ F.₁ f ≈ g ]
        *-uniq-sym {A} f g comm_proof = begin
          ε A D.∘ F.₁ f                               ≈˘⟨ refl⟩∘⟨ F.F-resp-≈ comm_proof ⟩
          ε A D.∘ F.₁ (U.₁ g C.∘ η₁ X)                ≈⟨ refl⟩∘⟨ F.homomorphism ⟩
          ε A D.∘ ( F.₁ (U.₁ g) D.∘ F.₁ (η₁ X) )      ≈˘⟨ D.assoc ⟩
          (ε A D.∘ F.₁ (U.₁ g)) D.∘ F.₁ (η₁ X)        ≈⟨ ε-commute g ⟩∘⟨refl ⟩
          (g D.∘ ε (F.₀ X)) D.∘ F.₁ (η₁ X)            ≈⟨ D.assoc ⟩
          (g D.∘ (ε (F.₀ X) D.∘ F.₁ (η₁ X)))          ≈⟨ refl⟩∘⟨ zig ⟩
          g D.∘ D.id                                  ≈⟨ D.identityʳ ⟩
          g                                           ∎
          where
            open D.HomReasoning

        *-uniq' : {A : D.Obj} (f : C [ X , U.₀ A ]) (g : D [ F.₀ X , A ]) → C [ U.₁ g C.∘ η₁ X ≈ f ] → D [ g ≈ ε A D.∘ F.₁ f ]
        *-uniq' {A} f g comm_proof =  begin
          g                             ≈˘⟨ *-uniq-sym f g comm_proof ⟩
          ε A D.∘ F.₁ f                 ∎
          where
            open D.HomReasoning

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
{- Jesper Cockx, 26-05-2014
   Issue 1023
-}

{-# OPTIONS --cubical-compatible #-}

module TerminationAndUnivalence where

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

J : ∀ {a b} {A : Set a} {x : A} (P : (y : A) → x ≡ y → Set b) →
    (p : P x refl) {y : A} (e : x ≡ y) → P y e
J P p refl = p

data ⊥ : Set where

data WOne : Set where
  wrap : (⊥ → WOne) → WOne

FOne = ⊥ → WOne

f : WOne → FOne
f x ()

g : FOne → WOne
g x = wrap (λ ())

postulate iso : WOne ≡ FOne

noo : (X : Set) → (WOne ≡ X) → X → ⊥
noo .WOne refl (wrap x) = noo FOne iso x

absurd : ⊥
absurd = noo FOne iso (λ ())


text:
{-# OPTIONS --without-K #-}
module Functoriality {a} {A : Set a} where

open import PathOperations
open import Types

ap⁻¹ : ∀ {b} {B : Set b} {x y : A} (f : A → B) (p : x ≡ y) →
  ap f (p ⁻¹) ≡ (ap f p) ⁻¹
ap⁻¹ f = J
  (λ _ _ p → ap f (p ⁻¹) ≡ ap f p ⁻¹)
  (λ _ → refl) _ _

ap· : ∀ {b} {B : Set b} {x y z : A} (f : A → B)
  (p : x ≡ y) (q : y ≡ z) →
  ap f (p · q) ≡ ap f p · ap f q
ap· {z = z} f = J
  (λ _ y p → (q : y ≡ z) → ap f (p · q) ≡ ap f p · ap f q)
  (λ _ _ → refl) _ _

ap-id : {x y : A} (p : x ≡ y) → ap id p ≡ p
ap-id = J (λ _ _ p → ap id p ≡ p) (λ _ → refl) _ _

ap-∘ : ∀ {b c} {B : Set b} {C : Set c} {x y : A}
  (f : B → C) (g : A → B) (p : x ≡ y) →
  ap (f ∘ g) p ≡ ap f (ap g p)
ap-∘ f g = J
  (λ _ _ p → ap (f ∘ g) p ≡ ap f (ap g p))
  (λ _ → refl) _ _

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


text:
-- Given p : A ⟷ B do action on X

act : (A ⟷ B) ⟷ (X ⟷ X)
act = ?

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

module Cubical.Homotopy.Loopspace where

open import Cubical.Core.Everything

open import Cubical.Data.Nat

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.GroupoidLaws
open import Cubical.HITs.SetTruncation
open import Cubical.HITs.Truncation hiding (elim2) renaming (rec to trRec)
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.Function
open import Cubical.Foundations.Path
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.Equiv
open import Cubical.Functions.Morphism
open import Cubical.Data.Sigma
open Iso

{- loop space of a pointed type -}
Ω : {ℓ : Level} → Pointed ℓ → Pointed ℓ
Ω (_ , a) = ((a ≡ a) , refl)

{- n-fold loop space of a pointed type -}
Ω^_ : ∀ {ℓ} → ℕ → Pointed ℓ → Pointed ℓ
(Ω^ 0) p = p
(Ω^ (suc n)) p = Ω ((Ω^ n) p)

{- loop space map -}
Ω→ : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'}
      → (A →∙ B) → (Ω A →∙ Ω B)
fst (Ω→ {A = A} {B = B} (f , p)) q = sym p ∙∙ cong f q ∙∙ p
snd (Ω→ {A = A} {B = B} (f , p)) = ∙∙lCancel p

Ω^→ : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'} (n : ℕ)
  → (A →∙ B) → ((Ω^ n) A →∙ (Ω^ n) B)
Ω^→ zero f = f
Ω^→ (suc n) f = Ω→ (Ω^→ n f)

{- loop space map functoriality (missing pointedness proof) -}
Ω→∘ : ∀ {ℓ ℓ' ℓ''} {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointed ℓ''}
  (g : B →∙ C) (f : A →∙ B)
  → ∀ p → Ω→ (g ∘∙ f) .fst p ≡ (Ω→ g ∘∙ Ω→ f) .fst p
Ω→∘ g f p k i =
  hcomp
    (λ j → λ
      { (i = i0) → compPath-filler' (cong (g .fst) (f .snd)) (g .snd) (~ k) j
      ; (i = i1) → compPath-filler' (cong (g .fst) (f .snd)) (g .snd) (~ k) j
      })
    (g .fst (doubleCompPath-filler (sym (f .snd)) (cong (f .fst) p) (f .snd) k i))

{- Ω→ is a homomorphism -}
Ω→pres∙ : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'} (f : A →∙ B)
        → (p q : typ (Ω A))
        → fst (Ω→ f) (p ∙ q) ≡ fst (Ω→ f) p ∙ fst (Ω→ f) q
Ω→pres∙ f p q i j =
  hcomp
    (λ k → λ
       { (i = i1) →
          (doubleCompPath-filler
            (sym (snd f)) (cong (fst f) p) (snd f) k
         ∙ doubleCompPath-filler
            (sym (snd f)) (cong (fst f) q) (snd f) k) j
       ; (j = i0) → snd f k
       ; (j = i1) → snd f k})
    (cong-∙ (fst f) p q i j)

isEquivΩ→ : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'}
           → (f : (A →∙ B))
           → isEquiv (fst f) → isEquiv (Ω→ f .fst)
isEquivΩ→ {B = (B , b)} =
  uncurry λ f →
    J (λ b y → isEquiv f
             → isEquiv (λ q → (λ i → y (~ i)) ∙∙ (λ i → f (q i)) ∙∙ y))
      λ eqf → subst isEquiv (funExt (rUnit ∘ cong f))
                     (isoToIsEquiv (congIso (equivToIso (f , eqf))))

ΩfunExtIso : ∀ {ℓ ℓ'} (A : Pointed ℓ) (B : Pointed ℓ')
  → Iso (typ (Ω (A →∙ B ∙))) (A →∙ Ω B)
fst (fun (ΩfunExtIso A B) p) x = funExt⁻ (cong fst p) x
snd (fun (ΩfunExtIso A B) p) i j = snd (p j) i
fst (inv (ΩfunExtIso A B) (f , p) i) x = f x i
snd (inv (ΩfunExtIso A B) (f , p) i) j = p j i
rightInv (ΩfunExtIso A B) _ = refl
leftInv (ΩfunExtIso A B) _ = refl

{- Commutativity of loop spaces -}
isComm∙ : ∀ {ℓ} (A : Pointed ℓ) → Type ℓ
isComm∙ A = (p q : typ (Ω A)) → p ∙ q ≡ q ∙ p

private
  mainPath : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ) → (α β : typ ((Ω^ (2 + n)) A))
           → (λ i → α i ∙ refl) ∙ (λ i → refl ∙ β i)
            ≡ (λ i → refl ∙ β i) ∙ (λ i → α i ∙ refl)
  mainPath n α β i = (λ j → α (j ∧ ~ i) ∙ β (j ∧ i)) ∙ λ j → α (~ i ∨ j) ∙ β (i ∨ j)

EH-filler : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ) → typ ((Ω^ (2 + n)) A)
  → typ ((Ω^ (2 + n)) A) → I → I → I → _
EH-filler {A = A} n α β i j z =
  hfill (λ k → λ { (i = i0) → ((cong (λ x → rUnit x (~ k)) α)
                                ∙ cong (λ x → lUnit x (~ k)) β) j
                  ; (i = i1) → ((cong (λ x → lUnit x (~ k)) β)
                                ∙ cong (λ x → rUnit x (~ k)) α) j
                  ; (j = i0) → rUnit refl (~ k)
                  ; (j = i1) → rUnit refl (~ k)})
        (inS (mainPath n α β i j)) z

{- Eckmann-Hilton -}
EH : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ) → isComm∙ ((Ω^ (suc n)) A)
EH {A = A} n α β i j = EH-filler n α β i j i1

{- Lemmas for the syllepsis : EH α β ≡ (EH β α) ⁻¹ -}

EH-refl-refl : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
             → EH {A = A} n refl refl ≡ refl
EH-refl-refl {A = A} n k i j =
  hcomp (λ r → λ { (k = i1) → (refl ∙ (λ _ → basep)) j
                  ; (j = i0) → rUnit basep (~ r ∧ ~ k)
                  ; (j = i1) → rUnit basep (~ r ∧ ~ k)
                  ; (i = i0) → (refl ∙ (λ _ → lUnit basep (~ r ∧ ~ k))) j
                  ; (i = i1) → (refl ∙ (λ _ → lUnit basep (~ r ∧ ~ k))) j})
        (((cong (λ x → rUnit x (~ k)) (λ _ → basep))
         ∙ cong (λ x → lUnit x (~ k)) (λ _ → basep)) j)
  where
  basep = snd (Ω ((Ω^ n) A))

{- Generalisations of EH α β when α or β is refl -}
EH-gen-l : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ) → {x y : typ ((Ω^ (suc n)) A)} (α : x ≡ y)
       → α ∙ refl ≡ refl ∙ α
EH-gen-l {ℓ = ℓ} {A = A} n {x = x} {y = y} α i j z =
  hcomp (λ k → λ { (i = i0) → ((cong (λ x → rUnit x (~ k)) α) ∙ refl) j z
                  ; (i = i1) → (refl ∙ cong (λ x → rUnit x (~ k)) α) j z
                  ; (j = i0) → rUnit (refl {x = x z}) (~ k) z
                  ; (j = i1) → rUnit (refl {x = y z}) (~ k) z
                  ; (z = i0) → x i1
                  ; (z = i1) → y i1})
        (((λ j → α (j ∧ ~ i) ∙ refl) ∙ λ j → α (~ i ∨ j) ∙ refl) j z)

EH-gen-r : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ) → {x y : typ ((Ω^ (suc n)) A)} (β : x ≡ y)
        → refl ∙ β ≡ β ∙ refl
EH-gen-r {A = A} n {x = x} {y = y} β i j z =
  hcomp (λ k → λ { (i = i0) → (refl ∙ cong (λ x → lUnit x (~ k)) β) j z
                  ; (i = i1) → ((cong (λ x → lUnit x (~ k)) β) ∙ refl) j z
                  ; (j = i0) → lUnit (λ k → x (k ∧ z)) (~ k) z
                  ; (j = i1) → lUnit (λ k → y (k ∧ z)) (~ k) z
                  ; (z = i0) → x i1
                  ; (z = i1) → y i1})
        (((λ j → refl ∙ β (j ∧ i)) ∙ λ j → refl ∙ β (i ∨ j)) j z)

{- characterisations of EH α β when α or β is refl  -}
EH-α-refl : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
             → (α : typ ((Ω^ (2 + n)) A))
             → EH n α refl ≡ sym (rUnit α) ∙ lUnit α
EH-α-refl {A = A} n α i j k =
  hcomp (λ r → λ { (i = i0) → EH-gen-l n (λ i → α (i ∧ r)) j k
                  ; (i = i1) → (sym (rUnit λ i → α (i ∧ r)) ∙ lUnit λ i → α (i ∧ r)) j k
                  ; (j = i0) → ((λ i → α (i ∧ r)) ∙ refl) k
                  ; (j = i1) → (refl ∙ (λ i → α (i ∧ r))) k
                  ; (k = i0) → refl
                  ; (k = i1) → α r})
        ((EH-refl-refl n ∙ sym (lCancel (rUnit refl))) i j k)

EH-refl-β : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
             → (β : typ ((Ω^ (2 + n)) A))
             → EH n refl β ≡ sym (lUnit β) ∙ rUnit β
EH-refl-β {A = A} n β i j k =
  hcomp (λ r → λ { (i = i0) → EH-gen-r n (λ i → β (i ∧ r)) j k
                  ; (i = i1) → (sym (lUnit λ i → β (i ∧ r)) ∙ rUnit λ i → β (i ∧ r)) j k
                  ; (j = i0) → (refl ∙ (λ i → β (i ∧ r))) k
                  ; (j = i1) → ((λ i → β (i ∧ r)) ∙ refl) k
                  ; (k = i0) → refl
                  ; (k = i1) → β r})
        ((EH-refl-refl n ∙ sym (lCancel (rUnit refl))) i j k)

syllepsis : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ) (α β : typ ((Ω^ 3) A))
         → EH 0 α β ≡ sym (EH 0 β α)
syllepsis {A = A} n α β k i j =
  hcomp (λ r → λ { (i = i0) → i=i0 r j k
                  ; (i = i1) → i=i1 r j k
                  ; (j = i0) → j-filler r j k
                  ; (j = i1) → j-filler r j k
                  ; (k = i0) → EH-filler 1 α β i j r
                  ; (k = i1) → EH-filler 1 β α (~ i) j r})
        (btm-filler (~ k) i j)
  where
  guy = snd (Ω (Ω A))

  btm-filler : I → I → I → typ (Ω (Ω A))
  btm-filler j i k =
    hcomp (λ r
      → λ {(j = i0) → mainPath 1 β α (~ i) k
          ; (j = i1) → mainPath 1 α β i k
          ; (i = i0) → (cong (λ x → EH-α-refl 0 x r (~ j)) α
                       ∙ cong (λ x → EH-refl-β 0 x r (~ j)) β) k
          ; (i = i1) → (cong (λ x → EH-refl-β 0 x r (~ j)) β
                       ∙ cong (λ x → EH-α-refl 0 x r (~ j)) α) k
          ; (k = i0) → EH-α-refl 0 guy r (~ j)
          ; (k = i1) → EH-α-refl 0 guy r (~ j)})
      (((λ l → EH 0 (α (l ∧ ~ i)) (β (l ∧ i)) (~ j))
       ∙ λ l → EH 0 (α (l ∨ ~ i)) (β (l ∨ i)) (~ j)) k)

  link : I → I → I → _
  link z i j =
    hfill (λ k → λ { (i = i1) → refl
                    ; (j = i0) → rUnit refl (~ i)
                    ; (j = i1) → lUnit guy (~ i ∧ k)})
          (inS (rUnit refl (~ i ∧ ~ j))) z

  i=i1 : I → I → I → typ (Ω (Ω A))
  i=i1 r j k =
    hcomp (λ i → λ { (r = i0) → (cong (λ x → compPath-filler (sym (lUnit x)) (rUnit x) i k) β
                                ∙ cong (λ x → compPath-filler (sym (rUnit x)) (lUnit x) i k) α) j
                    ; (r = i1) → (β ∙ α) j
                    ; (k = i0) → (cong (λ x → lUnit x (~ r)) β ∙
                                   cong (λ x → rUnit x (~ r)) α) j
                    ; (k = i1) → (cong (λ x → rUnit x (~ r ∧ i)) β ∙
                                   cong (λ x → lUnit x (~ r ∧ i)) α) j
                    ; (j = i0) → link i r k
                    ; (j = i1) → link i r k})
          (((cong (λ x → lUnit x (~ r ∧ ~ k)) β
           ∙ cong (λ x → rUnit x (~ r ∧ ~ k)) α)) j)

  i=i0 : I → I → I → typ (Ω (Ω A))
  i=i0 r j k =
    hcomp (λ i → λ { (r = i0) → (cong (λ x → compPath-filler (sym (rUnit x)) (lUnit x) i k) α
                                ∙ cong (λ x → compPath-filler (sym (lUnit x)) (rUnit x) i k) β) j
                    ; (r = i1) → (α ∙ β) j
                    ; (k = i0) → (cong (λ x → rUnit x (~ r)) α ∙
                                   cong (λ x → lUnit x (~ r)) β) j
                    ; (k = i1) → (cong (λ x → lUnit x (~ r ∧ i)) α ∙
                                   cong (λ x → rUnit x (~ r ∧ i)) β) j
                    ; (j = i0) → link i r k
                    ; (j = i1) → link i r k})
          ((cong (λ x → rUnit x (~ r ∧ ~ k)) α
           ∙ cong (λ x → lUnit x (~ r ∧ ~ k)) β) j)

  j-filler : I → I → I → typ (Ω (Ω A))
  j-filler r i k =
    hcomp (λ j → λ { (i = i0) → link j r k
                    ; (i = i1) → link j r k
                    ; (r = i0) → compPath-filler (sym (rUnit guy))
                                                  (lUnit guy) j k
                    ; (r = i1) → refl
                    ; (k = i0) → rUnit guy (~ r)
                    ; (k = i1) → rUnit guy (j ∧ ~ r)})
          (rUnit guy (~ r ∧ ~ k))

------ Ωⁿ⁺¹ A ≃ Ωⁿ(Ω A) ------
flipΩPath : {ℓ : Level} {A : Pointed ℓ} (n : ℕ)
                → ((Ω^ (suc n)) A) ≡ (Ω^ n) (Ω A)
flipΩPath {A = A} zero = refl
flipΩPath {A = A} (suc n) = cong Ω (flipΩPath {A = A} n)

flipΩIso : {ℓ : Level} {A : Pointed ℓ} (n : ℕ)
              → Iso (fst ((Ω^ (suc n)) A)) (fst ((Ω^ n) (Ω A)))
flipΩIso {A = A} n = pathToIso (cong fst (flipΩPath n))

flipΩIso⁻pres· : {ℓ : Level} {A : Pointed ℓ} (n : ℕ)
                      → (f g : fst ((Ω^ (suc n)) (Ω A)))
                      → inv (flipΩIso (suc n)) (f ∙ g)
                      ≡ (inv (flipΩIso (suc n)) f)
                      ∙ (inv (flipΩIso (suc n)) g)
flipΩIso⁻pres· {A = A} n f g i =
    transp (λ j → flipΩPath {A = A} n (~ i ∧ ~ j) .snd
                 ≡ flipΩPath n (~ i ∧ ~ j) .snd) i
                  (transp (λ j → flipΩPath {A = A} n (~ i ∨ ~ j) .snd
                 ≡ flipΩPath n (~ i ∨ ~ j) .snd) (~ i) f
                 ∙ transp (λ j → flipΩPath {A = A} n (~ i ∨ ~ j) .snd
                 ≡ flipΩPath n (~ i ∨ ~ j) .snd) (~ i) g)

flipΩIsopres· : {ℓ : Level} {A : Pointed ℓ} (n : ℕ)
                      → (f g : fst (Ω ((Ω^ (suc n)) A)))
                      → fun (flipΩIso (suc n)) (f ∙ g)
                      ≡ (fun (flipΩIso (suc n)) f)
                      ∙ (fun (flipΩIso (suc n)) g)
flipΩIsopres· n =
  morphLemmas.isMorphInv _∙_ _∙_
    (inv (flipΩIso (suc n)))
    (flipΩIso⁻pres· n)
    (fun (flipΩIso (suc n)))
    (Iso.leftInv (flipΩIso (suc n)))
    (Iso.rightInv (flipΩIso (suc n)))

flipΩrefl : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
  → fun (flipΩIso {A = A} (suc n)) refl ≡ refl
flipΩrefl {A = A} n j =
  transp (λ i₁ → fst (Ω (flipΩPath {A = A} n ((i₁ ∨ j)))))
         j (snd (Ω (flipΩPath n j)))

---- Misc. ----

isCommA→isCommTrunc : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ) → isComm∙ A
                    → isOfHLevel (suc n) (typ A)
                    → isComm∙ (∥ typ A ∥ (suc n) , ∣ pt A ∣)
isCommA→isCommTrunc {A = (A , a)} n comm hlev p q =
    ((λ i j → (leftInv (truncIdempotentIso (suc n) hlev) ((p ∙ q) j) (~ i)))
 ∙∙ (λ i → cong {B = λ _ → ∥ A ∥ (suc n) } (λ x → ∣ x ∣)
                 (cong (trRec hlev (λ x → x)) (p ∙ q)))
 ∙∙ (λ i → cong {B = λ _ → ∥ A ∥ (suc n) } (λ x → ∣ x ∣)
                 (congFunct {A = ∥ A ∥ (suc n)} {B = A} (trRec hlev (λ x → x)) p q i)))
 ∙ ((λ i → cong {B = λ _ → ∥ A ∥ (suc n) } (λ x → ∣ x ∣)
                 (comm (cong (trRec hlev (λ x → x)) p) (cong (trRec hlev (λ x → x)) q) i))
 ∙∙ (λ i → cong {B = λ _ → ∥ A ∥ (suc n) } (λ x → ∣ x ∣)
                 (congFunct {A = ∥ A ∥ (suc n)} {B = A} (trRec hlev (λ x → x)) q p (~ i)))
 ∙∙ (λ i j → (leftInv (truncIdempotentIso (suc n) hlev) ((q ∙ p) j) i)))

ptdIso→comm : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Type ℓ'} (e : Iso (typ A) B)
  → isComm∙ A → isComm∙ (B , fun e (pt A))
ptdIso→comm {A = (A , a)} {B = B} e comm p q =
       sym (rightInv (congIso e) (p ∙ q))
    ∙∙ (cong (fun (congIso e)) ((invCongFunct e p q)
                            ∙∙ (comm (inv (congIso e) p) (inv (congIso e) q))
                            ∙∙ (sym (invCongFunct e q p))))
    ∙∙ rightInv (congIso e) (q ∙ p)

{- Homotopy group version -}
π-comp : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ) → ∥ typ ((Ω^ (suc n)) A) ∥₂
      → ∥ typ ((Ω^ (suc n)) A) ∥₂ → ∥ typ ((Ω^ (suc n)) A) ∥₂
π-comp n = elim2 (λ _ _ → isSetSetTrunc) λ p q → ∣ p ∙ q ∣₂

EH-π : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ) (p q : ∥ typ ((Ω^ (2 + n)) A) ∥₂)
               → π-comp (1 + n) p q ≡ π-comp (1 + n) q p
EH-π  n = elim2 (λ x y → isOfHLevelPath 2 isSetSetTrunc _ _)
                             λ p q → cong ∣_∣₂ (EH n p q)

max_stars_repo_name: rnarkk/cubical

max_issues_repo_name: rnarkk/cubical

max_forks_repo_name: rnarkk/cubical


text:
module Serializer.Vec where

open import Data.Fin hiding (_+_)
open import Data.Nat
open import Data.Vec
open import Function using (_∘_ ; _$_ ; _∋_ ; id ; const)
open import Function.Bijection
open import Function.Injection
open import Function.Surjection
open import Function.Equality using (_⟶_ ;  _⟨$⟩_ ; Π )
open import Function.LeftInverse hiding (_∘_)
open import Relation.Binary
open import Relation.Binary.EqReasoning
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; cong ; setoid )
import Relation.Binary.Indexed as I

open import Serializer
open import Helper.Fin

open Serializer.Serializer {{...}}

-----------------------------------
-- Generic instance for Vec
-----------------------------------

2^ : ℕ -> ℕ
2^ zero = 1
2^ (suc b) = 2 * 2^ b

-- inverted exponent
_^_ : ℕ -> ℕ -> ℕ
zero ^ a = 1
suc b ^ a = a * (b ^ a)

fromVec : ∀ {n} {A : Set} -> {{t : Serializer A}} -> Vec A n -> Fin (n ^ (size {A}))
fromVec {zero} [] = zero
fromVec {suc n} {a} (x ∷ v) = × (size {a}) (n ^ (size {a})) (from x) (fromVec v)

toVec` : ∀ {n} {A : Set} -> {{t : Serializer A}} -> Fin (n ^ (size {A})) -> Vec A n
toVec` {zero} x = []
toVec` {suc n} {a} {{t}} x with Serializer.to t | toVec` {n} {a} {{t}}
... | to1 | to2 with Serializer.size t
... | s with ⨂ s (n ^ s) x
toVec` {suc n} .(× s (n ^ s) i j) | to1 | to2 | s | is× i j = to1 i ∷ to2 j

vec-from-cong : ∀ {n} {A : Set} -> {{t : Serializer A}} -> Setoid._≈_ (setoid (Vec A n)) I.=[ fromVec ]⇒ Setoid._≈_ (setoid (Fin (n ^ (size {A}))))
vec-from-cong refl = refl

vec-from-preserves-eq : ∀ {n} {A : Set} -> {{t : Serializer A}} -> setoid (Vec A n) ⟶ setoid (Fin (n ^ (size {A})))
vec-from-preserves-eq = record { _⟨$⟩_ = fromVec ; cong = vec-from-cong }

vec-from-injective : ∀ {n} {A : Set} -> {{t : Serializer A}} -> Injective (vec-from-preserves-eq {n} {A} {{t}})
vec-from-injective {zero} {a} {{t}} {x = []} {[]} x₁ with fromVec {A = a} {{t}} []
... | p1 = refl
vec-from-injective {suc n} {a} {{t}} {x ∷ x₁} {y ∷ y₁} p  with (⨂ (Serializer.size t) (n ^ (Serializer.size t)) (fromVec (x ∷ x₁))) | (⨂ (Serializer.size t) (n ^ (Serializer.size t)) (fromVec (y ∷ y₁)))
... | a1 | b2 with vec-from-injective {n} {_} {{t}} {x₁} {y₁}
... | c with c (×-equal₁ {x₁ = (Serializer.from t x)} {x₂ = (Serializer.from t y)} p) | (×-equal₂ {x₁ = (Serializer.from t x)} {x₂ = (Serializer.from t y)} p)
... | p1 | p2 with Serializer.from t
... | la = ?

--(Injection.injective (Serializer.injection t))

{-
vec-from-injective : ∀ {n} -> Injective (vec-from-preserves-eq {n})
vec-from-injective {zero} {[]} {[]} p with fromVec []
... | p2 = refl
vec-from-injective {suc n} {x ∷ x₁} {y ∷ y₁} p with (⨂ 2 (2^ n) (fromVec (x ∷ x₁))) | (⨂ 2 (2^ n) (fromVec (y ∷ y₁)))
... | a1 | b2 with vec-from-injective {n} {x₁} {y₁}
... | c with c (×-equal₁ {x₁ = (fromBool x)} {x₂ = (fromBool y)} p) | (×-equal₂ {x₁ = (fromBool x)} {x₂ = (fromBool y)} p)
... | p1 | p2 with from-bool-injective p2
vec-from-injective {suc n} {x ∷ x₁} {.x ∷ .x₁} p | a1 | b2 | c | refl | p2 | refl = refl

-}

vec-from-surjective : ∀ {n} {A : Set} -> {{t : Serializer A}} -> Surjective (vec-from-preserves-eq {n} {A} {{t}})
vec-from-surjective {n} {a} {{t}} = record { from = preserves-eq-inv ; right-inverse-of = (inv {n} {a} {{t}}) }
  where
    cong-inverse : ∀ {n} {A : Set} -> {{t : Serializer A}} -> Setoid._≈_ (setoid (Fin (n ^ (size {A})))) I.=[ toVec` ]⇒ Setoid._≈_ (setoid (Vec A n))
    cong-inverse refl = refl

    preserves-eq-inv : ∀ {n} {A : Set} -> {{t : Serializer A}} -> setoid (Fin (n ^ (size {A}))) ⟶ setoid (Vec A n)
    preserves-eq-inv = record { _⟨$⟩_ = toVec` ; cong = cong-inverse }

    inv : ∀ {n} {A : Set} -> {{t : Serializer A}} -> (preserves-eq-inv {n} {A} {{t}}) RightInverseOf (vec-from-preserves-eq {n} {A} {{t}})
    inv {zero} zero = refl
    inv {zero} (suc ())
    inv {suc n₁} {a} {{t}} x with ⨂ (Serializer.size t) (n₁ ^ (Serializer.size t)) x
    inv {suc n₁} {a} {{t}} ._ | is× i j with (Surjective.right-inverse-of (Bijective.surjective (Bijection.bijective (Serializer.bijection t)))) i
    ... | ple = {!!}
--      rewrite  (inv {n₁} {a} {{t}} j)
--      ... | ple = ?

--    ... | moo with (inv {n₁} {a} {{t}} j)
--    ... | moo1 = refl --  {!!}
{-
    inv {suc n₁} ._ | is× i j with  (Surjective.right-inverse-of (Bijective.surjective (Bijection.bijective (Serializer.bijection t))))
    ... | moo = {!!}-}

--      rewrite (Surjective.right-inverse-of (Bijective.surjective (Bijection.bijective (Serializer.bijection t)))) i | (inv {n₁} j) = refl

{-
vec-from-surjective : ∀ {n} -> Surjective (vec-from-preserves-eq {n})
vec-from-surjective {n} = record { from = preserves-eq-inv ; right-inverse-of = (inv {n}) }
  where
    cong-inverse : ∀ {n} -> Setoid._≈_ (setoid (Fin (2^ n))) I.=[ toVec` ]⇒ Setoid._≈_ (setoid (Vec Bool n))
    cong-inverse refl = refl

    preserves-eq-inv : ∀ {n} -> setoid (Fin  (2^ n)) ⟶ setoid (Vec Bool n)
    preserves-eq-inv = record { _⟨$⟩_ = toVec` ; cong = cong-inverse }

    inv : ∀ {n} -> (preserves-eq-inv {n}) RightInverseOf (vec-from-preserves-eq {n})
    inv {zero} zero = refl
    inv {zero} (suc ())
    inv {suc n₁} x with ⨂ 2 (2^ n₁) x
    inv {suc n₁} .(× 2 (2^ n₁) i j) | is× i j
      rewrite (Surjective.right-inverse-of (Bijective.surjective (Bijection.bijective (bijection {Bool})))) i | (inv {n₁} j) = refl
-}

max_stars_repo_name: mathijsb/generic-in-agda

max_issues_repo_name: mathijsb/generic-in-agda

max_forks_repo_name: mathijsb/generic-in-agda


text:
open import Data.List using ( [] )
open import Data.Product using ( proj₁ ; proj₂ )
open import Data.Sum using ( _⊎_ ; inj₁ ; inj₂ )
open import Relation.Binary.PropositionalEquality using ( refl )
open import Web.Semantic.DL.ABox.Interp using ( ⌊_⌋ ; ind ; _*_ )
open import Web.Semantic.DL.ABox.Interp.Morphism using ( _,_ )
open import Web.Semantic.DL.ABox.Model using
  ( _⊨a_ ; on-bnode ; bnodes ; _,_ ; ⊨a-resp-≲ )
open import Web.Semantic.DL.Category.Composition using ( _∙_ )
open import Web.Semantic.DL.Category.Properties.Composition.Assoc using
  ( compose-assoc )
open import Web.Semantic.DL.Category.Properties.Composition.Lemmas using
  ( compose-left ; compose-right ; compose-resp-⊨a )
open import Web.Semantic.DL.Category.Properties.Composition.RespectsEquiv using
  ( compose-resp-≣ )
open import Web.Semantic.DL.Category.Properties.Equivalence using
  ( ≣-refl ; ≣-sym ; ≣-trans )
open import Web.Semantic.DL.Category.Properties.Tensor.Coherence using
  ( symm-unit )
open import Web.Semantic.DL.Category.Properties.Tensor.Lemmas using
  ( tensor-up ; tensor-down ; tensor-resp-⊨a )
open import Web.Semantic.DL.Category.Properties.Tensor.SymmNatural using
  ( symm-natural )
open import Web.Semantic.DL.Category.Object using ( Object ; IN ; fin )
open import Web.Semantic.DL.Category.Morphism using
  ( _⇒_ ; BN ; impl ; _⊑_ ; _≣_ ; _,_ )
open import Web.Semantic.DL.Category.Tensor using ( _⟨⊗⟩_ )
open import Web.Semantic.DL.Category.Unit using ( I )
open import Web.Semantic.DL.Category.Wiring using
  ( wires-≈ ; wires-≈⁻¹ ; identity ; unit₁ ; unit₂ ; symm )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using ( TBox )
open import Web.Semantic.DL.TBox.Interp using ( Δ ; _⊨_≈_ ; ≈-refl ; ≈-sym )
open import Web.Semantic.DL.TBox.Interp.Morphism using ( ≲-refl )
open import Web.Semantic.Util using
  ( _∘_ ; False ; _⊕_⊕_ ; inode ; bnode ; enode ; left ; right ; up ; down )

module Web.Semantic.DL.Category.Properties.Tensor.UnitNatural
  {Σ : Signature} {S T : TBox Σ} where

unit₁-natural : ∀ {A B : Object S T} (F : A ⇒ B) →
  ((identity I ⟨⊗⟩ F) ∙ unit₁ B ≣ unit₁ A ∙ F)
unit₁-natural {A} {B} F = (LHS⊑RHS , RHS⊑LHS) where

  LHS⊑RHS : ((identity I ⟨⊗⟩ F) ∙ unit₁ B ⊑ unit₁ A ∙ F)
  LHS⊑RHS J J⊨STA J⊨LHS = (f , J⊨RHS) where

    f : False ⊕ IN A ⊕ BN F → Δ ⌊ J ⌋
    f (inode ())
    f (bnode x) = ind J (inode (inj₂ x))
    f (enode v) = ind J (bnode (inode (inj₂ v)))

    f✓ : ∀ x → ⌊ J ⌋ ⊨ ind J (left (down x)) ≈ on-bnode f (ind J) (right x)
    f✓ (inode x) = ≈-refl ⌊ J ⌋
    f✓ (bnode v) = ≈-refl ⌊ J ⌋
    f✓ (enode y) = wires-≈ inj₂ (proj₂ (fin B) y)
      (compose-right (identity I ⟨⊗⟩ F) (unit₁ B) J J⊨LHS)

    J⊨RHS : bnodes J f ⊨a impl (unit₁ A ∙ F)
    J⊨RHS = compose-resp-⊨a (unit₁ A) F (bnodes J f)
      (wires-≈⁻¹ inj₂ (λ x → ≈-refl ⌊ J ⌋) (proj₁ (fin A)))
      (⊨a-resp-≲ (≲-refl ⌊ J ⌋ , f✓) (impl F)
        (tensor-down (identity I) F (left * J)
          (compose-left (identity I ⟨⊗⟩ F) (unit₁ B) J J⊨LHS)))

  RHS⊑LHS : (unit₁ A ∙ F ⊑ (identity I ⟨⊗⟩ F) ∙ unit₁ B)
  RHS⊑LHS J J⊨STA J⊨RHS = (f , J⊨LHS) where

    f : ((False ⊎ BN F) ⊕ (False ⊎ IN B) ⊕ False) → Δ ⌊ J ⌋
    f (inode (inj₁ ()))
    f (inode (inj₂ v)) = ind J (bnode (enode v))
    f (bnode (inj₁ ()))
    f (bnode (inj₂ y)) = ind J (enode y)
    f (enode ())

    f✓ : ∀ x → ⌊ J ⌋ ⊨ ind J (right x) ≈ on-bnode f (ind J) (left (down x))
    f✓ (inode x) = ≈-sym ⌊ J ⌋ (wires-≈ inj₂ (proj₂ (fin A) x) (compose-left (unit₁ A) F J J⊨RHS))
    f✓ (bnode v) = ≈-refl ⌊ J ⌋
    f✓ (enode y) = ≈-refl ⌊ J ⌋

    J⊨LHS : bnodes J f ⊨a impl ((identity I ⟨⊗⟩ F) ∙ unit₁ B)
    J⊨LHS = compose-resp-⊨a (identity I ⟨⊗⟩ F) (unit₁ B) (bnodes J f)
      (tensor-resp-⊨a (identity I) F (left * bnodes J f)
        (wires-≈⁻¹ {I = up * left * bnodes J f} (λ ()) (λ ()) [])
        (⊨a-resp-≲ (≲-refl ⌊ J ⌋ , f✓) (impl F)
          (compose-right (unit₁ A) F J J⊨RHS)))
      (wires-≈⁻¹ inj₂ (λ x → ≈-refl ⌊ J ⌋) (proj₁ (fin B)))

unit₂-natural : ∀ {A B : Object S T} (F : A ⇒ B) →
  ((F ⟨⊗⟩ identity I) ∙ unit₂ B ≣ unit₂ A ∙ F)
unit₂-natural {A} {B} F =
  ≣-trans
    (compose-resp-≣ (≣-refl (F ⟨⊗⟩ identity I)) (≣-sym (symm-unit B)))
  (≣-trans
    (≣-sym (compose-assoc (F ⟨⊗⟩ identity I) (symm B I) (unit₁ B)))
  (≣-trans
    (compose-resp-≣ (symm-natural F (identity I)) (≣-refl (unit₁ B)))
  (≣-trans
    (compose-assoc (symm A I) (identity I ⟨⊗⟩ F) (unit₁ B))
  (≣-trans
    (compose-resp-≣ (≣-refl (symm A I)) (unit₁-natural F))
  (≣-trans
    (≣-sym (compose-assoc (symm A I) (unit₁ A) F))
    (compose-resp-≣ (symm-unit A) (≣-refl F)))))))

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: agda/agda-web-semantic

max_forks_repo_name: agda/agda-web-semantic


text:
module PiFrac where

open import Level
open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product

infixr 20 _◎_

data <_> {A : Set} : A → Set where
  singleton : (x : A) -> < x >

mutual

  data B : Set₁ where
    ZERO  : B
    ONE   : B
    PLUS  : B → B → B
    TIMES : B → B → B
    SING  : (b : B) → ⟦ b ⟧ → B
    RECIP : (b : B) → ⟦ b ⟧ → B
    DPAIR : (b : B) → (⟦ b ⟧ → B) → B

  ⟦_⟧ : B → Set
  ⟦ ZERO ⟧         = ⊥
  ⟦ ONE ⟧          = ⊤
  ⟦ PLUS b₁ b₂ ⟧   = ⟦ b₁ ⟧ ⊎ ⟦ b₂ ⟧
  ⟦ TIMES b₁ b₂ ⟧  = ⟦ b₁ ⟧ × ⟦ b₂ ⟧
  ⟦ SING b v ⟧  = <_> {⟦ b ⟧} v
  ⟦ RECIP b v ⟧      = <_> {⟦ b ⟧} v → ⊤
  ⟦ DPAIR b c ⟧ = Σ ⟦ b ⟧ (λ v → ⟦ c v ⟧)

data _⟷_ : B → B → Set₁ where
  unite₊ : {b : B} → PLUS ZERO b ⟷ b
  uniti₊ : {b : B} → b ⟷ PLUS ZERO b
  swap₊ : {b₁ b₂ : B} → PLUS b₁ b₂ ⟷ PLUS b₂ b₁
  assocl₊ : { b₁ b₂ b₃ : B } → PLUS b₁ (PLUS b₂ b₃) ⟷ PLUS (PLUS b₁ b₂) b₃
  assocr₊ : { b₁ b₂ b₃ : B } → PLUS (PLUS b₁ b₂) b₃ ⟷ PLUS b₁ (PLUS b₂ b₃)
  unite⋆  : { b : B } → TIMES ONE b ⟷ b
  uniti⋆  : { b : B } → b ⟷ TIMES ONE b
  swap⋆ : {b₁ b₂ : B} → TIMES b₁ b₂ ⟷ TIMES b₂ b₁
  assocl⋆ : { b₁ b₂ b₃ : B } → TIMES b₁ (TIMES b₂ b₃) ⟷ TIMES (TIMES b₁ b₂) b₃
  assocr⋆ : { b₁ b₂ b₃ : B } → TIMES (TIMES b₁ b₂) b₃ ⟷ TIMES b₁ (TIMES b₂ b₃)
  id⟷ : {b : B } → b ⟷ b
  sym    : { b₁ b₂ : B } → (b₁ ⟷ b₂) → (b₂ ⟷ b₁)
  _◎_    : { b₁ b₂ b₃ : B } → (b₁ ⟷ b₂) → (b₂ ⟷ b₃) → (b₁ ⟷ b₃)
  _⊕_    : { b₁ b₂ b₃ b₄ : B } →
           (b₁ ⟷ b₃) → (b₂ ⟷ b₄) → (PLUS b₁ b₂ ⟷ PLUS b₃ b₄)
  _⊗_    : { b₁ b₂ b₃ b₄ : B } →
           (b₁ ⟷ b₃) → (b₂ ⟷ b₄) → (TIMES b₁ b₂ ⟷ TIMES b₃ b₄)
  η : {b : B} → ONE ⟷ DPAIR b (λ v → RECIP b v)
  ε : {b : B} → DPAIR b (λ v → RECIP b v) ⟷ ONE

mutual
  eval : {b₁ b₂ : B} → (c : b₁ ⟷ b₂) → ⟦ b₁ ⟧ → ⟦ b₂ ⟧
  eval unite₊ (inj₁ ())
  eval unite₊ (inj₂ v) = v
  eval uniti₊ v = inj₂ v
  eval swap₊ (inj₁ x) = inj₂ x
  eval swap₊ (inj₂ y) = inj₁ y
  eval assocl₊ (inj₁ x) = inj₁ (inj₁ x)
  eval assocl₊ (inj₂ (inj₁ x)) = inj₁ (inj₂ x)
  eval assocl₊ (inj₂ (inj₂ x)) = inj₂ x
  eval assocr₊ (inj₁ (inj₁ x)) = inj₁ x
  eval assocr₊ (inj₁ (inj₂ y)) = inj₂ (inj₁ y)
  eval assocr₊ (inj₂ y) = inj₂ (inj₂ y)
  eval unite⋆ (tt , x) = x
  eval uniti⋆ v = ( tt , v)
  eval swap⋆ (v₁ , v₂) = (v₂ , v₁)
  eval assocl⋆ (x , (y , z)) = ((x , y), z)
  eval assocr⋆ ((x , y), z) = (x , (y , z))
  eval id⟷ v = v
  eval (sym c) v = evalB c v
  eval (c₁ ◎ c₂) v = eval c₂ (eval c₁ v)
  eval (c₁ ⊕ c₂) (inj₁ x) = inj₁ (eval c₁ x)
  eval (c₁ ⊕ c₂) (inj₂ y) = inj₂ (eval c₂ y)
  eval (c₁ ⊗ c₂) (x , y) = (eval c₁ x , eval c₂ y)
  eval (η {b}) tt = {!!}
  eval (ε {b}) (w , c) = c (singleton w)

  evalB :  {b₁ b₂ : B} → (c : b₁ ⟷ b₂) → ⟦ b₂ ⟧ → ⟦ b₁ ⟧
  evalB uniti₊ (inj₁ ())
  evalB uniti₊ (inj₂ v) = v
  evalB unite₊ v = inj₂ v
  evalB swap₊ (inj₁ x) = inj₂ x
  evalB swap₊ (inj₂ y) = inj₁ y
  evalB assocr₊ (inj₁ x) = inj₁ (inj₁ x)
  evalB assocr₊ (inj₂ (inj₁ x)) = inj₁ (inj₂ x)
  evalB assocr₊ (inj₂ (inj₂ x)) = inj₂ x
  evalB assocl₊ (inj₁ (inj₁ x)) = inj₁ x
  evalB assocl₊ (inj₁ (inj₂ y)) = inj₂ (inj₁ y)
  evalB assocl₊ (inj₂ y) = inj₂ (inj₂ y)
  evalB uniti⋆ (tt , x) = x
  evalB unite⋆ v = ( tt , v)
  evalB swap⋆ (v₁ , v₂) = (v₂ , v₁)
  evalB assocr⋆ (x , (y , z)) = ((x , y), z)
  evalB assocl⋆ ((x , y), z) = (x , (y , z))
  evalB id⟷ v = v
  evalB (sym c) v = eval c v
  evalB (c₁ ◎ c₂) v = evalB c₁ (evalB c₂ v)
  evalB (c₁ ⊕ c₂) (inj₁ x) = inj₁ (evalB c₁ x)
  evalB (c₁ ⊕ c₂) (inj₂ y) = inj₂ (evalB c₂ y)
  evalB (c₁ ⊗ c₂) (x , y) = (evalB c₁ x , evalB c₂ y)
  evalB (η {b}) (w , c) = c (singleton w)
  evalB (ε {b}) tt = {!!}

 -- this is better in that one can't use inj₂ tt on the rhs
-- the overly precise version doesn't type check, don't know why
test : ⊤
test = eval (ε {PLUS ONE ONE}) (inj₁ tt , f)
  where f : < inj₁ {B = ⊤} tt > → ⊤
--      f (singleton (inj₁ {B = ⊤} tt)) = tt
        f x = tt
{-
mutual
  data B : Set where
    ONE   : B
    PLUS  : B → B → B
    TIMES : B → B → B
    MATCH : {b : B} → Singleton b → B
    DPAIR : {b : B} → (Σ (BV b) Singleton) → B

mutual
  eval : {b₁ b₂ : B} → b₁ ⟷ b₂ → BV b₁ → BV b₂
  eval swap₊ (LEFT v) = RIGHT v
  eval swap₊ (RIGHT v) = LEFT v
  eval (η {b₁} {v}) UNIT = NCPROD b₁ v
  eval assocl₊ (LEFT v) = LEFT (LEFT v)
  eval assocl₊ (RIGHT (LEFT v)) = LEFT (RIGHT v)
  eval assocl₊ (RIGHT (RIGHT v)) = RIGHT v
  eval assocr₊ (LEFT (LEFT v)) = LEFT v
  eval assocr₊ (LEFT (RIGHT v)) = RIGHT (LEFT v)
  eval assocr₊ (RIGHT v) = RIGHT (RIGHT v)
  eval unite⋆ (PAIR UNIT v) = v
  eval uniti⋆ v = PAIR UNIT v
  eval (ε {b₁} {v}) (NCPROD .b₁ .v) = UNIT
  eval id⟷ v = v
  eval (c₁ ◎ c₂) v = eval c₂ (eval c₁ v)
  eval (c₁ ⊕ c₂) (LEFT v) = LEFT (eval c₁ v)
  eval (c₁ ⊕ c₂) (RIGHT v) = RIGHT (eval c₂ v)
  eval (c₁ ⊗ c₂) (PAIR v₁ v₂) = PAIR (eval c₁ v₁) (eval c₂ v₂)
  eval (lift {b₁} {b₂} {v} c) (NCPROD .b₁ .v) = NCPROD b₂ (eval c v)

-- name : {b₁ b₂ : B} {v : BV b₁} → (b₁ ⟷ b₂) → (ONE ⟷ DPAIR (v , singleton v))
-- name {b₁} {b₂} {v} c = η {b₁} {v} ◎ (lift (id⟷ ⊗ c))

--}

--------------------------------------------------------------------------------
-- Jacques's code

{--

data Singleton {A : Set} : A → Set where
  singleton : (x : A) -> Singleton x

mutual
  data B : Set where
    ONE   : B
    PLUS  : B → B → B
    TIMES : B → B → B
    MATCH : {b : B} → Singleton b → B
    DPAIR : {b : B} → (Σ (BV b) Singleton) → B

  data BV : B → Set where
    UNIT : BV ONE
    LEFT : {b₁ b₂ : B} → BV b₁ → BV (PLUS b₁ b₂)
    RIGHT : {b₁ b₂ : B} → BV b₂ → BV (PLUS b₁ b₂)
    PAIR : {b₁ b₂ : B} → BV b₁ → BV b₂ → BV (TIMES b₁ b₂)
    SINGLE : {b₁ : B} → BV b₁ → BV (MATCH {b₁} (singleton b₁))
    NCPROD : (b₁ : B) →  (v : BV b₁) → BV (DPAIR (v , (singleton v)))

mutual
  data _⟷_ : B → B → Set where
    swap₊ : {b₁ b₂ : B} → PLUS b₁ b₂ ⟷ PLUS b₂ b₁
    assocl₊ : { b₁ b₂ b₃ : B } → PLUS b₁ (PLUS b₂ b₃) ⟷ PLUS (PLUS b₁ b₂) b₃
    assocr₊ : { b₁ b₂ b₃ : B } → PLUS (PLUS b₁ b₂) b₃ ⟷ PLUS b₁ (PLUS b₂ b₃)
    unite⋆  : { b : B } → TIMES ONE b ⟷ b
    uniti⋆  : { b : B } → b ⟷ TIMES ONE b
    η : {b₁ : B} {v : BV b₁} → ONE ⟷ DPAIR (v , (singleton v))
    ε : {b₁ : B} {v : BV b₁} → DPAIR (v , (singleton v)) ⟷ ONE
    id⟷ : {b : B } → b ⟷ b
-- closure combinators
--   sym    : { b₁ b₂ : B } → (b₁ ⟷ b₂) → (b₂ ⟷ b₁)
    _◎_    : { b₁ b₂ b₃ : B } → (b₁ ⟷ b₂) → (b₂ ⟷ b₃) → (b₁ ⟷ b₃)
    _⊕_    : { b₁ b₂ b₃ b₄ : B } →
             (b₁ ⟷ b₃) → (b₂ ⟷ b₄) → (PLUS b₁ b₂ ⟷ PLUS b₃ b₄)
    _⊗_    : { b₁ b₂ b₃ b₄ : B } →
             (b₁ ⟷ b₃) → (b₂ ⟷ b₄) → (TIMES b₁ b₂ ⟷ TIMES b₃ b₄)
--   refe⋆  : { b : BF } → RECIP (RECIP b) ⟺ b
--   refi⋆  : { b : BF } → b ⟺ RECIP (RECIP b)
--   rile⋆  : { b : BF } → TIMESF b (TIMESF b (RECIP b)) ⟺ b
--   rili⋆  : { b : BF } → b ⟺ TIMESF b (TIMESF b (RECIP b))
    lift : {b₁ b₂ : B} {v : BV b₁} → (c : b₁ ⟷ b₂) →
      DPAIR (v , (singleton v)) ⟷ DPAIR (eval c v , (singleton (eval c v)))

  eval : {b₁ b₂ : B} → b₁ ⟷ b₂ → BV b₁ → BV b₂
  eval swap₊ (LEFT v) = RIGHT v
  eval swap₊ (RIGHT v) = LEFT v
  eval (η {b₁} {v}) UNIT = NCPROD b₁ v
  eval assocl₊ (LEFT v) = LEFT (LEFT v)
  eval assocl₊ (RIGHT (LEFT v)) = LEFT (RIGHT v)
  eval assocl₊ (RIGHT (RIGHT v)) = RIGHT v
  eval assocr₊ (LEFT (LEFT v)) = LEFT v
  eval assocr₊ (LEFT (RIGHT v)) = RIGHT (LEFT v)
  eval assocr₊ (RIGHT v) = RIGHT (RIGHT v)
  eval unite⋆ (PAIR UNIT v) = v
  eval uniti⋆ v = PAIR UNIT v
  eval (ε {b₁} {v}) (NCPROD .b₁ .v) = UNIT
  eval id⟷ v = v
  eval (c₁ ◎ c₂) v = eval c₂ (eval c₁ v)
  eval (c₁ ⊕ c₂) (LEFT v) = LEFT (eval c₁ v)
  eval (c₁ ⊕ c₂) (RIGHT v) = RIGHT (eval c₂ v)
  eval (c₁ ⊗ c₂) (PAIR v₁ v₂) = PAIR (eval c₁ v₁) (eval c₂ v₂)
  eval (lift {b₁} {b₂} {v} c) (NCPROD .b₁ .v) = NCPROD b₂ (eval c v)

-- name : {b₁ b₂ : B} {v : BV b₁} → (b₁ ⟷ b₂) → (ONE ⟷ DPAIR (v , singleton v))
-- name {b₁} {b₂} {v} c = η {b₁} {v} ◎ (lift (id⟷ ⊗ c))

--}


text:
T-to-≡ : ∀ {x} → T x → x ≡ true
T-to-≡ {true} tx = refl

≡-to-T : ∀ {x} → x ≡ true → T x
≡-to-T {true} x≡true = tt

≤-to-→ : ∀ {x y} → x 𝔹.≤ y → T x → T y
≤-to-→ {true} {true} x≤y _ = tt

→-to-≤ : ∀ {x y} → (T x → T y) → x 𝔹.≤ y
→-to-≤ {false} {false} Tx→Ty = b≤b
→-to-≤ {false} {true}  Tx→Ty = f≤t
→-to-≤ {true}  {false} Tx→Ty = ⊥-elim (Tx→Ty tt)
→-to-≤ {true}  {true}  Tx→Ty = b≤b

toFun : (x : ℕ → Bool) → (∀ i → x (suc i) 𝔹.≤ x i) →
        ∀ i → T (x (suc i)) → T (x i)
toFun x p i = ≤-to-→ (p i)

fromFun : (x : ℕ → Bool) → (∀ i → T (x (suc i)) → T (x i)) →
          ∀ i → x (suc i) 𝔹.≤ x i
fromFun _ f i = →-to-≤ (f i)

Dec-T : ∀ b → Dec (T b)
Dec-T false = no id
Dec-T true  = yes tt

private
  _≈Decidable_ : ∀ {P Q : ℕ → Set} (P? : U.Decidable P) (Q? : U.Decidable Q) → Set
  P? ≈Decidable Q? = ∀ x → isYes (P? x) ≡ isYes (Q? x)

  make≈Decidable : {P Q : ℕ → Set} → (∀ x → P x → Q x) → (∀ x → Q x → P x) →
                   (P? : U.Decidable P) (Q? : U.Decidable Q) → P? ≈Decidable Q?
  make≈Decidable P→Q Q→P P? Q? x with P? x | Q? x
  ... | yes p | yes q = refl
  ... | yes p | no ¬q = contradiction (P→Q _ p) ¬q
  ... | no ¬p | yes q = contradiction (Q→P _ q) ¬p
  ... | no ¬p | no ¬q = refl

  ℕ≤-all-dec′ : ∀ {P : ℕ → Set} → U.Decidable P → U.Decidable (λ n → ∀ i → i ≤ n → P i)
  ℕ≤-all-dec′ P? = DecU⇒decidable $ ℕ≤-all-dec (decidable⇒DecU P?)

idem-map-Pred : (α : ℕ → Bool) → ℕ → Set
idem-map-Pred α n = ∀ i → i ≤ n → T (α i)

idem-map-Pred? : (α : ℕ → Bool) → U.Decidable (idem-map-Pred α)
idem-map-Pred? α = ℕ≤-all-dec′ (λ i → Dec-T (α i))

idem-map : (ℕ → Bool) → (ℕ → Bool)
idem-map α n = isYes (idem-map-Pred? α n)

idem-map-idem : ∀ α → idem-map (idem-map α) ≈ idem-map α
idem-map-idem α =
  make≈Decidable
    (λ n x i i≤n → {!   !})
    {!   !}
    (idem-map-Pred? (λ n → isYes (idem-map-Pred? α n)))
    (idem-map-Pred? α)

-- x : idem-map-Pred (λ n₁ → isYes (idem-map-Pred? α n₁)) n
-- x : ∀ i → i ≤ n → T (isYes (idem-map-Pred? α i))

-- True   toWitness
-- hyp : idem-map-Pred α i
-- hyp : ∀ i →

-- Goal : ∀ i → i ≤ n → T (α i)

-- idem-map α n
-- isYes (ℕ-all-dec′ (λ i → Dec-⊤ (α i)) n)

idem-map-image : ∀ α → let x = idem-map α in (∀ i → T (x (suc i)) → T (x i))
idem-map-image α n ppp with ℕ≤-all-dec′ (λ i → Dec-T (α i)) n
... | yes _ = {!   !}
... | no _  = {!   !}


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

module Issue354 where

------------------------------------------------------------------------
-- Preliminaries

postulate
  Level : Set
  zero : Level
  suc  : (i : Level) → Level
  _⊔_ : Level → Level → Level

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO zero  #-}
{-# BUILTIN LEVELSUC  suc   #-}
{-# BUILTIN LEVELMAX  _⊔_   #-}

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

_≗_ : ∀ {a b} {A : Set a} {B : Set b} (f g : A → B) → Set (a ⊔ b)
f ≗ g = ∀ x → f x ≡ g x

------------------------------------------------------------------------
-- Example

postulate
  a     : Level
  A     : Set a
  P     : A → Set
  x     : A
  f     : ∀ {a} {A : Set a} → A → A
  g     : A → A
  lemma : f ≗ g

p : f x ≡ g x
p with f x | lemma x
... | .(g x) | refl = refl

-- The code above fails to type check, even though lemma x has the
-- type f x ≡ g x. However, if A is given the type Set zero, then the
-- code checks.

-- Excerpt from agda -vtc.with:100 --show-implicit Bug.agda:
--
--   checkWithFunction
--     delta1 =
--     delta2 =
--     gamma  =
--     as     = [A, _≡_ {a} {A} (f {a ⊔ a} {A} x) (g x)]
--     vs     = [f {a} {A} x, lemma x]
--     b      = _≡_ {a} {A} (f {a} {A} x) (g x)
--     qs     = []
--     perm   =  ->
--
-- Notice the occurrence of a ⊔ a.

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
module Optics.Iso where
open import Agda.Primitive using (Level; _⊔_; lsuc)
open import Function.Equality using (Π)
open import Function.Inverse using (_↔_; inverse; Inverse; _InverseOf_)
open import Relation.Binary.PropositionalEquality using (_≡_; →-to-⟶; refl)

open import Category.Functor.Arr
open import Category.Functor.Const
open import Category.Profunctor
open import Category.Profunctor.Star
open import Category.Profunctor.Joker
open import Optics

Iso : ∀ {l} (S T A B : Set l) → Set (lsuc l)
Iso = Optic ProfunctorImp

module Iso {l} {S T A B : Set l} (iso : Iso S T A B) where
  get : S → A
  get = getOptic S T A B (starProfunctor constFunctor) iso
  put : B → T
  put = putOptic S T A B (jokerProfunctor arrFunctor) iso

record LawfulIsoImp {l} {S A : Set l} (iso' : Iso S S A A) : Set (lsuc l) where
  open Iso iso'
  field
    putget : ∀ (s : S) → put (get s) ≡ s
    getput : ∀ (a : A) → get (put a) ≡ a

module LawfulIso {l} {S A : Set l} {iso' : Iso S S A A} (isLawful : LawfulIsoImp iso') where
  open Iso iso' public
  iso : Iso S S A A
  iso = iso'
  open LawfulIsoImp isLawful public

isoIso : ∀ {S A : Set} {iso : Iso S S A A} → (i : LawfulIsoImp iso) → S ↔ A
isoIso {S} {A} i = inverse to from from∘to to∘from
  where
    open LawfulIso i
    to = get
    from = put
    from∘to : (s : S) → from (to s) ≡ s
    from∘to = putget
    to∘from : (a : A) → to (from a) ≡ a
    to∘from = getput

invLawfulIso : ∀ {l} {S A : Set l} {get : S → A} {put : A → S} → (→-to-⟶ get) InverseOf (→-to-⟶ put) ↔ LawfulIsoImp (λ p → Profunctor.dimap p get put)
invLawfulIso = inverse invertibleIsLawful lawfulIsInvertible (λ _ → refl) (λ _ → refl)
  where
    invertibleIsLawful : ∀ {l} {S A : Set l} {get : S → A} {put : A → S} → (→-to-⟶ get) InverseOf (→-to-⟶ put) → LawfulIsoImp (λ p → Profunctor.dimap p get put)
    invertibleIsLawful i = record
      { putget = right-inverse-of
      ; getput = left-inverse-of
      } where
        open _InverseOf_ i

    lawfulIsInvertible : ∀ {l} {S A : Set l} {get : S → A} {put : A → S} → LawfulIsoImp (λ p → Profunctor.dimap p get put) → (→-to-⟶ get) InverseOf (→-to-⟶ put)
    lawfulIsInvertible isLawful = record
      { left-inverse-of = getput
      ; right-inverse-of = putget
      }
      where open LawfulIso isLawful

max_stars_repo_name: crisoagf/agda-optics

max_issues_repo_name: crisoagf/agda-optics

max_forks_repo_name: crisoagf/agda-optics


text:
----------------------------------------------------------------
-- This file contains the definition of natural isomorphisms. --
----------------------------------------------------------------
module Category.NatIsomorphism where

open import Category.NatTrans public
open import Category.Iso public

record NatIso {l₁ l₂ : Level}
              {ℂ₁ : Cat {l₁}}
              {ℂ₂ : Cat {l₂}}
              (F G : Functor ℂ₁ ℂ₂) : Set (l₁ ⊔ l₂) where
  field
    -- The natural transformation.
    natt : NatTrans F G

    -- Each component of (η natt) is an iso.
    η-iso-ax : ∀{A : Obj ℂ₁} → Iso {l₂}{ℂ₂}{A = omap F A}{omap G A} (η natt A)

open NatIso public

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
{-# OPTIONS --cubical-compatible #-}
module Common.Prelude where

import Common.Level

open import Agda.Builtin.Unit public
open import Common.Bool   public
open import Common.Char   public
open import Common.Float  public
open import Common.IO     public
open import Common.List   public
open import Common.Maybe  public
open import Common.Nat    public
open import Common.String public
open import Common.Unit   public

data   ⊥ : Set where


text:
module NonEmptyList where

infixr 5 _∷_

open import Data.Nat

data NList (A : Set) : Set where
  [_] : A → NList A
  _∷_ : A → NList A → NList A

map : {A B : Set} → (f : A → B) → NList A → NList B
map f [ x ] = [ f x ]
map f (x ∷ l) = f x ∷ map f l

length : ∀ {A} → NList A → ℕ
length [ _ ] = 1
length (_ ∷ l) = suc (length l)

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


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

-- Bundled version of Monoidal Category
module Categories.Category.Monoidal.Bundle where

open import Level

open import Categories.Category.Core using (Category)
open import Categories.Category.Monoidal.Core using (Monoidal)
open import Categories.Category.Monoidal.Braided using (Braided)
open import Categories.Category.Monoidal.Symmetric using (Symmetric)

record MonoidalCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
  field
    U        : Category o ℓ e
    monoidal : Monoidal U

  open Category U public
  open Monoidal monoidal public

record BraidedMonoidalCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
  field
    U         : Category o ℓ e
    monoidal  : Monoidal U
    braided   : Braided monoidal

  monoidalCategory : MonoidalCategory o ℓ e
  monoidalCategory = record { U = U ; monoidal = monoidal }

  open Category U public
  open Braided braided public

record SymmetricMonoidalCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
  field
    U         : Category o ℓ e
    monoidal  : Monoidal U
    symmetric : Symmetric monoidal

  open Category U public
  open Symmetric symmetric public

  braidedMonoidalCategory : BraidedMonoidalCategory o ℓ e
  braidedMonoidalCategory = record
    { U        = U
    ; monoidal = monoidal
    ; braided  = braided
    }

  open BraidedMonoidalCategory braidedMonoidalCategory public
    using (monoidalCategory)


text:
module Numeric.Nat.GCD where

open import Prelude
open import Control.WellFounded
open import Numeric.Nat.Properties
open import Numeric.Nat.DivMod
open import Numeric.Nat.Divide
open import Numeric.Nat.Divide.Properties
open import Tactic.Nat

--- GCD ---

record IsGCD (d a b : Nat) : Set where
  no-eta-equality
  constructor is-gcd
  field d|a : d Divides a
        d|b : d Divides b
        g   : ∀ k → k Divides a → k Divides b → k Divides d

record GCD (a b : Nat) : Set where
  no-eta-equality
  constructor gcd-res
  field d     : Nat
        isGCD : IsGCD d a b

open GCD public using () renaming (d to get-gcd)

-- Projections --

is-gcd-factor₁ : ∀ {a b d} → IsGCD d a b → Nat
is-gcd-factor₁ g = get-factor (IsGCD.d|a g)

is-gcd-factor₂ : ∀ {a b d} → IsGCD d a b → Nat
is-gcd-factor₂ g = get-factor (IsGCD.d|b g)

gcd-factor₁ : ∀ {a b} → GCD a b → Nat
gcd-factor₁ g = is-gcd-factor₁ (GCD.isGCD g)

gcd-factor₂ : ∀ {a b} → GCD a b → Nat
gcd-factor₂ g = is-gcd-factor₂ (GCD.isGCD g)

-- Euclid's algorithm --

isGCD-step : ∀ {d r₀ r₁ r₂} q → q * r₁ + r₂ ≡ r₀ → IsGCD d r₁ r₂ → IsGCD d r₀ r₁
isGCD-step q refl (is-gcd d|r₁ d|r₂ g) =
  is-gcd (divides-add (divides-mul-r q d|r₁) d|r₂)
         d|r₁ (λ k k|r₀ k|r₁ → g k k|r₁ (divides-sub-l k|r₀ (divides-mul-r q k|r₁)))

private
  gcd-step : ∀ {a b} q {r} → q * suc b + r ≡ a → GCD (suc b) r → GCD a (suc b)
  gcd-step q eq (gcd-res d p) = gcd-res d (isGCD-step q eq p)

  gcd-cert-acc : ∀ a b → Acc _<_ b → GCD a b
  gcd-cert-acc a zero _ = gcd-res a (is-gcd (factor 1 auto) (factor! 0) (λ k k|a _ → k|a))
  gcd-cert-acc a (suc b) (acc wf) =
    case a divmod suc b of λ
    { (qr q r lt eq) → gcd-step q eq (gcd-cert-acc (suc b) r (wf r lt)) }

eraseIsGCD : ∀ {d a b} → IsGCD d a b → IsGCD d a b
eraseIsGCD (is-gcd d|a d|b g) =
  is-gcd (fast-divides d|a) (fast-divides d|b)
         λ k k|a k|b → fast-divides (g k k|a k|b)

eraseGCD : ∀ {a b} → GCD a b → GCD a b
eraseGCD (gcd-res d p) = gcd-res d (eraseIsGCD p)

gcd : ∀ a b → GCD a b
gcd 0 b = gcd-res b (is-gcd (factor! 0) divides-refl (λ _ _ k|b → k|b))
gcd 1 b = gcd-res 1 (is-gcd divides-refl (factor b auto) (λ _ k|1 _ → k|1))
gcd a b = eraseGCD (gcd-cert-acc a b (wfNat b))

gcd! : Nat → Nat → Nat
gcd! a b = get-gcd (gcd a b)

Coprime : Nat → Nat → Set
Coprime a b = gcd! a b ≡ 1

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
primitive

ID : Set → Set
ID A = A


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

open import lib.Basics

module lib.types.Unit where

⊤ = Unit
tt = unit

abstract
  -- Unit is contractible
  Unit-is-contr : is-contr Unit
  Unit-is-contr = (unit , λ y → idp)

  Unit-has-level : {n : ℕ₋₂} → has-level n Unit
  Unit-has-level = contr-has-level Unit-is-contr

  -- [Unit-has-level#instance] produces unsolved metas
  Unit-has-level-S#instance : {n : ℕ₋₂} → has-level (S n) Unit
  Unit-has-level-S#instance = contr-has-level Unit-is-contr

  Unit-is-prop : is-prop Unit
  Unit-is-prop = Unit-has-level

  Unit-is-set : is-set Unit
  Unit-is-set = Unit-has-level

Unit-level = Unit-is-contr
⊤-is-contr = Unit-is-contr
⊤-level = Unit-is-contr
⊤-has-level = Unit-has-level
⊤-is-prop = Unit-is-prop
⊤-is-set = Unit-is-set

max_stars_repo_name: sattlerc/HoTT-Agda

max_issues_repo_name: sattlerc/HoTT-Agda

max_forks_repo_name: sattlerc/HoTT-Agda


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

-- Drop-in replacement for the module [Base].
module BaseOver where

-- We hide [apd] and [Σ-eq] because their type is not correct, we want to use
-- dependent paths instead
open import Base public hiding (apd; Σ-eq)

-- Notion of path over a path
path-over : ∀ {i j} {A : Set i} (B : A → Set j)
  {x y : A} (p : x == y) (u : B x) (v : B y) → Set j
path-over B refl u v = (u == v)

syntax path-over B p u v =
  u == v [ B ↓ p ]

-- New apd
apd : ∀ {i j} {A : Set i} {B : A → Set j} (f : (a : A) → B a) {x y : A}
  → (p : x == y) → f x == f y [ B ↓ p ]
apd f refl = refl

-- Σ-types are used to simulate telescopes and to be able to only use the
-- notion of path over a single path

-- Intro for paths in a Σ
Σ-eq : ∀ {i j} {A : Set i} {B : A → Set j} {x y : A} (p : x == y)
  {u : B x} {v : B y} (q : u == v [ B ↓ p ])
  → (x , u) == (y , v)
Σ-eq refl refl = refl

uncurryi : ∀ {i j k} {A : Set i} {B : A → Set j} {C : ∀ x → B x → Set k}
  → (∀ {x} y → C x y) → (∀ s → C (π₁ s) (π₂ s))
uncurryi f (x , y) = f y

apdd : ∀ {i j k} {A : Set i} {B : A → Set j} {C : (a : A) → B a → Set k}
  (g : {a : A} → Π (B a) (C a)) {x y : A} (p : x == y)
  {u : B x} {v : B y} (q : u == v [ B ↓ p ])
  → g u == g v [ uncurry C ↓ Σ-eq p q ]
apdd g p q = apd (uncurryi g) (Σ-eq p q)

-- Dependent paths in a constant fibration
module _ {i j} {A : Set i} {B : Set j} where

  ↓-cst-in : {x y : A} (p : x == y) {u v : B}
    → u == v
    → u == v [ (λ _ → B) ↓ p ]
  ↓-cst-in refl q = q

  ↓-cst-out : {x y : A} {p : x == y} {u v : B}
    → u == v [ (λ _ → B) ↓ p ]
    → u == v
  ↓-cst-out {p = refl} q = q

  ↓-cst-β : {x y : A} (p : x == y) {u v : B} (q : u == v)
    → (↓-cst-out (↓-cst-in p q) == q)
  ↓-cst-β refl q = refl

-- -- ap can be defined via apd, not sure whether it’s a good idea or not
-- ap : ∀ {i j} {A : Set i} {B : Set j} (f : A → B) {x y : A} (p : x == y)
--   → f x == f y
-- ap f p = ↓-cst-out (apd f p)

-- Dependent paths in a Π-type
module _ {i j k} {A : Set i} {B : A → Set j} {C : (a : A) → B a → Set k} where

  ↓-Π-in : {x x' : A} {p : x == x'} {u : Π (B x) (C x)} {u' : Π (B x') (C x')}
    → ({t : B x} {t' : B x'} (q : t == t' [ B ↓ p ])
        → u t == u' t' [ uncurry C ↓ Σ-eq p q ])
    → (u == u' [ (λ x → Π (B x) (C x)) ↓ p ])
  ↓-Π-in {p = refl} f = funext (λ x → f (refl {a = x}))

  ↓-Π-out : {x x' : A} {p : x == x'} {u : Π (B x) (C x)} {u' : Π (B x') (C x')}
    → (u == u' [ (λ x → Π (B x) (C x)) ↓ p ])
    → ({t : B x} {t' : B x'} (q : t == t' [ B ↓ p ])
        → u t == u' t' [ uncurry C ↓ Σ-eq p q ])
  ↓-Π-out {p = refl} q refl = happly q _

  ↓-Π-β : {x x' : A} {p : x == x'} {u : Π (B x) (C x)} {u' : Π (B x') (C x')}
    → (f : {t : B x} {t' : B x'} (q : t == t' [ B ↓ p ])
            → u t == u' t' [ uncurry C ↓ Σ-eq p q ])
    → {t : B x} {t' : B x'} (q : t == t' [ B ↓ p ])
    → ↓-Π-out (↓-Π-in f) q == f q
  ↓-Π-β {p = refl} f refl = happly (happly-funext (λ x → f (refl {a = x}))) _

-- Dependent paths in a Π-type where the codomain is not dependent on anything
module _ {i j k} {A : Set i} {B : A → Set j} {C : Set k} {x x' : A} {p : x == x'}
  {u : B x → C} {u' : B x' → C} where

  ↓-app→cst-in :
    ({t : B x} {t' : B x'} (q : t == t' [ B ↓ p ])
      → u t == u' t')
    → (u == u' [ (λ x → B x → C) ↓ p ])
  ↓-app→cst-in f = ↓-Π-in (λ q → ↓-cst-in (Σ-eq p q) (f q))

  ↓-app→cst-out :
    (u == u' [ (λ x → B x → C) ↓ p ])
    → ({t : B x} {t' : B x'} (q : t == t' [ B ↓ p ])
        → u t == u' t')
  ↓-app→cst-out r q = ↓-cst-out (↓-Π-out r q)

  ↓-app→cst-β :
    (f : ({t : B x} {t' : B x'} (q : t == t' [ B ↓ p ])
           → u t == u' t'))
    → {t : B x} {t' : B x'} (q : t == t' [ B ↓ p ])
    → ↓-app→cst-out (↓-app→cst-in f) q == f q
  ↓-app→cst-β f q =
    ↓-app→cst-out (↓-app→cst-in f) q
             ≡⟨ refl ⟩
    ↓-cst-out (↓-Π-out (↓-Π-in (λ qq → ↓-cst-in (Σ-eq p qq) (f qq))) q)
             ≡⟨ ↓-Π-β (λ qq → ↓-cst-in (Σ-eq p qq) (f qq)) q |in-ctx ↓-cst-out ⟩
    ↓-cst-out (↓-cst-in (Σ-eq p q) (f q))
             ≡⟨ ↓-cst-β (Σ-eq p q) (f q) ⟩
    f q ∎

-- Dependent paths in a Π-type where the domain is constant
module _ {i j k} {A : Set i} {B : Set j} {C : A → B → Set k}
  {x x' : A} {p : x == x'}
  {u : (b : B) → C x b} {u' : (b : B) → C x' b} where

  postulate
    ↓-cst→app-in :
      ({t t' : B} (q : t == t')
        → u t == u' t' [ uncurry C ↓ Σ-eq p (↓-cst-in p q) ])
      → (u == u' [ (λ x → (b : B) → C x b) ↓ p ])
--  ↓-cst→app-in f = ↓-Π-in (λ q → {!f (↓-cst-out q)!})

  postulate
    ↓-cst→app-out :
      (u == u' [ (λ x → (b : B) → C x b) ↓ p ])
      → ({t t' : B} (q : t == t')
        → u t == u' t' [ uncurry C ↓ Σ-eq p (↓-cst-in p q) ])

split-ap2 : ∀ {i j k} {A : Set i} {B : A → Set j} {C : Set k} (f : Σ A B → C)
  {x y : A} (p : x == y)
  {u : B x} {v : B y} (q : u == v [ B ↓ p ])
  → ap f (Σ-eq p q) == ↓-app→cst-out (apd (curry f) p) q
split-ap2 f refl refl = refl

↓-app='cst-in : ∀ {i j} {A : Set i} {B : Set j} {f : A → B} {b : B}
  {x y : A} {p : x == y} {u : f x == b} {v : f y == b}
  → u == (ap f p ∘' v)
  → (u == v [ (λ x → f x == b) ↓ p ])
↓-app='cst-in {p = refl} q = q ∘ refl-left-unit _

↓-app='cst-out : ∀ {i j} {A : Set i} {B : Set j} {f : A → B} {b : B}
  {x y : A} {p : x == y} {u : f x == b} {v : f y == b}
  → (u == v [ (λ x → f x == b) ↓ p ])
  → u == (ap f p ∘' v)
↓-app='cst-out {p = refl} refl = ! (refl-left-unit _)

↓-cst='app-in : ∀ {i j} {A : Set i} {B : Set j} {f : A → B} {b : B}
  {x y : A} {p : x == y} {u : b == f x} {v : b == f y}
  → (u ∘' ap f p) == v
  → (u == v [ (λ x → b == f x) ↓ p ])
↓-cst='app-in {p = refl} refl = refl

↓-cst='app-out : ∀ {i j} {A : Set i} {B : Set j} {f : A → B} {b : B}
  {x y : A} {p : x == y} {u : b == f x} {v : b == f y}
  → (u == v [ (λ x → b == f x) ↓ p ])
  → (u ∘' ap f p) == v
↓-cst='app-out {p = refl} refl = refl

↓-='-in : ∀ {i j} {A : Set i} {B : Set j} {f g : A → B}
  {x y : A} {p : x == y} {u : f x == g x} {v : f y == g y}
  → (u ∘ ap g p) == (ap f p ∘' v)
  → (u == v [ (λ x → f x == g x) ↓ p ])
↓-='-in {p = refl} q = ! (refl-right-unit _) ∘ (q ∘ refl-left-unit _)

-- Dependent vs nondependent whiskering
-- This definitional behaviour make [↓-=-in] slightly more complicated to prove
-- but [↓-=-in] is often used in the case where [u] and [v] are [refl]
_▹_ : ∀ {i j} {A : Set i} {B : A → Set j} {x y : A} {u : B x}
  {v w : B y} {p : x == y}
  → (u == v [ B ↓ p ]) → v == w
     → (u == w [ B ↓ p ])
_▹_ {p = refl} q refl = q

refl▹ : ∀ {i j} {A : Set i} {B : A → Set j} {x : A}
  {v w : B x} (q : v == w)
  → _▹_ {B = B} {p = refl} refl q == q
refl▹ refl = refl

_◃_ : ∀ {i j} {A : Set i} {B : A → Set j} {x y : A} {u v : B x}
  {w : B y} {p : x == y}
  → (u == v → (v == w [ B ↓ p ])
     → (u == w [ B ↓ p ]))
_◃_ {p = refl} refl q = q

◃refl : ∀ {i j} {A : Set i} {B : A → Set j} {x : A}
  {v w : B x} (q : v == w)
  → _◃_ {B = B} {p = refl} q refl == q
◃refl refl = refl

↓-=-in : ∀ {i j} {A : Set i} {B : A → Set j} {f g : Π A B}
  {x y : A} {p : x == y} {u : g x == f x} {v : g y == f y}
  → (u ◃ apd f p) == (apd g p ▹ v)
  → (u == v [ (λ x → g x == f x) ↓ p ])
↓-=-in {B = B} {p = refl} {u} {v} q =
  ! (◃refl {B = B} u) ∘ (q ∘ refl▹ {B = B} v)

postulate
 ↓-=-out : ∀ {i j} {A : Set i} {B : A → Set j} {f g : Π A B}
  {x y : A} {p : x == y} {u : g x == f x} {v : g y == f y}
  → (u == v [ (λ x → g x == f x) ↓ p ])
  → (u ◃ apd f p) == (apd g p ▹ v)
--↓-=-out {B = B} {p = refl} refl = {!!}

{- Not used yet

apdd-cst : ∀ {i j k} {A : Set i} {B : Set j} {C : A → B → Set k}
  (g : (a : A) → Π B (C a)) {x y : A} (p : x ≡ y)
  {u v : B} (q : u ≡ v) {r : u ≡[ (λ _ → B) ↓ p ] v} (α : ↓-cst-in p q ≡ r)
  → apdd (λ {a} b → g a b) p r ≡ apd (uncurry g) (Σ-eq p r)
apdd-cst g refl refl refl = refl
-}
-- This one seems a bit weird
↓-apd-out : ∀ {i j k} {A : Set i} {B : A → Set j} (C : (a : A) → B a → Set k)
  (f : Π A B) {x y : A} (p : x == y)
  {u : C x (f x)} {v : C y (f y)}
  → u == v [ uncurry C ↓ Σ-eq p (apd f p) ]
  → u == v [ (λ z → C z (f z)) ↓ p ]
↓-apd-out C f refl refl = refl
{-
-- Dependent paths over [ap f p]
module _ {i j k} {A : Set i} {B : Set j} (C : B → Set k) (f : A → B) where

  ↓-ap-in : {x y : A} {p : x ≡ y} {u : C (f x)} {v : C (f y)}
    → u ≡[ C ◯ f ↓ p ] v
    → u ≡[ C ↓ ap f p ] v
  ↓-ap-in {p = refl} refl = refl

  ↓-ap-out : {x y : A} (p : x ≡ y) {u : C (f x)} {v : C (f y)}
    → u ≡[ C ↓ ap f p ] v
    → u ≡[ C ◯ f ↓ p ] v
  ↓-ap-out refl refl = refl

--  ↓-ap-β

ap-, : ∀ {i j k} {A : Set i} {B : Set j} {C : B → Set k}
  (f : A → B) (g : (a : A) → C (f a)) {x y : A} (p : x ≡ y)
  → ap (λ x → _,_ {P = C} (f x) (g x)) p
       ≡ Σ-eq (ap f p) (↓-ap-in C f (apd g p))
ap-, f g refl = refl
-}

-- Special case of [ap-,]
ap-cst,id : ∀ {i j} {A : Set i} (B : A → Set j)
  {a : A} {x y : B a} (p : x == y)
  → ap (λ x → _,_ {P = B} a x) p == Σ-eq refl p
ap-cst,id B refl = refl

-- apd-nd : ∀ {i j} {A : Set i} {B : Set j} (f : A → B) {x y : A}
--   → (p : x ≡ y) → apd f p ≡ ↓-cst-in p (ap f p)
-- apd-nd f refl = refl

apd-◯ : ∀ {i j k} {A : Set i} {B : A → Set j} {C : (a : A) → B a → Set k}
  (f : Π A B) (g : {a : A} → Π (B a) (C a)) {x y : A} (p : x == y)
  → apd (g ◯ f) p == ↓-apd-out C f p (apdd g p (apd f p))
apd-◯ f g refl = refl

{- Not used yet

-- apd-apd : ∀ {i j k} {A : Set i} {B : A → Set j} {C : (a : A) → B a → Set k}
--   (g : (u : Σ A B) → C (π₁ u) (π₂ u)) (f : Π A B) {x y : A} (p : x ≡ y)
--   → apd g (Σ-eq p (apd f p)) ≡ {!↓-ap-in!}
-- apd-apd = {!!}

apd-π₁-β : ∀ {i j} {A : Set i} {B : A → Set j} {x x' : A} (p : x ≡ x')
  {y : B x} {y' : B x'} (q : y ≡[ B ↓ p ] y')
  → ap π₁ (Σ-eq p q) ≡ p
apd-π₁-β refl refl = refl

apd-π₂-β : ∀ {i j} {A : Set i} {B : A → Set j} {x x' : A} (p : x ≡ x')
  {y : B x} {y' : B x'} (q : y ≡[ B ↓ p ] y')
  → apd π₂ (Σ-eq p q) ≡ ↓-ap-out B π₁ (Σ-eq p q)
    (transport (λ p → y ≡[ B ↓ p ] y') (! (apd-π₁-β p q)) q)
apd-π₂-β refl refl = refl
-}

-- Dependent path in a type of the form [λ x → g (f x) ≡ x]
module _ {i j} {A : Set i} {B : Set j} (f : A → B) (g : B → A) where
  ↓-◯=id-in : {x y : A} {p : x == y} {u : g (f x) == x} {v : g (f y) == y}
    → ((ap g (ap f p) ∘' v) == (u ∘ p))
    → (u == v [ (λ x → g (f x) == x) ↓ p ])
  ↓-◯=id-in {p = refl} q = ! (refl-right-unit _) ∘ (! q ∘ refl-left-unit _)

-- WIP, derive it from more primitive principles
-- ↓-◯≡id-in f g {p = p} {u} {v} q =
--   ↓-≡-in (u ◃ apd (λ x → g (f x)) p ≡⟨ apd-◯ f g p |in-ctx (λ t → u ◃ t) ⟩
--         u ◃ ↓-apd-out _ f p (apdd g p (apd f p)) ≡⟨ apdd-cst (λ _ b → g b) p (ap f p) (! (apd-nd f p)) |in-ctx (λ t → u ◃ ↓-apd-out _ f p t) ⟩
--         u ◃ ↓-apd-out _ f p (apd (λ t → g (π₂ t)) (Σ-eq p (apd f p))) ≡⟨ apd-◯ π₂ g (Σ-eq p (apd f p)) |in-ctx (λ t → u ◃ ↓-apd-out _ f p t) ⟩
--         u ◃ ↓-apd-out _ f p (↓-apd-out _ π₂ (Σ-eq p (apd f p)) (apdd g (Σ-eq p (apd f p)) (apd π₂ (Σ-eq p (apd f p))))) ≡⟨ {!!} ⟩
--         apd (λ x → x) p ▹ v ∎)

ua-in : ∀ {i} {A B : Set i} → A ≃ B → A == B
ua-in = eq-to-path

ua-out : ∀ {i} {A B : Set i} → A == B → A ≃ B
ua-out = path-to-eq

ua-β : ∀ {i} {A B : Set i} (e : A ≃ B)
  → ua-out (ua-in e) == e
ua-β e = eq-to-path-right-inverse e

-- These lemmas do not really look computational, but they are only used in the
-- [↓-pp] lemmas which do look computational.

to-transp-in : ∀ {i j} {A : Set i} (B : A → Set j)
  {a a' : A} (p : a == a')
  {u : B a} {v : B a'}
  → (π₁ (ua-out (ap B p)) u == v)
  → (u == v [ B ↓ p ])
to-transp-in B refl refl = refl

to-transp-out : ∀ {i j} {A : Set i} {B : A → Set j}
  {a a' : A} {p : a == a'}
  {u : B a} {v : B a'}
  → (u == v [ B ↓ p ])
  → (π₁ (ua-out (ap B p)) u == v)
to-transp-out {p = refl} refl = refl

to-transp-β : ∀ {i j} {A : Set i} (B : A → Set j)
  {a a' : A} (p : a == a')
  {u : B a} {v : B a'}
  (q : π₁ (ua-out (ap B p)) u == v)
  → to-transp-out (to-transp-in B p q) == q
to-transp-β B refl refl = refl

-- Stuff that do not belong here

ap-∘' : ∀ {i j} {A : Set i} {B : Set j} (f : A → B)
  {x y z : A} (p : x == y) (q : y == z)
  → ap f (p ∘' q) == (ap f p ∘' ap f q)
ap-∘' f refl refl = refl

-- Dependent concatenation'
_∘'dep_ : ∀ {i j} {A : Set i} {B : A → Set j}
  {x y z : A} {p : x == y} {p' : y == z}
  {u : B x} {v : B y} {w : B z}
  → (u == v [ B ↓ p ]
   → v == w [ B ↓ p' ]
   → u == w [ B ↓ (p ∘' p') ])
_∘'dep_ {p' = refl} q refl = q

-- Implementation of [_∘'_] on Σ
Σ-∘' : ∀ {i j} {A : Set i} {B : A → Set j}
  {x y z : A} {p : x == y} {p' : y == z}
  {u : B x} {v : B y} {w : B z}
  (q : u == v [ B ↓ p ]) (r : v == w [ B ↓ p' ])
  → (Σ-eq p q ∘' Σ-eq p' r) == Σ-eq (p ∘' p') (q ∘'dep r)
Σ-∘' {p' = refl} q refl = refl

-- No idea what that is
to-transp-weird : ∀ {i j} {A : Set i} {B : A → Set j}
  {u v : A} {d : B u} {d' d'' : B v} {p : u == v}
  (q : d == d' [ B ↓ p ]) (r : π₁ (ua-out (ap B p)) d == d'')
  → (to-transp-in B p r ∘'dep (! r ∘ to-transp-out q)) == q
to-transp-weird {p = refl} refl refl = refl

_∘'2_ : ∀ {i j} {A : Set i} {B : A → Set j} {a b c : Π A B}
  {x y : A} {p : x == y} {q : a x == b x} {q' : a y == b y}
  {r : b x == c x} {r' : b y == c y}
  → (q == q'            [ (λ z → a z == b z) ↓ p ])
  → (r == r'            [ (λ z → b z == c z) ↓ p ])
  → (q ∘' r == q' ∘' r' [ (λ z → a z == c z) ↓ p ])
_∘'2_ {p = refl} refl refl = refl

stuff : ∀ {i j} {A : Set i} {B : Set j} {b : B} {c : A → B} {d : A → B}
  (q : (a : A) → b == c a) (r : (a : A) → c a == d a) {a a' : A} (p : a == a')
  → apd (λ a → q a ∘' r a) p == ((apd q p) ∘'2 (apd r p))
stuff q r refl = refl

apd= : ∀ {i j} {A : Set i} {B : A → Set j} {f g : Π A B} (q : (x : A) → f x == g x) {x y : A} (p : x == y)
--    → (q x == q y [ (λ z → f z == g z) ↓ p ])
  → (apd f p ▹ q y) == (q x ◃ apd g p)
apd= q p = ! (↓-=-out (apd q p))
--apd= q refl =

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module _ where

module M (_ : Set₁) where

  record R₁ (A : Set) : Set₁ where
    no-eta-equality

    postulate
      x : A

  open R₁ ⦃ … ⦄ public

  record R₂ (A : Set) : Set₁ where
    field
      instance
        r₁ : R₁ A

  open R₂ ⦃ … ⦄

open module MSet = M Set

postulate
  A : Set

instance
  postulate
    m : R₁ A

a : A
a = x

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module Tactic.Reflection.Free where

open import Prelude
open import Builtin.Reflection
open import Tactic.Reflection.DeBruijn

VarSet = List Nat -- ordered

private
  _∪_ : VarSet → VarSet → VarSet
  []       ∪ ys = ys
  xs       ∪ [] = xs
  (x ∷ xs) ∪ (y ∷ ys) with compare x y
  ... | (less    _) = x ∷ (xs ∪ (y ∷ ys))
  ... | (equal   _) = x ∷ (xs ∪ ys)
  ... | (greater _) = y ∷ ((x ∷ xs) ∪ ys)

  ∅ : VarSet
  ∅ = []

record FreeVars {a} (A : Set a) : Set a where
  field freeVars : A → VarSet

open FreeVars {{...}} public

-- Instances --

private
  freeTerm : Nat → Term → VarSet
  freeSort : Nat → Sort → VarSet
  freeArgTerm : Nat → Arg Term → VarSet
  freeArgs : Nat → List (Arg Term) → VarSet
  freeClauses : Nat → List Clause → VarSet
  freeClause : Nat → Clause → VarSet

  freeTerm n (var x args) = freeArgs n args ∪
    (case compare (suc x) n of
    λ { (greater (diff k _)) → [ k ]
      ; _ → ∅
      })
  freeTerm n (con c args) = freeArgs n args
  freeTerm n (def f args) = freeArgs n args
  freeTerm n (meta x args) = freeArgs n args
  freeTerm n (lam _ (abs _ v)) = freeTerm (suc n) v
  freeTerm n (pat-lam cs args) = freeClauses n cs ∪ freeArgs n args
  freeTerm n (pi a (abs _ b))  = freeArgTerm n a ∪ freeTerm (suc n) b
  freeTerm n (agda-sort s) = freeSort n s
  freeTerm n (lit l) = ∅
  freeTerm n unknown = ∅

  freeSort n (set t) = freeTerm n t
  freeSort _ (lit n) = ∅
  freeSort _ unknown = ∅

  freeArgTerm n (arg i x) = freeTerm n x
  freeArgs n [] = ∅
  freeArgs n (a ∷ as) = freeArgTerm n a ∪ freeArgs n as

  freeClauses n [] = ∅
  freeClauses n (c ∷ cs) = freeClause n c ∪ freeClauses n cs

  freeClause n (clause ps b)     = freeTerm (patternBindings ps + n) b
  freeClause n (absurd-clause _) = ∅

instance
  FreeTerm : FreeVars Term
  freeVars {{FreeTerm}} = freeTerm 0

  FreeSort : FreeVars Sort
  freeVars {{FreeSort}} = freeSort 0

  FreeArg : ∀ {A} {{_ : FreeVars A}} → FreeVars (Arg A)
  freeVars {{FreeArg}} (arg _ x) = freeVars x

  FreeList : ∀ {a} {A : Set a} {{_ : FreeVars A}} → FreeVars (List A)
  freeVars {{FreeList}} = foldr (λ x → freeVars x ∪_) ∅


text:
{-# OPTIONS --cubical-compatible --rewriting --confluence-check #-}

module _ where

{- Rewriting relation -}

postulate
  _↦_ : ∀ {i} {A : Set i} → A → A → Set i
  idr : ∀ {i} {A : Set i} {a : A} → a ↦ a
{-# BUILTIN REWRITE _↦_ #-}

{- Identity type -}

infixr 3 _==_

data _==_ {i} {A : Set i} (a : A) : A → Set i where
  idp : a == a

ap : ∀ {i j} {A : Set i} {B : Set j} (f : A → B) {x y : A}
  → (p : x == y) → f x == f y
ap f idp = idp

postulate
  A : Set
  C : A → Set

-- Definition of W

postulate
  W : Set
  c : A → W

module _ {l} {P : W → Set l} (c* : (a : A) → P (c a)) where
  postulate
    W-elim : (w : W) → P w
    W-c-β : (a : A) → W-elim (c a) ↦ c* a
    {-# REWRITE W-c-β #-}

-- Definition of P

P : W → Set
P = W-elim C

-- Definition of WT

postulate
  WT : Set
  cT : (a : A) (x : C a) → WT

-- Definition of TotP

record TotP : Set where
  constructor _,_
  field
    fst : W
    snd : P fst

-- Function from TotP to WT

from-curry : (x : W) (y : P x) → WT
from-curry = W-elim cT

from : TotP → WT
from (x , y) = from-curry x y

postulate
  a : A
  x y : C a
  foo : (c a , x) == (c a , y)
  bar : cT a x == cT a y

  rew1 : ap from foo ↦ bar
{-# REWRITE rew1 #-}

-- The following has exactly the same type as [rew1], so [idr] should work
rew1' : ap from foo ↦ bar
rew1' = idr