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

open import lib.Basics
open import lib.types.Paths
open import lib.types.Pi
open import lib.types.Unit
open import lib.types.Nat
open import lib.types.TLevel
open import lib.types.Pointed
open import lib.types.Sigma
open import lib.NType2
open import lib.types.PathSeq

open import nicolai.pseudotruncations.Liblemmas
open import nicolai.pseudotruncations.SeqColim

{- The main work is done in two separate files.

   The first defines some general lemmas
   and constructs what is overline(i) in the paper.

   The second is the 'heptagon-argument', a very
   tedious calculation with paths, which constructs
   what is overline(g) in the paper -- the coherence
   laws for overline (i). -}
open import nicolai.pseudotruncations.wconst-preparation
open import nicolai.pseudotruncations.heptagon

module nicolai.pseudotruncations.wconstSequence where

  {- As a first step, assume we are given a weakly constant
     sequence with an inhabitant of the first type. -}
  module _ {i} {C : Sequence {i}} (wc : wconst-chain C) (a₀ : fst C O) where

    {- We want to show that the colimit of this sequence is
       contractible.
       The heart of the argument are the definitions of the data
       that is needed in order to apply the induction principle
       of the sequential colimit.
       We call these î and ĝ. They are not constructed here, but
       in two separate files; the construction of ĝ is very tedious.
       Here, we just load them from the files where they are defined.
    -}

    {- First, some preliminary lemmas and the definition of î,
       defined in the following module: -}
    open wconst-init {i} {C} wc a₀

    î : (n : ℕ) → (a : A n) → (ins {C = C} n a) =-= (ins O a₀)
    î = î-def

    {- from î, we get the 'real' overline(i) just by applying ↯,
       i.e. by getting the path out of the sequence î -}
    ins-n-O : (n : ℕ) → (a : A n) → ins {C = C} n a == ins O a₀
    ins-n-O n a = ↯ (î-def n a)

    {- The difficult part is ĝ, in the paper called 'overline(g)'.
       It is defined in heptagon.agda and just loaded here. -}

    ĝ : (n : ℕ) → (a : A n)
        → (↯ ((î (S n) (f n a)) ⋯ (‼ (î n a) ⋯ toSeq (glue n a)))) == idp
    ĝ n a = ĝ-def wc a₀ n a

    -- from ĝ, we should be able to get this postulate:
    postulate
      ins-glue-coh : (n : ℕ) (a : A n)
                     → ins-n-O (S n) (f n a) ∙ ! (ins-n-O n a) ∙ glue n a == idp
    -- ins-glue-coh n a = {!ins-n-O n a !} --  {!ĝ n a!}

    {- Now, we define the 'real' overline(g) from the text;
       this is just the 'unwrapped' version of ĝ, and not much happens
       here!
       All we are doing is showing that commutativity of the 'triangle'
       is really enough. The hard part is the commutativity of the
       'triangle' which, is shown via commutativity of the 'heptagon',
       which we have already done! -}
    glue-n-O : (n : ℕ) (a : A n)
               → (ins-n-O n a)
                  ==
                 (ins-n-O (S n) (f n a)) [ (λ w → w == ins O a₀) ↓ glue n a ]

    glue-n-O n a = from-transp _ (glue n a)
      -- now, let use calculate...
      (transport (λ w → w == ins O a₀) (glue n a) (ins-n-O n a)
        -- we use the version of trans-ap where the second function is constant
        =⟨ trans-ap₁ (idf _) (ins O a₀) (glue n a) (ins-n-O n a) ⟩
      ! (ap (idf _) (glue n a)) ∙ (ins-n-O n a)
        =⟨ ap (λ p → (! p) ∙ (ins-n-O n a)) (ap-idf (glue n a)) ⟩
      ! (glue n a) ∙ (ins-n-O n a)
        -- we use the adhoc lemma to 're-order' paths
        =⟨ ! (adhoc-lemma (ins-n-O (S n) (f n a)) (ins-n-O n a) (glue n a) (ins-glue-coh n a)) ⟩
      ins-n-O (S n) (f n a)
        ∎)

    -- We combine 'overline(i)' and 'overline(g)' to conclude:
    equal-n-O : (w : SC) → w == ins O a₀
    equal-n-O = SeqCo-ind ins-n-O glue-n-O

    -- Thus, the sequential colimit is contractible:
    SC-contr : is-contr SC
    SC-contr = ins O a₀ , (λ w → ! (equal-n-O w))

{- This completes the proof that the sequential colimit of a weakly constant
   sequence with *inhabited first type* is contractible.
   Let us now work with general weakly constant sequences again.

   First, let us now show that removing the first map from a weakly constant sequence
   gives a weakly constant sequence.
   Then, we show that we can remove any finite initial sequence.
   Of course, this is trivial; the conclusion of the statement asks for weak
   constancy of nearly all of the maps, while the assumption gives weak constancy
   of all maps. -}
removeFst-preserves-wconst : ∀ {i} → (C : Sequence {i}) → wconst-chain C → wconst-chain (removeFst C)
removeFst-preserves-wconst C wc n = wc (S n)

removeInit-preserves-wconst : ∀ {i} → (C : Sequence {i}) → (n : ℕ) → wconst-chain C → wconst-chain (removeInit C n)
removeInit-preserves-wconst C O wc = wc
removeInit-preserves-wconst C (S n) wc =
  removeInit-preserves-wconst (removeFst C) n
    (removeFst-preserves-wconst C wc)

{- THE FIRST MAIN RESULT:
   the colimit of a weakly constant sequence is propositional. -}

wconst-prop : ∀ {i} → (C : Sequence {i}) → wconst-chain C → is-prop (SeqCo C)
wconst-prop C wc = inhab-to-contr-is-prop (SeqCo-rec wc-prp-ins automatic) where

  A = fst C
  f = snd C

  wc-prp-ins : (n : ℕ) → A n → is-contr (SeqCo C)
  wc-prp-ins n a = equiv-preserves-level {n = ⟨-2⟩} (ignore-init C n ⁻¹) C'-contr where

    C' = removeInit C n
    A' = fst C'
    f' = snd C'

    a₀' : A' O
    a₀' = new-initial C n a

    wc' : wconst-chain C'
    wc' = removeInit-preserves-wconst C n wc

    C'-contr : is-contr (SeqCo C')
    C'-contr = SC-contr wc' a₀'

  automatic : (n : ℕ) (a : fst C n) → wc-prp-ins n a == wc-prp-ins (S n) (snd C n a)
  automatic n a = prop-has-all-paths (has-level-is-prop {n = ⟨-2⟩} {A = SeqCo C}) _ _

max_stars_repo_name: nicolaikraus/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module _ where

module M where

record S : Set₁ where
  open M
  field
    F1 : Set
    F2 : {!!}

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --without-K --no-pattern-matching #-}

module Ch2-9 where

open import Level hiding (lift)

open import Ch2-1
open import Ch2-2
open import Ch2-3
open import Ch2-4
open import Ch2-5
open import Ch2-6
open import Ch2-7
open import Ch2-8

open import Data.Product
open import Function using (id; _∘_)

-- happly (Definition 2.9.2)
happly : ∀ {a} {b} {A : Set a} {B : A → Set b}
  → {f g : (x : A) → B x}
  → (f ≡ g) → (f ~ g)
happly {_} {_} {A} {B} {f} {g} p = J ((x : A) → B x) D d f g p
  where
    D : (f g : (x : A) → B x) (p : f ≡ g) → Set _
    D f g p = f ~ g

    d : (x : (x : A) → B x) → D x x refl
    d f x = refl

postulate
  funext : ∀ {a} {b} {A : Set a} {B : A → Set b}
    → {f g : (x : A) → B x}
    → (f ~ g) → (f ≡ g)

Theorem-2-9-1 : ∀ {a} {b} {A : Set a} {B : A → Set b}
  → (f g : (x : A) → B x)
  → (f ≡ g) ≅ (f ~ g)
Theorem-2-9-1 {_} {_} {A} {B} f g = happly , (funext , α) , (funext , {!   !})

  where
    α : happly ∘ funext ~ id
    α p = J {!   !} D {!   !} f g (funext p)
      -- J ((x : A) → B x) D d f g (funext p)
      --
      where
        D : (f g : (x : A) → B x) (p : {!   !}) → Set _
        D f g p = {!   !}
          -- ((λ {x} → happly) ∘ funext) p ≡ id p
          -- ((λ {x} → happly) ∘ funext) p ≡ id p
          -- happly ∘ funext ~ id

        -- d : (x : (x : A) → B x) → D x x refl
        -- d x = refl

    -- happly-isequiv : isequiv (happly f g)
    -- happly-isequiv =

  -- where
  --   f : x ≡ y → ⊤
  --   f p = tt
  --
  --   f' : ⊤ → x ≡ y
  --   f' x = refl
  --
  --   α : (λ _ → f refl) ~ id
  --   α w = refl
  --
  --   β : (λ _ → refl) ~ id
  --   β w = J ⊤ D d x y w
  --     where
  --       D : (x y : ⊤) (p : x ≡ y) → Set _
  --       D x y p = refl ≡ id p
  --
  --       d : (x : ⊤) → D x x refl
  --       d x = refl
  --
  --   f-isequiv : isequiv f
  --   f-isequiv = (f' , α) , f' , β

max_stars_repo_name: banacorn/hott

max_issues_repo_name: banacorn/hott

max_forks_repo_name: banacorn/hott


text:
module Unique where

open import Category

module Uniq (ℂ : Cat) where

  private open module C = Cat ℂ

  -- We say that f ∈! P iff f is the unique arrow satisfying P.
  data _∈!_ {A B : Obj}(f : A ─→ B)(P : A ─→ B -> Set) : Set where
    unique : (forall g -> P g -> f == g) -> f ∈! P

  itsUnique : {A B : Obj}{f : A ─→ B}{P : A ─→ B -> Set} ->
	      f ∈! P -> (g : A ─→ B) -> P g -> f == g
  itsUnique (unique h) = h

  data ∃! {A B : Obj}(P : A ─→ B -> Set) : Set where
    witness : (f : A ─→ B) -> f ∈! P -> ∃! P

  getWitness : {A B : Obj}{P : A ─→ B -> Set} -> ∃! P -> A ─→ B
  getWitness (witness w _) = w

  uniqueWitness : {A B : Obj}{P : A ─→ B -> Set}(u : ∃! P) ->
		  getWitness u ∈! P
  uniqueWitness (witness _ u) = u

  witnessEqual : {A B : Obj}{P : A ─→ B -> Set} -> ∃! P ->
		 {f g : A ─→ B} -> P f -> P g -> f == g
  witnessEqual u {f} {g} pf pg = trans (sym hf) hg
    where
      h = getWitness u

      hf : h == f
      hf = itsUnique (uniqueWitness u) f pf

      hg : h == g
      hg = itsUnique (uniqueWitness u) g pg

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module MLib.Fin.Parts.Nat.Simple.Properties where

open import MLib.Prelude
open import MLib.Fin.Parts.Nat
import MLib.Fin.Parts.Nat.Simple as S

module P a b = Partsℕ (S.repl a b)

open Nat using (_*_; _+_; _<_)
open Fin using (toℕ; fromℕ≤)
open List

fromAny : ∀ a b → Any Fin (S.repl a b) → ℕ × ℕ
fromAny zero b ()
fromAny (suc a) b (here j) = 0 , Fin.toℕ j
fromAny (suc a) b (there js) =
  let i , j = fromAny a b js
  in suc i , j

intoPart-prop : ∀ a b {ps : Any Fin (S.repl a b)} → P.intoPart a b ps ≡ S.intoPart a b (fromAny a b ps)
intoPart-prop zero b {()}
intoPart-prop (suc a) b {here px} = ≡.sym (Nat.+-identityʳ _)
intoPart-prop (suc a) b {there ps} =
  let ind = intoPart-prop a b {ps}
      i , j = fromAny a b ps
      open ≡.Reasoning
      open Nat.SemiringSolver
  in begin
    b + Impl.intoPart ps ≡⟨ ≡.cong₂ _+_ ≡.refl ind ⟩
    b + (j + i * b)         ≡⟨ solve 3 (λ b j ib → b :+ (j :+ ib) := j :+ (b :+ ib)) ≡.refl b j (i * b) ⟩
    j + (b + i * b)       ∎

lem : ∀ a b {k} → k < a * b → k < sum (S.repl a b)
lem a b p = Nat.≤-trans p (Nat.≤-reflexive (≡.sym (S.sum-replicate-* a b)))

fromPart-prop : ∀ a b {k} → k < a * b → Maybe.map (fromAny a b) (Impl.fromPart (S.repl a b) k) ≡ just (S.fromPart a b k)
fromPart-prop zero b ()
fromPart-prop (suc a) b {k} p with Impl.compare′ k b
fromPart-prop (suc a) .(suc (m + k)) {.m} p | Impl.less m k = ≡.cong just (Σ.≡×≡⇒≡ (≡.refl , Fin.toℕ-fromℕ≤ _))
fromPart-prop (suc a) b {.(b + k)} p | Impl.gte .b k with Impl.fromPart (S.repl a b) k | fromPart-prop a b {k} (Nat.+-cancelˡ-< b p)
fromPart-prop (suc a) b {.(b + k)} p | Impl.gte .b k | just x | ind =
  let e1 , e2 = Σ.≡⇒≡×≡ (Maybe.just-injective ind)
  in ≡.cong just (Σ.≡×≡⇒≡ (≡.cong suc e1 , e2))
fromPart-prop (suc a) b {.(b + k)} p | Impl.gte .b k | nothing | ()

fromPart′-prop : ∀ a b {k} (p : k < a * b) → fromAny a b (P.fromPart a b {k} (lem a b p)) ≡ S.fromPart a b k
fromPart′-prop a b {k} p with Impl.fromPart (S.repl a b) k | Impl.fromPart-prop (S.repl a b) (lem a b p) | fromPart-prop a b p
fromPart′-prop a b {k} p | just x | y | z = Maybe.just-injective z
fromPart′-prop a b {k} p | nothing | () | z


text:
module Luau.Substitution where

open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; _⟨_⟩ ; name; fun; arg; number; binexp)
open import Luau.Value using (Value; val)
open import Luau.Var using (Var; _≡ⱽ_)
open import Properties.Dec using (Dec; yes; no)

_[_/_]ᴱ : ∀ {a} → Expr a → Value → Var → Expr a
_[_/_]ᴮ : ∀ {a} → Block a → Value → Var → Block a
var_[_/_]ᴱwhenever_ : ∀ {a P} → Var → Value → Var → (Dec P) → Expr a
_[_/_]ᴮunless_ : ∀ {a P} → Block a → Value → Var → (Dec P) → Block a

nil [ v / x ]ᴱ = nil
var y [ v / x ]ᴱ = var y [ v / x ]ᴱwhenever (x ≡ⱽ y)
addr a [ v / x ]ᴱ = addr a
(number y) [ v / x ]ᴱ = number y
(M $ N) [ v / x ]ᴱ = (M [ v / x ]ᴱ) $ (N [ v / x ]ᴱ)
function F is C end [ v / x ]ᴱ = function F is C [ v / x ]ᴮunless (x ≡ⱽ name(arg F)) end
block b is C end [ v / x ]ᴱ = block b is C [ v / x ]ᴮ end
(binexp e₁ op e₂) [ v / x ]ᴱ = binexp (e₁ [ v / x ]ᴱ) op (e₂ [ v / x ]ᴱ)

(function F is C end ∙ B) [ v / x ]ᴮ = function F is (C [ v / x ]ᴮunless (x ≡ⱽ name(arg F))) end ∙ (B [ v / x ]ᴮunless (x ≡ⱽ fun F))
(local y ← M ∙ B) [ v / x ]ᴮ = local y ← (M [ v / x ]ᴱ) ∙ (B [ v / x ]ᴮunless (x ≡ⱽ name y))
(return M ∙ B) [ v / x ]ᴮ = return (M [ v / x ]ᴱ) ∙ (B [ v / x ]ᴮ)
done [ v / x ]ᴮ = done

var y [ v / x ]ᴱwhenever yes p = val v
var y [ v / x ]ᴱwhenever no p = var y

B [ v / x ]ᴮunless yes p = B
B [ v / x ]ᴮunless no p = B [ v / x ]ᴮ


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

open import M-types.Base.Core
open import M-types.Base.Sum
open import M-types.Base.Prod
open import M-types.Base.Eq

module M-types.Base.Contr where
    IsContr : ∏[ X ∈ Ty ℓ ] Ty ℓ
    IsContr X = ∑[ x ∈ X ] ∏[ x′ ∈ X ] x′ ≡ x

    Contr : Ty (ℓ-suc ℓ)
    Contr {ℓ} = ∑[ X ∈ Ty ℓ ] IsContr X

