text:
open import Relation.Binary.Core

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

open import Data.Sum
open import PLRTree {A}
open import PLRTree.Complete {A}
open import PLRTree.Compound {A}
open import PLRTree.Drop _≤_ tot≤
open import PLRTree.DropLast.Complete _≤_ tot≤
open import PLRTree.Equality {A}
open import PLRTree.Order.Properties {A}
open import PLRTree.Push.Complete _≤_ tot≤

lemma-setRoot-complete : {t : PLRTree}(x : A) → Complete t → Complete (setRoot x t)
lemma-setRoot-complete x leaf = leaf
lemma-setRoot-complete x (perfect _ cl cr l≃r) = perfect x cl cr l≃r
lemma-setRoot-complete x (left _ cl cr l⋘r) = left x cl cr l⋘r
lemma-setRoot-complete x (right _ cl cr l⋙r) = right x cl cr l⋙r

lemma-drop-complete : {t : PLRTree} → Complete t → Complete (drop t)
lemma-drop-complete leaf = leaf
lemma-drop-complete (perfect _ _ _ ≃lf) = leaf
lemma-drop-complete (perfect {node perfect x' l' r'} {node perfect x'' l'' r''} x (perfect .x' cl' cr' _) (perfect .x'' cl'' cr'' _) (≃nd .x' .x'' l'≃r' l''≃r'' l'≃l'')) =
                 let z = last (node perfect x (node perfect x' l' r') (node perfect x'' l'' r'')) compound ;
                      t' = dropLast (node perfect x (node perfect x' l' r') (node perfect x'' l'' r'')) ;
                      ct' = right x (perfect x' cl' cr' l'≃r') (lemma-dropLast-complete (perfect x'' cl'' cr'' l''≃r'')) (lemma-dropLast-≃ (≃nd x' x'' l'≃r' l''≃r'' l'≃l'') compound)
                 in lemma-push-complete (lemma-setRoot-complete z ct') (≺-wf (setRoot z t'))
lemma-drop-complete (left {l} {r} x cl cr l⋘r)
    with l | r | l⋘r | lemma-dropLast-⋘ l⋘r
... | leaf | _ | () | _
... | node perfect x' l' r' | _ | () | _
... | node left x' l' r' | node perfect x'' l'' r'' | l⋘ .x' .x'' l'⋘r' l''≃r'' r'≃l'' | inj₁ ld⋘r
    with dropLast (node left x' l' r') | ld⋘r | lemma-dropLast-complete cl
... | leaf | () | _
... | node perfect _ _ _ | () | _
... | node left x''' l''' r''' | ld⋘r' | cld =
                 let z = last (node left x (node left x' l' r') (node perfect x'' l'' r'')) compound ;
                      t' = node left x (node left x''' l''' r''') (node perfect x'' l'' r'') ;
                      ct' = left x cld cr ld⋘r'
                 in lemma-push-complete (lemma-setRoot-complete z ct') (≺-wf (setRoot z t'))
... | node right x''' l''' r''' | ld⋘r' | cld =
                 let z = last (node left x (node left x' l' r') (node perfect x'' l'' r'')) compound ;
                      t' = node left x (node right x''' l''' r''') (node perfect x'' l'' r'') ;
                      ct' = left x cld cr ld⋘r'
                 in lemma-push-complete (lemma-setRoot-complete z ct') (≺-wf (setRoot z t'))
lemma-drop-complete (left x cl cr l⋘r) | node left x' l' r' | node perfect x'' l'' r'' | l⋘ .x' .x'' l'⋘r' l''≃r'' r'≃l'' | inj₂ ld≃r
    with dropLast (node left x' l' r') | ld≃r | lemma-dropLast-complete cl
... | leaf | () | _
... | node perfect x''' l''' r''' | ld≃r' | cld =
                 let z = last (node left x (node left x' l' r') (node perfect x'' l'' r'')) compound ;
                      t' = node perfect x (node perfect x''' l''' r''') (node perfect x'' l'' r'') ;
                      ct' = perfect x cld cr ld≃r'
                 in lemma-push-complete (lemma-setRoot-complete z ct') (≺-wf (setRoot z t'))