max_stars_repo_name: DDOtten/M-types

max_issues_repo_name: DDOtten/M-types

max_forks_repo_name: DDOtten/M-types


text:
{-# OPTIONS --without-K #-}
module Model.Product where

open import Cats.Category
open import Data.Product using (<_,_>)

open import Model.Type.Core
open import Util.HoTT.HLevel
open import Util.Prelude hiding (_×_)

infixr 5 _×_

_×_ : ∀ {Γ} (T U : ⟦Type⟧ Γ) → ⟦Type⟧ Γ
T × U = record
  { ObjHSet = λ δ → T .ObjHSet δ ×-HSet U .ObjHSet δ
  ; eqHProp = λ where
      γ≈γ′ (x , x′) (y , y′) → T .eqHProp γ≈γ′ x y ×-HProp U .eqHProp γ≈γ′ x′ y′
  ; eq-refl = λ where
      (x , y) → T .eq-refl x , U .eq-refl y
  }

π₁ : ∀ {Γ} {T} (U : ⟦Type⟧ Γ) → T × U ⇒ T
π₁ U = record
  { fobj = proj₁
  ; feq = λ p → proj₁
  }

π₂ : ∀ {Γ} T {U : ⟦Type⟧ Γ} → T × U ⇒ U
π₂ T = record
  { fobj = proj₂
  ; feq = λ p → proj₂
  }

⟨_,_⟩ : ∀ {Γ} {X T U : ⟦Type⟧ Γ}
  → X ⇒ T → X ⇒ U → X ⇒ T × U
⟨ f , g ⟩ = record
  { fobj = < f .fobj , g .fobj >
  ; feq = λ γ≈γ′ → < f .feq γ≈γ′ , g .feq γ≈γ′ >
  }

instance
  hasBinaryProducts : ∀ {Γ} → HasBinaryProducts (⟦Types⟧ Γ)
  hasBinaryProducts .HasBinaryProducts._×′_ T U = record
    { prod = T × U
    ; proj = λ where
        true → π₁ U
        false → π₂ T
    ; isProduct = λ π′ → record
      { arr = ⟨ π′ true , π′ false ⟩
      ; prop = λ where
          true → ≈⁺ λ γ x → refl
          false → ≈⁺ λ γ x → refl
      ; unique = λ {f} f-prop → ≈⁺ λ γ x
          → cong₂ _,_ (f-prop true .≈⁻ γ x) (f-prop false .≈⁻ γ x)
      }
    }

open module ⟦Types⟧× {Γ}
  = HasBinaryProducts (hasBinaryProducts {Γ})
  public using
  ( ⟨_×_⟩ ) renaming
  ( ×-resp-≅ to ×-resp-≈⟦Type⟧ )

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
{-

This file contains:

Properties of the FreeGroup:
- FreeGroup A is Set, SemiGroup, Monoid, Group
- Recursion principle for the FreeGroup
- Induction principle for the FreeGroup on hProps
- Condition for the equality of Group Homomorphisms from FreeGroup
- Equivalence of the types (A → Group .fst) (GroupHom (freeGroupGroup A) Group)

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

module Cubical.HITs.FreeGroup.Properties where

open import Cubical.HITs.FreeGroup.Base

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Path
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.BiInvertible

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Monoid.Base
open import Cubical.Algebra.Semigroup.Base

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ

freeGroupIsSet : isSet (FreeGroup A)
freeGroupIsSet = trunc

freeGroupIsSemiGroup : IsSemigroup {A = FreeGroup A} _·_
freeGroupIsSemiGroup = issemigroup freeGroupIsSet assoc

freeGroupIsMonoid : IsMonoid {A = FreeGroup A} ε _·_
freeGroupIsMonoid = ismonoid freeGroupIsSemiGroup (λ x → sym (idr x)) (λ x → sym (idl x))

freeGroupIsGroup : IsGroup {G = FreeGroup A} ε _·_ inv
freeGroupIsGroup = isgroup freeGroupIsMonoid invr invl

freeGroupGroupStr : GroupStr (FreeGroup A)
freeGroupGroupStr = groupstr ε _·_ inv freeGroupIsGroup

-- FreeGroup is indeed a group
freeGroupGroup : Type ℓ → Group ℓ
freeGroupGroup A = FreeGroup A , freeGroupGroupStr

-- The recursion principle for the FreeGroup
rec : {Group : Group ℓ'} → (A → Group .fst) → GroupHom (freeGroupGroup A) Group
rec {Group = G , groupstr 1g _·g_ invg (isgroup (ismonoid isSemigroupg ·gIdR ·gIdL) ·gInvR ·gInvL)} f = f' , isHom
  where
  f' : FreeGroup _ → G
  f' (η a)                  = f a
  f' (g1 · g2)              = (f' g1) ·g (f' g2)
  f' ε                      = 1g
  f' (inv g)                = invg (f' g)
  f' (assoc g1 g2 g3 i)     = IsSemigroup.·Assoc isSemigroupg (f' g1) (f' g2) (f' g3) i
  f' (idr g i)              = sym (·gIdR (f' g)) i
  f' (idl g i)              = sym (·gIdL (f' g)) i
  f' (invr g i)             = ·gInvR (f' g) i
  f' (invl g i)             = ·gInvL (f' g) i
  f' (trunc g1 g2 p q i i₁) = IsSemigroup.is-set isSemigroupg (f' g1) (f' g2) (cong f' p) (cong f' q) i i₁

  isHom : IsGroupHom freeGroupGroupStr f' _
  IsGroupHom.pres·   isHom = λ g1 g2 → refl
  IsGroupHom.pres1   isHom = refl
  IsGroupHom.presinv isHom = λ g → refl

-- The induction principle for the FreeGroup for hProps
elimProp : {B : FreeGroup A → Type ℓ'}
         → ((x : FreeGroup A) → isProp (B x))
         → ((a : A) → B (η a))
         → ((g1 g2 : FreeGroup A) → B g1 → B g2 → B (g1 · g2))
         → (B ε)
         → ((g : FreeGroup A) → B g → B (inv g))
         → (x : FreeGroup A)
         → B x
elimProp {B = B} Bprop η-ind ·-ind ε-ind inv-ind = induction where
  induction : ∀ g → B g
  induction (η a) = η-ind a
  induction (g1 · g2) = ·-ind g1 g2 (induction g1) (induction g2)
  induction ε = ε-ind
  induction (inv g) = inv-ind g (induction g)
  induction (assoc g1 g2 g3 i) = path i where
    p1 : B g1
    p1 = induction g1
    p2 : B g2
    p2 = induction g2
    p3 : B g3
    p3 = induction g3
    path : PathP (λ i → B (assoc g1 g2 g3 i)) (·-ind g1 (g2 · g3) p1 (·-ind g2 g3 p2 p3))
                                              (·-ind (g1 · g2) g3 (·-ind g1 g2 p1 p2) p3)
    path = isProp→PathP (λ i → Bprop (assoc g1 g2 g3 i)) (·-ind g1 (g2 · g3) p1 (·-ind g2 g3 p2 p3))
                                                         (·-ind (g1 · g2) g3 (·-ind g1 g2 p1 p2) p3)
  induction (idr g i) = path i where
    p : B g
    p = induction g
    pε : B ε
    pε = induction ε
    path : PathP (λ i → B (idr g i)) p (·-ind g ε p pε)
    path = isProp→PathP (λ i → Bprop (idr g i)) p (·-ind g ε p pε)
  induction (idl g i) = path i where
    p : B g
    p = induction g
    pε : B ε
    pε = induction ε
    path : PathP (λ i → B (idl g i)) p (·-ind ε g pε p)
    path = isProp→PathP (λ i → Bprop (idl g i)) p (·-ind ε g pε p)
  induction (invr g i) = path i where
    p : B g
    p = induction g
    pinv : B (inv g)
    pinv = inv-ind g p
    pε : B ε
    pε = induction ε
    path : PathP (λ i → B (invr g i)) (·-ind g (inv g) p pinv) pε
    path = isProp→PathP (λ i → Bprop (invr g i)) (·-ind g (inv g) p pinv) pε
  induction (invl g i) = path i where
    p : B g
    p = induction g
    pinv : B (inv g)
    pinv = inv-ind g p
    pε : B ε
    pε = induction ε
    path : PathP (λ i → B (invl g i)) (·-ind (inv g) g pinv p) pε
    path = isProp→PathP (λ i → Bprop (invl g i)) (·-ind (inv g) g pinv p) pε
  induction (trunc g1 g2 q1 q2 i i₁) = square i i₁ where
    p1 : B g1
    p1 = induction g1
    p2 : B g2
    p2 = induction g2
    dq1 : PathP (λ i → B (q1 i)) p1 p2
    dq1 = cong induction q1
    dq2 : PathP (λ i → B (q2 i)) p1 p2
    dq2 = cong induction q2
    square : SquareP (λ i i₁ → B (trunc g1 g2 q1 q2 i i₁))
                {a₀₀ = p1} {a₀₁ = p2} dq1
                {a₁₀ = p1} {a₁₁ = p2} dq2
                (cong induction (refl {x = g1})) (cong induction (refl {x = g2}))
    square = isProp→SquareP (λ i i₁ → Bprop (trunc g1 g2 q1 q2 i i₁))
             (cong induction (refl {x = g1})) (cong induction (refl {x = g2}))
             dq1 dq2

-- Two group homomorphisms from FreeGroup to G are the same if they agree on every a : A
freeGroupHom≡ : {Group : Group ℓ'}{f g : GroupHom (freeGroupGroup A) Group}
               → (∀ a → (fst f) (η a) ≡ (fst g) (η a)) → f ≡ g
freeGroupHom≡ {Group = G , (groupstr 1g _·g_ invg isGrp)} {f} {g} eqOnA = GroupHom≡ (funExt pointwise) where
  B : ∀ x → Type _
  B x = (fst f) x ≡ (fst g) x
  Bprop : ∀ x → isProp (B x)
  Bprop x = (isSetGroup (G , groupstr 1g _·g_ invg isGrp)) ((fst f) x) ((fst g) x)
  η-ind : ∀ a → B (η a)
  η-ind = eqOnA
  ·-ind : ∀ g1 g2 → B g1 → B g2 → B (g1 · g2)
  ·-ind g1 g2 ind1 ind2 =
    (fst f) (g1 · g2)
    ≡⟨ IsGroupHom.pres· (f .snd) g1 g2 ⟩
    ((fst f) g1) ·g ((fst f) g2)
    ≡⟨ cong (λ x → x ·g ((fst f) g2)) ind1 ⟩
    ((fst g) g1) ·g ((fst f) g2)
    ≡⟨ cong (λ x → ((fst g) g1) ·g x) ind2 ⟩
    ((fst g) g1) ·g ((fst g) g2)
    ≡⟨ sym (IsGroupHom.pres· (g .snd) g1 g2) ⟩
    (fst g) (g1 · g2) ∎
  ε-ind : B ε
  ε-ind =
    (fst f) ε
    ≡⟨ IsGroupHom.pres1 (f .snd) ⟩
    1g
    ≡⟨ sym (IsGroupHom.pres1 (g .snd)) ⟩
    (fst g) ε ∎
  inv-ind : ∀ x → B x → B (inv x)
  inv-ind x ind =
    (fst f) (inv x)
    ≡⟨ IsGroupHom.presinv (f .snd) x ⟩
    invg ((fst f) x)
    ≡⟨ cong invg ind ⟩
    invg ((fst g) x)
    ≡⟨ sym (IsGroupHom.presinv (g .snd) x) ⟩
    (fst g) (inv x) ∎
  pointwise : ∀ x → (fst f) x ≡ (fst g) x
  pointwise = elimProp Bprop η-ind ·-ind ε-ind inv-ind

-- The type of Group Homomorphisms from the FreeGroup A into G
-- is equivalent to the type of functions from A into G .fst
A→Group≃GroupHom : {Group : Group ℓ'} → (A → Group .fst) ≃ GroupHom (freeGroupGroup A) Group
A→Group≃GroupHom {Group = Group} = biInvEquiv→Equiv-right biInv where
  biInv : BiInvEquiv (A → Group .fst) (GroupHom (freeGroupGroup A) Group)
  BiInvEquiv.fun  biInv              = rec
  BiInvEquiv.invr biInv (hom , _) a  = hom (η a)
  BiInvEquiv.invr-rightInv biInv hom = freeGroupHom≡ (λ a → refl)
  BiInvEquiv.invl biInv (hom ,  _) a = hom (η a)
  BiInvEquiv.invl-leftInv biInv f    = funExt (λ a → refl)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- Andreas, 2013-11-11 Better error for wrongly named implicit arg.
module Issue949 where

postulate
  S   : Set
  F   : {A : Set} → Set
  ok  : F {A = S}
  err : F {B = S}

-- Old error:
--
-- Set should be a function type, but it isn't
-- when checking that {B = S} are valid arguments to a function of
-- type Set

-- New error (after fixing also issue 951):
--
-- Function does not accept argument {B = _}
-- when checking that {B = S} are valid arguments to a function of
-- type {A : Set} → Set


text:
open import Common.Prelude
open import Common.Reflect

module TermSplicingLooping where

mutual
  f : Set -> Set
  f = unquote (def (quote f) [])


text:
module Lec1Start where

-- the -- mark introduces a "comment to end of line"

------------------------------------------------------------------------------
-- some basic "logical" types
------------------------------------------------------------------------------

data Zero : Set where
  -- to give a value in a data, choose one constructor
  -- there are no constructors
  -- so that's impossible

record One : Set where
  -- to give a value in a record type, fill all its fields
  -- there are no fields
  -- so that's trivial
  --   (can we have a constructor, for convenience?)

data _+_ (S : Set)(T : Set) : Set where -- "where" wants an indented block
  -- to offer a choice of constructors, list them with their types
  inl : S -> S + T     -- constructors can pack up stuff
  inr : T -> S + T
  -- in Haskell, this was called "Either S T"

record _*_ (S : Set)(T : Set) : Set where
  field -- introduces a bunch of fields, listed with their types
    fst : S
    snd : T
  -- in Haskell, this was called "(S, T)"

------------------------------------------------------------------------------
-- some simple proofs
------------------------------------------------------------------------------

{-+}
comm-* : {A : Set}{B : Set} -> A * B -> B * A
comm-* x = ?
{+-}

{-+}
assocLR-+ : {A B C : Set} -> (A + B) + C -> A + (B + C)
assocLR-+ x = ?
{+-}

{-+}
_$*_ : {A A' B B' : Set} -> (A -> A') -> (B -> B') -> A * B -> A' * B'
(f $* g) x = r?
{+-}

-- record syntax is rather ugly for small stuff; can we have constructors?

{-+}
_$+_ : {A A' B B' : Set} -> (A -> A') -> (B -> B') -> A + B -> A' + B'
(f $+ g) x = ?
{+-}

{-+}
combinatorK : {A E : Set} -> A -> E -> A
combinatorK = ?

combinatorS : {S T E : Set} -> (E -> S -> T) -> (E -> S) -> E -> T
combinatorS = ?
{+-}

{-+}
id : {X : Set} -> X -> X
-- id x = x -- is the easy way; let's do it a funny way to make a point
id = ?
{+-}

{-+}
naughtE : {X : Set} -> Zero -> X
naughtE x = ?
{+-}

------------------------------------------------------------------------------
-- from logic to data
------------------------------------------------------------------------------

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat     -- recursive data type

{-# BUILTIN NATURAL Nat #-}
--  ^^^^^^^^^^^^^^^^^^^       this pragma lets us use decimal notation

{-+}
_+N_ : Nat -> Nat -> Nat
x +N y = ?

four : Nat
four = 2 +N 2
{+-}

------------------------------------------------------------------------------
-- and back to logic
------------------------------------------------------------------------------

{-+}
data _==_ {X : Set} : X -> X -> Set where
  refl : (x : X) -> x == x           -- the relation that's "only reflexive"

{-# BUILTIN EQUALITY _==_ #-}  -- we'll see what that's for, later

_=$=_ : {X Y : Set}{f f' : X -> Y}{x x' : X} ->
        f == f' -> x == x' -> f x == f' x'
fq =$= xq = ?
{+-}

{-+}
zero-+N : (n : Nat) -> (zero +N n) == n
zero-+N n = ?

+N-zero : (n : Nat) -> (n +N zero) == n
+N-zero n = ?

assocLR-+N : (x y z : Nat) -> ((x +N y) +N z) == (x +N (y +N z))
assocLR-+N x y z = ?
{+-}

------------------------------------------------------------------------------
-- computing types
------------------------------------------------------------------------------

{-+}
_>=_ : Nat -> Nat -> Set
x     >= zero   = One
zero  >= suc y  = Zero
suc x >= suc y  = x >= y

refl->= : (n : Nat) -> n >= n
refl->= n = {!!}

trans->= : (x y z : Nat) -> x >= y -> y >= z -> x >= z
trans->= x y z x>=y y>=z = {!!}
{+-}

------------------------------------------------------------------------------
-- construction by proof
------------------------------------------------------------------------------

{-+}
record Sg (S : Set)(T : S -> Set) : Set where  -- Sg is short for "Sigma"
  constructor _,_
  field -- introduces a bunch of fields, listed with their types
    fst : S
    snd : T fst
-- make _*_ from Sg ?

difference : (m n : Nat) -> m >= n -> Sg Nat \ d -> m == (n +N d)
                                   --       (                    )
difference m       zero    m>=n = m , refl m
difference zero    (suc n) ()
difference (suc m) (suc n) m>=n with difference m n m>=n
difference (suc m) (suc n) m>=n | d , q = d , (refl suc =$= q)

tryMe      = difference 42 37 _
don'tTryMe = difference 37 42 {!!}
{+-}

------------------------------------------------------------------------------
-- things to remember to say
------------------------------------------------------------------------------

-- why the single colon?

-- what's with all the spaces?

-- what's with identifiers mixing letters and symbols?

-- what's with all the braces?

-- what is Set?

-- are there any lowercase/uppercase conventions?

-- what's with all the underscores?
--   (i)   placeholders in mixfix operators
--   (ii)  don't care (on the left)
--   (iii) go figure (on the right)

-- why use arithmetic operators for types?

-- what's the difference between = and == ?

-- can't we leave out cases?

-- can't we loop?

-- the function type is both implication and universal quantification,
-- but why is it called Pi?

-- why is Sigma called Sigma?

-- B or nor B?

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

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

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


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Comonad.Relative where

open import Level

open import Categories.Category using (Category)
open import Categories.Functor using (Functor; Endofunctor; _∘F_) renaming (id to idF)
import Categories.Morphism.Reasoning as MR
open import Categories.NaturalTransformation renaming (id to idN)
open import Categories.NaturalTransformation.NaturalIsomorphism hiding (_≃_)
open import Categories.NaturalTransformation.Equivalence
open NaturalIsomorphism

private
  variable
    o ℓ e o′ ℓ′ e′ : Level
    C : Category o ℓ e
    D : Category o′ ℓ′ e′

record Comonad {C : Category o ℓ e} {D : Category o′ ℓ′ e′} (J : Functor C D) : Set (o ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  private
    module C = Category C
    module D = Category D
    module J = Functor J
    open D using (_⇒_; _∘_; _≈_)
  field
    F₀ : C.Obj → D.Obj
    counit : {c : C.Obj} → F₀ c ⇒ J.₀ c
    cobind : {x y : C.Obj} → (F₀ x ⇒ J.₀ y) → F₀ x ⇒ F₀ y
    identityʳ : {x y : C.Obj} { k : F₀ x ⇒ J.₀ y} → counit ∘ cobind k ≈ k
    identityˡ : {x : C.Obj} → cobind {x} counit ≈ D.id
    assoc : {x y z : C.Obj} {k : F₀ x ⇒ J.₀ y} {l : F₀ y ⇒ J.₀ z} →
      cobind (l ∘ cobind k) ≈ cobind l ∘ cobind k
    cobind-≈ : {x y : C.Obj} {k h : F₀ x ⇒ J.₀ y} → k ≈ h → cobind k ≈ cobind h

-- From a Relative Comonad, we can extract a functor
RComonad⇒Functor : {J : Functor C D} → Comonad J → Functor C D
RComonad⇒Functor {C = C} {D = D} {J = J} r = record
  { F₀ = F₀
  ; F₁ = λ f → cobind (J.₁ f ∘ counit)
  ; identity = identity′
  ; homomorphism = hom′
  ; F-resp-≈ = λ f≈g → cobind-≈ (∘-resp-≈ˡ (J.F-resp-≈ f≈g))
  }
  where
  open Comonad r
  module C = Category C
  module D = Category D
  module J = Functor J
  open Category D hiding (identityˡ; identityʳ; assoc)
  open HomReasoning
  open MR D
  identity′ : {c : C.Obj} → cobind {c} (J.₁ C.id ∘ counit) ≈ id
  identity′ = begin
     cobind (J.₁ C.id ∘ counit) ≈⟨ cobind-≈ (elimˡ J.identity) ⟩
     cobind counit              ≈⟨ identityˡ ⟩
     id                         ∎
  hom′ : {X Y Z : C.Obj} {f : X C.⇒ Y} {g : Y C.⇒ Z} →
      cobind (J.₁ (g C.∘ f) ∘ counit) ≈ cobind (J.₁ g ∘ counit) ∘ cobind (J.₁ f ∘ counit)
  hom′ {f = f} {g} = begin
    cobind (J.₁ (g C.∘ f) ∘ counit)                         ≈⟨ cobind-≈ (pushˡ J.homomorphism) ⟩
    cobind (J.₁ g ∘ J.₁ f ∘ counit)                         ≈⟨ cobind-≈ (pushʳ (⟺ identityʳ)) ⟩
    cobind ((J.₁ g ∘ counit) ∘ (cobind (J.F₁ f ∘ counit)))  ≈⟨ assoc ⟩
    cobind (J.₁ g ∘ counit) ∘ cobind (J.F₁ f ∘ counit)      ∎

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:
-- This is an implementation of the equality type for Sets. Agda's
-- standard equality is more powerful. The main idea here is to
-- illustrate the equality type.
module Equality where

open import Level
-- The equality of two elements of type A. The type a ≡ b is a family
-- of types which captures the statement of equality in A. Not all of
-- the types are inhabited as in general not all elements are equal
-- here. The only type that are inhabited are a ≡ a by the element
-- that we call definition. This is called refl (for reflection in
-- agda).
data _≡_  {ℓ} {A : Set ℓ} : (a b : A) → Set ℓ where
  refl : {x : A} → x ≡ x

-- ≡ is a symmetric relation.
sym : ∀{ℓ} {A : Set ℓ} {a b : A} → a ≡ b → b ≡ a
sym refl = refl

-- ≡ is a transitive relation.
trans : ∀ {ℓ} {A : Set ℓ} {a b c : A} → a ≡ b → b ≡ c → a ≡ c
trans pAB refl = pAB
-- trans refl pBC = pBC  -- alternate proof of transitivity.

-- Congruence. If we apply f to equals the result are also equal.
cong : ∀{ℓ₀ ℓ₁} {A : Set ℓ₀} {B : Set ℓ₁}
       {a₀ a₁ : A} → (f : A → B) → a₀ ≡ a₁ → f a₀ ≡ f a₁
cong f refl = refl

-- Pretty way of doing equational reasoning.  If we want to prove a₀ ≡
-- b through an intermediate set of equations use this. The general
-- form will look like.
--
-- begin a  ≈ a₀ by p₀
--          ≈ a₁ by p₁
--          ...
--          ≈ b  by p
-- ∎

begin : ∀{ℓ} {A : Set ℓ} (a : A) →  a ≡ a
_≈_by_ : ∀{ℓ} {A : Set ℓ} {a b : A} → a ≡ b → (c : A) → b ≡ c → a ≡ c
_∎ : ∀{ℓ} {A : Set ℓ} (a : A) → A

begin a = refl
aEb ≈ c by bEc = trans aEb bEc
x ∎ = x

infixl 1 _≈_by_
infixl 1 _≡_

max_stars_repo_name: piyush-kurur/sample-code

max_issues_repo_name: piyush-kurur/sample-code

max_forks_repo_name: piyush-kurur/sample-code


text:
{-# OPTIONS --copatterns --sized-types #-}

open import Level
open import Algebra.Structures
open import Relation.Binary
open import Algebra.FunctionProperties

module Comb (K : Set) (_≈_ : Rel K zero)
         (_+_ _⋆_ : Op₂ K) (-_ : Op₁ K) (0# 1# : K)
         (isRing : IsRing _≈_ _+_ _⋆_ -_ 0# 1#) where

open import Size
open import Function hiding (const)
open import Relation.Nullary
open import Stream
open import Data.Nat renaming (_+_ to _+ℕ_)
open import Data.Fin hiding (_+_)
open import Data.Product hiding (_×_)
open import Data.Empty
open import Relation.Binary.PropositionalEquality as P
  using (_≡_) --; refl; sym; trans; cong; module ≡-Reasoning)

K-setoid : Setoid _ _
K-setoid = record { Carrier = K
                  ; _≈_ = _≈_
                  ; isEquivalence = IsRing.isEquivalence isRing }

open Bisim K-setoid
import Relation.Binary.EqReasoning as EqR
open EqR (K-setoid) public hiding (_≡⟨_⟩_)
--open IsEquivalence (IsRing.isEquivalence isRing)
open ∼-Reasoning renaming (begin_ to begin∼_; _∎ to _∎∼)

open IsRing isRing -- using (+-cong ; +-identity)
+-identityˡ = proj₁ +-identity
+-identityʳ = proj₂ +-identity

-- zeroʳ : RightZero 0# _⋆_
-- zeroʳ = ?

----------------------
--- Basic operators --
----------------------

const : ∀ {A} → A → Str A
hd (const x) = x
tl (const x) = const x

-- | Point-wise unary operations
pw₁ : ∀ {A i} → Op₁ A → Op₁ (Str {i} A)
hd (pw₁ f σ) = f (hd σ)
tl (pw₁ f σ) = pw₁ f (tl σ)

-- | Point-wise binary operations
pw₂ : ∀ {A i} → Op₂ A → Op₂ (Str {i} A)
hd (pw₂ f σ τ) = f (hd σ) (hd τ)
tl (pw₂ f σ τ) = pw₂ f (tl σ) (tl τ)

[_] : K → Str K
hd [ r ] = r
tl [ r ] = [ 0# ]

-- | Can, in conjunction with _×_, delay stream.
X : Str K
hd X = 0#
tl X = [ 1# ]

_⊕_ : ∀{i} → Str {i} K → Str {i} K → Str {i} K
_⊕_ = pw₂ _+_

⊝_ : ∀{i} → Str {i} K → Str {i} K
⊝_ = pw₁ (-_)

_×_ : ∀ {i} → Str {i} K → Str {i} K → Str {i} K
hd (σ × τ) = hd σ ⋆ hd τ
tl (σ × τ) = (tl σ × τ) ⊕ ([ hd σ ] × tl τ)

-- | We restrict attention to the case where the head is 1,
-- which is trivially invertible in any ring.
hasInv : ∀ {i} → Str {i} K → Set
hasInv σ = hd σ ≈ 1#

-- | Construct convolution inverse, if it exists.
inv : ∀ {i} → (σ : Str {i} K) → hasInv σ → Str {i} K
hd (inv σ p) = hd σ
tl (inv σ p) = ⊝ (tl σ × inv σ p)

-- | Powers of delay stream
X^_ : ℕ → Str K
X^ 0 = [ 1# ]
X^ (suc k) = X × (X^ k)

{-
record Summable (σ : Str (Str K)) : Set where
  coinductive
  field
    hd-smble : ∃ λ n → δ n (hd σ) ∼ [ 0# ]
    tl-smble : Summable (tl σ)
open Summable
-}

SummableDiag : {A : Set} (f : A → K) → Set
SummableDiag {A} f =
  ∃ λ n →
  Σ (Fin n → A) (λ g →
  (a : A) → ¬ ((f a) ≈ 0#) → ∃ λ i → a ≡ g i)

record Summable {A : Set} (f : A → Str K) : Set where
  coinductive
  field
    hd-smble : SummableDiag (hd ∘ f)
    tl-smble : Summable (tl' ∘ f)
open Summable

-- | Sum a finitely indexed family of elements of K.
-- This relies on commutativity etc. of addition in K.
sum : {n : ℕ} → (Fin n → K) → K
sum {ℕ.zero}  f = 0#
sum {ℕ.suc n} f = f Fin.zero + sum (f ∘ Fin.suc)

-- | Sum a family of streams.
∑ : ∀ {A} → (f : A → Str K) → Summable f → Str K
hd (∑ f p) =
  let (_ , g , _) = hd-smble p
  in  sum (hd ∘ f ∘ g)
tl (∑ f p) = ∑ (tl' ∘ f) (tl-smble p)

-- | Constant family of zero streams is summable
zero-summable : Summable {ℕ} (λ n → [ 0# ])
hd-smble zero-summable
  = (0 , f , q)
  where
    f : Fin 0 → ℕ
    f ()

    q : (n : ℕ) → ¬ (hd [ 0# ] ≈ 0#) → ∃ λ i → n ≡ f i
    q n p = ⊥-elim (p (IsRing.refl isRing))
tl-smble zero-summable = zero-summable

polySeq : ∀{i} → Str {i} (Str K) → Str {i} (Str K)
hd (polySeq σ) = hd σ × (X^ 0)
tl (polySeq σ) = pw₂ _×_ (polySeq (tl σ)) (const X)

polySeq₁ : Str (Str K) → (ℕ → Str K)
polySeq₁ σ = _at_ (polySeq σ)

polySeq₂ : (ℕ → Str K) → (ℕ → Str K)
polySeq₂ f = polySeq₁ (toStr f)

polySeq-summable : (σ : Str (Str K)) → Summable (polySeq₁ σ)
hd-smble (polySeq-summable σ) = q
  where
    q : SummableDiag (hd ∘ polySeq₁ σ)
    q = {!!}
tl-smble (polySeq-summable σ) = {!!}

{-
polySeq-expl : (σ : Str (Str K)) → (i : ℕ) → (polySeq σ at i) ≡ (σ at i) × (X^ i)
polySeq-expl σ zero    = refl
polySeq-expl σ (suc i) =
  polySeq σ at (ℕ.suc i)
    ≡⟨ ? ⟩
  (σ at (ℕ.suc i)) × (X × (X^ i))
    ∎
-}

-- lem : {f : ℕ → Str K} {k n : ℕ} → ¬ (polySeq f k at n) ≈ 0# → k ≡ n
-- lem = {!!}

{-
polySeq-summable-aux : {f : ℕ → Str K} →
                       (n : ℕ) → (g : ℕ → Str K) → Summable (polySeq f)
hd-smble (polySeq-summable-aux f n) = (1 , supp , {!!})
  where
    p = polySeq f

    supp : Fin 1 → ℕ
    supp Fin.zero = n
    supp (Fin.suc ())

    is-supp : (k : ℕ) → ¬ (hd (p k) ≈ 0#) → ∃ λ i → k ≡ supp i
    is-supp k q = (Fin.zero , {!!})

tl-smble (polySeq-summable-aux f n) = {!!}
-}

hd-delay-zero : (σ : Str K) → hd (X × σ) ≈ 0#
hd-delay-zero σ = zeroˡ (hd σ)
  where
    open IsNearSemiring (IsRing.isNearSemiring isRing)

⊕-cong : ∀ {i s t u v} → s ∼[ i ] t → u ∼[ i ] v → (s ⊕ u) ∼[ i ] (t ⊕ v)
hd≈ (⊕-cong s~t u~v) = +-cong (hd≈ s~t) (hd≈ u~v)
tl∼ (⊕-cong s~t u~v) = ⊕-cong (tl∼ s~t) (tl∼ u~v)

⊕-unitˡ : ∀ {i} → LeftIdentity (_∼_ {i}) [ 0# ] _⊕_
hd≈ (⊕-unitˡ s) = proj₁ +-identity (hd s)
tl∼ (⊕-unitˡ s) = ⊕-unitˡ (tl s)

⊕-comm : ∀ {i} → Commutative (_∼_ {i}) _⊕_
hd≈ (⊕-comm s t) = +-comm (hd s) (hd t)
tl∼ (⊕-comm s t) = ⊕-comm (tl s) (tl t)

⊕-unitʳ : ∀ {i} → RightIdentity (_∼_ {i}) [ 0# ] _⊕_
⊕-unitʳ s =
  s-bisim-trans
  (⊕-comm s [ 0# ])
  (⊕-unitˡ s)

×-zeroˡ : ∀ {i} → LeftZero (_∼_ {i}) [ 0# ] _×_
hd≈ (×-zeroˡ s) = zeroˡ (hd s)
  where
    open IsNearSemiring (IsRing.isNearSemiring isRing)
tl∼ (×-zeroˡ s) {j} =
  s-bisim-trans
  (⊕-cong {j} (×-zeroˡ s) (×-zeroˡ (tl s)))
  (⊕-unitˡ [ 0# ])

×-unitˡ : ∀ {i} → LeftIdentity (_∼_ {i}) [ 1# ] _×_
hd≈ (×-unitˡ s) = proj₁ *-identity (hd s)
tl∼ (×-unitˡ s) {j} =
  s-bisim-trans
  (⊕-cong {j} (×-zeroˡ s) (×-unitˡ (tl s)))
  (⊕-unitˡ (tl s))

tl-delay-id : (σ : Str K) → tl (X × σ) ∼ σ
tl-delay-id σ =
  begin∼
    tl (X × σ)
  ∼⟨ S.refl ⟩
    (tl X × σ) ⊕ ([ hd X ] × tl σ)
  ∼⟨ S.refl ⟩
    ([ 1# ] × σ) ⊕ ([ 0# ] × tl σ)
  ∼⟨ ⊕-cong (×-unitˡ σ) (×-zeroˡ (tl σ)) ⟩
    σ ⊕ [ 0# ]
  ∼⟨ ⊕-unitʳ σ ⟩
    σ
  ∎∼
  where
    module S = Setoid stream-setoid

-- | The analogue of the fundamental theorem
decomp-str : (σ : Str K) → σ ∼ ([ hd σ ] ⊕ (X × tl σ))
hd≈ (decomp-str σ) =
    begin
  hd σ
    ≈⟨ sym (+-identityʳ (hd σ)) ⟩
  hd σ + 0#
    ≈⟨ sym (+-cong refl (hd-delay-zero (tl σ))) ⟩
  hd [ hd σ ] + hd (X × tl σ)
    ≈⟨ refl ⟩
  hd ([ hd σ ] ⊕ (X × tl σ))
    ∎
tl∼ (decomp-str σ) =
  begin∼
    tl σ
  ∼⟨ S.sym (tl-delay-id (tl σ)) ⟩
    tl (X × tl σ)
  ∼⟨ S.sym (⊕-unitˡ (tl (X × tl σ))) ⟩
    [ 0# ] ⊕ tl (X × tl σ)
  ∼⟨ S.refl ⟩
    tl ([ hd σ ] ⊕ (X × tl σ))
  ∎∼
  where
    module S = Setoid stream-setoid

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
-- We apply the theory of quasi equivalence relations (QERs) to finite multisets and association lists.
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Relation.ZigZag.Applications.MultiSet where

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.RelationalStructure
open import Cubical.Foundations.Structure
open import Cubical.Foundations.SIP
open import Cubical.Foundations.Univalence
open import Cubical.Data.Unit
open import Cubical.Data.Empty
open import Cubical.Data.Nat
open import Cubical.Data.List hiding ([_])
open import Cubical.Data.Sigma
open import Cubical.HITs.SetQuotients
open import Cubical.HITs.FiniteMultiset as FMS hiding ([_])
open import Cubical.HITs.FiniteMultiset.CountExtensionality
open import Cubical.Relation.Nullary
open import Cubical.Relation.ZigZag.Base

open import Cubical.Structures.MultiSet
open import Cubical.Structures.Relational.Macro

-- we define simple association lists without any higher constructors
data AList {ℓ} (A : Type ℓ) : Type ℓ where
 ⟨⟩ : AList A
 ⟨_,_⟩∷_ : A → ℕ → AList A → AList A

infixr 5 ⟨_,_⟩∷_

private
 variable
  ℓ : Level
  A : Type ℓ

-- We have a CountStructure on List and AList and use these to get a QER between the two
module Lists&ALists {A : Type ℓ} (discA : Discrete A) where

 module S = RelMacro ℓ (param A (recvar (constant (ℕ , isSetℕ))))

 ι = CountEquivStr A (Discrete→isSet discA)

 -- the CountStructures
 aux : (a x : A) → Dec (a ≡ x) → ℕ → ℕ
 aux a x (yes a≡x) n = suc n
 aux a x (no  a≢x) n = n

 Lcount : S.structure (List A)
 Lcount a [] = zero
 Lcount a (x ∷ xs) = aux a x (discA a x) (Lcount a xs)

 ALcount : S.structure (AList A)
 ALcount a ⟨⟩ = zero
 ALcount a (⟨ x , zero ⟩∷ xs) = ALcount a xs
 ALcount a (⟨ x , suc n ⟩∷ xs) = aux a x (discA a x) (ALcount a (⟨ x , n ⟩∷ xs))

 -- now for the QER between List and Alist

 R : List A → AList A → Type ℓ
 R xs ys = ∀ a → Lcount a xs ≡ ALcount a ys

 φ : List A → AList A
 φ [] = ⟨⟩
 φ (x ∷ xs) = ⟨ x , 1 ⟩∷ φ xs

 ψ : AList A → List A
 ψ ⟨⟩ = []
 ψ (⟨ x , zero ⟩∷ xs) = ψ xs
 ψ (⟨ x , suc n ⟩∷ xs) = x ∷ ψ (⟨ x , n ⟩∷ xs)

 η : ∀ x → R x (φ x)
 η [] a = refl
 η (x ∷ xs) a with (discA a x)
 ...          | yes a≡x = cong suc (η xs a)
 ...          | no  a≢x = η xs a

 -- for the other direction we need a little helper function
 ε : ∀ y → R (ψ y) y
 ε' : (x : A) (n : ℕ) (xs : AList A) (a : A)
    → Lcount a (ψ (⟨ x , n ⟩∷ xs)) ≡ ALcount a (⟨ x , n ⟩∷ xs)

 ε ⟨⟩ a = refl
 ε (⟨ x , n ⟩∷ xs) a = ε' x n xs a

 ε' x zero xs a = ε xs a
 ε' x (suc n) xs a with discA a x
 ...                 | yes a≡x = cong suc (ε' x n xs a)
 ...                 | no  a≢x = ε' x n xs a

 -- Induced quotients and equivalence

 open isQuasiEquivRel

 -- R is a QER
 QuasiR : QuasiEquivRel _ _ ℓ
 QuasiR .fst .fst = R
 QuasiR .fst .snd _ _ = isPropΠ λ _ → isSetℕ _ _
 QuasiR .snd .zigzag r r' r'' a = (r a) ∙∙ sym (r' a) ∙∙ (r'' a)
 QuasiR .snd .fwd = φ
 QuasiR .snd .fwdRel = η
 QuasiR .snd .bwd = ψ
 QuasiR .snd .bwdRel = ε

 module E = QER→Equiv QuasiR
 open E renaming (Rᴸ to Rᴸ; Rᴿ to Rᴬᴸ)

 List/Rᴸ = (List A) / Rᴸ
 AList/Rᴬᴸ = (AList A) / Rᴬᴸ

 List/Rᴸ≃AList/Rᴬᴸ : List/Rᴸ ≃ AList/Rᴬᴸ
 List/Rᴸ≃AList/Rᴬᴸ = E.Thm

 main : QERDescends _ S.relation (List A , Lcount) (AList A , ALcount) QuasiR
 main = structuredQER→structuredEquiv _ S.suitable _ _ QuasiR (λ a r → r a)

 open QERDescends

 LQcount : S.structure List/Rᴸ
 LQcount = main .quoᴸ .fst

 ALQcount : S.structure AList/Rᴬᴸ
 ALQcount = main .quoᴿ .fst

 -- We get a path between CountStructures over the equivalence directly from the fact that the QER
 -- is structured
 List/Rᴸ≡AList/Rᴬᴸ :
   Path (TypeWithStr ℓ S.structure) (List/Rᴸ , LQcount) (AList/Rᴬᴸ , ALQcount)
 List/Rᴸ≡AList/Rᴬᴸ =
   sip S.univalent _ _ (E.Thm , (S.matches _ _ E.Thm .fst (main .rel)))

 -- We now show that List/Rᴸ≃FMSet
 _∷/_ : A → List/Rᴸ → List/Rᴸ
 a ∷/ [ xs ] = [ a ∷ xs ]
 a ∷/ eq/ xs xs' r i = eq/ (a ∷ xs) (a ∷ xs') r' i
  where
  r' : Rᴸ (a ∷ xs) (a ∷ xs')
  r' a' = cong (aux a' a (discA a' a)) (r a')
 a ∷/ squash/ xs xs₁ p q i j = squash/ (a ∷/ xs) (a ∷/ xs₁) (cong (a ∷/_) p) (cong (a ∷/_) q) i j

 infixr 5 _∷/_

 μ : FMSet A → List/Rᴸ
 μ = FMS.Rec.f squash/ [ [] ] _∷/_ β
  where
  β : ∀ a b [xs] → a ∷/ b ∷/ [xs] ≡ b ∷/ a ∷/ [xs]
  β a b = elimProp (λ _ → squash/ _ _) (λ xs → eq/ _ _ (γ xs))
   where
     γ : ∀ xs → Rᴸ (a ∷ b ∷ xs) (b ∷ a ∷ xs)
     γ xs c = δ c ∙ η (b ∷ a ∷ xs) c
      where
      δ : ∀ c → Lcount c (a ∷ b ∷ xs) ≡ Lcount c (b ∷ a ∷ xs)
      δ c with discA c a | discA c b
      δ c | yes _        | yes _ = refl
      δ c | yes _        | no  _ = refl
      δ c | no  _        | yes _ = refl
      δ c | no  _        | no  _ = refl

 -- The inverse is induced by the standard projection of lists into finite multisets,
 -- which is a morphism of CountStructures
 -- Moreover, we need 'count-extensionality' for finite multisets
 List→FMSet : List A → FMSet A
 List→FMSet [] = []
 List→FMSet (x ∷ xs) = x ∷ List→FMSet xs

 List→FMSet-count : ∀ a xs → Lcount a xs ≡ FMScount discA a (List→FMSet xs)
 List→FMSet-count a [] = refl
 List→FMSet-count a (x ∷ xs) with discA a x
 ...                         | yes _ = cong suc (List→FMSet-count a xs)
 ...                         | no  _ = List→FMSet-count a xs

 ν : List/Rᴸ → FMSet A
 ν [ xs ] = List→FMSet xs
 ν (eq/ xs ys r i) = path i
  where
   countsAgree : ∀ a → Lcount a xs ≡ Lcount a ys
   countsAgree a = r a ∙ sym (η ys a)

   θ : ∀ a → FMScount discA a (List→FMSet xs) ≡ FMScount discA a (List→FMSet ys)
   θ a = sym (List→FMSet-count a xs) ∙∙ countsAgree a ∙∙ List→FMSet-count a ys

   path : List→FMSet xs ≡ List→FMSet ys
   path = FMScountExt.Thm discA _ _ θ
 ν (squash/ xs/ xs/' p q i j) = trunc (ν xs/) (ν xs/') (cong ν p) (cong ν q) i j

 σ : section μ ν
 σ = elimProp (λ _ → squash/ _ _) θ
  where
  θ : (xs : List A) → μ (ν [ xs ]) ≡ [ xs ]
  θ [] = refl
  θ (x ∷ xs) = cong (x ∷/_) (θ xs)

 ν-∷/-commute : (x : A) (ys : List/Rᴸ) → ν (x ∷/ ys) ≡ x ∷ ν ys
 ν-∷/-commute x = elimProp (λ _ → FMS.trunc _ _) λ xs → refl

 τ : retract μ ν
 τ = FMS.ElimProp.f (FMS.trunc _ _) refl θ
  where
  θ : ∀ x {xs} → ν (μ xs) ≡ xs → ν (μ (x ∷ xs)) ≡ x ∷ xs
  θ x {xs} p = ν-∷/-commute x (μ xs) ∙ cong (x ∷_) p

 List/Rᴸ≃FMSet : List/Rᴸ ≃ FMSet A
 List/Rᴸ≃FMSet = isoToEquiv (iso ν μ τ σ)

 List/Rᴸ≃FMSet-is-CountEquivStr : ι (List/Rᴸ , LQcount) (FMSet A , FMScount discA) List/Rᴸ≃FMSet
 List/Rᴸ≃FMSet-is-CountEquivStr a = elimProp (λ _ → isSetℕ _ _) (List→FMSet-count a)

 {-
 Putting everything together we get:
               ≃
 List/Rᴸ ------------> AList/Rᴬᴸ
   |
   |≃
   |
   ∨
               ≃
 FMSet A ------------> AssocList A
 We thus get that AList/Rᴬᴸ≃AssocList.
 Constructing such an equivalence directly requires count extensionality for association lists,
 which should be even harder to prove than for finite multisets.
 This strategy should work for all implementations of multisets with HITs.
 We just have to show that:
  ∙ The HIT is equivalent to FMSet (like AssocList)
  ∙ There is a QER between lists and the basic data type of the HIT
    with the higher constructors removed (like AList)
 Then we get that this HIT is equivalent to the corresponding set quotient that identifies elements
 that give the same count on each a : A.
 TODO: Show that all the equivalences are indeed isomorphisms of multisets not only of CountStructures!
 -}

max_stars_repo_name: RobertHarper/cubical

max_issues_repo_name: RobertHarper/cubical

max_forks_repo_name: RobertHarper/cubical


text:
{-# OPTIONS --warning=error #-}

{-# POLARITY F #-}
{-# POLARITY G #-}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- An alternative definition of equality
------------------------------------------------------------------------

module TotalParserCombinators.CoinductiveEquality where

open import Codata.Musical.Notation
open import Data.List
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Relation.Binary.BagAndSetEquality
  using () renaming (_∼[_]_ to _List-∼[_]_)
open import Function.Equivalence as Eq using (_⇔_)
import Function.Related as Related

open Related using (SK-sym)
open Related.EquationalReasoning

open import TotalParserCombinators.Parser
open import TotalParserCombinators.Semantics
import TotalParserCombinators.InitialBag as I
open import TotalParserCombinators.Derivative as D using (D)

infix 5 _∷_
infix 4 _∼[_]c_

-- Two recognisers/languages are equal if their nullability indices
-- are equal (according to _List-∼[_]_) and all their derivatives are
-- equal (coinductively). Note that the inhabitants of this type are
-- bisimulations (if the Kind stands for a symmetric relation).

data _∼[_]c_ {Tok R xs₁ xs₂}
             (p₁ : Parser Tok R xs₁) (k : Kind)
             (p₂ : Parser Tok R xs₂) : Set where
  _∷_ : (init : xs₁ List-∼[ k ] xs₂)
        (rest : ∀ t → ∞ (D t p₁ ∼[ k ]c D t p₂)) →
        p₁ ∼[ k ]c p₂

-- The two definitions of parser/language equivalence are equivalent.

sound : ∀ {k Tok R xs₁ xs₂}
          {p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂} →
        p₁ ∼[ k ]c p₂ → p₁ ∼[ k ] p₂
sound {xs₁ = xs₁} {xs₂} {p₁} {p₂} (xs₁≈xs₂ ∷ rest) {x} {[]} =
  x ∈ p₁ · []  ↔⟨ I.correct ⟩
  (x ∈ xs₁)    ∼⟨ xs₁≈xs₂ ⟩
  (x ∈ xs₂)    ↔⟨ SK-sym I.correct ⟩
  x ∈ p₂ · []  ∎
sound {xs₁ = xs₁} {xs₂} {p₁} {p₂} (xs₁≈xs₂ ∷ rest) {x} {t ∷ s} =
  x ∈   p₁   · t ∷ s  ↔⟨ SK-sym D.correct ⟩
  x ∈ D t p₁ ·     s  ∼⟨ sound (♭ (rest t)) ⟩
  x ∈ D t p₂ ·     s  ↔⟨ D.correct ⟩
  x ∈   p₂   · t ∷ s  ∎

complete : ∀ {k Tok R xs₁ xs₂}
             {p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂} →
           p₁ ∼[ k ] p₂ → p₁ ∼[ k ]c p₂
complete p₁≈p₂ =
  (λ {_} → I.cong p₁≈p₂) ∷ λ t → ♯ complete (D.cong p₁≈p₂)

correct : ∀ {k Tok R xs₁ xs₂}
            {p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂} →
          p₁ ∼[ k ]c p₂ ⇔ p₁ ∼[ k ] p₂
correct = Eq.equivalence sound complete

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
{-# OPTIONS --type-in-type --guardedness #-}

module IO.Instance where

open import Class.Monad using (Monad)
open import Class.Monad.IO
open import Class.Monoid
open import Data.Product
open import Data.Sum
open import IO
open import Monads.ExceptT
open import Monads.StateT
open import Monads.WriterT
open import Level

instance
  IO-Monad : Monad IO
  IO-Monad = record { _>>=_ = _>>=_ ; return = return }

  IO-MonadIO : MonadIO IO
  IO-MonadIO = record { liftIO = λ x -> x }

module _ {a} {M : Set a -> Set a} {{_ : Monad M}} {{_ : MonadIO M}} where

  ExceptT-MonadIO : ∀ {E} -> MonadIO (ExceptT M E) {{ExceptT-Monad}}
  ExceptT-MonadIO = record { liftIO = λ x -> liftIO (x >>= λ a -> return (inj₂ a)) }

  StateT-MonadIO : ∀ {S} -> MonadIO (StateT M S)
  StateT-MonadIO = record { liftIO = λ x -> λ s -> liftIO (x >>= (λ a -> return (a , s))) }

  WriterT-MonadIO : ∀ {W} {{_ : Monoid W}} -> MonadIO (WriterT M W) {{WriterT-Monad}}
  WriterT-MonadIO = record { liftIO = λ x -> liftIO (x >>= λ a -> return (a , mzero)) }

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
------------------------------------------------------------------------------
-- The FOTC lists type
------------------------------------------------------------------------------

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

-- N.B. This module is re-exported by FOTC.Data.List.

module FOTC.Data.List.Type where

open import FOTC.Base
open import FOTC.Base.List

------------------------------------------------------------------------------
-- The FOTC lists type (inductive predicate for total lists).
data List : D → Set where
  lnil  : List []
  lcons : ∀ x {xs} → List xs → List (x ∷ xs)
{-# ATP axioms lnil lcons #-}

-- Induction principle.
List-ind : (A : D → Set) →
           A [] →
           (∀ x {xs} → A xs → A (x ∷ xs)) →
           ∀ {xs} → List xs → A xs
List-ind A A[] h lnil          = A[]
List-ind A A[] h (lcons x Lxs) = h x (List-ind A A[] h Lxs)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- Andreas, 2012-10-18
module Issue481 where

as = Set

open import Common.Issue481ParametrizedModule as as -- as clause
open import Common.Issue481ParametrizedModule as as as -- as clause, duplicate def.

max_stars_repo_name: np/agda-git-experiment


text:
open import MLib.Algebra.PropertyCode
open import MLib.Algebra.PropertyCode.Structures

module MLib.Matrix.SemiTensor.Associativity {c ℓ} (struct : Struct bimonoidCode c ℓ) where

open import MLib.Prelude
open import MLib.Matrix.Core
open import MLib.Matrix.Equality struct
open import MLib.Matrix.Mul struct
open import MLib.Matrix.Tensor struct
open import MLib.Matrix.SemiTensor.Core struct
open import MLib.Algebra.Operations struct

open Nat using () renaming (_+_ to _+ℕ_; _*_ to _*ℕ_)

open import MLib.Fin.Parts.Simple

open import Data.Nat.LCM
open import Data.Nat.Divisibility

module _ ⦃ props : Has (1# is rightIdentity for * ∷ associative on * ∷ []) ⦄ where
  open _≃_

  {-
  m *ℕ (lcm n (p * (lcm q r) / q))/n ≡ m *ℕ (lcm n p)/n *ℕ (lcm (q *ℕ (lcm n p)/p) r) / r

  m * lcm(n, p * lcm(q, r) / q) / n =
  m * (lcm(n, p) / n) * lcm (q * lcm(n, p) / p,  r) / r

  lcm(n, p * lcm(q, r) / q) = lcm (q * lcm(n, p) / p,  r) * p / q

  f(a, b) = lcm(a, b) / a

  lcm(n, p * f(q, r)) = lcm(r, q * f(p, n)) * p / q
  -}

  module _ {m n p q r s} (A : Matrix S m n) (B : Matrix S p q) (C : Matrix S r s) where
    t₁ = lcm n p .proj₁
    lcm-n-p=t₁ = lcm n p .proj₂

    open Defn lcm-n-p=t₁ using () renaming (t/n to t₁/n; t/p to t₁/p)

    t₂ = lcm q r .proj₁
    lcm-q-r=t₂ = lcm q r .proj₂

    open Defn lcm-q-r=t₂ using () renaming (t/n to t₂/q; t/p to t₂/r)

    t₃ = lcm n (p *ℕ t₂/q) .proj₁
    lcm-n-pt₂/q=t₃ = lcm n (p *ℕ t₂/q) .proj₂

    open Defn lcm-n-pt₂/q=t₃ using () renaming (t/n to t₃/n; t/p to t₃/[p*t₂/q])

    t₄ = lcm (q *ℕ t₁/p) r .proj₁
    lcm-qt₁/p-r=t₄ = lcm (q *ℕ t₁/p) r .proj₂

    open Defn lcm-qt₁/p-r=t₄ using () renaming (t/n to t₄/[q*t₁/p]; t/p to t₄/r)
    -- module D₁ = Defn {n} {p} {q}
    -- module D₂ = Defn {q} {r} {s}

    ⋉-associative : A ⋉ (B ⋉ C) ≃ (A ⋉ B) ⋉ C
    ⋉-associative .m≡p = {!!}
    ⋉-associative .n≡q = {!!}
    ⋉-associative .equal = {!!}


text:
{-# OPTIONS -v interaction.case:65 #-}

data Bool : Set where
  true false : Bool

test : Bool → Bool
test x = {!x!}


text:
module CTL.Modalities where

open import CTL.Modalities.AF public
open import CTL.Modalities.AG public
open import CTL.Modalities.AN public
-- open import CTL.Modalities.AU public -- TODO Unfinished
open import CTL.Modalities.EF public
open import CTL.Modalities.EG public
open import CTL.Modalities.EN public
-- open import CTL.Modalities.EU public -- TODO Unfinished

max_stars_repo_name: Aerate/condatis

max_issues_repo_name: zimbatm/condatis

max_forks_repo_name: zimbatm/condatis


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import Agda.Primitive

module Basic where

data False : Set where

record True : Set where

data _||_ {a b : _} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  inl : A → A || B
  inr : B → A || B
infix 1 _||_


text:
------------------------------------------------------------------------
-- A formalisation of some definitions and laws from Section 3 of Ralf
-- Hinze's paper "Streams and Unique Fixed Points"
------------------------------------------------------------------------

module Hinze.Section3 where

open import Stream.Programs
open import Stream.Equality
open import Stream.Pointwise
open import Hinze.Section2-4
open import Hinze.Lemmas

open import Codata.Musical.Notation hiding (∞)
open import Data.Product
open import Data.Bool
open import Data.Vec hiding (_⋎_)
open import Data.Nat
import Data.Nat.Properties as Nat
import Relation.Binary.PropositionalEquality as P
open import Algebra.Structures
private
  module CS = IsCommutativeSemiring Nat.+-*-isCommutativeSemiring

------------------------------------------------------------------------
-- Definitions

pot : Prog Bool
pot = true ≺ ♯ (pot ⋎ false ∞)

msb : Prog ℕ
msb = 1 ≺ ♯ (2 ∞ ⟨ _*_ ⟩ msb ⋎ 2 ∞ ⟨ _*_ ⟩ msb)

ones′ : Prog ℕ
ones′ = 1 ≺ ♯ (ones′ ⋎ ones′ ⟨ _+_ ⟩ 1 ∞)

ones : Prog ℕ
ones = 0 ≺♯ ones′

carry : Prog ℕ
carry = 0 ≺ ♯ (carry ⟨ _+_ ⟩ 1 ∞ ⋎ 0 ∞)

carry-folded : carry ≊ 0 ∞ ⋎ carry ⟨ _+_ ⟩ 1 ∞
carry-folded = carry ∎

2^carry : Prog ℕ
2^carry = 2 ∞ ⟨ _^_ ⟩ carry

turn-length : ℕ → ℕ
turn-length zero    = zero
turn-length (suc n) = ℓ + suc ℓ
  where ℓ = turn-length n

turn : (n : ℕ) → Vec ℕ (turn-length n)
turn zero    = []
turn (suc n) = turn n ++ [ n ] ++ turn n

tree : ℕ → Prog ℕ
tree n = n ≺ ♯ (turn n ≺≺ tree (suc n))

frac : Prog ℕ
frac = 0 ≺ ♯ (frac ⋎ nat ⟨ _+_ ⟩ 1 ∞)

frac-folded : frac ≊ nat ⋎ frac
frac-folded = frac ∎

god : Prog ℕ
god = (2 ∞ ⟨ _*_ ⟩ frac) ⟨ _+_ ⟩ 1 ∞

------------------------------------------------------------------------
-- Laws and properties

god-lemma : god ≊ 2*nat+1 ⋎ god
god-lemma =
  god
                                          ≡⟨ P.refl ⟩
  (2 ∞ ⟨ _*_ ⟩ (nat ⋎ frac)) ⟨ _+_ ⟩ 1 ∞
                                          ≊⟨ ⟨ _+_ ⟩-cong (2 ∞ ⟨ _*_ ⟩ (nat ⋎ frac))
                                                          (2*nat ⋎ 2 ∞ ⟨ _*_ ⟩ frac)
                                                          (zip-const-⋎ _*_ 2 nat frac)
                                                          (1 ∞) (1 ∞) (1 ∞ ∎)  ⟩
  (2*nat ⋎ 2 ∞ ⟨ _*_ ⟩ frac) ⟨ _+_ ⟩ 1 ∞
                                          ≊⟨ zip-⋎-const _+_ 2*nat (2 ∞ ⟨ _*_ ⟩ frac) 1 ⟩
  2*nat+1 ⋎ god
                                          ∎

carry-god-nat : 2^carry ⟨ _*_ ⟩ god ≊ tailP nat
carry-god-nat =
  2^carry ⟨ _*_ ⟩ god
                                                           ≡⟨ P.refl ⟩
  (2 ∞ ⟨ _^_ ⟩ (0 ∞ ⋎ carry ⟨ _+_ ⟩ 1 ∞)) ⟨ _*_ ⟩ god
                                                           ≊⟨ ⟨ _*_ ⟩-cong (2 ∞ ⟨ _^_ ⟩ (0 ∞ ⋎ carry ⟨ _+_ ⟩ 1 ∞))
                                                                           (1 ∞ ⋎ 2 ∞ ⟨ _*_ ⟩ 2^carry) lemma
                                                                           god (2*nat+1 ⋎ god) god-lemma ⟩
  (1 ∞ ⋎ 2 ∞ ⟨ _*_ ⟩ 2^carry) ⟨ _*_ ⟩ (2*nat+1 ⋎ god)
                                                           ≊⟨ ≅-sym (abide-law _*_ (1 ∞) 2*nat+1
                                                                                (2 ∞ ⟨ _*_ ⟩ 2^carry) god) ⟩
  1 ∞ ⟨ _*_ ⟩ 2*nat+1 ⋎ (2 ∞ ⟨ _*_ ⟩ 2^carry) ⟨ _*_ ⟩ god
                                                           ≊⟨ ⋎-cong (1 ∞ ⟨ _*_ ⟩ 2*nat+1) 2*nat+1
                                                                     (pointwise 1 (λ s → 1 ∞ ⟨ _*_ ⟩ s) (λ s → s)
                                                                                (proj₁ CS.*-identity) 2*nat+1)
                                                                     ((2 ∞ ⟨ _*_ ⟩ 2^carry) ⟨ _*_ ⟩ god)
                                                                     (2 ∞ ⟨ _*_ ⟩ (2^carry ⟨ _*_ ⟩ god))
                                                                     (pointwise 3 (λ s t u → (s ⟨ _*_ ⟩ t) ⟨ _*_ ⟩ u)
                                                                                (λ s t u → s ⟨ _*_ ⟩ (t ⟨ _*_ ⟩ u))
                                                                                CS.*-assoc (2 ∞) 2^carry god) ⟩
  2*nat+1 ⋎ 2 ∞ ⟨ _*_ ⟩ (2^carry ⟨ _*_ ⟩ god)
                                                           ≊⟨ P.refl ≺ coih ⟩
  2*nat+1 ⋎ 2 ∞ ⟨ _*_ ⟩ tailP nat
                                                           ≊⟨ ≅-sym (tailP-cong nat (2*nat ⋎ 2*nat+1) nat-lemma₂) ⟩
  tailP nat
                                                           ∎
  where
  coih = ♯ ⋎-cong (2 ∞ ⟨ _*_ ⟩ (2^carry ⟨ _*_ ⟩ god))
                  (2 ∞ ⟨ _*_ ⟩ (tailP nat))
                  (⟨ _*_ ⟩-cong (2 ∞) (2 ∞) (2 ∞ ∎)
                                (2^carry ⟨ _*_ ⟩ god) (tailP nat)
                                carry-god-nat)
                  (tailP 2*nat+1) (tailP 2*nat+1) (tailP 2*nat+1 ∎)

  lemma =
    2^carry
                                                       ≡⟨ P.refl ⟩
    2 ∞ ⟨ _^_ ⟩ (0 ∞ ⋎ carry ⟨ _+_ ⟩ 1 ∞)
                                                       ≊⟨ zip-const-⋎ _^_ 2 (0 ∞) (carry ⟨ _+_ ⟩ 1 ∞) ⟩
    2 ∞ ⟨ _^_ ⟩ 0 ∞ ⋎ 2 ∞ ⟨ _^_ ⟩ (carry ⟨ _+_ ⟩ 1 ∞)
                                                       ≊⟨ ⋎-cong (2 ∞ ⟨ _^_ ⟩ 0 ∞) (1 ∞)
                                                                 (pointwise 0 (2 ∞ ⟨ _^_ ⟩ 0 ∞) (1 ∞) P.refl)
                                                                 (2 ∞ ⟨ _^_ ⟩ (carry ⟨ _+_ ⟩ 1 ∞))
                                                                 (2 ∞ ⟨ _*_ ⟩ 2^carry)
                                                                 (pointwise 1 (λ s → 2 ∞ ⟨ _^_ ⟩ (s ⟨ _+_ ⟩ 1 ∞))
                                                                              (λ s → 2 ∞ ⟨ _*_ ⟩ (2 ∞ ⟨ _^_ ⟩ s))
                                                                              (λ x → P.cong (_^_ 2) (CS.+-comm x 1))
                                                                              carry) ⟩
    1 ∞ ⋎ 2 ∞ ⟨ _*_ ⟩ 2^carry
                                                       ∎

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
------------------------------------------------------------------------
-- The one-sided Step function, used to define similarity and the
-- two-sided Step function
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

open import Prelude

open import Labelled-transition-system

module Similarity.Step
         {ℓ}
         (lts : LTS ℓ)
         (open LTS lts)
         (_[_]↝_ : Proc → Label → Proc → Type ℓ)
         where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)

open import Bijection equality-with-J as Bijection using (_↔_)
import Equivalence equality-with-J as Eq
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J

open import Indexed-container hiding (⟨_⟩)
open import Relation

private
 module Temporarily-private where

  -- If _[_]↝_ is instantiated with _[_]⟶_, then this is basically the
  -- function s from Section 6.3.4.2 in Pous and Sangiorgi's
  -- "Enhancements of the bisimulation proof method", except that
  -- clause (3) is omitted.
  --
  -- Similarly, if _[_]↝_ is instantiated with _[_]⇒̂_, then this is
  -- basically the function w from Section 6.5.2.4, except that
  -- "P R Q" is omitted.

  record Step {r} (R : Rel₂ r Proc) (pq : Proc × Proc) :
              Type (ℓ ⊔ r) where
    constructor ⟨_⟩

    private
      p = proj₁ pq
      q = proj₂ pq

    field
      challenge : ∀ {p′ μ} →
                  p [ μ ]⟶ p′ → ∃ λ q′ → q [ μ ]↝ q′ × R (p′ , q′)

open Temporarily-private using (Step)

-- Used to aid unification. Note that this type is parametrised (see
-- the module telescope above). The inclusion of a value of this type
-- in the definition of StepC below makes it easier for Agda to infer
-- the LTS parameter from the types ν StepC i (p , q) and
-- ν′ StepC i (p , q).

record Magic : Type where

-- The Magic type is isomorphic to the unit type.

Magic↔⊤ : Magic ↔ ⊤
Magic↔⊤ = record
  { surjection = record
    { right-inverse-of = λ _ → refl
    }
  ; left-inverse-of = λ _ → refl
  }

-- The Step function, expressed as an indexed container.

StepC : Container (Proc × Proc) (Proc × Proc)
StepC =
  (λ { (p , q) → Magic  -- Included in order to aid type inference.
                   ×
                 (∀ {p′ μ} → p [ μ ]⟶ p′ → ∃ λ q′ → q [ μ ]↝ q′)
     })
    ◁
  (λ { {o = p , q} (_ , lr) (p′ , q′) →
       ∃ λ μ → ∃ λ (p⟶p′ : p [ μ ]⟶ p′) → proj₁ (lr p⟶p′) ≡ q′
     })

-- The definition of Step in terms of a container is pointwise
-- logically equivalent to the direct definition, and in the presence
-- of extensionality it is pointwise isomorphic to the direct
-- definition.

Step↔StepC :
  ∀ {k r} {R : Rel₂ r Proc} {pq} →
  Extensionality? k ℓ (ℓ ⊔ r) →
  Step R pq ↝[ k ] ⟦ StepC ⟧ R pq
Step↔StepC {r = r} {R} {pq} =
  generalise-ext?
    Step⇔StepC
    (λ ext →
         (λ (_ , f) →
            Σ-≡,≡→≡ refl $
              implicit-extensionality ext λ _ →
              apply-ext (lower-extensionality lzero ℓ ext) $
                to₂∘from f)
       , (λ _ → refl))
  where
  to₁ : Step R pq → Container.Shape StepC pq
  to₁ Temporarily-private.⟨ lr ⟩ =
      _
    , (λ p⟶p′ → Σ-map id proj₁ (lr p⟶p′))

  to₂ :
    (s : Step R pq) →
    Container.Position StepC (to₁ s) ⊆ R
  to₂ Temporarily-private.⟨ lr ⟩ (_ , p⟶p′ , refl) =
    proj₂ (proj₂ (lr p⟶p′))

  from : ⟦ StepC ⟧ R pq → Step R pq
  from ((_ , lr) , f) =
    Temporarily-private.⟨ (λ p⟶p′ →
                             let q′ , q⟶q′ = lr p⟶p′
                             in  q′ , q⟶q′ , f (_ , p⟶p′ , refl))
                        ⟩

  Step⇔StepC : Step R pq ⇔ ⟦ StepC ⟧ R pq
  Step⇔StepC = record
    { to   = λ s → to₁ s , to₂ s
    ; from = from
    }

  to₂∘from :
    ∀ {p′q′} {s : Container.Shape StepC pq}
    (f : Container.Position StepC s ⊆ R) →
    (pos : Container.Position StepC s p′q′) →
    proj₂ (_⇔_.to Step⇔StepC (_⇔_.from Step⇔StepC (s , f))) pos ≡ f pos
  to₂∘from f (_ , _ , refl) = refl

module StepC {r} {R : Rel₂ r Proc} {p q} where

  -- A "constructor".

  ⟨_⟩ :
    (∀ {p′ μ} → p [ μ ]⟶ p′ → ∃ λ q′ → q [ μ ]↝ q′ × R (p′ , q′)) →
    ⟦ StepC ⟧ R (p , q)
  ⟨ lr ⟩ = _⇔_.to (Step↔StepC _) Temporarily-private.⟨ lr ⟩

  -- A "projection".

  challenge :
    ⟦ StepC ⟧ R (p , q) →
    ∀ {p′ μ} → p [ μ ]⟶ p′ → ∃ λ q′ → q [ μ ]↝ q′ × R (p′ , q′)
  challenge = Step.challenge ∘ _⇔_.from (Step↔StepC _)

open Temporarily-private public

-- An unfolding lemma for ⟦ StepC ⟧₂.

⟦StepC⟧₂↔ :
  ∀ {x} {X : Rel₂ x Proc} →
  Extensionality ℓ ℓ →
  (R : ∀ {o} → Rel₂ ℓ (X o)) →
  ∀ {p q} (p∼q₁ p∼q₂ : ⟦ StepC ⟧ X (p , q)) →

  ⟦ StepC ⟧₂ R (p∼q₁ , p∼q₂)

    ↔

  (∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
   let q′₁ , q⟶q′₁ , p′≤q′₁ = StepC.challenge p∼q₁ p⟶p′
       q′₂ , q⟶q′₂ , p′≤q′₂ = StepC.challenge p∼q₂ p⟶p′
   in ∃ λ (q′₁≡q′₂ : q′₁ ≡ q′₂) →
        subst (q [ μ ]↝_) q′₁≡q′₂ q⟶q′₁ ≡ q⟶q′₂
          ×
        R (subst (X ∘ (p′ ,_)) q′₁≡q′₂ p′≤q′₁ , p′≤q′₂))

⟦StepC⟧₂↔ {X = X} ext R {p} {q}
          (s₁@(_ , ch₁) , f₁) (s₂@(_ , ch₂) , f₂) =

  (∃ λ (eq : s₁ ≡ s₂) →
   ∀ {o} (p : Container.Position StepC s₁ o) →
   R (f₁ p , f₂ (subst (λ s → Container.Position StepC s o) eq p)))    ↝⟨ inverse $ Σ-cong ≡×≡↔≡ (λ _ → F.id) ⟩

  (∃ λ (eq : proj₁ s₁ ≡ proj₁ s₂ × (λ {_ _} → ch₁) ≡ ch₂) →
   ∀ {o} (p : Container.Position StepC s₁ o) →
   R (f₁ p , f₂ (subst (λ s → Container.Position StepC s o)
                       (cong₂ _,_ (proj₁ eq) (proj₂ eq)) p)))          ↝⟨ inverse Σ-assoc ⟩

  (∃ λ (eq₁ : proj₁ s₁ ≡ proj₁ s₂) →
   ∃ λ (eq₂ : (λ {_ _} → ch₁) ≡ ch₂) →
   ∀ {o} (p : Container.Position StepC s₁ o) →
   R (f₁ p , f₂ (subst (λ s → Container.Position StepC s o)
                       (cong₂ _,_ eq₁ eq₂) p)))                        ↝⟨ drop-⊤-left-Σ $ _⇔_.to contractible⇔↔⊤ $
                                                                          +⇒≡ $ mono₁ 0 (_⇔_.from contractible⇔↔⊤ Magic↔⊤) ⟩
  (∃ λ (eq : (λ {_ _} → ch₁) ≡ ch₂) →
   ∀ {o} (p : Container.Position StepC s₁ o) →
   R (f₁ p , f₂ (subst (λ s → Container.Position StepC s o)
                       (cong₂ _,_ refl eq) p)))                        ↝⟨ (∃-cong λ eq → implicit-∀-cong ext $ ∀-cong ext λ _ →
                                                                           ≡⇒↝ _ $
                                                                           cong (λ (eq : s₁ ≡ s₂) →
                                                                                R (f₁ _ ,
                                                                                f₂ (subst (λ s → Container.Position StepC s _) eq _))) $
                                                                           trans-reflˡ (cong (_ ,_) eq)) ⟩
  (∃ λ (eq : (λ {_ _} → ch₁) ≡ ch₂) →
   ∀ {o} (p : Container.Position StepC s₁ o) →
   R (f₁ p , f₂ (subst (λ (s : _ × _) → Container.Position StepC s o)
                       (cong (_ ,_) eq) p)))                           ↝⟨ (∃-cong λ eq → implicit-∀-cong ext λ {o} → ∀-cong ext λ p →
                                                                           ≡⇒↝ _ $ cong (λ p → R {o = o} (f₁ _ , f₂ p)) $ sym $
                                                                           subst-∘ (λ (s : Container.Shape StepC _) → Container.Position StepC s o)
                                                                                _ eq) ⟩
  (∃ λ (eq : (λ {_ _} → ch₁) ≡ ch₂) →
   ∀ {o} (p : Container.Position StepC s₁ o) →
   R (f₁ p , f₂ (subst (λ (ch : ∀ {_ _} → _) →
                          Container.Position StepC (_ , ch) o)
                       eq p)))                                         ↔⟨⟩

  (∃ λ (eq : _≡_ {A = ∀ {p′ μ} → _} ch₁ ch₂) →
   ∀ {p′q′} →
   (pos : ∃ λ μ → ∃ λ (p⟶p′ : p [ μ ]⟶ proj₁ p′q′) →
          proj₁ (ch₁ p⟶p′) ≡ proj₂ p′q′) →
   R (f₁ pos ,
      f₂ (subst (λ ch → ∃ λ μ → ∃ λ (p⟶p′ : p [ μ ]⟶ proj₁ p′q′) →
                        proj₁ (ch p⟶p′) ≡ proj₂ p′q′)
                eq pos)))                                              ↝⟨ (∃-cong λ _ → Bijection.implicit-Π↔Π) ⟩

  (∃ λ (eq : _≡_ {A = ∀ {p′ μ} → _} ch₁ ch₂) →
   ∀ p′q′ →
   (pos : ∃ λ μ → ∃ λ (p⟶p′ : p [ μ ]⟶ proj₁ p′q′) →
          proj₁ (ch₁ p⟶p′) ≡ proj₂ p′q′) →
   R (f₁ pos ,
      f₂ (subst (λ ch → ∃ λ μ → ∃ λ (p⟶p′ : p [ μ ]⟶ proj₁ p′q′) →
                        proj₁ (ch p⟶p′) ≡ proj₂ p′q′)
                eq pos)))                                              ↝⟨ (∃-cong λ _ → currying) ⟩

  (∃ λ (eq : _≡_ {A = ∀ {p′ μ} → _} ch₁ ch₂) →
   ∀ p′ q′ →
   (pos : ∃ λ μ → ∃ λ (p⟶p′ : p [ μ ]⟶ p′) → proj₁ (ch₁ p⟶p′) ≡ q′) →
   R (f₁ pos ,
      f₂ (subst (λ ch → ∃ λ μ → ∃ λ (p⟶p′ : p [ μ ]⟶ p′) →
                        proj₁ (ch p⟶p′) ≡ q′)
                eq pos)))                                              ↝⟨ (∃-cong λ _ → ∀-cong ext λ _ → ∀-cong ext λ _ → currying) ⟩

  (∃ λ (eq : _≡_ {A = ∀ {p′ μ} → _} ch₁ ch₂) →
   ∀ p′ q′ μ →
   (pos : ∃ λ (p⟶p′ : p [ μ ]⟶ p′) → proj₁ (ch₁ p⟶p′) ≡ q′) →
   R (f₁ (μ , pos) ,
      f₂ (subst (λ ch → ∃ λ μ → ∃ λ (p⟶p′ : p [ μ ]⟶ p′) →
                        proj₁ (ch p⟶p′) ≡ q′)
                eq (μ , pos))))                                        ↝⟨ (∃-cong λ _ → ∀-cong ext λ _ → ∀-cong ext λ _ → ∀-cong ext λ _ →
                                                                           currying) ⟩
  (∃ λ (eq : _≡_ {A = ∀ {p′ μ} → _} ch₁ ch₂) →
   ∀ p′ q′ μ (p⟶p′ : p [ μ ]⟶ p′) (≡q′ : proj₁ (ch₁ p⟶p′) ≡ q′) →
   R (f₁ (μ , p⟶p′ , ≡q′) ,
      f₂ (subst (λ ch → ∃ λ μ → ∃ λ (p⟶p′ : p [ μ ]⟶ p′) →
                        proj₁ (ch p⟶p′) ≡ q′)
                eq (μ , p⟶p′ , ≡q′))))                                 ↝⟨ (∃-cong λ _ → ∀-cong ext λ _ → Π-comm) ⟩

  (∃ λ (eq : _≡_ {A = ∀ {p′ μ} → _} ch₁ ch₂) →
   ∀ p′ μ q′ (p⟶p′ : p [ μ ]⟶ p′) (≡q′ : proj₁ (ch₁ p⟶p′) ≡ q′) →
   R (f₁ (μ , p⟶p′ , ≡q′) ,
      f₂ (subst (λ ch → ∃ λ μ → ∃ λ (p⟶p′ : p [ μ ]⟶ p′) →
                        proj₁ (ch p⟶p′) ≡ q′)
                eq (μ , p⟶p′ , ≡q′))))                                 ↝⟨ (∃-cong λ _ → ∀-cong ext λ _ → ∀-cong ext λ _ → Π-comm) ⟩

  (∃ λ (eq : _≡_ {A = ∀ {p′ μ} → _} ch₁ ch₂) →
   ∀ p′ μ (p⟶p′ : p [ μ ]⟶ p′) q′ (≡q′ : proj₁ (ch₁ p⟶p′) ≡ q′) →
   R (f₁ (μ , p⟶p′ , ≡q′) ,
      f₂ (subst (λ ch → ∃ λ μ → ∃ λ (p⟶p′ : p [ μ ]⟶ p′) →
                        proj₁ (ch p⟶p′) ≡ q′)
                eq (μ , p⟶p′ , ≡q′))))                                 ↝⟨ (∃-cong λ _ → ∀-cong ext λ _ → ∀-cong ext λ _ → ∀-cong ext λ _ →
                                                                              inverse $ ∀-intro _ ext) ⟩
  (∃ λ (eq : _≡_ {A = ∀ {p′ μ} → _} ch₁ ch₂) →
   ∀ p′ μ (p⟶p′ : p [ μ ]⟶ p′) →
   R (f₁ (μ , p⟶p′ , refl) ,
      f₂ (subst (λ ch → ∃ λ μ → ∃ λ (p⟶p′′ : p [ μ ]⟶ p′) →
                        proj₁ (ch p⟶p′′) ≡ proj₁ (ch₁ p⟶p′))
                eq (μ , p⟶p′ , refl))))                                ↝⟨ (∃-cong λ eq → ∀-cong ext λ _ → ∀-cong ext λ _ → ∀-cong ext λ _ →
                                                                           ≡⇒↝ _ $ cong (R ∘ (f₁ _ ,_) ∘ f₂) $ lemma₁ eq) ⟩
  (∃ λ (eq : _≡_ {A = ∀ {p′ μ} → _} ch₁ ch₂) →
   ∀ p′ μ (p⟶p′ : p [ μ ]⟶ p′) →
   R (f₁ (μ , p⟶p′ , refl) ,
      f₂ (μ , p⟶p′ , sym (cong (λ ch → proj₁ (ch p⟶p′)) eq))))         ↝⟨ (∃-cong λ eq → ∀-cong ext λ _ → inverse Bijection.implicit-Π↔Π) ⟩

  (∃ λ (eq : _≡_ {A = ∀ {p′ μ} → _} ch₁ ch₂) →
   ∀ p′ {μ} (p⟶p′ : p [ μ ]⟶ p′) →
   R (f₁ (μ , p⟶p′ , refl) ,
      f₂ (μ , p⟶p′ , sym (cong (λ ch → proj₁ (ch p⟶p′)) eq))))         ↝⟨ (∃-cong λ eq → inverse Bijection.implicit-Π↔Π) ⟩

  (∃ λ (eq : _≡_ {A = ∀ {p′ μ} → _} ch₁ ch₂) →
   ∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
   R (f₁ (μ , p⟶p′ , refl) ,
      f₂ (μ , p⟶p′ , sym (cong (λ ch → proj₁ (ch p⟶p′)) eq))))         ↝⟨ (Σ-cong (inverse $ implicit-extensionality-isomorphism
                                                                                {k = bijection} ext) λ eq →
                                                                           implicit-∀-cong ext $ implicit-∀-cong ext $ ∀-cong ext λ p⟶p′ →
                                                                           ≡⇒↝ _ $ sym $ cong (λ eq →
                                                                             R (f₁ _ , f₂ (_ , p⟶p′ , sym (cong (λ ch → proj₁ (ch p⟶p′)) eq)))) $
                                                                           _↔_.right-inverse-of (implicit-extensionality-isomorphism ext) eq) ⟩
  (∃ λ (eq : ∀ p′ → (λ {μ} → ch₁ {p′ = p′} {μ = μ}) ≡ ch₂) →
   let eq′ = _↔_.to (implicit-extensionality-isomorphism ext) eq in
   ∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
   R (f₁ (μ , p⟶p′ , refl) ,
      f₂ (μ , p⟶p′ , sym (cong (λ ch → proj₁ (ch p⟶p′)) eq′))))        ↝⟨ (∃-cong λ eq →
                                                                           implicit-∀-cong ext $ implicit-∀-cong ext $ ∀-cong ext λ p⟶p′ →
                                                                           ≡⇒↝ _ $ cong (λ eq → R (f₁ _ , f₂ (_ , p⟶p′ , sym eq))) $
                                                                           lemma₂ eq) ⟩
  (∃ λ (eq : ∀ p′ → (λ {μ} → ch₁ {p′ = p′} {μ = μ}) ≡ ch₂) →
   ∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
   R (f₁ (μ , p⟶p′ , refl) ,
      f₂ (μ , p⟶p′ , sym (cong (λ ch → proj₁ (ch p′ p⟶p′))
                               (apply-ext (Eq.good-ext ext) eq)))))    ↝⟨ (Σ-cong (inverse $ ∀-cong ext λ _ →
                                                                                implicit-extensionality-isomorphism
                                                                                {k = bijection} ext) λ eq →
                                                                           implicit-∀-cong ext $ implicit-∀-cong ext $ ∀-cong ext λ p⟶p′ →
                                                                           ≡⇒↝ _ $ sym $ cong (λ eq →
                                                                             R (f₁ _ , f₂ (_ , p⟶p′ , sym (cong (λ ch → proj₁ (ch _ p⟶p′))
                                                                                (apply-ext (Eq.good-ext ext) eq))))) $
                                                                           apply-ext ext $
                                                                           _↔_.right-inverse-of (implicit-extensionality-isomorphism ext) ∘ eq) ⟩
  (∃ λ (eq : ∀ p′ μ → ch₁ {p′ = p′} {μ = μ} ≡ ch₂) →
   let eq′ = implicit-extensionality (Eq.good-ext ext) ∘ eq in
   ∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
   R (f₁ (μ , p⟶p′ , refl) ,
      f₂ (μ , p⟶p′ , sym (cong (λ ch → proj₁ (ch p′ p⟶p′))
                               (apply-ext (Eq.good-ext ext) eq′)))))   ↝⟨ (∃-cong λ _ →
                                                                           implicit-∀-cong ext $ implicit-∀-cong ext $ ∀-cong ext λ _ →
                                                                           ≡⇒↝ _ $ cong (λ eq → R (f₁ _ , f₂ (_ , _ , sym eq))) $
                                                                           lemma₃ _) ⟩
  (∃ λ (eq : ∀ p′ μ → ch₁ {p′ = p′} {μ = μ} ≡ ch₂) →
   ∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
   R (f₁ (μ , p⟶p′ , refl) ,
      f₂ (μ , p⟶p′ , sym (cong (λ ch → proj₁ (ch p⟶p′)) (eq p′ μ)))))  ↝⟨ Σ-cong (inverse Bijection.implicit-Π↔Π) (λ _ → F.id) ⟩

  (∃ λ (eq : ∀ {p′} μ → ch₁ {p′ = p′} {μ = μ} ≡ ch₂) →
   ∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
   R (f₁ (μ , p⟶p′ , refl) ,
      f₂ (μ , p⟶p′ , sym (cong (λ ch → proj₁ (ch p⟶p′)) (eq μ)))))     ↝⟨ Σ-cong (implicit-∀-cong ext $ inverse Bijection.implicit-Π↔Π)
                                                                                (λ _ → F.id) ⟩
  (∃ λ (eq : ∀ {p′ μ} → ch₁ {p′ = p′} {μ = μ} ≡ ch₂) →
   ∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
   R (f₁ (μ , p⟶p′ , refl) ,
      f₂ (μ , p⟶p′ , sym (cong (λ ch → proj₁ (ch p⟶p′)) eq))))         ↝⟨ (∃-cong λ eq →
                                                                           implicit-∀-cong ext $ implicit-∀-cong ext $ ∀-cong ext λ p⟶p′ →
                                                                           ≡⇒↝ _ $ cong (λ eq → R (f₁ _ , f₂ (_ , _ , sym eq))) $ sym $
                                                                           cong-∘ proj₁ (_$ p⟶p′) (eq {μ = _})) ⟩
  (∃ λ (eq : ∀ {p′ μ} → ch₁ {p′ = p′} {μ = μ} ≡ ch₂) →
   ∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
   R (f₁ (μ , p⟶p′ , refl) ,
      f₂ (μ , p⟶p′ , sym (cong proj₁ $ cong (_$ p⟶p′) eq))))           ↝⟨ Σ-cong (implicit-∀-cong ext $ implicit-∀-cong ext $ inverse $
                                                                                Eq.extensionality-isomorphism ext)
                                                                                (λ _ → F.id) ⟩
  (∃ λ (eq : ∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) → ch₁ p⟶p′ ≡ ch₂ p⟶p′) →
   ∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
   R (f₁ (μ , p⟶p′ , refl) ,
      f₂ (μ , p⟶p′ , sym (cong proj₁ (eq p⟶p′)))))                     ↝⟨ inverse implicit-ΠΣ-comm ⟩

  (∀ {p′} →
   ∃ λ (eq : ∀ {μ} (p⟶p′ : p [ μ ]⟶ p′) → ch₁ p⟶p′ ≡ ch₂ p⟶p′) →
   ∀ {μ} (p⟶p′ : p [ μ ]⟶ p′) →
   R (f₁ (μ , p⟶p′ , refl) ,
      f₂ (μ , p⟶p′ , sym (cong proj₁ (eq p⟶p′)))))                     ↝⟨ implicit-∀-cong ext $ inverse implicit-ΠΣ-comm ⟩

  (∀ {p′ μ} →
   ∃ λ (eq : (p⟶p′ : p [ μ ]⟶ p′) → ch₁ p⟶p′ ≡ ch₂ p⟶p′) →
   ∀ p⟶p′ → R (f₁ (μ , p⟶p′ , refl) ,
               f₂ (μ , p⟶p′ , sym (cong proj₁ (eq p⟶p′)))))            ↝⟨ implicit-∀-cong ext $ implicit-∀-cong ext $ inverse ΠΣ-comm ⟩

  (∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
   ∃ λ (eq : ch₁ p⟶p′ ≡ ch₂ p⟶p′) →
   R (f₁ (μ , p⟶p′ , refl) , f₂ (μ , p⟶p′ , sym (cong proj₁ eq))))     ↝⟨ (inverse $ implicit-∀-cong ext $ implicit-∀-cong ext $ ∀-cong ext λ _ →
                                                                           Σ-cong Bijection.Σ-≡,≡↔≡ λ _ → F.id) ⟩
  (∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
   let q′₁ , q⟶q′₁ = ch₁ p⟶p′
       q′₂ , q⟶q′₂ = ch₂ p⟶p′
   in ∃ λ (eq : ∃ λ (q′₁≡q′₂ : q′₁ ≡ q′₂) →
                  subst (q [ μ ]↝_) q′₁≡q′₂ q⟶q′₁ ≡ q⟶q′₂) →
      R (f₁ (μ , p⟶p′ , refl) ,
         f₂ (μ , p⟶p′ , sym (cong proj₁ (uncurry Σ-≡,≡→≡ eq)))))       ↝⟨ (implicit-∀-cong ext $ implicit-∀-cong ext $ ∀-cong ext λ _ →
                                                                           ∃-cong λ eq →
                                                                           ≡⇒↝ _ $ cong (λ eq → R (f₁ _ , f₂ (_ , _ , sym eq))) $
                                                                           proj₁-Σ-≡,≡→≡ (proj₁ eq) (proj₂ eq)) ⟩
  (∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
   let q′₁ , q⟶q′₁ = ch₁ p⟶p′
       q′₂ , q⟶q′₂ = ch₂ p⟶p′
   in ∃ λ (eq : ∃ λ (q′₁≡q′₂ : q′₁ ≡ q′₂) →
                  subst (q [ μ ]↝_) q′₁≡q′₂ q⟶q′₁ ≡ q⟶q′₂) →
      R (f₁ (μ , p⟶p′ , refl) , f₂ (μ , p⟶p′ , sym (proj₁ eq))))       ↝⟨ (implicit-∀-cong ext $ implicit-∀-cong ext $ ∀-cong ext λ _ →
                                                                           inverse Σ-assoc) ⟩
  (∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
   let q′₁ , q⟶q′₁ = ch₁ p⟶p′
       q′₂ , q⟶q′₂ = ch₂ p⟶p′
   in ∃ λ (q′₁≡q′₂ : q′₁ ≡ q′₂) →
        subst (q [ μ ]↝_) q′₁≡q′₂ q⟶q′₁ ≡ q⟶q′₂
          ×
        R (f₁ (μ , p⟶p′ , refl) , f₂ (μ , p⟶p′ , sym q′₁≡q′₂)))        ↝⟨ (implicit-∀-cong ext $ implicit-∀-cong ext $ ∀-cong ext λ p⟶p′ →
                                                                           ∃-cong λ q′₁≡q′₂ → ∃-cong λ _ → ≡⇒↝ _ $
                                                                           lemma₄ q′₁≡q′₂) ⟩
  (∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
   let q′₁ , q⟶q′₁ = ch₁ p⟶p′
       q′₂ , q⟶q′₂ = ch₂ p⟶p′
   in ∃ λ (q′₁≡q′₂ : q′₁ ≡ q′₂) →
        subst (q [ μ ]↝_) q′₁≡q′₂ q⟶q′₁ ≡ q⟶q′₂
          ×
        R (subst (X ∘ (p′ ,_)) q′₁≡q′₂ (f₁ (_ , p⟶p′ , refl)) ,
           f₂ (_ , p⟶p′ , refl)))                                      ↔⟨⟩

  (∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
   let q′₁ , q⟶q′₁ , p′≤q′₁ = StepC.challenge (s₁ , f₁) p⟶p′
       q′₂ , q⟶q′₂ , p′≤q′₂ = StepC.challenge (s₂ , f₂) p⟶p′
   in ∃ λ (q′₁≡q′₂ : q′₁ ≡ q′₂) →
        subst (q [ μ ]↝_) q′₁≡q′₂ q⟶q′₁ ≡ q⟶q′₂
          ×
        R (subst (X ∘ (p′ ,_)) q′₁≡q′₂ p′≤q′₁ , p′≤q′₂))               □

  where

  lemma₁ :
    ∀ {p q} {f g : ∀ {p′ μ} → p [ μ ]⟶ p′ → ∃ (q [ μ ]↝_)}
    (eq : (λ {p′ μ} → f {p′ = p′} {μ = μ}) ≡ g)
    {p′ μ} {p⟶p′ : p [ μ ]⟶ p′} →
    _
  lemma₁ {p} {q} {f} {g} eq {p′} {μ} {p⟶p′} =

    subst (λ ch →
             ∃ λ μ → ∃ λ (p⟶p′′ : p [ μ ]⟶ p′) →
             proj₁ (ch p⟶p′′) ≡ proj₁ (f p⟶p′))
          eq (μ , p⟶p′ , refl)                          ≡⟨ push-subst-pair′ {y≡z = eq} _ _ _ ⟩

    ( μ
    , subst₂ (λ { (ch , μ) →
                  ∃ λ (p⟶p′′ : p [ μ ]⟶ p′) →
                  proj₁ (ch p⟶p′′) ≡ proj₁ (f p⟶p′) })
             eq (subst-const eq) (p⟶p′ , refl)
    )                                                   ≡⟨ cong (μ ,_) $
                                                           cong (λ eq → subst (λ { (ch , μ) →
                                                                                ∃ λ (p⟶p′′ : p [ μ ]⟶ p′) →
                                                                                proj₁ (ch p⟶p′′) ≡ proj₁ (f p⟶p′) })
                                                                              eq (p⟶p′ , refl)) $
                                                           Σ-≡,≡→≡-subst-const eq refl ⟩
    ( μ
    , subst (λ { (ch , μ) →
                 ∃ λ (p⟶p′′ : p [ μ ]⟶ p′) →
                 proj₁ (ch p⟶p′′) ≡ proj₁ (f p⟶p′) })
            (cong₂ _,_ eq refl) (p⟶p′ , refl)
    )                                                   ≡⟨⟩

    ( μ
    , subst (λ { (ch , μ) →
                 ∃ λ (p⟶p′′ : p [ μ ]⟶ p′) →
                 proj₁ (ch p⟶p′′) ≡ proj₁ (f p⟶p′) })
            (cong (_, _) eq) (p⟶p′ , refl)
    )                                                   ≡⟨ cong (μ ,_) $ sym $
                                                           subst-∘ _ _ eq ⟩
    ( μ
    , subst (λ ch →
               ∃ λ (p⟶p′′ : p [ μ ]⟶ p′) →
               proj₁ (ch p⟶p′′) ≡ proj₁ (f p⟶p′))
            eq (p⟶p′ , refl)
    )                                                   ≡⟨ cong (μ ,_) $
                                                           push-subst-pair′ {y≡z = eq} _ _ _ ⟩
    ( μ
    , p⟶p′
    , subst₂ (λ { (ch , p⟶p′′) →
                  proj₁ (ch p⟶p′′) ≡ proj₁ (f p⟶p′) })
             eq (subst-const eq) refl
    )                                                   ≡⟨ cong (λ eq → (_ , p⟶p′ , subst (λ { (ch , p⟶p′′) → proj₁ (ch p⟶p′′) ≡ proj₁ (f p⟶p′) })
                                                                                eq refl)) $
                                                           Σ-≡,≡→≡-subst-const eq refl ⟩
    ( μ
    , p⟶p′
    , subst (λ { (ch , p⟶p′′) →
                 proj₁ (ch p⟶p′′) ≡ proj₁ (f p⟶p′) })
            (cong (_, _) eq) refl
    )                                                   ≡⟨ cong (λ eq → (_ , p⟶p′ , eq)) $ sym $
                                                           subst-∘ _ _ eq ⟩
    ( μ
    , p⟶p′
    , subst (λ ch → proj₁ (ch p⟶p′) ≡ proj₁ (f p⟶p′))
            eq refl
    )                                                   ≡⟨ cong (λ eq → (_ , p⟶p′ , eq)) $
                                                           subst-∘ _ _ eq ⟩
    ( μ
    , p⟶p′
    , subst (_≡ proj₁ (f p⟶p′))
            (cong (λ ch → proj₁ (ch p⟶p′)) eq) refl
    )                                                   ≡⟨ cong (λ eq → (_ , p⟶p′ , subst (_≡ _) eq refl)) $
                                                           sym $ sym-sym (cong (λ ch → proj₁ (ch p⟶p′)) eq) ⟩
    ( μ
    , p⟶p′
    , subst (_≡ proj₁ (f p⟶p′))
            (sym $ sym $
               cong (λ ch → proj₁ (ch p⟶p′)) eq)
            refl
    )                                                   ≡⟨ cong (λ eq → (_ , p⟶p′ , eq)) $
                                                           subst-trans (sym $ cong (λ ch → proj₁ (ch p⟶p′)) eq) ⟩∎
    ( μ
    , p⟶p′
    , sym (cong (λ ch → proj₁ (ch p⟶p′)) eq)
    )                                                   ∎

  lemma₂ :
    ∀ {p q} {f g : ∀ {p′ μ} → p [ μ ]⟶ p′ → ∃ (q [ μ ]↝_)}
    (eq : ∀ p′ → (λ {μ} → f {p′ = p′} {μ = μ}) ≡ g)
    {p′ μ} {p⟶p′ : p [ μ ]⟶ p′} →
    _
  lemma₂ {p} {q} {f} {g} eq {p′} {μ} {p⟶p′} =

    cong (λ ch → proj₁ (ch p⟶p′))
         (_↔_.to (implicit-extensionality-isomorphism ext) eq)         ≡⟨⟩

    cong (λ ch → proj₁ (ch p⟶p′))
         (implicit-extensionality (Eq.good-ext ext) eq)                ≡⟨ cong-∘ _ _ (apply-ext (Eq.good-ext ext) eq) ⟩∎

    cong (λ ch → proj₁ (ch p′ p⟶p′)) (apply-ext (Eq.good-ext ext) eq)  ∎

  lemma₃ :
    ∀ {p q} {f g : ∀ {p′ μ} → p [ μ ]⟶ p′ → ∃ (q [ μ ]↝_)}
    (eq : ∀ p′ μ → f {p′ = p′} {μ = μ} ≡ g) {p′ μ p⟶p′} →
    _
  lemma₃ {p} {q} {f} {g} eq {p′} {μ} {p⟶p′} =

    cong (λ (ch : ∀ _ {μ} → _) → proj₁ (ch p′ {μ = μ} p⟶p′))
         (apply-ext (Eq.good-ext ext)
            (implicit-extensionality (Eq.good-ext ext) ∘ eq))             ≡⟨⟩

    cong (λ ch → proj₁ (ch p′ p⟶p′))
         (apply-ext (Eq.good-ext ext)
            (cong (λ f {x} → f x) ∘ (apply-ext (Eq.good-ext ext) ∘ eq)))  ≡⟨ cong (cong (λ ch → proj₁ (ch p′ p⟶p′))) $ sym $
                                                                             Eq.cong-post-∘-good-ext {h = λ f {x} → f x} ext ext
                                                                                (apply-ext (Eq.good-ext ext) ∘ eq) ⟩
    cong (λ ch → proj₁ (ch p′ p⟶p′))
         (cong (λ f x {y} → f x y)
               (apply-ext (Eq.good-ext ext)
                  (apply-ext (Eq.good-ext ext) ∘ eq)))                    ≡⟨ cong-∘ _ _ (apply-ext (Eq.good-ext ext)
                                                                                (apply-ext (Eq.good-ext ext) ∘ eq)) ⟩
    cong (λ ch → proj₁ (ch p′ μ p⟶p′))
         (apply-ext (Eq.good-ext ext)
            (apply-ext (Eq.good-ext ext) ∘ eq))                           ≡⟨ sym $ cong-∘ _ _ (apply-ext (Eq.good-ext ext)
                                                                                (apply-ext (Eq.good-ext ext) ∘ eq)) ⟩
    cong (λ ch → proj₁ (ch μ p⟶p′))
         (cong (_$ p′) (apply-ext (Eq.good-ext ext)
                          (apply-ext (Eq.good-ext ext) ∘ eq)))            ≡⟨ cong (cong (λ ch → proj₁ (ch μ p⟶p′))) $ Eq.cong-good-ext ext _ ⟩

    cong (λ ch → proj₁ (ch μ p⟶p′))
         (apply-ext (Eq.good-ext ext) (eq p′))                            ≡⟨ sym $ cong-∘ _ _ (apply-ext (Eq.good-ext ext) (eq p′)) ⟩

    cong (λ ch → proj₁ (ch p⟶p′))
         (cong (_$ μ) (apply-ext (Eq.good-ext ext) (eq p′)))              ≡⟨ cong (cong (λ ch → proj₁ (ch p⟶p′))) $ Eq.cong-good-ext ext _ ⟩∎

    cong (λ ch → proj₁ (ch p⟶p′)) (eq p′ μ)                               ∎

  lemma₄ :
    ∀ {p′ μ} {p⟶p′ : p [ μ ]⟶ p′}
    (q′₁≡q′₂ : proj₁ (ch₁ p⟶p′) ≡ proj₁ (ch₂ p⟶p′)) →
    R (f₁ (μ , p⟶p′ , refl) , f₂ (μ , p⟶p′ , sym q′₁≡q′₂))
      ≡
    R (subst (X ∘ (p′ ,_)) q′₁≡q′₂ (f₁ (_ , p⟶p′ , refl)) ,
       f₂ (_ , p⟶p′ , refl))
  lemma₄ {p′} {μ} {p⟶p′} q′₁≡q′₂ =
    R (f₁ (μ , p⟶p′ , refl) , f₂ (μ , p⟶p′ , sym q′₁≡q′₂))        ≡⟨ cong (R ∘ (f₁ _ ,_)) $ lemma′ q′₁≡q′₂ ⟩

    R (f₁ (μ , p⟶p′ , refl) ,
       subst (X ∘ (p′ ,_)) (sym q′₁≡q′₂) (f₂ (_ , p⟶p′ , refl)))  ≡⟨ lemma″ q′₁≡q′₂ ⟩∎

    R (subst (X ∘ (p′ ,_)) q′₁≡q′₂ (f₁ (_ , p⟶p′ , refl)) ,
       f₂ (_ , p⟶p′ , refl))                                      ∎
    where
    lemma′ :
      ∀ {q′₁} (q′₁≡q′₂ : q′₁ ≡ proj₁ (ch₂ p⟶p′)) →
      f₂ (μ , p⟶p′ , sym q′₁≡q′₂)
        ≡
      subst (X ∘ (p′ ,_)) (sym q′₁≡q′₂) (f₂ (_ , p⟶p′ , refl))
    lemma′ refl = refl

    lemma″ :
      ∀ {q′₂ x} (q′₁≡q′₂ : proj₁ (ch₁ p⟶p′) ≡ q′₂) →
      R (f₁ (μ , p⟶p′ , refl) , subst (X ∘ (p′ ,_)) (sym q′₁≡q′₂) x)
        ≡
      R (subst (X ∘ (p′ ,_)) q′₁≡q′₂ (f₁ (_ , p⟶p′ , refl)) , x)
    lemma″ refl = refl

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
module Holes.Util where

open import Holes.Prelude

private
  Rel : ∀ {a} → Set a → ∀ ℓ → Set (a ⊔ lsuc ℓ)
  Rel A ℓ = A → A → Set ℓ

module CongSplit {ℓ x} {X : Set x} (_≈_ : Rel X ℓ) (reflexive : ∀ {x} → x ≈ x) where

  two→one₁ : {_+_ : X → X → X}
            → (∀ {x x′ y y′} → x ≈ x′ → y ≈ y′ → (x + y) ≈ (x′ + y′))
            → (∀ x y {x′} → x ≈ x′ → (x + y) ≈ (x′ + y))
  two→one₁ cong² _ _ eq = cong² eq reflexive

  two→one₂ : {_+_ : X → X → X}
           → (∀ {x x′ y y′} → x ≈ x′ → y ≈ y′ → (x + y) ≈ (x′ + y′))
           → (∀ x y {y′} → y ≈ y′ → (x + y) ≈ (x + y′))
  two→one₂ cong² _ _ eq = cong² reflexive eq


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

open import HoTT
open import homotopy.CircleHSpace
open import homotopy.LoopSpaceCircle
open import homotopy.Pi2HSusp
open import homotopy.IterSuspensionStable

-- This summerizes all [πₙ Sⁿ]
module homotopy.PinSn where

  private
    -- another way is to use path induction to prove the other direction,
    -- but personally I do not feel it is easier.
    abstract
      -- proved in LoopSpaceCircle
      -- loop^succ : ∀ (z : ℤ) → loop^ z ∙ loop == loop^ (succ z)

      -- mimicking [loop^pred]
      loop^pred : ∀ (z : ℤ) → loop^ z ∙ ! loop == loop^ (pred z)
      loop^pred (negsucc n) = idp
      loop^pred (pos O) = idp
      loop^pred (pos (S n)) =
        (loop^ (pos n) ∙ loop) ∙ ! loop
          =⟨ ∙-assoc (loop^ (pos n)) loop (! loop) ⟩
        loop^ (pos n) ∙ (loop ∙ ! loop)
          =⟨ !-inv-r loop |in-ctx loop^ (pos n) ∙_ ⟩
        loop^ (pos n) ∙ idp
          =⟨ ∙-unit-r $ loop^ (pos n) ⟩
        loop^ (pos n)
          ∎

      -- because of how [loop^] is defined,
      -- it is easier to prove the swapped version
      loop^-ℤ+' : ∀ (z₁ z₂ : ℤ) →
        loop^ (z₁ ℤ+ z₂) == loop^ z₂ ∙ loop^ z₁
      loop^-ℤ+' (pos O) z₂ = ! $ ∙-unit-r (loop^ z₂)
      loop^-ℤ+' (pos (S n₁)) z₂ =
        loop^ (succ (pos n₁ ℤ+ z₂))
          =⟨ ! $ loop^succ (pos n₁ ℤ+ z₂) ⟩
        loop^ (pos n₁ ℤ+ z₂) ∙ loop
          =⟨ loop^-ℤ+' (pos n₁) z₂ |in-ctx _∙ loop ⟩
        (loop^ z₂ ∙ loop^ (pos n₁)) ∙ loop
          =⟨ ∙-assoc (loop^ z₂) (loop^ (pos n₁)) loop ⟩
        loop^ z₂ ∙ (loop^ (pos n₁) ∙ loop)
          ∎
      loop^-ℤ+' (negsucc O) z₂ = ! $ loop^pred z₂
      loop^-ℤ+' (negsucc (S n₁)) z₂ =
        loop^ (pred (negsucc n₁ ℤ+ z₂))
          =⟨ ! $ loop^pred (negsucc n₁ ℤ+ z₂) ⟩
        loop^ (negsucc n₁ ℤ+ z₂) ∙ ! loop
          =⟨ loop^-ℤ+' (negsucc n₁) z₂ |in-ctx _∙ ! loop ⟩
        (loop^ z₂ ∙ loop^ (negsucc n₁)) ∙ ! loop
          =⟨ ∙-assoc (loop^ z₂) (loop^ (negsucc n₁)) (! loop) ⟩
        loop^ z₂ ∙ (loop^ (negsucc n₁) ∙ ! loop)
          ∎

    loop^-ℤ+ : ∀ (z₁ z₂ : ℤ) →
      loop^ (z₁ ℤ+ z₂) == loop^ z₁ ∙ loop^ z₂
    loop^-ℤ+ z₁ z₂ = ap loop^ (ℤ+-comm z₁ z₂) ∙ loop^-ℤ+' z₂ z₁

    ℤ-to-π₁S¹ : ℤ-group →ᴳ πS 0 ⊙S¹
    ℤ-to-π₁S¹ =
      record { f = [_] ∘ loop^
             ; pres-comp = λ z₁ z₂ → ap [_] $ loop^-ℤ+ z₁ z₂
             }

    ℤ-to-π₁S¹-equiv : ℤ-group ≃ᴳ πS 0 ⊙S¹
    ℤ-to-π₁S¹-equiv = ℤ-to-π₁S¹ , snd (unTrunc-equiv (Ω^ 1 ⊙S¹) (ΩS¹-is-set base) ⁻¹ ∘e ΩS¹≃ℤ ⁻¹)

  π₁S¹ : πS 0 ⊙S¹ == ℤ-group
  π₁S¹ = ! $ group-ua ℤ-to-π₁S¹-equiv

  π₂S² : πS 1 ⊙S² == ℤ-group
  π₂S² =
    πS 1 ⊙S²
      =⟨ Pi2HSusp.π₂-Suspension S¹ S¹-level S¹-connected S¹-hSpace ⟩
    πS 0 ⊙S¹
      =⟨ π₁S¹ ⟩
    ℤ-group
      ∎

  private
    πₙ₊₂Sⁿ⁺² : ∀ n → πS (S n) (⊙Susp^ (S n) ⊙S¹) == ℤ-group
    πₙ₊₂Sⁿ⁺² 0 = π₂S²
    πₙ₊₂Sⁿ⁺² (S n) =
      πS (S (S n)) (⊙Susp^ (S (S n)) ⊙S¹)
        =⟨ Susp^StableSucc.stable ⊙S¹ S¹-connected
             (S n) (S n) (≤-ap-S $ ≤-ap-S $ *2-increasing n) ⟩
      πS (S n) (⊙Susp^ (S n) ⊙S¹)
        =⟨ πₙ₊₂Sⁿ⁺² n ⟩
      ℤ-group
        ∎

    lemma : ∀ n → ⊙Susp^ n ⊙S¹ == ⊙Sphere (S n)
    lemma n = ⊙Susp^-+ n 1 ∙ ap ⊙Sphere (+-comm n 1)

  πₙ₊₁Sⁿ⁺¹ : ∀ n → πS n (⊙Sphere (S n)) == ℤ-group
  πₙ₊₁Sⁿ⁺¹ 0 = π₁S¹
  πₙ₊₁Sⁿ⁺¹ (S n) = ap (πS (S n)) (! $ lemma (S n)) ∙ πₙ₊₂Sⁿ⁺² n

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
open import MLib.Algebra.PropertyCode
open import MLib.Algebra.PropertyCode.Structures

module MLib.Matrix.Bimonoid {c ℓ} (struct : Struct bimonoidCode c ℓ) where

open import MLib.Prelude
open import MLib.Matrix.Core
open import MLib.Matrix.Equality struct
open import MLib.Matrix.Mul struct
open import MLib.Matrix.Plus struct
open import MLib.Algebra.Operations struct
open import MLib.Algebra.PropertyCode.Dependent struct

open FunctionProperties

matrixRawStruct : ∀ n → RawStruct BimonoidK _ _
matrixRawStruct n = record
  { appOp = λ
    { + (A ∷ B ∷ []) → A ⊕ B
    ; * (A ∷ B ∷ []) → A ⊗ B
    ; 0# [] → 0●
    ; 1# [] → 1●
    }
  ; isRawStruct = record
    { isEquivalence = isEquivalence {n} {n}
    ; congⁿ = λ
      { + (p ∷ q ∷ []) i j → cong + (p i j) (q i j)
      ; * (p ∷ q ∷ []) → ⊗-cong p q
      ; 0# [] _ _ → S.refl
      ; 1# [] _ _ → S.refl
      }
    }
  }

matrixStruct : ∀ n → Struct bimonoidCode _ _
matrixStruct n = dependentStruct (matrixRawStruct n)
  ( (commutative on + , _ , ⊕-comm)
  ∷ (associative on + , _ , ⊕-assoc)
  ∷ (0# is leftIdentity for + , _ , ⊕-identityˡ)
  ∷ (0# is rightIdentity for + , _ , ⊕-identityʳ)
  ∷ (associative on * , _ , ⊗-assoc)
  ∷ (* ⟨ distributesOverˡ ⟩ₚ + , _ , ⊗-distributesOverˡ-⊕)
  ∷ [])


text:
open import Common.Prelude

record IsNumber (A : Set) : Set where
  field fromNat : Nat → A

open IsNumber {{...}} public

{-# BUILTIN FROMNAT fromNat #-}

instance
  IsNumberNat : IsNumber Nat
  IsNumberNat = record { fromNat = λ n → n }

record IsNegative (A : Set) : Set where
  field fromNeg : Nat → A

open IsNegative {{...}} public

{-# BUILTIN FROMNEG fromNeg #-}

data Int : Set where
  pos : Nat → Int
  neg : Nat → Int

instance
  IsNumberInt : IsNumber Int
  IsNumberInt = record { fromNat = pos }

  IsNegativeInt : IsNegative Int
  IsNegativeInt = record { fromNeg = neg }

fiveN : Nat
fiveN = 5

fiveZ : Int
fiveZ = 5

minusFive : Int
minusFive = -5

open import Common.Equality

thm : pos 5 ≡ 5
thm = refl

thm′ : neg 5 ≡ -5
thm′ = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --cubical #-}

module Cubical.Categories.Category where

open import Cubical.Foundations.Prelude

record Precategory ℓ ℓ' : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  no-eta-equality
  field
    ob : Type ℓ
    hom : ob → ob → Type ℓ'
    idn : ∀ x → hom x x
    seq : ∀ {x y z} (f : hom x y) (g : hom y z) → hom x z
    seq-λ : ∀ {x y : ob} (f : hom x y) → seq (idn x) f ≡ f
    seq-ρ : ∀ {x y} (f : hom x y) → seq f (idn y) ≡ f
    seq-α : ∀ {u v w x} (f : hom u v) (g : hom v w) (h : hom w x) → seq (seq f g) h ≡ seq f (seq g h)

open Precategory public

record isCategory {ℓ ℓ'} (𝒞 : Precategory ℓ ℓ') : Type (ℓ-max ℓ ℓ') where
  field
    homIsSet : ∀ {x y} → isSet (𝒞 .hom x y)

open isCategory public

_^op : ∀ {ℓ ℓ'} → Precategory ℓ ℓ' → Precategory ℓ ℓ'
(𝒞 ^op) .ob = 𝒞 .ob
(𝒞 ^op) .hom x y = 𝒞 .hom y x
(𝒞 ^op) .idn = 𝒞 .idn
(𝒞 ^op) .seq f g = 𝒞 .seq g f
(𝒞 ^op) .seq-λ = 𝒞 .seq-ρ
(𝒞 ^op) .seq-ρ = 𝒞 .seq-λ
(𝒞 ^op) .seq-α f g h = sym (𝒞 .seq-α _ _ _)

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


text:
------------------------------------------------------------------------
-- Acyclic precedence graphs
------------------------------------------------------------------------

module Mixfix.Acyclic.PrecedenceGraph where

open import Data.List
open import Data.Product

open import Mixfix.Fixity
open import Mixfix.Operator
open import Mixfix.Expr

-- Precedence graphs are represented by their unfoldings as forests
-- (one tree for every node in the graph). This does not take into
-- account the sharing of the precedence graphs, but this code is
-- not aimed at efficiency.

-- Precedence trees.

data Precedence : Set where
  precedence : (o : (fix : Fixity) → List (∃ (Operator fix)))
               (s : List Precedence) →
               Precedence

-- Precedence forests.

PrecedenceGraph : Set
PrecedenceGraph = List Precedence

-- The operators of the given precedence.

ops : Precedence → (fix : Fixity) → List (∃ (Operator fix))
ops (precedence o s) = o

-- The immediate successors of the precedence level.

↑ : Precedence → List Precedence
↑ (precedence o s) = s

-- Acyclic precedence graphs.

acyclic : PrecedenceGraphInterface
acyclic = record
  { PrecedenceGraph = PrecedenceGraph
  ; Precedence      = λ _ → Precedence
  ; ops             = λ _ → ops
  ; ↑               = λ _ → ↑
  ; anyPrecedence   = λ g → g
  }

max_stars_repo_name: yurrriq/parser-combinators