... | node left _ _ _ | () | _
... | node right _ _ _ | () | _
lemma-drop-complete (left x cl cr l⋘r) | node right x' l' r' | leaf | () | _
lemma-drop-complete (left x cl cr l⋘r) | node right x' (node perfect x'' leaf leaf) leaf | node perfect x''' leaf leaf | x⋘ .x' .x'' .x''' | inj₁ ()
lemma-drop-complete (left x cl cr l⋘r) | node right x' (node perfect x'' leaf leaf) leaf | node perfect x''' leaf leaf | x⋘ .x' .x'' .x''' | inj₂ x'≃x''' =
                 let z = last (node left x (node right x' (node perfect x'' leaf leaf) leaf) (node perfect x''' leaf leaf)) compound ;
                      t' = dropLast (node left x (node right x' (node perfect x'' leaf leaf) leaf) (node perfect x''' leaf leaf)) ;
                      ct' = perfect x (perfect x' leaf leaf ≃lf) cr x'≃x'''
                 in lemma-push-complete (lemma-setRoot-complete z ct') (≺-wf (setRoot z t'))
lemma-drop-complete (left x cl cr l⋘r) | node right x' l' r' | node perfect x'' l'' r'' | r⋘ .x' .x'' l⋙r l''≃r'' l'⋗l'' | inj₁ ld⋘r
    with dropLast (node right x' l' r') | ld⋘r | lemma-dropLast-complete cl
... | leaf | () | _
... | node perfect _ _ _ | () | _
... | node left x''' l''' r''' | ld⋘r' | cld =
                 let z = last (node left x (node right x' l' r') (node perfect x'' l'' r'')) compound ;
                      t' = node left x (node left x''' l''' r''') (node perfect x'' l'' r'') ;
                      ct' = left x cld cr ld⋘r'
                 in lemma-push-complete (lemma-setRoot-complete z ct') (≺-wf (setRoot z t'))
... | node right x''' l''' r''' | ld⋘r' | cld =
                 let z = last (node left x (node right x' l' r') (node perfect x'' l'' r'')) compound ;
                      t' = node left x (node right x''' l''' r''') (node perfect x'' l'' r'') ;
                      ct' = left x cld cr ld⋘r'
                 in lemma-push-complete (lemma-setRoot-complete z ct') (≺-wf (setRoot z t'))
lemma-drop-complete (left x cl cr l⋘r) | node right x' l' r' | node perfect x'' l'' r'' | r⋘ .x' .x'' l⋙r l''≃r'' l'⋗l'' | inj₂ ld≃r
    with dropLast (node right x' l' r') | ld≃r | lemma-dropLast-complete cl
... | leaf | () | _
... | node perfect x''' l''' r''' | ld≃r' | cld =
                 let z = last (node left x (node right x' l' r') (node perfect x'' l'' r'')) compound ;
                      t' = node perfect x (node perfect x''' l''' r''') (node perfect x'' l'' r'') ;
                      ct' = perfect x cld cr ld≃r'
                 in lemma-push-complete (lemma-setRoot-complete z ct') (≺-wf (setRoot z t'))
... | node left _ _ _ | () | _
... | node right _ _ _ | () | _
lemma-drop-complete (left x cl cr l⋘r) | node right x' l' r' | node left x'' l'' r'' | () | _
lemma-drop-complete (left x cl cr l⋘r) | node right x' l' r' | node right x'' l'' r'' | () | _
lemma-drop-complete (right {l} {r} x cl cr l⋙r)
    with l | r | l⋙r | lemma-dropLast-⋙ l⋙r
... | leaf | leaf | ⋙p () | _
... | node perfect x' leaf leaf | leaf | ⋙p (⋗lf .x') | _ = cl
... | node perfect _ _ (node _ _ _ _) | leaf | ⋙p () | _
... | node perfect _ (node _ _ _ _) _ | leaf | ⋙p () | _
... | node left _ _ _ | leaf | ⋙p () | _
... | node right _ _ _ | leaf | ⋙p () | _
... | leaf | node perfect _ _ _ | ⋙p () | _
... | node perfect x' l' r' | node perfect x'' l'' r'' | ⋙p (⋗nd .x' .x'' l'≃r' l''≃r'' l'⋗l'') | _ =
                 let z = last (node right x (node perfect x' l' r') (node perfect x'' l'' r'')) compound ;
                      t' = dropLast (node right x (node perfect x' l' r') (node perfect x'' l'' r'')) ;
                      ct' = left x (lemma-dropLast-complete cl) cr (lemma-dropLast-⋗ (⋗nd x' x'' l'≃r' l''≃r'' l'⋗l'') compound)
                 in lemma-push-complete (lemma-setRoot-complete z ct') (≺-wf (setRoot z t'))
... | node left _ _ _ | node perfect _ _ _ | ⋙p () | _
... | node right _ _ _ | node perfect _ _ _ | ⋙p () | _
... | leaf | node left _ _ _ | ⋙p () | _
... | node perfect x' l' r' | node left x'' l'' r'' | _ | inj₁ l⋙rd =
                 let z = last (node right x (node perfect x' l' r') (node left x'' l'' r'')) compound ;
                      t' = dropLast (node right x (node perfect x' l' r') (node left x'' l'' r'')) ;
                      ct' = right x cl (lemma-dropLast-complete cr) l⋙rd
                 in lemma-push-complete (lemma-setRoot-complete z ct') (≺-wf (setRoot z t'))
... | node perfect _ _ _ | node left _ _ _ | _  | inj₂ ()
... | node left _ _ _ | node left _ _ _ | ⋙p () | _
... | node right _ _ _ | node left _ _ _ | ⋙p () | _
... | leaf | node right _ _ _ | ⋙p () | _
... | node perfect x' l' r' | node right x'' l'' r'' | _ | inj₁ l⋙rd =
                 let z = last (node right x (node perfect x' l' r') (node right x'' l'' r'')) compound ;
                      t' = dropLast (node right x (node perfect x' l' r') (node right x'' l'' r'')) ;
                      ct' = right x cl (lemma-dropLast-complete cr) l⋙rd
                 in lemma-push-complete (lemma-setRoot-complete z ct') (≺-wf (setRoot z t'))
... | node perfect _ _ _ | node right _ _ _ | _ | inj₂ ()
... | node left _ _ _ | node right _ _ _ | ⋙p () | _
... | node right _ _ _ | node right _ _ _ | ⋙p () | _

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


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

module Cubical.Categories.Equivalence.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Categories.Category
open import Cubical.Categories.Functor
open import Cubical.Categories.NaturalTransformation

open Precategory
open Functor

private
  variable
    ℓC ℓC' ℓD ℓD' : Level

-- Definition

record isEquivalence {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'}
                     (func : Functor C D) : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
  field
    invFunc : Functor D C

    η : 𝟙⟨ C ⟩ ≅ᶜ invFunc ∘F func
    ε : func ∘F invFunc ≅ᶜ 𝟙⟨ D ⟩

record _≃ᶜ_ (C : Precategory ℓC ℓC') (D : Precategory ℓD ℓD') : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
  field
    func : Functor C D
    isEquiv : isEquivalence func

ext: agda

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
-- Let-definitions cannot pattern match (or be recursive). Use where for that.
module NotAValidLetBinding where

data N : Set where
  z : N
  s : N -> N

bad = let pred : N -> N
          pred z     = z
          pred (s n) = n
      in pred (s (s z))

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import Categories.Category

module Categories.Diagram.Equalizer.Properties {o ℓ e} (C : Category o ℓ e) where

open import Categories.Diagram.Equalizer C
open import Categories.Morphism C
open import Categories.Morphism.Reasoning C

private
  module C = Category C
  open C

  variable
    X Y Z : Obj
    f g : X ⇒ Y

module _ (equalizer : Equalizer f g) where
  open Equalizer equalizer
  open HomReasoning

  equalizer-≈⇒≈ : ∀ {h} → arr ∘ h ≈ id → f ≈ g
  equalizer-≈⇒≈ {h} eq = begin
    f             ≈⟨ introʳ eq ⟩
    f ∘ arr ∘ h   ≈⟨ pullˡ equality ⟩
    (g ∘ arr) ∘ h ≈⟨ cancelʳ eq ⟩
    g             ∎

section-equalizer : ∀ {X Y} {f : Y ⇒ X} {g : X ⇒ Y} → f SectionOf g → IsEqualizer f (f ∘ g) id
section-equalizer {X = X} {Y = Y} {f = f} {g = g} g∘f≈id = record
  { equality = equality
  ; equalize = equalize
  ; universal = λ {_} {_} {eq} → universal {eq = eq}
  ; unique = unique
  }
  where
    open HomReasoning

    equality : (f ∘ g) ∘ f ≈ id ∘ f
    equality = begin
      (f ∘ g) ∘ f ≈⟨ pullʳ g∘f≈id ⟩
      f ∘ id      ≈⟨ id-comm ⟩
      id ∘ f      ∎

    equalize : ∀ {Z} {h : Z ⇒ X} → (f ∘ g) ∘ h ≈ id ∘ h → Z ⇒ Y
    equalize {h = h} _ = g ∘ h

    universal : ∀ {Z} {h : Z ⇒ X} {eq : (f ∘ g) ∘ h ≈ id ∘ h} → h ≈ f ∘ g ∘ h
    universal {h = h} {eq = eq} = begin
      h           ≈˘⟨ identityˡ ⟩
      id ∘ h      ≈˘⟨ eq ⟩
      (f ∘ g) ∘ h ≈⟨ assoc ⟩
      f ∘ g ∘ h   ∎

    unique : ∀ {Z} {h : Z ⇒ X} {i : Z ⇒ Y} → h ≈ f ∘ i → i ≈ g ∘ h
    unique {h = h} {i = i} h≈g∘i = begin
      i           ≈⟨ introˡ g∘f≈id ⟩
      (g ∘ f) ∘ i ≈⟨ pullʳ (⟺ h≈g∘i) ⟩
      g ∘ h       ∎

max_stars_repo_name: maxsnew/agda-categories

max_issues_repo_name: maxsnew/agda-categories

max_forks_repo_name: maxsnew/agda-categories


text:
-- Andreas, 2011-10-02
module IrrelevantLet where

postulate
  A : Set

test : (.A → A) → .A → A
test = λ f a →
         let .b : A
             b  = f a
         in  f a

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
data Size : Set where

↑ : Size → Size
↑ ()

data N : Size → Set where
  suc : ∀{i} (a : N i) → N (↑ i)

data Val : ∀{i} (t : N i) → Set where
  val : ∀{i} (n : N i) → Val (suc n)

record R (j : Size) : Set where
  field num : N j

data W {j} (ft : R j) : Set where
  immed : (v : Val (R.num ft)) → W ft

postulate
  E : ∀{j} (ft : R j) (P : (w : W ft) → Set) → Set

test : ∀ {j} (ft : R j) → Set
test {j} ft = E {j} ft testw
  where
  testw : ∀ {ft : R _} (w : W ft) → Set
  testw (immed (val a)) = test record{ num = a }

-- testw passes without quantification over ft
-- or with _ := j

{- OLD ERROR

Cannot instantiate the metavariable _35 to solution ↑ i since it
contains the variable i which is not in scope of the metavariable
or irrelevant in the metavariable but relevant in the solution
when checking that the pattern val a has type Val (R.num ft₁)
-}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --sized-types #-}
open import Relation.Binary.Core

module BubbleSort  {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_) where

open import Data.List
open import Data.Product
open import Data.Sum
open import Size
open import SList

swap* : {ι : Size} → A → SList A {ι} → SList A {ι} × A
swap* x snil = (snil , x)
swap* x (y ∙ ys)
    with tot≤ x y
... | inj₁ x≤y
     with swap* y ys
swap* x (y ∙ ys) | inj₁ x≤y | (zs , z) = (x ∙ zs , z)
swap* x (y ∙ ys) | inj₂ y≤x
    with swap* x ys
swap* x (y ∙ ys) | inj₂ y≤x | (zs , z) = (y ∙ zs , z)

bubbleSort : {ι : Size} → SList A {ι} → SList A
bubbleSort snil = snil
bubbleSort (x ∙ xs)
    with swap* x xs
... | (ys , y) = _⊕_ A (bubbleSort ys) (y ∙ snil)


text:
module Issue2649-2 where

open import Issue2649-1

open module M (A : Set) (a : A) = MyModule A a public


text:
open import Data.String using (String)
open import Data.List using (List; []; _∷_)
open import Data.Nat using (ℕ)
open import Data.Product
open import Data.Bool
open import Data.Maybe
open import Data.Vec as V using (Vec; []; _∷_)
open import Data.Fin as F using (Fin; zero; suc)

open import Reflection using (TC)
open import Reflection.Name using (Names)
import Reflection.TypeChecking.Monad.Categorical as RCat

open import Category.Monad.State using (State; StateT; StateMonad; StateTMonad)
open import Category.Monad using (RawMonad)

--open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Nullary
import      Relation.Unary as UR
open import Relation.Nullary.Negation using (contradiction)

open import Function

-- This is a `Maybe`-like data type except that nothing
-- is extended with a string argument, to carry around the error.
data Err {a} (A : Set a) : Set a where
  error : String → Err A
  ok : A → Err A

-- Our representation for programs: it is either a string containing
-- textual representation of the extracted program or an error that
-- happened during extraction.
Prog = Err String

-- Simply for convenience
Strings = List String

-- We define a custom RawMonoid to add `_++/_` (list join)
-- an its overloadings.
record RawMonoid {a}(A : Set a) : Set a where
  field
    _++_ : A → A → A
    ε : A
  _++/_ : (delim : A) → List A → A
  d ++/ [] = ε
  d ++/ (x ∷ []) = x
  d ++/ (x ∷ xs) = x ++ d ++ d ++/ xs

  infixr 5 _++_

open RawMonoid {{...}} public

instance
  monoidLst : ∀ {a}{A : Set a} → RawMonoid (List A)
  monoidLst {A = A} = record {
    _++_ = λ a b → (Data.List._++_ $! a) $! b ;
    ε = []
    }

  monoidStr : RawMonoid String
  monoidStr = record {
    _++_ = λ a b → (Data.String._++_ $! a) $! b;
    ε = ""
    }

  monoidErrStr : RawMonoid (Err String)
  monoidErrStr = record {
    _++_ =  λ where
      (error s) _ → error s
      _ (error s) → error s
      (ok s₁) (ok s₂) → ok (s₁ ++ s₂)
    ;
    ε = ok ""
    }

-- Simplify handling concatenation of `Prog`s and `String`s
data Err++Ty : Set → Set → Set where
  instance
    s-s : Err++Ty String String
    e-s : Err++Ty Prog String
    s-e : Err++Ty String Prog
    e-e : Err++Ty Prog Prog

infixr 5 _⊕_
_⊕_ : ∀ {A B}{{t : Err++Ty A B}} → A → B → Prog
_⊕_ {{t = s-s}} a         b = ok $! (a ++ b)
_⊕_ {{t = e-s}} (error x) b = error $! x
_⊕_ {{t = e-s}} (ok x)    b = ok $! (x ++ b)
_⊕_ {{t = s-e}} a (error x) = error $! x
_⊕_ {{t = s-e}} a    (ok x) = ok $! (a ++ x)
_⊕_ {{t = e-e}} a         b = id $! (a ++ b)

-- The state used at the top-most and term-level compilation.
record KS : Set where
  constructor ks
  field funs : Names   -- Functions to compile
        base : Names   -- Atomic functions that we do not traverse into.
        done : Names   -- Functions that we have processed.
        defs : Prog    -- Definitions such as lifted functions, function declarations, etc.
        cnt  : ℕ       -- Source of fresh variables

defaultKS = ks [] [] [] ε 1

SKS = State KS
TCS = StateT KS TC

instance
  monadTC = RCat.monad

  monadTCS : RawMonad TCS
  monadTCS = StateTMonad KS monadTC

  monadSKS : ∀ {S : Set} → RawMonad (State S)
  monadSKS {S} = StateMonad S

  monadErr : ∀ {f} → RawMonad {f} Err
  monadErr = record {
    return = ok ;
    _>>=_ = λ { (error s) f → error s ; (ok a) f → f a }
    }

lift-state : ∀ {f}{M}{RM : RawMonad {f} M}{A}{S} → M A → StateT S M A
lift-state {RM = RM} x = λ s → return (_, s) ⊛ x
          where open RawMonad RM

lift-mstate : ∀ {f}{M}{RM : RawMonad {f} M}{A}{S} → State S A → StateT S M A
lift-mstate {RM = RM}{S = S} sa = λ s → return (sa s)
                          where open RawMonad RM

-- Modify error message in Prog, in case Prog is error.
err-modify : Prog → (String → String) → Prog
err-modify (error s) f = error (f s)
err-modify p _ = p

-- Check if there exists an element in the list that satisfies the predicate P.
list-has-el : ∀ {a b}{A : Set a}{P : UR.Pred A b} → UR.Decidable P → List A → Bool
list-has-el P? [] = false
list-has-el P? (x ∷ xs) with P? x
... | yes _ = true
... | no  _ = list-has-el P? xs

-- Check if there exists an element in the list that satisfies the predicate P.
list-find-el : ∀ {a b}{A : Set a}{P : UR.Pred A b} → UR.Decidable P → List A → Maybe A
list-find-el P? [] = nothing
list-find-el P? (x ∷ xs) with P? x
... | yes _ = just x
... | no  _ = list-find-el P? xs

list-update-fst : ∀ {a b}{A : Set a}{P : UR.Pred A b} → UR.Decidable P → List A → (A → A) → List A
list-update-fst P? [] f = []
list-update-fst P? (x ∷ xs) f with P? x
... | yes _ = f x ∷ xs
... | no  _ = x ∷ list-update-fst P? xs f

list-filter : ∀ {a b}{A : Set a}{P : UR.Pred A b} → UR.Decidable P → List A → List A
list-filter P? [] = []
list-filter P? (x ∷ xs) with P? x
... | yes _ = x ∷ list-filter P? xs
... | no  _ = list-filter P? xs

dec-neg :  ∀ {a b}{A : Set a}{P : UR.Pred A b} → UR.Decidable P → UR.Decidable (UR._∉ P)
dec-neg P? x with P? x
... | yes p = no λ ¬p → contradiction p ¬p
... | no ¬p = yes ¬p

vec-find-el-idx : ∀ {a b}{A : Set a}{n}{P : UR.Pred A b} → UR.Decidable P → Vec A n → Maybe (Fin n × A)
vec-find-el-idx P? [] = nothing
vec-find-el-idx P? (x ∷ xs) with P? x
... | yes _ = just (zero , x)
... | no  _ with vec-find-el-idx P? xs
... | just (i , x′) = just (suc i , x′)
... | nothing = nothing

max_stars_repo_name: ashinkarov/agda-extractor

max_issues_repo_name: ashinkarov/agda-extractor

max_forks_repo_name: ashinkarov/agda-extractor


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

open import HoTT

open import stash.modalities.gbm.GbmUtil
open import stash.modalities.GbmCodes

module stash.modalities.Gbm {ℓ} (M : Modality ℓ)
  {A : Type ℓ} {B : Type ℓ}
  (Q : A → B → Type ℓ)
  (H : BM-Relation M Q) where

  open Modality M

  import stash.modalities.gbm.Pushout
  open import stash.modalities.gbm.PushoutMono
  open import stash.modalities.gbm.PullbackSplit
  open import homotopy.PushoutSplit

  private

    A' : Type ℓ
    A' = Σ A (λ a → Trunc (S ⟨-2⟩) (Σ B (λ b → Q a b)))

    Q' : A' → B → Type ℓ
    Q' (a , _) b = Q a b

    Q'-pth-ovr-lemma : {a₀ a₁ : A'} {b : B} (q₀ : Q' a₀ b) (q₁ : Q' a₁ b) (p : a₀ == a₁)
                 → (q₀ == q₁ [ (λ a → Q' a b) ↓ p ]) ≃ (q₀ == q₁ [ (λ a → Q a b) ↓ fst= p ])
    Q'-pth-ovr-lemma q₀ q₁ idp = ide (q₀ == q₁)

    Q'-is-BM-Relation : BM-Relation M Q'
    Q'-is-BM-Relation {a₀} {b₀} q₀ {a₁} q₁ {b₁} q₂ =
      equiv-preserves-◯-conn (*-emap eqv (ide _))
        (H {fst a₀} {b₀} q₀ {fst a₁} q₁ {b₁} q₂)

      where eqv = =Σ-econv (a₀ , q₀) (a₁ , q₁)
                    ∘e (Σ-emap-r (Q'-pth-ovr-lemma q₀ q₁)) ⁻¹
                    ∘e (Σ-emap-l (λ p → q₀ == q₁ [ (λ a → Q a b₀) ↓ p ])
                         (Subtype=-econv ((λ a → Trunc -1 (Σ B λ b → Q a b)), λ a → Trunc-level) a₀ a₁ ⁻¹)) ⁻¹
                    ∘e (=Σ-econv (fst a₀ , q₀) (fst a₁ , q₁)) ⁻¹

    module W = stash.modalities.gbm.Pushout Q
    module W' = stash.modalities.gbm.Pushout Q'
    W  = W.BMPushout
    W' = W'.BMPushout

    Z = (Σ A λ a → Σ B λ b → Q a b)
    Z' = (Σ A' λ a → Σ B λ b → Q (fst a) b)

    Z-to-Z' : Z → Z'
    Z-to-Z' (a , b , q) = (a , [ b , q ]) , b , q

    Z'-to-Z : Z' → Z
    Z'-to-Z ((a , e) , b , q) = a , b , q

    Z≃Z' : is-equiv Z-to-Z'
    Z≃Z' = is-eq Z-to-Z' Z'-to-Z to-from from-to

      where to-from : (z : Z') → Z-to-Z' (Z'-to-Z z) == z
            to-from ((a , e) , b , q) = pair= (pair= idp (prop-has-all-paths Trunc-level _ e))
              (↓-cst2-in idp (prop-has-all-paths Trunc-level _ e) idp)

            from-to : (z : Z) → Z'-to-Z (Z-to-Z' z) == z
            from-to (a , b , q) = idp

    W-span = span A B Z fst (fst ∘ snd)
    W''-span = span A B Z' (fst ∘ fst) (fst ∘ snd)

    W'' = Pushout W''-span

    W≃W'' : W ≃ W''
    W≃W'' = Pushout-emap span-eqv

      where span-eqv : SpanEquiv W-span W''-span
            span-eqv = (span-map (idf A) (idf B) Z-to-Z'
                         (comm-sqr (λ a → idp))
                         (comm-sqr (λ b → idp))) ,
                         ( idf-is-equiv A
                         , idf-is-equiv B
                         , Z≃Z')

    --
    --  But the PushoutSplit lemma, we find that
    --
    --    Z' ---------> B
    --    |             |
    --    |             |
    --    v             v
    --    A' ---------> W'
    --    |             |
    --    |             |
    --    v             v
    --    A ----------> W'' ≃ X
    --

    X = Pushout (span A W' A' fst left)

    W''≃X : W'' ≃ X
    W''≃X = PS.split-equiv

      where module PS = PushoutLSplit {A = A'} {B = A} {C = B} {D = Z'} fst fst (fst ∘ snd)

    --
    --  Now we switch gears and take pullbacks.  We
    --  have the following diagram:
    --
    -- U'' ≃  U' ≃ U ---------> B
    --             |            |
    --             |            |
    --             v            v
    --        A' ≃ V ---------> W'  outer = cospan₀
    --             |            |
    --             |  cospan₂   |
    --             v            v
    --             A ---------> X ≃ W''

    V = Pullback (cospan A W' X left right)

    U = Pullback (cospan A B X left (right ∘ W'.bmright))
    U' = Pullback (cospan A B W'' left right)
    U'' = Pullback (cospan V B W' Pullback.b right)

    U≃U'' : U ≃ U''
    U≃U'' = PBSplit.split-equiv

      where module PBSplit = PullbackLSplit {A = W'} {B = B} {C = A} {D = X} right right left

    --
    --  The map A' --> A is a mono.  Hence by
    --  the PushoutMono lemma we get that it
    --  is also a pullback and consequently
    --  equivalent to V
    --

    V≃A' : V ≃ A'
    V≃A' = (ML.pushout-mono-is-pullback) ⁻¹ ∘e (pullback-decomp-equiv (cospan A W' X left right))

      where module ML = MonoLemma
              (span A W' A' fst left)
              (λ b → equiv-preserves-level ((hfiber-fst b) ⁻¹) Trunc-level)

    -- We need this for commutivity below
    V≃A'-coh : (v : V) → Pullback.b v == left (fst V≃A' v)
    V≃A'-coh (pullback a b h) = ! (ML.witness-for-coh₀ h)

      where module ML = MonoLemma
              (span A W' A' fst left)
              (λ b → equiv-preserves-level ((hfiber-fst b) ⁻¹) Trunc-level)

    --
    --  Now on to the main theorem
    --

    A×WB = Pullback (cospan A B W left right)
    A'×W'B = Pullback (cospan A' B W' left right)

    U''≃A'×W'B : U'' ≃ A'×W'B
    U''≃A'×W'B = Pullback-emap cospan-eqv

      where cospan-eqv : CospanEquiv (cospan V B W' Pullback.b right)
                                     (cospan A' B W' left right)
            cospan-eqv = (cospan-map (fst (V≃A')) (idf B) (idf W')
                                     (comm-sqr V≃A'-coh)
                                     (comm-sqr (λ b → idp))) ,
                                     snd (V≃A') ,
                                     idf-is-equiv B ,
                                     idf-is-equiv W'

    A×WB≃U : A×WB ≃ U
    A×WB≃U = Pullback-emap cospan-eqv

      where cospan-eqv : CospanEquiv (cospan A B W left right) (cospan A B X left (right ∘ W'.bmright))
            cospan-eqv = (cospan-map (idf A) (idf B) (fst (W''≃X ∘e W≃W''))
                                     (comm-sqr (λ a → idp))
                                     (comm-sqr (λ b → idp))) ,
                                     idf-is-equiv A ,
                                     (idf-is-equiv B) ,
                                     (snd (W''≃X ∘e W≃W''))

    Pb = Σ A (λ a → Σ B (λ b →  W.bmleft a == W.bmright b))
    Pb' = Σ A' (λ a → Σ B (λ b →  W'.bmleft a == W'.bmright b))

    Pb≃Pb' = Pb ≃⟨ Σ-assoc ⁻¹  ⟩
             Σ (A × B) (λ ab → W.bmleft (fst ab) == W.bmright (snd ab)) ≃⟨ (pullback-decomp-equiv (cospan A B W left right)) ⁻¹  ⟩
             A×WB ≃⟨ A×WB≃U ⟩
             U ≃⟨ U≃U'' ⟩
             U'' ≃⟨ U''≃A'×W'B ⟩
             A'×W'B ≃⟨ pullback-decomp-equiv (cospan A' B W' left right) ⟩
             Σ (A' × B) (λ ab → W'.bmleft (fst ab) == W'.bmright (snd ab)) ≃⟨ Σ-assoc ⟩
             Pb' ≃∎

    bm-map : Z → Pb
    bm-map (a , b , q) = a , b , W.bmglue q

    bm-map' : Z' → Pb'
    bm-map' (a' , b , q) = a' , b , W'.bmglue q

    bm-map'-is-◯-equiv : is-◯-equiv bm-map'
    bm-map'-is-◯-equiv =
      total-◯-equiv
        (λ a' → λ { (b , q) → b , W'.bmglue q})
        (λ a' → total-◯-equiv (λ b q → W'.bmglue q)
          (λ b r → Trunc-rec (prop-has-level-S is-◯-connected-is-prop)
            (λ{(_ , q₀₀) → code-contr M Q' Q'-is-BM-Relation q₀₀ r}) (snd a')))

  --
  --  We have a commutative diagram with top and bottom
  --  maps equivalences.  This induces an equivalence on
  --  homotopy fibers, from which the theorem follows
  --          ~
  --    Z --------> Z'
  --    |           |
  --  s |           | t
  --    |           |
  --    v           v
  --    Pb -------> Pb'
  --          ~
  --

  sq-coh : (z : Z) → (fst Pb≃Pb' (bm-map z)) == bm-map' (Z-to-Z' z)
  sq-coh (a , b , q) = {!!}

    where test = fst Pb≃Pb' (a , b , W.bmglue q) =⟨ idp ⟩
                 (–> Σ-assoc) (–> (pullback-decomp-equiv (cospan A' B W' left right)) {!–> U''≃A'×W'B ?!} )  =⟨ idp ⟩
                 fst Pb≃Pb' (a , b , W.bmglue q) ∎

    -- Pb≃Pb' = Pb ≃⟨ Σ-assoc ⁻¹  ⟩
    --          Σ (A × B) (λ ab → W.bmleft (fst ab) == W.bmright (snd ab)) ≃⟨ (pullback-decomp-equiv (cospan A B W left right)) ⁻¹  ⟩
    --          A×WB ≃⟨ A×WB≃U ⟩
    --          U ≃⟨ U≃U'' ⟩
    --          U'' ≃⟨ U''≃A'×W'B ⟩
    --          A'×W'B ≃⟨ pullback-decomp-equiv (cospan A' B W' left right) ⟩
    --          Σ (A' × B) (λ ab → W'.bmleft (fst ab) == W'.bmright (snd ab)) ≃⟨ Σ-assoc ⟩
    --          Pb' ≃∎

    -- fst Pb≃Pb' (a , b , W.bmglue q) =⟨ {!!} ⟩
    -- (a , [ b , q ]) , (b , W'.bmglue q) ∎

  generalized-blakers-massey : is-◯-equiv bm-map
  generalized-blakers-massey pb = equiv-preserves-◯-conn (lemma ⁻¹) (bm-map'-is-◯-equiv (fst Pb≃Pb' pb))

    where

          lemma : hfiber bm-map pb ≃ hfiber bm-map' (fst Pb≃Pb' pb)
          lemma = hfiber-sq-eqv bm-map bm-map' Z-to-Z' (fst Pb≃Pb')
            (comm-sqr sq-coh) Z≃Z' (snd Pb≃Pb') pb

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda