text:
------------------------------------------------------------------------
-- The partiality monads in Partiality-monad.Inductive and
-- Partiality-monad.Coinductive are pointwise equivalent, for sets,
-- assuming extensionality and countable choice
------------------------------------------------------------------------

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

open import Prelude hiding (⊥; ↑)

module Partiality-monad.Equivalence {a} {A : Type a} where

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

open import Bijection equality-with-J using (_↔_)
open import Embedding equality-with-J
  using (Is-embedding; Injective≃Is-embedding)
open import Equivalence equality-with-J as Eq
  using (_≃_; Is-equivalence)
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 H-level.Truncation.Propositional equality-with-paths
  as Trunc
open import Injection equality-with-J using (Injective)
open import Quotient equality-with-paths as Quotient hiding ([_])
open import Univalence-axiom equality-with-J

import Delay-monad as D
open import Delay-monad.Alternative as A using (_↓_; _↑)
import Delay-monad.Alternative.Equivalence as A
import Delay-monad.Alternative.Partial-order as A
import Delay-monad.Alternative.Termination as A
import Delay-monad.Alternative.Weak-bisimilarity as A
import Delay-monad.Bisimilarity as B
import Partiality-monad.Coinductive as C
import Partiality-monad.Coinductive.Alternative as CA
open import Partiality-monad.Inductive as I
  hiding (_⊥; _⊑_; Increasing-sequence; _⇓_)
open import Partiality-monad.Inductive.Alternative-order
open import Partiality-monad.Inductive.Eliminators

------------------------------------------------------------------------
-- A function from the partiality monad defined in
-- Partiality-monad.Coinductive.Alternative to the inductive
-- partiality monad

-- Turns potential values into partial values.

Maybe→⊥ : Maybe A → A I.⊥
Maybe→⊥ nothing  = never
Maybe→⊥ (just y) = now y

-- Maybe→⊥ is monotone.

Maybe→⊥-mono : ∀ {x y} → A.LE x y → Maybe→⊥ x I.⊑ Maybe→⊥ y
Maybe→⊥-mono (inj₁ refl) = ⊑-refl _
Maybe→⊥-mono (inj₂ (refl , y≢n)) = never⊑ _

-- Maybe→⊥ can be used to turn increasing sequences of one kind into
-- increasing sequences of another kind.

Delay→Inc-seq : A.Delay A → I.Increasing-sequence A
Delay→Inc-seq (f , inc) = Maybe→⊥ ∘ f , Maybe→⊥-mono ∘ inc

-- Turns increasing sequences of potential values into partial values.

Delay→⊥ : A.Delay A → A I.⊥
Delay→⊥ = ⨆ ∘ Delay→Inc-seq

-- Delay→⊥ is monotone (if A is a set).

Delay→⊥-mono :
  Is-set A → ∀ x y → x A.∥⊑∥ y → Delay→⊥ x I.⊑ Delay→⊥ y
Delay→⊥-mono A-set x@(f , _) y@(g , _) x⊑y = ∃⊑→⨆⊑⨆ inc
  where
  inc : ∀ m → ∃ λ n → Maybe→⊥ (f m) I.⊑ Maybe→⊥ (g n)
  inc m with inspect (f m)
  inc m | nothing , fm↑  = 0 , (Maybe→⊥ (f m)  ≡⟨ cong Maybe→⊥ fm↑ ⟩⊑
                                never          ⊑⟨ never⊑ _ ⟩■
                                Maybe→⊥ (g 0)  ■)
  inc m | just z  , fm↓z =
    k , (Maybe→⊥ (f m)     ≡⟨ cong Maybe→⊥ fm↓z ⟩⊑
         Maybe→⊥ (just z)  ≡⟨ cong Maybe→⊥ (sym $ proj₂ y⇓z) ⟩⊑
         Maybe→⊥ (g k)     ■)
    where
    y⇓z =        $⟨ ∣ m , fm↓z ∣ ⟩
      x A.∥⇓∥ z  ↝⟨ x⊑y z ⟩
      y A.∥⇓∥ z  ↝⟨ _⇔_.from (A.⇓⇔∥⇓∥ A-set y) ⟩□
      y A.⇓ z    □

    k : ℕ
    k = proj₁ y⇓z

-- Delay→⊥ maps weakly bisimilar values to equal values (if A is a
-- set).

Delay→⊥-≈→≡ : Is-set A → ∀ x y → x A.≈ y → Delay→⊥ x ≡ Delay→⊥ y
Delay→⊥-≈→≡ A-set x y =
  x A.≈ y                                            ↝⟨ Σ-map (Delay→⊥-mono A-set x y) (Delay→⊥-mono A-set y x) ⟩
  Delay→⊥ x I.⊑ Delay→⊥ y × Delay→⊥ x I.⊒ Delay→⊥ y  ↝⟨ uncurry antisymmetry ⟩□
  Delay→⊥ x ≡ Delay→⊥ y                              □

-- If A is a set, then values in A CA.⊥ can be mapped to values in the
-- inductive partiality monad.

⊥→⊥ : Is-set A → A CA.⊥ → A I.⊥
⊥→⊥ A-set = Quotient.rec λ where
  .[]ʳ                                   → Delay→⊥
  .[]-respects-relationʳ {x = x} {y = y} → Delay→⊥-≈→≡ A-set x y
  .is-setʳ                               → ⊥-is-set

------------------------------------------------------------------------
-- A lemma

-- I._⇓_ and A._∥⇓∥_ are pointwise logically equivalent (via Delay→⊥),
-- for sets.

⇓⇔∥⇓∥ :
  Is-set A →
  ∀ x {y} → Delay→⊥ x I.⇓ y ⇔ x A.∥⇓∥ y
⇓⇔∥⇓∥ A-set x@(f , _) {y} =
  Delay→⊥ x I.⇓ y                    ↔⟨⟩
  ⨆ (Delay→Inc-seq x) I.⇓ y          ↔⟨ ⨆⇓≃∥∃⇓∥ ⟩
  ∥ (∃ λ n → Maybe→⊥ (f n) I.⇓ y) ∥  ↝⟨ ∥∥-cong-⇔ (∃-cong λ _ → record { to = to _; from = cong Maybe→⊥ }) ⟩
  ∥ (∃ λ n → f n ↓ y) ∥              ↝⟨ F.id ⟩□
  x A.∥⇓∥ y                          □
  where
  to : ∀ n → Maybe→⊥ (f n) I.⇓ y → f n ↓ y
  to n f⇓y with f n
  ... | nothing = ⊥-elim $ now≢never _ (sym f⇓y)
  ... | just y′ =
    just y′  ≡⟨ cong just y′≡y ⟩∎
    just y   ∎
    where
    y′≡y =            $⟨ f⇓y ⟩
      now y′ ≡ now y  ↔⟨ now≡now≃∥≡∥ ⟩
      ∥ y′ ≡ y ∥      ↝⟨ ∥∥↔ A-set ⟩□
      y′ ≡ y          □

------------------------------------------------------------------------
-- ⊥→⊥ is injective

-- Delay→⊥ is (kind of) injective (if A is a set).

Delay→⊥-injective :
  Is-set A →
  ∀ x y → Delay→⊥ x ≡ Delay→⊥ y → x A.≈ y
Delay→⊥-injective A-set x y x≡y =
    lemma A-set x y (≡→⊑      x≡y)
  , lemma A-set y x (≡→⊑ (sym x≡y))
  where
  ≡→⊑ : ∀ {x y} → x ≡ y → x I.⊑ y
  ≡→⊑ refl = ⊑-refl _

  lemma :
    Is-set A →
    ∀ x y → Delay→⊥ x I.⊑ Delay→⊥ y → x A.∥⊑∥ y
  lemma A-set x y x⊑y z =
    x A.∥⇓∥ z            ↝⟨ _⇔_.from (⇓⇔∥⇓∥ A-set x) ⟩
    Delay→⊥ x I.⇓ z      ↔⟨ ⇓≃now⊑ ⟩
    now z I.⊑ Delay→⊥ x  ↝⟨ flip ⊑-trans x⊑y ⟩
    now z I.⊑ Delay→⊥ y  ↔⟨ inverse ⇓≃now⊑ ⟩
    Delay→⊥ y I.⇓ z      ↝⟨ _⇔_.to (⇓⇔∥⇓∥ A-set y) ⟩□
    y A.∥⇓∥ z            □

-- ⊥→⊥ A-set is injective.

⊥→⊥-injective :
  (A-set : Is-set A) →
  Injective (⊥→⊥ A-set)
⊥→⊥-injective A-set {x} {y} = Quotient.elim-prop
  {P = λ x → ⊥→⊥ A-set x ≡ ⊥→⊥ A-set y → x ≡ y}
  (λ where
     .[]ʳ x → Quotient.elim-prop
       {P = λ y → Delay→⊥ x ≡ ⊥→⊥ A-set y → Quotient.[ x ] ≡ y}
       (λ where
          .[]ʳ y → []-respects-relation ∘
                   Delay→⊥-injective A-set x y
          .is-propositionʳ _ →
            Π-closure ext 1 λ _ →
            /-is-set)
       y
     .is-propositionʳ _ →
       Π-closure ext 1 λ _ →
       /-is-set)
  x

------------------------------------------------------------------------
-- ⊥→⊥ is surjective

-- Delay→⊥ is surjective (if A is a set, assuming countable choice).

Delay→⊥-surjective :
  Is-set A →
  Axiom-of-countable-choice a →
  Surjective Delay→⊥
Delay→⊥-surjective A-set cc =
  ⊥-rec-⊥ (record
    { pe = constant-sequence nothing
    ; po = constant-sequence ∘ just
    ; pl = λ s →
             (∀ n → ∥ (∃ λ x → Delay→⊥ x ≡ s [ n ]) ∥)    ↝⟨ cc ⟩
             ∥ (∀ n → ∃ λ x → Delay→⊥ x ≡ s [ n ]) ∥      ↔⟨ ∥∥-cong ΠΣ-comm ⟩
             ∥ (∃ λ f → ∀ n → Delay→⊥ (f n) ≡ s [ n ]) ∥  ↝⟨ ∥∥-map (uncurry $ flip construct s) ⟩□
             ∥ (∃ λ x → Delay→⊥ x ≡ ⨆ s) ∥                □
    ; pp = λ _ → truncation-is-proposition
    })
  where
  -- The increasing sequences (of type A.Delay A) returned by this
  -- function are constant.

  constant-sequence : ∀ x → ∥ (∃ λ y → Delay→⊥ y ≡ Maybe→⊥ x) ∥
  constant-sequence x = ∣ (const x , const (inj₁ refl)) , ⨆-const ∣

  -- Given a sequence and an increasing sequence s that are pointwise
  -- equal (via Delay→⊥) one can construct an increasing sequence that
  -- is equal (via Delay→⊥) to ⨆ s.

  construct :
    (f : ℕ → A.Delay A)
    (s : I.Increasing-sequence A) →
    (∀ n → Delay→⊥ (f n) ≡ s [ n ]) →
    ∃ λ x → Delay→⊥ x ≡ ⨆ s
  construct f s h = x , x-correct
    where
    -- We use f and an isomorphism between ℕ and ℕ × ℕ to construct a
    -- function from ℕ to Maybe A.

    f₂ : ℕ → ℕ → Maybe A
    f₂ m n = proj₁ (f m) n

    f₁ : ℕ → Maybe A
    f₁ =
      ℕ        ↔⟨ ℕ↔ℕ² ⟩
      ℕ × ℕ    ↝⟨ uncurry f₂ ⟩□
      Maybe A  □

    -- All values that this function can terminate with are equal.

    termination-value-unique-f₂ :
      ∀ {m n y m′ n′ y′} →
      f₂ m n ↓ y × f₂ m′ n′ ↓ y′ →
      y ≡ y′
    termination-value-unique-f₂ {m} {n} {y} {m′} {n′} {y′} =
      f₂ m n ↓ y × f₂ m′ n′ ↓ y′  ↝⟨ f₂↓→⨆s⇓ ×-cong f₂↓→⨆s⇓ ⟩
      ⨆ s I.⇓ y × ⨆ s I.⇓ y′      ↝⟨ uncurry termination-value-merely-unique ⟩
      ∥ y ≡ y′ ∥                  ↔⟨ ∥∥↔ A-set ⟩□
      y ≡ y′                      □
      where
      f₂↓→⨆s⇓ : ∀ {y m n} → f₂ m n ↓ y → ⨆ s I.⇓ y
      f₂↓→⨆s⇓ {y} {m} f₂↓ =
        terminating-element-is-⨆ s
          (s [ m ]        ≡⟨ sym (h m) ⟩
           Delay→⊥ (f m)  ≡⟨ _⇔_.from (⇓⇔∥⇓∥ A-set (f m)) ∣ _ , f₂↓ ∣ ⟩∎
           now y          ∎)

    termination-value-unique-f₁ :
      ∀ {y y′} →
      (∃ λ n → f₁ n ↓ y) →
      (∃ λ n → f₁ n ↓ y′) →
      y ≡ y′
    termination-value-unique-f₁ (_ , ↓y) (_ , ↓y′) =
      termination-value-unique-f₂ (↓y , ↓y′)

    abstract

      -- Thus the function can be completed to an increasing sequence.

      completed-f₁ : ∃ λ x → ∀ {y} → x A.⇓ y ⇔ ∃ λ n → f₁ n ↓ y
      completed-f₁ = A.complete-function f₁ termination-value-unique-f₁

    -- The increasing sequence that is returned above.

    x : A.Delay A
    x = proj₁ completed-f₁

    -- Every potential value in the increasing sequence x is smaller
    -- than or equal to (via Maybe→⊥) some value in s.

    x⊑s : ∀ m → ∃ λ n → Maybe→⊥ (proj₁ x m) I.⊑ s [ n ]
    x⊑s m with inspect (proj₁ x m)
    x⊑s m | nothing , x↑ =
        zero
      , (Maybe→⊥ (proj₁ x m)  ≡⟨ cong Maybe→⊥ x↑ ⟩⊑
         never                ⊑⟨ never⊑ _ ⟩■
         s [ 0 ]              ■)
    x⊑s m | just y , x↓ =
        n₁
      , (Maybe→⊥ (proj₁ x m)  ≡⟨ cong Maybe→⊥ x↓ ⟩⊑
         now y                ≡⟨ sym f⇓ ⟩⊑
         Delay→⊥ (f n₁)       ≡⟨ h n₁ ⟩⊑
         s [ n₁ ]             ■)
      where
      f₁↓ : ∃ λ n → f₁ n ↓ y
      f₁↓ = _⇔_.to (proj₂ completed-f₁) (_ , x↓)

      n  = proj₁ f₁↓
      n₁ = proj₁ (_↔_.to ℕ↔ℕ² n)
      n₂ = proj₂ (_↔_.to ℕ↔ℕ² n)

      f⇓ : Delay→⊥ (f n₁) I.⇓ y
      f⇓ =
        _≃_.from ⇓≃now⊑
          (now y                        ≡⟨ cong Maybe→⊥ $ sym $ proj₂ f₁↓ ⟩⊑
           Maybe→⊥ (f₁ n)               ⊑⟨⟩
           Maybe→⊥ (f₂ n₁ n₂)           ⊑⟨⟩
           Maybe→⊥ (proj₁ (f n₁) n₂)    ⊑⟨⟩
           Delay→Inc-seq (f n₁) [ n₂ ]  ⊑⟨ upper-bound (Delay→Inc-seq (f n₁)) _ ⟩■
           Delay→⊥ (f n₁)               ■)

    -- Furthermore every potential value in f is smaller than or equal
    -- to x.

    f⊑x : ∀ m → f m A.⊑ x
    f⊑x m y =
      f m A.⇓ y                                                 ↝⟨ Σ-map (_↔_.from ℕ↔ℕ² ∘ (m ,_)) (λ {n} →

          f₂ m n ↓ y                                                 ↝⟨ ≡⇒→ (cong ((_↓ y) ∘ uncurry f₂) $ sym $ _↔_.right-inverse-of ℕ↔ℕ² (m , n)) ⟩
          uncurry f₂ (_↔_.to ℕ↔ℕ² (_↔_.from ℕ↔ℕ² (m , n))) ↓ y       ↝⟨ F.id ⟩□
          f₁ (_↔_.from ℕ↔ℕ² (m , n)) ↓ y                             □) ⟩

      (∃ λ n → f₁ n ↓ y)                                        ↝⟨ _⇔_.from (proj₂ completed-f₁) ⟩□
      x A.⇓ y                                                   □

    -- Thus x is correctly defined.

    x-correct : Delay→⊥ x ≡ ⨆ s
    x-correct = antisymmetry
      (⊑→⨆⊑⨆ λ n →
         Delay→Inc-seq x [ n ]  ⊑⟨ proj₂ (x⊑s n) ⟩■
         s [ proj₁ (x⊑s n) ]    ■)
      (least-upper-bound _ _ λ m →
         s [ m ]        ≡⟨ sym (h m) ⟩⊑
         Delay→⊥ (f m)  ⊑⟨ Delay→⊥-mono A-set (f m) x (∥∥-map ∘ f⊑x m) ⟩■
         Delay→⊥ x      ■)

-- ⊥→⊥ A-set is surjective (assuming countable choice).

⊥→⊥-surjective :
  (A-set : Is-set A) →
  Axiom-of-countable-choice a →
  Surjective (⊥→⊥ A-set)
⊥→⊥-surjective A-set cc x =
  ∥∥-map (λ { (pre , can-pre≡x) → Quotient.[ pre ] , can-pre≡x })
         (Delay→⊥-surjective A-set cc x)

------------------------------------------------------------------------
-- ⊥→⊥ is an equivalence

-- ⊥→⊥ A-set is an equivalence (assuming countable choice).

⊥→⊥-equiv :
  (A-set : Is-set A) →
  Axiom-of-countable-choice a →
  Is-equivalence (⊥→⊥ A-set)
⊥→⊥-equiv A-set cc =                                 $⟨ _,_ {B = const _}
                                                            (⊥→⊥-surjective A-set cc)
                                                            (λ {_ _} → ⊥→⊥-injective A-set) ⟩
  Surjective (⊥→⊥ A-set) × Injective (⊥→⊥ A-set)     ↝⟨ Σ-map id (_≃_.to (Injective≃Is-embedding ext /-is-set ⊥-is-set _)) ⟩
  Surjective (⊥→⊥ A-set) × Is-embedding (⊥→⊥ A-set)  ↝⟨ _≃_.to surjective×embedding≃equivalence ⟩□
  Is-equivalence (⊥→⊥ A-set)                         □

-- Thus the inductive definition of the partiality monad is equivalent
-- to the definition in Partiality-monad.Coinductive.Alternative, for
-- sets, assuming countable choice.

⊥≃⊥′ :
  Is-set A →
  Axiom-of-countable-choice a →
  A CA.⊥ ≃ A I.⊥
⊥≃⊥′ A-set choice = Eq.⟨ _ , ⊥→⊥-equiv A-set choice ⟩

------------------------------------------------------------------------
-- The two definitions of the partiality monad are equivalent

-- The inductive and coinductive definitions of the partiality monad
-- are pointwise equivalent, for sets, assuming extensionality and
-- countable choice.

⊥≃⊥ :
  Is-set A →
  B.Extensionality a →
  Axiom-of-countable-choice a →
  A I.⊥ ≃ A C.⊥
⊥≃⊥ A-set delay-ext choice =
  A I.⊥   ↝⟨ inverse (⊥≃⊥′ A-set choice) ⟩
  A CA.⊥  ↔⟨ CA.⊥↔⊥ A-set delay-ext ⟩□
  A C.⊥   □

-- The previous result has a number of preconditions. None of these
-- preconditions are needed to translate from the delay monad to the
-- quotient inductive-inductive partiality monad.

Delay→⊥′ : D.Delay A ∞ → A I.⊥
Delay→⊥′ =
  D.Delay A ∞  ↝⟨ _⇔_.from A.Delay⇔Delay ⟩
  A.Delay A    ↝⟨ Delay→⊥ ⟩□
  A I.⊥        □

-- This translation turns weakly bisimilar computations into equal
-- computations, assuming that the underlying type is a set.

Delay→⊥′-≈→≡ :
  Is-set A →
  ∀ {x y} → x B.≈ y → Delay→⊥′ x ≡ Delay→⊥′ y
Delay→⊥′-≈→≡ A-set {x} {y} =
  x B.≈ y                                                ↝⟨ _⇔_.to (A.≈⇔≈′ A-set) ⟩
  _⇔_.from A.Delay⇔Delay x A.≈ _⇔_.from A.Delay⇔Delay y  ↝⟨ Delay→⊥-≈→≡ A-set (_⇔_.from A.Delay⇔Delay x) (_⇔_.from A.Delay⇔Delay y) ⟩□
  Delay→⊥′ x ≡ Delay→⊥′ y                                □

-- One can also translate from the coinductive to the inductive
-- partiality monad, as long as the underlying type is a set.

⊥→⊥′ : Is-set A → A C.⊥ → A I.⊥
⊥→⊥′ A-set = Quotient.rec λ where
  .[]ʳ                   → Delay→⊥′
  .[]-respects-relationʳ → Trunc.rec I.⊥-is-set (Delay→⊥′-≈→≡ A-set)
  .is-setʳ               → I.⊥-is-set

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
{-# OPTIONS --universe-polymorphism #-}
-- {-# OPTIONS --verbose tc.rec:15 #-}
-- {-# OPTIONS --verbose tc.records.ifs:15 #-}
-- {-# OPTIONS --verbose tc.constr.findInScope:15 #-}
-- {-# OPTIONS --verbose tc.term.args.ifs:15 #-}

module InstanceArguments.05-equality-std2 where

open import Agda.Primitive
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Data.Bool hiding (_≟_)

open DecSetoid {{...}}

instance
  decBool = Data.Bool.decSetoid

test : IsDecEquivalence (_≡_ {A = Bool})
test = isDecEquivalence

test2 = false ≟ false

ext: agda

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


text:
module Syntax.Substitution where

open import Syntax.Substitution.Kits public
open import Syntax.Substitution.Instances public
open import Syntax.Substitution.Lemmas public

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
------------------------------------------------------------------------
-- Properties related to Any
------------------------------------------------------------------------

-- The other modules under Data.List.Any also contain properties
-- related to Any.

module Any where

open import Algebra
import Algebra.Definitions as FP
open import Effect.Monad
open import Data.Bool
open import Data.Bool.Properties
open import Data.Empty
open import Data.List as List
open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
import Data.List.Effectful
open import Data.Product as Prod hiding (swap)
open import Data.Product.Function.NonDependent.Propositional
  using (_×-cong_)
open import Data.Product.Relation.Binary.Pointwise.NonDependent
import Data.Product.Function.Dependent.Propositional as Σ
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
open import Data.Sum.Relation.Binary.Pointwise
open import Data.Sum.Function.Propositional using (_⊎-cong_)
open import Function using (_$_; _$′_; _∘_; id; flip; const)
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence as Eq using (_⇔_; module Equivalence)
open import Function.Inverse as Inv using (_↔_; module Inverse)
open import Function.Related as Related using (Related; SK-sym)
open import Function.Related.TypeIsomorphisms
open import Level
open import Relation.Binary hiding (_⇔_)
import Relation.Binary.HeterogeneousEquality as H
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; refl; inspect) renaming ([_] to P[_])
open import Relation.Unary using (_⟨×⟩_; _⟨→⟩_) renaming (_⊆_ to _⋐_)

open import Data.List.Membership.Propositional
open import Data.List.Relation.Binary.BagAndSetEquality
open Related.EquationalReasoning

private
  module ×⊎ {k ℓ} = CommutativeSemiring (×-⊎-commutativeSemiring k ℓ)
  open module ListMonad {ℓ} =
    RawMonad (Data.List.Effectful.monad {ℓ = ℓ})

------------------------------------------------------------------------
-- Some lemmas related to map, find and lose

-- Any.map is functorial.

map-id : ∀ {a p} {A : Set a} {P : A → Set p} (f : P ⋐ P) {xs} →
         (∀ {x} (p : P x) → f p ≡ p) →
         (p : Any P xs) → Any.map f p ≡ p
map-id f hyp (here  p) = P.cong here (hyp p)
map-id f hyp (there p) = P.cong there $ map-id f hyp p

map-∘ : ∀ {a p q r}
          {A : Set a} {P : A → Set p} {Q : A → Set q} {R : A → Set r}
        (f : Q ⋐ R) (g : P ⋐ Q)
        {xs} (p : Any P xs) →
        Any.map (f ∘ g) p ≡ Any.map f (Any.map g p)
map-∘ f g (here  p) = refl
map-∘ f g (there p) = P.cong there $ map-∘ f g p

-- Lemmas relating map and find.

map∘find : ∀ {a p} {A : Set a} {P : A → Set p} {xs}
           (p : Any P xs) → let p′ = find p in
           {f : _≡_ (proj₁ p′) ⋐ P} →
           f refl ≡ proj₂ (proj₂ p′) →
           Any.map f (proj₁ (proj₂ p′)) ≡ p
map∘find (here  p) hyp = P.cong here  hyp
map∘find (there p) hyp = P.cong there (map∘find p hyp)

find∘map : ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q}
           {xs : List A} (p : Any P xs) (f : P ⋐ Q) →
           find (Any.map f p) ≡ Prod.map id (Prod.map id f) (find p)
find∘map (here  p) f = refl
find∘map (there p) f rewrite find∘map p f = refl

-- find satisfies a simple equality when the predicate is a
-- propositional equality.

find-∈ : ∀ {a} {A : Set a} {x : A} {xs : List A} (x∈xs : x ∈ xs) →
         find x∈xs ≡ (x , x∈xs , refl)
find-∈ (here refl)  = refl
find-∈ (there x∈xs) rewrite find-∈ x∈xs = refl

private

  -- find and lose are inverses (more or less).

  lose∘find : ∀ {a p} {A : Set a} {P : A → Set p} {xs : List A}
              (p : Any P xs) →
              uncurry′ lose (proj₂ (find p)) ≡ p
  lose∘find p = map∘find p P.refl

  find∘lose : ∀ {a p} {A : Set a} (P : A → Set p) {x xs}
              (x∈xs : x ∈ xs) (pp : P x) →
              find {P = P} (lose x∈xs pp) ≡ (x , x∈xs , pp)
  find∘lose P x∈xs p
    rewrite find∘map x∈xs (flip (P.subst P) p)
          | find-∈ x∈xs
          = refl

-- Any can be expressed using _∈_.

Any↔ : ∀ {a p} {A : Set a} {P : A → Set p} {xs} →
       (∃ λ x → x ∈ xs × P x) ↔ Any P xs
Any↔ {P = P} {xs} = record
  { to         = P.→-to-⟶ to
  ; from       = P.→-to-⟶ (find {P = P})
  ; inverse-of = record
      { left-inverse-of  = λ p →
          find∘lose P (proj₁ (proj₂ p)) (proj₂ (proj₂ p))
      ; right-inverse-of = lose∘find
      }
  }
  where
  to : (∃ λ x → x ∈ xs × P x) → Any P xs
  to = uncurry′ lose ∘ proj₂

------------------------------------------------------------------------
-- Any is a congruence

Any-cong : ∀ {k ℓ} {A : Set ℓ} {P₁ P₂ : A → Set ℓ} {xs₁ xs₂ : List A} →
           (∀ x → Related k (P₁ x) (P₂ x)) → xs₁ ∼[ k ] xs₂ →
           Related k (Any P₁ xs₁) (Any P₂ xs₂)
Any-cong {P₁ = P₁} {P₂} {xs₁} {xs₂} P₁↔P₂ xs₁≈xs₂ =
  Any P₁ xs₁                ↔⟨ SK-sym $ Any↔ {P = P₁} ⟩
  (∃ λ x → x ∈ xs₁ × P₁ x)  ∼⟨ Σ.cong Inv.id (xs₁≈xs₂ ×-cong P₁↔P₂ _) ⟩
  (∃ λ x → x ∈ xs₂ × P₂ x)  ↔⟨ Any↔ {P = P₂} ⟩
  Any P₂ xs₂                ∎

------------------------------------------------------------------------
-- Swapping

-- Nested occurrences of Any can sometimes be swapped. See also ×↔.

swap : ∀ {ℓ} {A B : Set ℓ} {P : A → B → Set ℓ} {xs ys} →
       Any (λ x → Any (P x) ys) xs ↔ Any (λ y → Any (flip P y) xs) ys
swap {ℓ} {P = P} {xs} {ys} =
  Any (λ x → Any (P x) ys) xs                ↔⟨ SK-sym Any↔ ⟩
  (∃ λ x → x ∈ xs × Any (P x) ys)            ↔⟨ SK-sym $ Σ.cong Inv.id (Σ.cong Inv.id Any↔) ⟩
  (∃ λ x → x ∈ xs × ∃ λ y → y ∈ ys × P x y)  ↔⟨ Σ.cong Inv.id (∃∃↔∃∃ _) ⟩
  (∃₂ λ x y → x ∈ xs × y ∈ ys × P x y)       ↔⟨ ∃∃↔∃∃ _ ⟩
  (∃₂ λ y x → x ∈ xs × y ∈ ys × P x y)       ↔⟨ Σ.cong Inv.id (Σ.cong Inv.id (∃∃↔∃∃ _)) ⟩
  (∃₂ λ y x → y ∈ ys × x ∈ xs × P x y)       ↔⟨ Σ.cong Inv.id (∃∃↔∃∃ _) ⟩
  (∃ λ y → y ∈ ys × ∃ λ x → x ∈ xs × P x y)  ↔⟨ Σ.cong Inv.id (Σ.cong Inv.id Any↔) ⟩
  (∃ λ y → y ∈ ys × Any (flip P y) xs)       ↔⟨ Any↔ ⟩
  Any (λ y → Any (flip P y) xs) ys           ∎

------------------------------------------------------------------------
-- Lemmas relating Any to ⊥

⊥↔Any⊥ : ∀ {a} {A : Set a} {xs : List A} → ⊥ ↔ Any (const ⊥) xs
⊥↔Any⊥ {A = A} = record
  { to         = P.→-to-⟶ (λ ())
  ; from       = P.→-to-⟶ (λ p → from p)
  ; inverse-of = record
    { left-inverse-of  = λ ()
    ; right-inverse-of = λ p → from p
    }
  }
  where
  from : {xs : List A} → Any (const ⊥) xs → ∀ {b} {B : Set b} → B
  from (here ())
  from (there p) = from p

⊥↔Any[] : ∀ {a} {A : Set a} {P : A → Set} → ⊥ ↔ Any P []
⊥↔Any[] = record
  { to         = P.→-to-⟶ (λ ())
  ; from       = P.→-to-⟶ (λ ())
  ; inverse-of = record
    { left-inverse-of  = λ ()
    ; right-inverse-of = λ ()
    }
  }

------------------------------------------------------------------------
-- Lemmas relating Any to sums and products

-- Sums commute with Any (for a fixed list).

⊎↔ : ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} {xs} →
     (Any P xs ⊎ Any Q xs) ↔ Any (λ x → P x ⊎ Q x) xs
⊎↔ {P = P} {Q} = record
  { to         = P.→-to-⟶ to
  ; from       = P.→-to-⟶ from
  ; inverse-of = record
    { left-inverse-of  = from∘to
    ; right-inverse-of = to∘from
    }
  }
  where
  to : ∀ {xs} → Any P xs ⊎ Any Q xs → Any (λ x → P x ⊎ Q x) xs
  to = [ Any.map inj₁ , Any.map inj₂ ]′

  from : ∀ {xs} → Any (λ x → P x ⊎ Q x) xs → Any P xs ⊎ Any Q xs
  from (here (inj₁ p)) = inj₁ (here p)
  from (here (inj₂ q)) = inj₂ (here q)
  from (there p)       = Sum.map there there (from p)

  from∘to : ∀ {xs} (p : Any P xs ⊎ Any Q xs) → from (to p) ≡ p
  from∘to (inj₁ (here  p)) = P.refl
  from∘to (inj₁ (there p)) rewrite from∘to (inj₁ p) = P.refl
  from∘to (inj₂ (here  q)) = P.refl
  from∘to (inj₂ (there q)) rewrite from∘to (inj₂ q) = P.refl

  to∘from : ∀ {xs} (p : Any (λ x → P x ⊎ Q x) xs) →
            to (from p) ≡ p
  to∘from (here (inj₁ p)) = P.refl
  to∘from (here (inj₂ q)) = P.refl
  to∘from (there p) with from p | to∘from p
  to∘from (there .(Any.map inj₁ p)) | inj₁ p | P.refl = P.refl
  to∘from (there .(Any.map inj₂ q)) | inj₂ q | P.refl = P.refl

-- Products "commute" with Any.

×↔ : {A B : Set} {P : A → Set} {Q : B → Set}
     {xs : List A} {ys : List B} →
     (Any P xs × Any Q ys) ↔ Any (λ x → Any (λ y → P x × Q y) ys) xs
×↔ {P = P} {Q} {xs} {ys} = record
  { to         = P.→-to-⟶ to
  ; from       = P.→-to-⟶ from
  ; inverse-of = record
    { left-inverse-of  = from∘to
    ; right-inverse-of = to∘from
    }
  }
  where
  to : Any P xs × Any Q ys → Any (λ x → Any (λ y → P x × Q y) ys) xs
  to (p , q) = Any.map (λ p → Any.map (λ q → (p , q)) q) p

  from : Any (λ x → Any (λ y → P x × Q y) ys) xs → Any P xs × Any Q ys
  from pq with Prod.map id (Prod.map id find) (find pq)
  ... | (x , x∈xs , y , y∈ys , p , q) = (lose x∈xs p , lose y∈ys q)

  from∘to : ∀ pq → from (to pq) ≡ pq
  from∘to (p , q)
    rewrite find∘map {Q = λ x → Any (λ y → P x × Q y) ys}
                     p (λ p → Any.map (λ q → (p , q)) q)
          | find∘map {Q = λ y → P (proj₁ (find p)) × Q y}
                     q (λ q → proj₂ (proj₂ (find p)) , q)
          | lose∘find p
          | lose∘find q
      = refl

  to∘from : ∀ pq → to (from pq) ≡ pq
  to∘from pq
    with find pq
       | (λ (f : _≡_ (proj₁ (find pq)) ⋐ _) → map∘find pq {f})
  ... | (x , x∈xs , pq′) | lem₁
    with find pq′
       | (λ (f : _≡_ (proj₁ (find pq′)) ⋐ _) → map∘find pq′ {f})
  ... | (y , y∈ys , p , q) | lem₂
    rewrite P.sym $ map-∘ {R = λ x → Any (λ y → P x × Q y) ys}
                          (λ p → Any.map (λ q → p , q) (lose y∈ys q))
                          (λ y → P.subst P y p)
                          x∈xs
      = lem₁ _ helper
    where
    helper : Any.map (λ q → p , q) (lose y∈ys q) ≡ pq′
    helper rewrite P.sym $ map-∘ {R = λ y → P x × Q y}
                                 (λ q → p , q)
                                 (λ y → P.subst Q y q)
                                 y∈ys
      = lem₂ _ refl

------------------------------------------------------------------------
-- Invertible introduction (⁺) and elimination (⁻) rules for various
-- list functions

-- map.

private

  map⁺ : ∀ {a b p} {A : Set a} {B : Set b} {P : B → Set p}
           {f : A → B} {xs} →
         Any (P ∘ f) xs → Any P (List.map f xs)
  map⁺ (here p)  = here p
  map⁺ (there p) = there $ map⁺ p

  map⁻ : ∀ {a b p} {A : Set a} {B : Set b} {P : B → Set p}
           {f : A → B} {xs} →
         Any P (List.map f xs) → Any (P ∘ f) xs
  map⁻ {xs = []}     ()
  map⁻ {xs = x ∷ xs} (here p)  = here p
  map⁻ {xs = x ∷ xs} (there p) = there $ map⁻ p

  map⁺∘map⁻ : ∀ {a b p} {A : Set a} {B : Set b} {P : B → Set p}
                {f : A → B} {xs} →
              (p : Any P (List.map f xs)) →
              map⁺ (map⁻ p) ≡ p
  map⁺∘map⁻ {xs = []}     ()
  map⁺∘map⁻ {xs = x ∷ xs} (here  p) = refl
  map⁺∘map⁻ {xs = x ∷ xs} (there p) = P.cong there (map⁺∘map⁻ p)

  map⁻∘map⁺ : ∀ {a b p} {A : Set a} {B : Set b} (P : B → Set p)
                {f : A → B} {xs} →
              (p : Any (P ∘ f) xs) →
              map⁻ {P = P} (map⁺ p) ≡ p
  map⁻∘map⁺ P (here  p) = refl
  map⁻∘map⁺ P (there p) = P.cong there (map⁻∘map⁺ P p)

map↔ : ∀ {a b p} {A : Set a} {B : Set b} {P : B → Set p}
         {f : A → B} {xs} →
       Any (P ∘ f) xs ↔ Any P (List.map f xs)
map↔ {P = P} {f = f} = record
  { to         = P.→-to-⟶ $ map⁺ {P = P} {f = f}
  ; from       = P.→-to-⟶ $ map⁻ {P = P} {f = f}
  ; inverse-of = record
    { left-inverse-of  = map⁻∘map⁺ P
    ; right-inverse-of = map⁺∘map⁻
    }
  }

-- _++_.

private

  ++⁺ˡ : ∀ {a p} {A : Set a} {P : A → Set p} {xs ys} →
         Any P xs → Any P (xs ++ ys)
  ++⁺ˡ (here p)  = here p
  ++⁺ˡ (there p) = there (++⁺ˡ p)

  ++⁺ʳ : ∀ {a p} {A : Set a} {P : A → Set p} xs {ys} →
         Any P ys → Any P (xs ++ ys)
  ++⁺ʳ []       p = p
  ++⁺ʳ (x ∷ xs) p = there (++⁺ʳ xs p)

  ++⁻ : ∀ {a p} {A : Set a} {P : A → Set p} xs {ys} →
        Any P (xs ++ ys) → Any P xs ⊎ Any P ys
  ++⁻ []       p         = inj₂ p
  ++⁻ (x ∷ xs) (here p)  = inj₁ (here p)
  ++⁻ (x ∷ xs) (there p) = Sum.map there id (++⁻ xs p)

  ++⁺∘++⁻ : ∀ {a p} {A : Set a} {P : A → Set p} xs {ys}
            (p : Any P (xs ++ ys)) →
            [ ++⁺ˡ , ++⁺ʳ xs ]′ (++⁻ xs p) ≡ p
  ++⁺∘++⁻ []       p         = refl
  ++⁺∘++⁻ (x ∷ xs) (here  p) = refl
  ++⁺∘++⁻ (x ∷ xs) (there p) with ++⁻ xs p | ++⁺∘++⁻ xs p
  ++⁺∘++⁻ (x ∷ xs) (there p) | inj₁ p′ | ih = P.cong there ih
  ++⁺∘++⁻ (x ∷ xs) (there p) | inj₂ p′ | ih = P.cong there ih

  ++⁻∘++⁺ : ∀ {a p} {A : Set a} {P : A → Set p} xs {ys}
            (p : Any P xs ⊎ Any P ys) →
            ++⁻ xs ([ ++⁺ˡ , ++⁺ʳ xs ]′ p) ≡ p
  ++⁻∘++⁺ []            (inj₁ ())
  ++⁻∘++⁺ []            (inj₂ p)         = refl
  ++⁻∘++⁺ (x ∷ xs)      (inj₁ (here  p)) = refl
  ++⁻∘++⁺ (x ∷ xs) {ys} (inj₁ (there p)) rewrite ++⁻∘++⁺ xs {ys} (inj₁ p) = refl
  ++⁻∘++⁺ (x ∷ xs)      (inj₂ p)         rewrite ++⁻∘++⁺ xs      (inj₂ p) = refl

++↔ : ∀ {a p} {A : Set a} {P : A → Set p} {xs ys} →
      (Any P xs ⊎ Any P ys) ↔ Any P (xs ++ ys)
++↔ {P = P} {xs = xs} = record
  { to         = P.→-to-⟶ [ ++⁺ˡ {P = P}, ++⁺ʳ {P = P} xs ]′
  ; from       = P.→-to-⟶ $ ++⁻ {P = P} xs
  ; inverse-of = record
    { left-inverse-of  = ++⁻∘++⁺ xs
    ; right-inverse-of = ++⁺∘++⁻ xs
    }
  }

-- return.

private

  return⁺ : ∀ {a p} {A : Set a} {P : A → Set p} {x} →
            P x → Any P (return x)
  return⁺ = here

  return⁻ : ∀ {a p} {A : Set a} {P : A → Set p} {x} →
            Any P (return x) → P x
  return⁻ (here p)   = p
  return⁻ (there ())

  return⁺∘return⁻ : ∀ {a p} {A : Set a} {P : A → Set p} {x}
                    (p : Any P (return x)) →
                    return⁺ (return⁻ p) ≡ p
  return⁺∘return⁻ (here p)   = refl
  return⁺∘return⁻ (there ())

  return⁻∘return⁺ : ∀ {a p} {A : Set a} (P : A → Set p) {x} (p : P x) →
                    return⁻ {P = P} (return⁺ p) ≡ p
  return⁻∘return⁺ P p = refl

return↔ : ∀ {a p} {A : Set a} {P : A → Set p} {x} →
          P x ↔ Any P (return x)
return↔ {P = P} = record
  { to         = P.→-to-⟶ $ return⁺ {P = P}
  ; from       = P.→-to-⟶ $ return⁻ {P = P}
  ; inverse-of = record
    { left-inverse-of  = return⁻∘return⁺ P
    ; right-inverse-of = return⁺∘return⁻
    }
  }

-- _∷_.

∷↔ : ∀ {a p} {A : Set a} (P : A → Set p) {x xs} →
     (P x ⊎ Any P xs) ↔ Any P (x ∷ xs)
∷↔ P {x} {xs} =
  (P x         ⊎ Any P xs)  ↔⟨ return↔ {P = P} ⊎-cong (Any P xs ∎) ⟩
  (Any P [ x ] ⊎ Any P xs)  ↔⟨ ++↔ {P = P} {xs = [ x ]} ⟩
  Any P (x ∷ xs)            ∎

-- concat.

private

  concat⁺ : ∀ {a p} {A : Set a} {P : A → Set p} {xss} →
            Any (Any P) xss → Any P (concat xss)
  concat⁺ (here p)           = ++⁺ˡ p
  concat⁺ (there {x = xs} p) = ++⁺ʳ xs (concat⁺ p)

  concat⁻ : ∀ {a p} {A : Set a} {P : A → Set p} xss →
            Any P (concat xss) → Any (Any P) xss
  concat⁻ []               ()
  concat⁻ ([]       ∷ xss) p         = there $ concat⁻ xss p
  concat⁻ ((x ∷ xs) ∷ xss) (here  p) = here (here p)
  concat⁻ ((x ∷ xs) ∷ xss) (there p)
    with concat⁻ (xs ∷ xss) p
  ... | here  p′ = here (there p′)
  ... | there p′ = there p′

  concat⁻∘++⁺ˡ : ∀ {a p} {A : Set a} {P : A → Set p} {xs} xss (p : Any P xs) →
                 concat⁻ (xs ∷ xss) (++⁺ˡ p) ≡ here p
  concat⁻∘++⁺ˡ xss (here  p) = refl
  concat⁻∘++⁺ˡ xss (there p) rewrite concat⁻∘++⁺ˡ xss p = refl

  concat⁻∘++⁺ʳ : ∀ {a p} {A : Set a} {P : A → Set p} xs xss (p : Any P (concat xss)) →
                 concat⁻ (xs ∷ xss) (++⁺ʳ xs p) ≡ there (concat⁻ xss p)
  concat⁻∘++⁺ʳ []       xss p = refl
  concat⁻∘++⁺ʳ (x ∷ xs) xss p rewrite concat⁻∘++⁺ʳ xs xss p = refl

  concat⁺∘concat⁻ : ∀ {a p} {A : Set a} {P : A → Set p} xss (p : Any P (concat xss)) →
                    concat⁺ (concat⁻ xss p) ≡ p
  concat⁺∘concat⁻ []               ()
  concat⁺∘concat⁻ ([]       ∷ xss) p         = concat⁺∘concat⁻ xss p
  concat⁺∘concat⁻ ((x ∷ xs) ∷ xss) (here p)  = refl
  concat⁺∘concat⁻ ((x ∷ xs) ∷ xss) (there p)
    with concat⁻ (xs ∷ xss) p | concat⁺∘concat⁻ (xs ∷ xss) p
  concat⁺∘concat⁻ ((x ∷ xs) ∷ xss) (there .(++⁺ˡ p′))              | here  p′ | refl = refl
  concat⁺∘concat⁻ ((x ∷ xs) ∷ xss) (there .(++⁺ʳ xs (concat⁺ p′))) | there p′ | refl = refl

  concat⁻∘concat⁺ : ∀ {a p} {A : Set a} {P : A → Set p} {xss} (p : Any (Any P) xss) →
                    concat⁻ xss (concat⁺ p) ≡ p
  concat⁻∘concat⁺ (here                      p) = concat⁻∘++⁺ˡ _ p
  concat⁻∘concat⁺ (there {x = xs} {xs = xss} p)
    rewrite concat⁻∘++⁺ʳ xs xss (concat⁺ p) =
      P.cong there $ concat⁻∘concat⁺ p

concat↔ : ∀ {a p} {A : Set a} {P : A → Set p} {xss} →
          Any (Any P) xss ↔ Any P (concat xss)
concat↔ {P = P} {xss = xss} = record
  { to         = P.→-to-⟶ $ concat⁺ {P = P}
  ; from       = P.→-to-⟶ $ concat⁻ {P = P} xss
  ; inverse-of = record
    { left-inverse-of  = concat⁻∘concat⁺
    ; right-inverse-of = concat⁺∘concat⁻ xss
    }
  }

-- _>>=_.

>>=↔ : ∀ {ℓ p} {A B : Set ℓ} {P : B → Set p} {xs} {f : A → List B} →
       Any (Any P ∘ f) xs ↔ Any P (xs >>= f)
>>=↔ {P = P} {xs} {f} =
  Any (Any P ∘ f) xs           ↔⟨ map↔ {P = Any P} {f = f} ⟩
  Any (Any P) (List.map f xs)  ↔⟨ concat↔ {P = P} ⟩
  Any P (xs >>= f)             ∎

-- _⊛_.

⊛↔ : ∀ {ℓ} {A B : Set ℓ} {P : B → Set ℓ}
       {fs : List (A → B)} {xs : List A} →
     Any (λ f → Any (P ∘ f) xs) fs ↔ Any P (fs ⊛ xs)
⊛↔ {ℓ} {P = P} {fs} {xs} =
  Any (λ f → Any (P ∘ f) xs) fs               ↔⟨ Any-cong (λ _ → Any-cong (λ _ → return↔ {a = ℓ} {p = ℓ}) (_ ∎)) (_ ∎) ⟩
  Any (λ f → Any (Any P ∘ return ∘ f) xs) fs  ↔⟨ Any-cong (λ _ → >>=↔ {ℓ = ℓ} {p = ℓ}) (_ ∎) ⟩
  Any (λ f → Any P (xs >>= return ∘ f)) fs    ↔⟨ >>=↔ {ℓ = ℓ} {p = ℓ} ⟩
  Any P (fs ⊛ xs)                             ∎

-- An alternative introduction rule for _⊛_.

⊛⁺′ : ∀ {ℓ} {A B : Set ℓ} {P : A → Set ℓ} {Q : B → Set ℓ}
      {fs : List (A → B)} {xs} →
      Any (P ⟨→⟩ Q) fs → Any P xs → Any Q (fs ⊛ xs)
⊛⁺′ {ℓ} pq p =
  Inverse.to (⊛↔ {ℓ = ℓ}) ⟨$⟩
    Any.map (λ pq → Any.map (λ {x} → pq {x}) p) pq

-- _⊗_.

⊗↔ : ∀ {ℓ} {A B : Set ℓ} {P : A × B → Set ℓ}
       {xs : List A} {ys : List B} →
     Any (λ x → Any (λ y → P (x , y)) ys) xs ↔ Any P (xs ⊗ ys)
⊗↔ {ℓ} {P = P} {xs} {ys} =
  Any (λ x → Any (λ y → P (x , y)) ys) xs                             ↔⟨ return↔ {a = ℓ} {p = ℓ} ⟩
  Any (λ _,_ → Any (λ x → Any (λ y → P (x , y)) ys) xs) (return _,_)  ↔⟨ ⊛↔ ⟩
  Any (λ x, → Any (P ∘ x,) ys) (_,_ <$> xs)                           ↔⟨ ⊛↔ ⟩
  Any P (xs ⊗ ys)                                                     ∎

⊗↔′ : {A B : Set} {P : A → Set} {Q : B → Set}
      {xs : List A} {ys : List B} →
      (Any P xs × Any Q ys) ↔ Any (P ⟨×⟩ Q) (xs ⊗ ys)
⊗↔′ {P = P} {Q} {xs} {ys} =
  (Any P xs × Any Q ys)                    ↔⟨ ×↔ ⟩
  Any (λ x → Any (λ y → P x × Q y) ys) xs  ↔⟨ ⊗↔ ⟩
  Any (P ⟨×⟩ Q) (xs ⊗ ys)                  ∎

-- map-with-∈.

map-with-∈↔ :
  ∀ {a b p} {A : Set a} {B : Set b} {P : B → Set p} {xs : List A}
    {f : ∀ {x} → x ∈ xs → B} →
  (∃₂ λ x (x∈xs : x ∈ xs) → P (f x∈xs)) ↔ Any P (mapWith∈ xs f)
map-with-∈↔ {A = A} {B} {P} = record
  { to         = P.→-to-⟶ (map-with-∈⁺ _)
  ; from       = P.→-to-⟶ (map-with-∈⁻ _ _)
  ; inverse-of = record
    { left-inverse-of  = from∘to _
    ; right-inverse-of = to∘from _ _
    }
  }
  where
  map-with-∈⁺ : ∀ {xs : List A}
                (f : ∀ {x} → x ∈ xs → B) →
                (∃₂ λ x (x∈xs : x ∈ xs) → P (f x∈xs)) →
                Any P (mapWith∈ xs f)
  map-with-∈⁺ f (_ , here refl  , p) = here p
  map-with-∈⁺ f (_ , there x∈xs , p) =
    there $ map-with-∈⁺ (f ∘ there) (_ , x∈xs , p)

  map-with-∈⁻ : ∀ (xs : List A)
                (f : ∀ {x} → x ∈ xs → B) →
                Any P (mapWith∈ xs f) →
                ∃₂ λ x (x∈xs : x ∈ xs) → P (f x∈xs)
  map-with-∈⁻ []       f ()
  map-with-∈⁻ (y ∷ xs) f (here  p) = (y , here refl , p)
  map-with-∈⁻ (y ∷ xs) f (there p) =
    Prod.map id (Prod.map there id) $ map-with-∈⁻ xs (f ∘ there) p

  from∘to : ∀ {xs : List A} (f : ∀ {x} → x ∈ xs → B)
            (p : ∃₂ λ x (x∈xs : x ∈ xs) → P (f x∈xs)) →
            map-with-∈⁻ xs f (map-with-∈⁺ f p) ≡ p
  from∘to f (_ , here refl  , p) = refl
  from∘to f (_ , there x∈xs , p)
    rewrite from∘to (f ∘ there) (_ , x∈xs , p) = refl

  to∘from : ∀ (xs : List A) (f : ∀ {x} → x ∈ xs → B)
            (p : Any P (mapWith∈ xs f)) →
            map-with-∈⁺ f (map-with-∈⁻ xs f p) ≡ p
  to∘from []       f ()
  to∘from (y ∷ xs) f (here  p) = refl
  to∘from (y ∷ xs) f (there p) =
    P.cong there $ to∘from xs (f ∘ there) p

------------------------------------------------------------------------
-- Any and any are related via T

-- These introduction and elimination rules are not inverses, though.

private

  any⁺ : ∀ {a} {A : Set a} (p : A → Bool) {xs} →
         Any (T ∘ p) xs → T (any p xs)
  any⁺ p (here  px)          = Equivalence.from T-∨ ⟨$⟩ inj₁ px
  any⁺ p (there {x = x} pxs) with p x
  ... | true  = _
  ... | false = any⁺ p pxs

  any⁻ : ∀ {a} {A : Set a} (p : A → Bool) xs →
         T (any p xs) → Any (T ∘ p) xs
  any⁻ p []       ()
  any⁻ p (x ∷ xs) px∷xs with p x | inspect p x
  any⁻ p (x ∷ xs) px∷xs | true  | P[ eq ] = here (Equivalence.from T-≡ ⟨$⟩ eq)
  any⁻ p (x ∷ xs) px∷xs | false | _       = there (any⁻ p xs px∷xs)

any⇔ : ∀ {a} {A : Set a} {p : A → Bool} {xs} →
       Any (T ∘ p) xs ⇔ T (any p xs)
any⇔ = Eq.equivalence (any⁺ _) (any⁻ _ _)

------------------------------------------------------------------------
-- _++_ is commutative

private

  ++-comm : ∀ {a p} {A : Set a} {P : A → Set p} xs ys →
            Any P (xs ++ ys) → Any P (ys ++ xs)
  ++-comm xs ys = [ ++⁺ʳ ys , ++⁺ˡ ]′ ∘ ++⁻ xs

  ++-comm∘++-comm : ∀ {a p} {A : Set a} {P : A → Set p}
                    xs {ys} (p : Any P (xs ++ ys)) →
                    ++-comm ys xs (++-comm xs ys p) ≡ p
  ++-comm∘++-comm [] {ys} p
    rewrite ++⁻∘++⁺ ys {ys = []} (inj₁ p) = P.refl
  ++-comm∘++-comm {P = P} (x ∷ xs) {ys} (here p)
    rewrite ++⁻∘++⁺ {P = P} ys {ys = x ∷ xs} (inj₂ (here p)) = P.refl
  ++-comm∘++-comm (x ∷ xs)      (there p) with ++⁻ xs p | ++-comm∘++-comm xs p
  ++-comm∘++-comm (x ∷ xs) {ys} (there .([ ++⁺ʳ xs , ++⁺ˡ ]′ (++⁻ ys (++⁺ʳ ys p))))
    | inj₁ p | P.refl
    rewrite ++⁻∘++⁺ ys (inj₂                  p)
          | ++⁻∘++⁺ ys (inj₂ $′ there {x = x} p) = refl
  ++-comm∘++-comm (x ∷ xs) {ys} (there .([ ++⁺ʳ xs , ++⁺ˡ ]′ (++⁻ ys (++⁺ˡ    p))))
    | inj₂ p | P.refl
    rewrite ++⁻∘++⁺ ys {ys =     xs} (inj₁ p)
          | ++⁻∘++⁺ ys {ys = x ∷ xs} (inj₁ p) = P.refl

++↔++ : ∀ {a p} {A : Set a} {P : A → Set p} xs ys →
        Any P (xs ++ ys) ↔ Any P (ys ++ xs)
++↔++ {P = P} xs ys = record
  { to         = P.→-to-⟶ $ ++-comm {P = P} xs ys
  ; from       = P.→-to-⟶ $ ++-comm {P = P} ys xs
  ; inverse-of = record
    { left-inverse-of  = ++-comm∘++-comm xs
    ; right-inverse-of = ++-comm∘++-comm ys
    }
  }


text:
------------------------------------------------------------------------
-- A variant of Coherently that is defined without the use of
-- coinduction
------------------------------------------------------------------------

{-# OPTIONS --cubical #-}

import Equality.Path as P

module Lens.Non-dependent.Higher.Coherently.Not-coinductive
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq

open import Prelude

open import Container.Indexed equality-with-J
open import Container.Indexed.M.Function equality-with-J
open import H-level.Truncation.Propositional.One-step eq using (∥_∥¹)

private
  variable
    a b p : Level

-- A container that is used to define Coherently.

Coherently-container :
  {B : Type b}
  (P : {A : Type a} → (A → B) → Type p)
  (step : {A : Type a} (f : A → B) → P f → ∥ A ∥¹ → B) →
  Container (∃ λ (A : Type a) → A → B) p lzero
Coherently-container P step = λ where
  .Shape (_ , f)               → P f
  .Position _                  → ⊤
  .index {o = A , f} {s = p} _ → ∥ A ∥¹ , step f p

-- A variant of Coherently, defined using an indexed container.

Coherently :
  {A : Type a} {B : Type b}
  (P : {A : Type a} → (A → B) → Type p)
  (step : {A : Type a} (f : A → B) → P f → ∥ A ∥¹ → B) →
  (f : A → B) →
  Type (lsuc a ⊔ b ⊔ p)
Coherently P step f =
  M (Coherently-container P step) (_ , f)

max_stars_repo_name: nad/dependent-lenses

max_issues_repo_name: nad/dependent-lenses

max_forks_repo_name: nad/dependent-lenses


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Maps from keys to values, based on AVL trees
-- This modules provides a simpler map interface, without a dependency
-- between the key and value types.
------------------------------------------------------------------------

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

open import Relation.Binary using (StrictTotalOrder)

module Data.AVL.Map
  {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
  where

open import Data.Bool.Base using (Bool)
open import Data.List.Base using (List)
open import Data.Maybe.Base using (Maybe)
open import Data.Product using (_×_)
open import Level using (_⊔_)

import Data.AVL strictTotalOrder as AVL
open StrictTotalOrder strictTotalOrder renaming (Carrier to Key)

------------------------------------------------------------------------
-- The map type

Map : ∀ {v} → (V : Set v) → Set (a ⊔ v ⊔ ℓ₂)
Map v = AVL.Tree (AVL.const v)

------------------------------------------------------------------------
-- Repackaged functions

module _ {v} {V : Set v} where

  empty : Map V
  empty = AVL.empty

  singleton : Key → V → Map V
  singleton = AVL.singleton

  insert : Key → V → Map V → Map V
  insert = AVL.insert

  insertWith : Key → (Maybe V → V) → Map V → Map V
  insertWith = AVL.insertWith

  delete : Key → Map V → Map V
  delete = AVL.delete

  lookup : Key → Map V → Maybe V
  lookup = AVL.lookup

module _ {v w} {V : Set v} {W : Set w} where

  map : (V → W) → Map V → Map W
  map f = AVL.map f

module _ {v} {V : Set v} where

  infix 4 _∈?_

  _∈?_ : Key → Map V → Bool
  _∈?_ = AVL._∈?_

  headTail : Map V → Maybe ((Key × V) × Map V)
  headTail = AVL.headTail

  initLast : Map V → Maybe (Map V × (Key × V))
  initLast = AVL.initLast

  fromList : List (Key × V) → Map V
  fromList = AVL.fromList

  toList : Map V → List (Key × V)
  toList = AVL.toList

module _ {v w} {V : Set v} {W : Set w} where

  unionWith : (V → Maybe W → W) →
              Map V → Map W → Map W
  unionWith f = AVL.unionWith f

module _ {v} {V : Set v} where

  union : Map V → Map V → Map V
  union = AVL.union

  unionsWith : (V → Maybe V → V) → List (Map V) → Map V
  unionsWith f = AVL.unionsWith f

  unions : List (Map V) → Map V
  unions = AVL.unions


text:
open import Agda.Builtin.IO
open import Agda.Builtin.List
open import Agda.Builtin.Size
open import Agda.Builtin.String

record Thunk (F : Size → Set) (i : Size) : Set where
  coinductive
  field force : {j : Size< i} → F j
open Thunk public

FilePath = String

-- A directory tree is rooted in the current directory; it comprises:
-- * a list of files in the current directory
-- * an IO action returning a list of subdirectory trees

-- This definition does not typecheck if IO is not marked as strictly positive
data DirectoryTree (i : Size) : Set where
  _:<_ : List FilePath → IO (List (Thunk DirectoryTree i)) →
         DirectoryTree i

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Issue358 where

postulate Sigma : Set -> (Set -> Set) -> Set
syntax Sigma A (\x -> B)  = x colon A operator B

postulate T : Set
test = x colon T operator {!!}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Data.Variant where

open import Data.List using (List) renaming ([_] to [_]ₗ)
open import Data.List.Membership.Propositional using (_∈_)

open import Data.Product using (∃; ∃-syntax; _,_)

open import Data.Maybe using (Maybe; _>>=_; just)

open import Data.Union using (Union; here) renaming (inj to injᵤ; proj to projᵤ)

open import Relation.Binary.PropositionalEquality using (_≡_; refl)

open import Level using (Level)

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

-- A variant is tagged tag. It is motiviated by the existence
-- of familys of tags.

data Variant {a} (A : Set a) : A → Set a where
  -- injects a into a Variant indexed by a
  [_] : (a : A) → Variant A a

-- A polymorphic variant is a open union of variants

Variants : ∀ {a} (A : Set a) → List A → Set a
Variants A ts = Union A (Variant A) ts

-- ----------------------------------------------------------------------
-- Injections and projects to (and from) variants

private
  variable
    a b : Level
    A : Set a
    t : A
    ts ts′ : List A

inj : (t : A) → t ∈ ts → Variants A ts
inj t t∈ts = injᵤ t∈ts ([ t ])

`_ : (t : A) → ⦃ t ∈ ts ⦄ → Variants A ts
`_ t ⦃ t∈ts ⦄ = inj t t∈ts

Proj : ∀ {a} (A : Set a) → (t : A) → Set a
Proj A t = ∃ λ t′ → t ≡ t′

proj : t ∈ ts → Variants A ts → Maybe (Proj A t)
proj t∈ts x = projᵤ t∈ts x >>= λ{ [ t ] → just (t , refl)}

`proj : ⦃ t ∈ ts ⦄ → Variants A ts → Maybe (Proj A t)
`proj ⦃ t∈ts ⦄ x = proj t∈ts x

proj₀ : Variants A [ t ]ₗ → Proj A t
proj₀ (here [ t ]) = t , refl

max_stars_repo_name: johnyob/agda-union

max_issues_repo_name: johnyob/agda-union

max_forks_repo_name: johnyob/agda-union


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

open import Categories.Category

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

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

open import Categories.Adjoint.Properties
open import Categories.Category.Complete
open import Categories.Category.Complete.Properties
open import Categories.Category.Cocomplete
open import Categories.Category.Cocomplete.Finitely
open import Categories.Category.Duality
open import Categories.Category.Construction.Functors
open import Categories.Functor
open import Categories.Functor.Cocontinuous
open import Categories.Functor.Duality
open import Categories.NaturalTransformation as N
open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_)
open import Categories.Diagram.Limit
open import Categories.Diagram.Limit.Properties
open import Categories.Diagram.Colimit
open import Categories.Diagram.Duality

import Categories.Morphism.Reasoning as MR

private
  variable
    o′ ℓ′ e′ o″ ℓ″ e″ : Level
  module C = Category C

Cocomplete⇒FinitelyCocomplete : Cocomplete o′ ℓ′ e′ C → FinitelyCocomplete C
Cocomplete⇒FinitelyCocomplete Coc =
  coFinitelyComplete⇒FinitelyCocomplete C (Complete⇒FinitelyComplete C.op (Cocomplete⇒coComplete C Coc))

module _ {D : Category o′ ℓ′ e′} (Coc : Cocomplete o″ ℓ″ e″ D) where
  private
    module D = Category D

  Functors-Cocomplete : Cocomplete o″ ℓ″ e″ (Functors C D)
  Functors-Cocomplete {J} F = coLimit⇒Colimit (Functors C D) LFop
    where module J = Category J
          module F = Functor F
          open Functor F
          F′ : Functor J.op (Functors C.op D.op)
          F′ = opF⇒ ∘F F.op

          L : (H : Functor J.op (Functors C.op D.op)) → Limit H
          L = Functors-Complete C.op {D = D.op} (λ G → Colimit⇒coLimit D (Coc (Functor.op G)))

          LF′ : Limit F′
          LF′ = L F′

          LF″ : Limit (opF⇐ ∘F F′)
          LF″ = rapl (Functorsᵒᵖ-equiv.L⊣R C.op D.op) F′ LF′

          iso : opF⇐ ∘F F′ ≃ F.op
          iso = record
            { F⇒G = ntHelper record
              { η       = λ _ → N.id
              ; commute = λ f → id-comm
              }
            ; F⇐G = ntHelper record
              { η       = λ _ → N.id
              ; commute = λ f → id-comm
              }
            ; iso = λ j → record
              { isoˡ = D.identity²
              ; isoʳ = D.identity²
              }
            }
            where open MR D

          LFop : Limit op
          LFop = ≃-resp-lim iso LF″

  -- TODO: need to refactor the where block above to show cocontinuous. there is no need to do it now.
  --
  -- evalF-Cocontinuous : ∀ X → Cocontinuous o″ ℓ″ e″ (evalF C D X)
  -- evalF-Cocontinuous X {J} {F} L = Coc (evalF C D X ∘F F) , {!!}
  --   where

max_stars_repo_name: laMudri/agda-categories

max_issues_repo_name: laMudri/agda-categories

max_forks_repo_name: laMudri/agda-categories


text:
module STLCRef.Examples where

-- This file contains a few example programs for the definitional
-- interpreter for STLC+Ref using monadic strength, defined in Section
-- 3.

open import STLCRef.Semantics
open import Data.List
open import Data.List.Relation.Unary.Any
open import Data.List.Relation.Unary.All
open import Relation.Binary.PropositionalEquality
open import Data.Integer hiding (suc)
open import Agda.Builtin.Nat hiding (_+_)
open import Data.Maybe
open import Data.Product

-------------------
-- STLC FRAGMENT --
-------------------

-- The identity function: λ x . x
idexpr : Expr [] (unit ⇒ unit)
idexpr = ƛ (var (here refl))

-- id () = ()
test-idexpr : eval 2 (idexpr · unit) [] [] ≡ just (_ , [] , unit , _)
test-idexpr = refl

-- curried addition: λ x . λ y . y + x
curry+ : Expr [] (int ⇒ (int ⇒ int))
curry+ = ƛ (ƛ (iop _+_ (var (here refl)) (var (there (here refl)))))

-- 1 + 1 = 2
test-curry+ : eval 3 ((curry+ · (num (+ (suc zero)))) · (num (+ (suc zero)))) [] []
              ≡ just (_ , [] , num (+ (suc (suc zero))) , _)
test-curry+ = refl

------------------
-- REF FRAGMENT --
------------------

-- Sugar for let: LET e1 e2 = (λ x . e2) e1
LET : ∀ {Γ a b} → Expr Γ a → Expr (a ∷ Γ) b → Expr Γ b
LET bnd bod = (ƛ bod) · bnd

-- Factorial function, defined via Landin's knot:
--
-- let r = ref (λ x . x) in
-- let f = λ n . ifz n then 1 else n * (!r (n - 1)) in
-- let _ = r := f in
-- f 4
landin-fac : Expr [] int
landin-fac =
  LET (ref {t = int ⇒ int} (ƛ (var (here refl))))
  (LET (ƛ {a = int} (ifz (var (here refl))
                         (num (+ 1))
                         (iop (Data.Integer._*_) (var (here refl))
                              ((! (var (there (here refl)))) · (iop (Data.Integer._-_) (var (here refl)) (num (+ 1)))))))
  (LET ((var (there (here refl))) ≔ var (here refl))
  (var (there (here refl))) · (num (+ 4))))

test-landin-fac : eval 20 landin-fac [] [] ≡ just (_ , _ , num (+ 24) , _)
test-landin-fac = refl

-- Divergence via Landin's knot:
--
-- let r = ref (λ x . x) in
-- let f = λ x . !r 0 in
-- let _ = r := f in
-- f 0
landin-div : Expr [] int
landin-div =
  LET (ref {t = int ⇒ int} (ƛ (var (here refl))))
  (LET (ƛ {a = int} ((! (var (there (here refl)))) · num (+ zero)))
  (LET ((var (there (here refl))) ≔ var (here refl))
  (var (there (here refl))) · (num (+ zero))))

test-landin-div : eval 1337 landin-div [] [] ≡ nothing
test-landin-div = refl


text:
-- Proof: if we non-deterministically select an element
-- which is less-than-or-equal than all other elements,
-- such a result is the minimum of the list.
-- This holds for any non-deterministically selected element.

-- Basically, this is the translation of the Curry rule:
--
--   min-nd xs@(_++[x]++_) | all (x<=) xs = x
--

open import bool

module minlist-is-correct
  (Choice : Set)
  (choose : Choice → 𝔹)
  (lchoice : Choice → Choice)
  (rchoice : Choice → Choice)
 where

open import eq
open import bool-thms
open import bool-thms2
open import nat
open import nat-thms
open import list
open import maybe
open import inspect

----------------------------------------------------------------------
-- Some auxiliaries:

-- We define our own less-or-equal since the standard definition with
-- if-then-else produces too many branches:

_<=_ : ℕ → ℕ → 𝔹
0 <= y = tt
(suc x) <= 0 = ff
(suc x) <= (suc y) = x <= y

-- Some properties about less-or-equal:

<=-refl : ∀ (x : ℕ) → x <= x ≡ tt
<=-refl 0 = refl
<=-refl (suc x) = <=-refl x

<=-trans : ∀ (x y z : ℕ) → x <= y ≡ tt → y <= z ≡ tt → x <= z ≡ tt
<=-trans zero y z p1 p2 = refl
<=-trans (suc x) zero z p1 p2 = 𝔹-contra p1
<=-trans (suc x) (suc y) zero p1 p2 = 𝔹-contra p2
<=-trans (suc x) (suc y) (suc z) p1 p2 = <=-trans x y z p1 p2

<=-< : ∀ (x y : ℕ) → x <= y ≡ ff → y < x ≡ tt
<=-< zero x ()
<=-< (suc x) zero p = refl
<=-< (suc x) (suc y) p = <=-< x y p

<-<= : ∀ (x y : ℕ) → x < y ≡ tt → y <= x ≡ ff
<-<= x zero p rewrite <-0 x = 𝔹-contra p
<-<= zero (suc y) p = refl
<-<= (suc x) (suc y) p = <-<= x y p

<-<=-ff : ∀ (x y : ℕ) → x < y ≡ ff → y <= x ≡ tt
<-<=-ff zero zero p = refl
<-<=-ff zero (suc y) p = 𝔹-contra (sym p)
<-<=-ff (suc x) zero p = refl
<-<=-ff (suc x) (suc y) p = <-<=-ff x y p

<-<=-trans : ∀ (x y z : ℕ) → x < y ≡ tt → y <= z ≡ tt → x < z ≡ tt
<-<=-trans zero zero z p1 p2 = 𝔹-contra p1
<-<=-trans zero (suc y) zero p1 p2 = 𝔹-contra p2
<-<=-trans zero (suc y) (suc z) p1 p2 = refl
<-<=-trans (suc x) zero z p1 p2 = 𝔹-contra p1
<-<=-trans (suc x) (suc y) zero p1 p2 = 𝔹-contra p2
<-<=-trans (suc x) (suc y) (suc z) p1 p2 = <-<=-trans x y z p1 p2

----------------------------------------------------------------------
-- More lemmas about ordering relations:

leq-if : ∀ (x y z : ℕ)
      → y <= x && y <= z ≡ (if x <= z then y <= x else y <= z)
leq-if x y z with inspect (y <= x)
leq-if x y z | it tt p1 with inspect (x <= z)
... | it tt p2 rewrite p1 | p2 | <=-trans y x z p1 p2 = refl
... | it ff p2 rewrite p1 | p2 = refl
leq-if x y z | it ff p1 with inspect (x <= z)
... | it tt p2 rewrite p1 | p2 = refl
... | it ff p2 rewrite p1 | p2
           | <-<= z y (<-trans {z} {x} {y} (<=-< x z p2) (<=-< y x p1)) = refl

le-if : ∀ (x y z : ℕ)
     → y < x && y < z ≡ (if x <= z then y < x else y < z)
le-if x y z with inspect (y < x)
le-if x y z | it tt p1 with inspect (x <= z)
... | it tt p2 rewrite p1 | p2 | <-<=-trans y x z p1 p2 = refl
... | it ff p2 rewrite p1 | p2 = refl
le-if x y z | it ff p1 with inspect (x <= z)
... | it tt p2 rewrite p1 | p2 = refl
... | it ff p2 rewrite p1 | p2
         | <-asym {z} {y} (<-<=-trans z x y (<=-< x z p2) (<-<=-ff y x p1))
  = refl

----------------------------------------------------------------------
-- A lemma relating equality and orderings:

=ℕ-not-le : ∀ (m n : ℕ) → m =ℕ n  ≡ ~ (m < n) && m <= n
=ℕ-not-le zero zero = refl
=ℕ-not-le zero (suc m) = refl
=ℕ-not-le (suc n) zero = refl
=ℕ-not-le (suc n) (suc m) = =ℕ-not-le n m

----------------------------------------------------------------------
-- This is the translation of the Curry program:

-- Check whether all elements of a list satisfy a given predicate:
all : {A : Set} → (A → 𝔹) → 𝕃 A → 𝔹
all _ [] = tt
all p (x :: xs) = p x && all p xs

-- Deterministic min-d:
min-d : (l : 𝕃 ℕ) → is-empty l ≡ ff → ℕ
min-d []        ()
min-d (x :: []) _ = x
min-d (x :: y :: xs) _ =
  --if x <= min-d (y :: xs) refl then x else min-d (y :: xs) refl
  let z = min-d (y :: xs) refl
   in if x <= z then x else z

-- Select some element from a list:
select : {A : Set} → Choice → 𝕃 A -> maybe A
select _  []        = nothing
select ch (x :: xs) = if choose ch then just x
                                   else select (lchoice ch) xs

-- Select elements with a property from a list:
select-with : {A : Set} → Choice → (A → 𝔹) → 𝕃 A  → maybe A
select-with _  p [] = nothing
select-with ch p (x :: xs) =
  if choose ch then (if p x then just x else nothing)
               else select-with (lchoice ch) p xs

{-
-- more or less original definition:
min-nd : Choice → 𝕃 ℕ -> maybe ℕ
min-nd ch xs = (select ch xs) ≫=maybe
               (λ y → if all (_<=_ y) xs then just y else nothing)
-}

min-nd : Choice → (xs : 𝕃 ℕ) → maybe ℕ
min-nd ch xs = select-with ch (λ x → all (_<=_ x) xs) xs

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

-- Proof of the correctness of the operation select-with:
select-with-correct : ∀ {A : Set}
                   → (ch : Choice) (p : A → 𝔹) (xs : 𝕃 A) (z : A)
                   → select-with ch p xs ≡ just z → p z ≡ tt
select-with-correct ch p [] z ()
select-with-correct ch p (x :: xs) z u with choose ch
select-with-correct ch p (x :: xs) z u | tt with inspect (p x)
select-with-correct ch p (x :: xs) z u | tt | it tt v rewrite v | u | down-≡ u
 = v
select-with-correct ch p (x :: xs) z u | tt | it ff v rewrite v with u
select-with-correct ch p (x :: xs) z u | tt | it ff v | ()
select-with-correct ch p (x :: xs) z u | ff =
  select-with-correct (lchoice ch) p xs z u

----------------------------------------------------------------------
-- First step: if y smaller than all elements, y is smaller than the minimum:
all-leq-min : ∀ (y x : ℕ) (xs : 𝕃 ℕ)
           → all (_<=_ y) (x :: xs) ≡ y <= min-d (x :: xs) refl
all-leq-min y x [] = &&-tt (y <= x)
all-leq-min y x (z :: zs)
  rewrite all-leq-min y z zs
    | ite-arg (_<=_ y) (x <= min-d (z :: zs) refl) x (min-d (z :: zs) refl)
 = leq-if x y (min-d (z :: zs) refl)

-- Now we can prove:
-- if min-nd selects an element, it is smaller or equal than the minimum:
min-nd-select-min-d : ∀ (ch : Choice) (x : ℕ) (xs : 𝕃 ℕ) (z : ℕ)
      → min-nd ch (x :: xs) ≡ just z → z <= min-d (x :: xs) refl ≡ tt
min-nd-select-min-d ch x xs z u
 rewrite sym (all-leq-min z x xs)
       | select-with-correct ch (λ y → all (_<=_ y) (x :: xs)) (x :: xs) z u
 = refl

----------------------------------------------------------------------
-- Next step: if y smaller than all elements, y is smaller than the minimum:
all-less-min : ∀ (y x : ℕ) (xs : 𝕃 ℕ)
           → all (_<_ y) (x :: xs) ≡ y < min-d (x :: xs) refl
all-less-min y x [] rewrite &&-tt (y < x) = refl
all-less-min y x (z :: zs)
  rewrite all-less-min y z zs
    | ite-arg (_<_ y) (x <= min-d (z :: zs) refl) x (min-d (z :: zs) refl)
 = le-if x y (min-d (z :: zs) refl)

-- Next want to prove that the element selected by min-nd cannot be smaller
-- than the minimum.

-- For this purpose, we prove an auxiliary lemma:
-- If an element is selected from a list, it cannot be smaller than all elements
select-with-all<-ff : ∀ (ch : Choice) (p : ℕ → 𝔹) (xs : 𝕃 ℕ) (z : ℕ)
                   → select-with ch p xs ≡ just z → all (_<_ z) xs ≡ ff
select-with-all<-ff ch _ [] z ()
select-with-all<-ff ch p (x :: xs) z u with (choose ch)
select-with-all<-ff ch p (x :: xs) z u | tt with (p x)
select-with-all<-ff ch p (x :: xs) z u | tt | tt rewrite down-≡ u | <-irrefl z
  = refl
select-with-all<-ff ch p (x :: xs) z () | tt | ff
select-with-all<-ff ch p (x :: xs) z u | ff
  rewrite select-with-all<-ff (lchoice ch) p xs z u | &&-ff (z < x) = refl

-- Now we can prove: if min-nd selects an element, it cannot be smaller
-- than all other elements:
min-nd-select-all<-ff : ∀ (ch : Choice) (xs : 𝕃 ℕ) (z : ℕ)
      → min-nd ch xs ≡ just z → all (_<_ z) xs ≡ ff
min-nd-select-all<-ff ch xs z u
 rewrite select-with-all<-ff ch (λ y → all (_<=_ y) xs) xs z u  = refl

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

-- This is the main theorem:
min-nd-theorem : ∀ (ch : Choice) (x : ℕ) (xs : 𝕃 ℕ) (z : ℕ)
           → min-nd ch (x :: xs) ≡ just z → z =ℕ min-d (x :: xs) refl ≡ tt
min-nd-theorem ch x xs z u
 rewrite
   =ℕ-not-le z (min-d (x :: xs) refl)   -- split equality into no less and leq
 | min-nd-select-min-d ch x xs z u       -- min-nd selects leq min. elements
 | sym (all-less-min z x xs)             -- less-than min. elements satisfy all<
 | min-nd-select-all<-ff ch (x :: xs) z u -- min-nd can't select any all< element
 = refl

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

max_stars_repo_name: mihanus/curry-agda

max_issues_repo_name: mihanus/curry-agda

max_forks_repo_name: mihanus/curry-agda


text:
{-

A Cubical proof of Blakers-Massey Theorem (KANG Rongji, Oct. 2021)

Based on the previous type-theoretic proof described in
  Kuen-Bang Hou (Favonia), Eric Finster, Dan Licata, Peter LeFanu Lumsdaine,
  "A Mechanization of the Blakers–Massey Connectivity Theorem in Homotopy Type Theory"
  (https://arxiv.org/abs/1605.03227)

Also the HoTT-Agda formalization by Favonia:
  (https://github.com/HoTT/HoTT-Agda/blob/master/theorems/homotopy/BlakersMassey.agda)

Using cubes explicitly as much as possible.

-}
{-# OPTIONS  --safe #-}
module Cubical.Homotopy.BlakersMassey where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Transport
open import Cubical.Foundations.HLevels

open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence

open import Cubical.Data.Nat hiding (elim)
open import Cubical.Data.Sigma

open import Cubical.HITs.Truncation renaming (hLevelTrunc to Trunc)

open import Cubical.Homotopy.Connected
open import Cubical.Homotopy.WedgeConnectivity

module BlakersMassey {ℓ₁ ℓ₂ ℓ₃ : Level}
  (X : Type ℓ₁)(Y : Type ℓ₂)(Q : X → Y → Type ℓ₃)
  {m : HLevel} (leftConn  : (x : X) → isConnected (1 + m) (Σ[ y ∈ Y ] Q x y))
  {n : HLevel} (rightConn : (y : Y) → isConnected (1 + n) (Σ[ x ∈ X ] Q x y))
  where

  ℓ : Level
  ℓ = ℓ-max (ℓ-max ℓ₁ ℓ₂) ℓ₃

  leftFiber  : X → Type (ℓ-max ℓ₂ ℓ₃)
  leftFiber x  = Σ[ y ∈ Y ] Q x y

  rightFiber : Y → Type (ℓ-max ℓ₁ ℓ₃)
  rightFiber y = Σ[ x ∈ X ] Q x y

  {- An alternative formulation of pushout with fewer parameters -}

  data Pushout : Type ℓ
    where
      inl : X → Pushout
      inr : Y → Pushout
      push : {x : X}{y : Y} → Q x y → inl x ≡ inr y

  {- Some preliminary definitions for convenience -}

  fiberSquare :
      {x₀ x₁ : X}{y₀ : Y}{p : Pushout}(q₀₀ : Q x₀ y₀)(q₁₀ : Q x₁ y₀)
    → inl x₁ ≡ p → inl x₀ ≡ p → Type ℓ
  fiberSquare q₀₀ q₁₀ r' r = PathP (λ i → push q₀₀ (~ i) ≡ r' i) (sym (push q₁₀)) r

  fiberSquarePush :
      {x₀ x₁ : X}{y₀ y₁ : Y}(q₀₀ : Q x₀ y₀)(q₁₀ : Q x₁ y₀)(q₁₁ : Q x₁ y₁)
    → inl x₀ ≡ inr y₁ → Type ℓ
  fiberSquarePush q₀₀ q₁₀ q₁₁ = fiberSquare q₀₀ q₁₀ (push q₁₁)

  fiber' : {x₀ : X}{y₀ : Y}(q₀₀ : Q x₀ y₀){x₁ : X}{p : Pushout} → inl x₁ ≡ p → inl x₀ ≡ p → Type ℓ
  fiber' {y₀ = y₀} q₀₀ {x₁ = x₁} r' r = Σ[ q₁₀ ∈ Q x₁ y₀ ] fiberSquare q₀₀ q₁₀ r' r

  fiber'Push : {x₀ x₁ : X}{y₀ y₁ : Y}(q₀₀ : Q x₀ y₀)(q₁₁ : Q x₁ y₁) → inl x₀ ≡ inr y₁ → Type ℓ
  fiber'Push q₀₀ q₁₁ = fiber' q₀₀ (push q₁₁)

  leftCodeExtended :
      {x₀ : X}{y₀ : Y}(q₀₀ : Q x₀ y₀)
    → (x₁ : X){p : Pushout} → inl x₁ ≡ p → inl x₀ ≡ p → Type ℓ
  leftCodeExtended {y₀ = y₀} q₀₀ x₁ r' r = Trunc (m + n) (fiber' q₀₀ r' r)

  rightCode : {x₀ : X}(y : Y) → inl x₀ ≡ inr y → Type ℓ
  rightCode y r = Trunc (m + n) (fiber push r)

  {- Bunch of coherence data that will be used to construct Code -}

  {- Definitions of fiber→ -}

  module _
    {x₁ : X}{y₀ : Y}(q₁₀ : Q x₁ y₀) where

    {- (x₀ , q₀₀) = (x₁ , q₁₀) -}
    module _
      {y₁ : Y}(q₁₁ : Q x₁ y₁)
      (r : inl x₁ ≡ inr y₁)
      (p : fiberSquarePush q₁₀ q₁₀ q₁₁ r) where

      fiber→[q₀₀=q₁₀]-filler : (i j k : I) → Pushout
      fiber→[q₀₀=q₁₀]-filler i j k' =
        hfill (λ k → λ { (i = i0) → push q₁₁ (j ∧ k)
                       ; (i = i1) → p k j
                       ; (j = i0) → push q₁₀ (i ∧ ~ k)
                       ; (j = i1) → push q₁₁ k })
              (inS (push q₁₀ (i ∧ ~ j))) k'

      fiber→[q₀₀=q₁₀] : fiber push r
      fiber→[q₀₀=q₁₀] .fst = q₁₁
      fiber→[q₀₀=q₁₀] .snd i j = fiber→[q₀₀=q₁₀]-filler i j i1

      ∣fiber→[q₀₀=q₁₀]∣ : rightCode _ r
      ∣fiber→[q₀₀=q₁₀]∣ = ∣ fiber→[q₀₀=q₁₀] ∣ₕ

    {- (y₁ , q₁₁) = (y₀ , q₁₀) -}
    module _
      {x₀ : X}(q₀₀ : Q x₀ y₀)
      (r : inl x₀ ≡ inr y₀)
      (p : fiberSquarePush q₀₀ q₁₀ q₁₀ r) where

      fiber→[q₁₁=q₁₀]-filler : (i j k : I) → Pushout
      fiber→[q₁₁=q₁₀]-filler i j k' =
        hfill (λ k → λ { (i = i0) → push q₀₀ (j ∨ ~ k)
                       ; (i = i1) → p k j
                       ; (j = i0) → push q₀₀ (~ k)
                       ; (j = i1) → push q₁₀ (~ i ∨ k) })
              (inS (push q₁₀ (~ i ∨ ~ j))) k'

      fiber→[q₁₁=q₁₀] : fiber push r
      fiber→[q₁₁=q₁₀] .fst = q₀₀
      fiber→[q₁₁=q₁₀] .snd i j = fiber→[q₁₁=q₁₀]-filler i j i1

      ∣fiber→[q₁₁=q₁₀]∣ : rightCode _ r
      ∣fiber→[q₁₁=q₁₀]∣ = ∣ fiber→[q₁₁=q₁₀] ∣ₕ

    {- q₀₀ = q₁₁ = q₁₀ -}
    fiber→[q₀₀=q₁₀=q₁₁]-filler :
        (r : inl x₁ ≡ inr y₀)
      → (p : fiberSquarePush q₁₀ q₁₀ q₁₀ r)
      → (i j k l : I) → Pushout
    fiber→[q₀₀=q₁₀=q₁₁]-filler r p i j k l' =
      hfill (λ l → λ { (i = i0) → fiber→[q₀₀=q₁₀]-filler q₁₀ r p j k l
                     ; (i = i1) → fiber→[q₁₁=q₁₀]-filler q₁₀ r p j k l
                     ; (j = i0) → push q₁₀ ((i ∨ (k ∧ l)) ∧ (k ∨ (i ∧ ~ l)))
                     ; (j = i1) → p l k
                     ; (k = i0) → push q₁₀ ((i ∨ j) ∧ ~ l)
                     ; (k = i1) → push q₁₀ ((i ∧ ~ j) ∨ l) })
            (inS (push q₁₀ ((i ∨ (~ k ∧ j)) ∧ (~ k ∨ (i ∧ ~ j))))) l'

    fiber→[q₀₀=q₁₀=q₁₁] : fiber→[q₀₀=q₁₀] q₁₀ ≡ fiber→[q₁₁=q₁₀] q₁₀
    fiber→[q₀₀=q₁₀=q₁₁] i r p .fst = q₁₀
    fiber→[q₀₀=q₁₀=q₁₁] i r p .snd j k = fiber→[q₀₀=q₁₀=q₁₁]-filler r p i j k i1

    ∣fiber→[q₀₀=q₁₀=q₁₁]∣ : ∣fiber→[q₀₀=q₁₀]∣ q₁₀ ≡ ∣fiber→[q₁₁=q₁₀]∣ q₁₀
    ∣fiber→[q₀₀=q₁₀=q₁₁]∣ i r p = ∣ fiber→[q₀₀=q₁₀=q₁₁] i r p ∣ₕ

  {- Definitions of fiber← -}

  module _
    {x₀ : X}{y₁ : Y}(q₀₁ : Q x₀ y₁) where

    {- (x₁ , q₁₁) = (x₀ , q₀₁) -}
    module _
      {y₀ : Y}(q₀₀ : Q x₀ y₀)
      (r : inl x₀ ≡ inr y₁)
      (p : push q₀₁ ≡ r) where

      fiber←[q₁₁=q₀₁]-filler : (i j k : I) → Pushout
      fiber←[q₁₁=q₀₁]-filler i j k' =
        hfill (λ k → λ { (i = i0) → push q₀₀ (~ j ∧ k)
                       ; (i = i1) → p k j
                       ; (j = i0) → push q₀₀ (~ i ∧ k)
                       ; (j = i1) → push q₀₁ i })
              (inS (push q₀₁ (i ∧ j))) k'

      fiber←[q₁₁=q₀₁] : fiber'Push  q₀₀ q₀₁ r
      fiber←[q₁₁=q₀₁] .fst = q₀₀
      fiber←[q₁₁=q₀₁] .snd i j = fiber←[q₁₁=q₀₁]-filler i j i1

      ∣fiber←[q₁₁=q₀₁]∣ : leftCodeExtended q₀₀ _ (push q₀₁) r
      ∣fiber←[q₁₁=q₀₁]∣ = ∣ fiber←[q₁₁=q₀₁] ∣ₕ

    {- (y₀ , q₀₀) = (y₁ , q₀₁) -}
    module _
      {x₁ : X}(q₁₁ : Q x₁ y₁)
      (r : inl x₀ ≡ inr y₁)
      (p : push q₀₁ ≡ r) where

      fiber←[q₀₀=q₀₁]-filler : (i j k : I) → Pushout
      fiber←[q₀₀=q₀₁]-filler i j k' =
        hfill (λ k → λ { (i = i0) → push q₁₁ (~ j ∨ ~ k)
                       ; (i = i1) → p k j
                       ; (j = i0) → push q₀₁ (~ i)
                       ; (j = i1) → push q₁₁ (i ∨ ~ k) })
              (inS (push q₀₁ (~ i ∨ j))) k'

      fiber←[q₀₀=q₀₁] : fiber'Push q₀₁ q₁₁ r
      fiber←[q₀₀=q₀₁] .fst = q₁₁
      fiber←[q₀₀=q₀₁] .snd i j = fiber←[q₀₀=q₀₁]-filler i j i1

      ∣fiber←[q₀₀=q₀₁]∣ : leftCodeExtended q₀₁ _ (push q₁₁) r
      ∣fiber←[q₀₀=q₀₁]∣ = ∣ fiber←[q₀₀=q₀₁] ∣ₕ

    {- q₀₀ = q₀₁ = q₁₁ -}
    fiber←[q₀₀=q₀₁=q₁₁]-filler :
        (r : inl x₀ ≡ inr y₁)
      → (p : push q₀₁ ≡ r)
      → (i j k l : I) → Pushout
    fiber←[q₀₀=q₀₁=q₁₁]-filler r p i j k l' =
      hfill (λ l → λ { (i = i0) → fiber←[q₁₁=q₀₁]-filler q₀₁ r p j k l
                     ; (i = i1) → fiber←[q₀₀=q₀₁]-filler q₀₁ r p j k l
                     ; (j = i0) → push q₀₁ ((i ∨ (~ k ∧ l)) ∧ (~ k ∨ (i ∧ ~ l)))
                     ; (j = i1) → p l k
                     ; (k = i0) → push q₀₁ ((i ∨ l) ∧ ~ j)
                     ; (k = i1) → push q₀₁ ((i ∧ ~ l) ∨ j) })
            (inS (push q₀₁ ((i ∨ (k ∧ j)) ∧ (k ∨ (i ∧ ~ j))))) l'

    fiber←[q₀₀=q₀₁=q₁₁] : fiber←[q₁₁=q₀₁] q₀₁ ≡ fiber←[q₀₀=q₀₁] q₀₁
    fiber←[q₀₀=q₀₁=q₁₁] i r p .fst = q₀₁
    fiber←[q₀₀=q₀₁=q₁₁] i r p .snd j k = fiber←[q₀₀=q₀₁=q₁₁]-filler r p i j k i1

    ∣fiber←[q₀₀=q₀₁=q₁₁]∣ : ∣fiber←[q₁₁=q₀₁]∣ q₀₁ ≡ ∣fiber←[q₀₀=q₀₁]∣ q₀₁
    ∣fiber←[q₀₀=q₀₁=q₁₁]∣ i r p = ∣ fiber←[q₀₀=q₀₁=q₁₁] i r p ∣ₕ

  {- Definitions of fiber→← -}

  module _
    {x₁ : X}{y₀ : Y}(q₁₀ : Q x₁ y₀) where

    {- (x₀ , q₀₀) = (x₁ , q₁₀) -}
    module _
      {y₁ : Y}(q₁₁ : Q x₁ y₁)
      (r : inl x₁ ≡ inr y₁)
      (p : fiberSquarePush q₁₀ q₁₀ q₁₁ r) where

      fiber→←[q₀₀=q₁₀]-filler : (i j k l : I) → Pushout
      fiber→←[q₀₀=q₁₀]-filler i j k l' =
        let p' = fiber→[q₀₀=q₁₀] q₁₀ q₁₁ r p .snd in
        hfill (λ l → λ { (i = i0) → fiber←[q₁₁=q₀₁]-filler q₁₁ q₁₀ r p' j k l
                       ; (i = i1) → fiber→[q₀₀=q₁₀]-filler q₁₀ q₁₁ r p l k j
                       ; (j = i0) → push q₁₀ (~ k ∧ l)
                       ; (j = i1) → p' l k
                       ; (k = i0) → push q₁₀ (~ j ∧ l)
                       ; (k = i1) → push q₁₁ j })
              (inS (push q₁₁ (j ∧ k))) l'

      fiber→←[q₀₀=q₁₀] : fiber←[q₁₁=q₀₁] q₁₁ q₁₀ r (fiber→[q₀₀=q₁₀] q₁₀ q₁₁ r p .snd) .snd ≡ p
      fiber→←[q₀₀=q₁₀] i j k = fiber→←[q₀₀=q₁₀]-filler i j k i1

    {- (y₁ , q₁₁) = (y₀ , q₁₀) -}
    module _
      {x₀ : X}(q₀₀ : Q x₀ y₀)
      (r : inl x₀ ≡ inr y₀)
      (p : fiberSquarePush q₀₀ q₁₀ q₁₀ r) where

      fiber→←[q₁₁=q₁₀]-filler : (i j k l : I) → Pushout
      fiber→←[q₁₁=q₁₀]-filler i j k l' =
        let p' = fiber→[q₁₁=q₁₀] q₁₀ q₀₀ r p .snd in
        hfill (λ l → λ { (i = i0) → fiber←[q₀₀=q₀₁]-filler q₀₀ q₁₀ r p' j k l
                       ; (i = i1) → fiber→[q₁₁=q₁₀]-filler q₁₀ q₀₀ r p l k j
                       ; (j = i0) → push q₁₀ (~ k ∨ ~ l)
                       ; (j = i1) → p' l k
                       ; (k = i0) → push q₀₀ (~ j)
                       ; (k = i1) → push q₁₀ (j ∨ ~ l) })
              (inS (push q₀₀ (~ j ∨ k))) l'

      fiber→←[q₁₁=q₁₀] : fiber←[q₀₀=q₀₁] q₀₀ q₁₀ r (fiber→[q₁₁=q₁₀] q₁₀ q₀₀ r p .snd) .snd ≡ p
      fiber→←[q₁₁=q₁₀] i j k = fiber→←[q₁₁=q₁₀]-filler i j k i1

    {- q₀₀ = q₁₀ = q₁₁ -}
    fiber→←hypercube :
        (r : inl x₁ ≡ inr y₀)
      → (p : fiberSquarePush q₁₀ q₁₀ q₁₀ r)
      → PathP (λ i → fiber←[q₀₀=q₀₁=q₁₁] q₁₀ i r (fiber→[q₀₀=q₁₀=q₁₁] q₁₀ i r p .snd) .snd ≡ p)
              (fiber→←[q₀₀=q₁₀] q₁₀ r p) (fiber→←[q₁₁=q₁₀] q₁₀ r p)
    fiber→←hypercube r p i j u v =
      hcomp (λ l → λ { (i = i0) → fiber→←[q₀₀=q₁₀]-filler q₁₀ r p j u v l
                     ; (i = i1) → fiber→←[q₁₁=q₁₀]-filler q₁₀ r p j u v l
                     ; (j = i0) → fiber←[q₀₀=q₀₁=q₁₁]-filler q₁₀ r (fiber→[q₀₀=q₁₀=q₁₁] q₁₀ i r p .snd) i u v l
                     ; (j = i1) → fiber→[q₀₀=q₁₀=q₁₁]-filler q₁₀ r p i l v u
                     ; (u = i0) → push q₁₀ ((i ∨ (~ v ∧ l)) ∧ (~ v ∨ (i ∧ ~ l)))
                     ; (u = i1) → fiber→[q₀₀=q₁₀=q₁₁] q₁₀ i r p .snd l v
                     ; (v = i0) → push q₁₀ ((i ∨ l) ∧ ~ u)
                     ; (v = i1) → push q₁₀ ((i ∧ ~ l) ∨ u) })
            (push q₁₀ ((i ∨ (v ∧ u)) ∧ (v ∨ (i ∧ ~ u))))

  {- Definitions of fiber←→ -}

  module _
    {x₀ : X}{y₁ : Y}(q₀₁ : Q x₀ y₁) where

    {- (x₁ , q₁₁) = (x₀ , q₀₁) -}
    module _
      {y₀ : Y}(q₀₀ : Q x₀ y₀)
      (r : inl x₀ ≡ inr y₁)
      (p : push q₀₁ ≡ r) where

      fiber←→[q₁₁=q₀₁]-filler : (i j k l : I) → Pushout
      fiber←→[q₁₁=q₀₁]-filler i j k l' =
        let p' = fiber←[q₁₁=q₀₁] q₀₁ q₀₀ r p .snd in
        hfill (λ l → λ { (i = i0) → fiber→[q₀₀=q₁₀]-filler q₀₀ q₀₁ r p' j k l
                       ; (i = i1) → fiber←[q₁₁=q₀₁]-filler q₀₁ q₀₀ r p l k j
                       ; (j = i0) → push q₀₁ (k ∧ l)
                       ; (j = i1) → p' l k
                       ; (k = i0) → push q₀₀ (j ∧ ~ l)
                       ; (k = i1) → push q₀₁ l })
              (inS (push q₀₀ (j ∧ ~ k))) l'

      fiber←→[q₁₁=q₀₁] : fiber→[q₀₀=q₁₀] q₀₀ q₀₁ r (fiber←[q₁₁=q₀₁] q₀₁ q₀₀ r p .snd) .snd ≡ p
      fiber←→[q₁₁=q₀₁] i j k = fiber←→[q₁₁=q₀₁]-filler i j k i1

    {- (y₀ , q₀₀) = (y₁ , q₀₁) -}
    module _
      {x₁ : X}(q₁₁ : Q x₁ y₁)
      (r : inl x₀ ≡ inr y₁)
      (p : push q₀₁ ≡ r) where

      fiber←→[q₀₀=q₀₁]-filler : (i j k l : I) → Pushout
      fiber←→[q₀₀=q₀₁]-filler i j k l' =
        let p' = fiber←[q₀₀=q₀₁] q₀₁ q₁₁ r p .snd in
        hfill (λ l → λ { (i = i0) → fiber→[q₁₁=q₁₀]-filler q₁₁ q₀₁ r p' j k l
                       ; (i = i1) → fiber←[q₀₀=q₀₁]-filler q₀₁ q₁₁ r p l k j
                       ; (j = i0) → push q₀₁ (k ∨ ~ l)
                       ; (j = i1) → p' l k
                       ; (k = i0) → push q₀₁ (~ l)
                       ; (k = i1) → push q₁₁ (~ j ∨ l) })
              (inS (push q₁₁ (~ j ∨ ~ k))) l'

      fiber←→[q₀₀=q₀₁] : fiber→[q₁₁=q₁₀] q₁₁ q₀₁ r (fiber←[q₀₀=q₀₁] q₀₁ q₁₁ r p .snd) .snd ≡ p
      fiber←→[q₀₀=q₀₁] i j k = fiber←→[q₀₀=q₀₁]-filler i j k i1

    {- q₀₀ = q₀₁ = q₁₁ -}
    fiber←→hypercube :
        (r : inl x₀ ≡ inr y₁)
      → (p : push q₀₁ ≡ r)
      → PathP (λ i → fiber→[q₀₀=q₁₀=q₁₁] q₀₁ i r (fiber←[q₀₀=q₀₁=q₁₁] q₀₁ i r p .snd) .snd ≡ p)
              (fiber←→[q₁₁=q₀₁] q₀₁ r p) (fiber←→[q₀₀=q₀₁] q₀₁ r p)
    fiber←→hypercube r p i j u v =
      hcomp (λ l → λ { (i = i0) → fiber←→[q₁₁=q₀₁]-filler q₀₁ r p j u v l
                     ; (i = i1) → fiber←→[q₀₀=q₀₁]-filler q₀₁ r p j u v l
                     ; (j = i0) → fiber→[q₀₀=q₁₀=q₁₁]-filler q₀₁ r (fiber←[q₀₀=q₀₁=q₁₁] q₀₁ i r p .snd) i u v l
                     ; (j = i1) → fiber←[q₀₀=q₀₁=q₁₁]-filler q₀₁ r p i l v u
                     ; (u = i0) → push q₀₁ ((i ∨ (v ∧ l)) ∧ (v ∨ (i ∧ ~ l)))
                     ; (u = i1) → fiber←[q₀₀=q₀₁=q₁₁] q₀₁ i r p .snd l v
                     ; (v = i0) → push q₀₁ ((i ∨ u) ∧ ~ l)
                     ; (v = i1) → push q₀₁ ((i ∧ ~ u) ∨ l) })
           (push q₀₁ ((i ∨ (~ v ∧ u)) ∧ (~ v ∨ (i ∧ ~ u))))

  module Fiber→
    {x₁ : X}{y₀ : Y}(q₁₀ : Q x₁ y₀) =
    WedgeConnectivity m n
      (leftFiber  x₁ , (y₀ , q₁₀)) (leftConn  x₁)
      (rightFiber y₀ , (x₁ , q₁₀)) (rightConn y₀)
      (λ (y₁ , q₁₁) (x₀ , q₀₀) →
        (((r : inl x₀ ≡ inr y₁) → fiberSquarePush q₀₀ q₁₀ q₁₁ r → rightCode _ r)
        , isOfHLevelΠ2 _ (λ x y → isOfHLevelTrunc _)))
      (λ (y₁ , q₁₁) → ∣fiber→[q₀₀=q₁₀]∣ q₁₀ q₁₁)
      (λ (x₀ , q₀₀) → ∣fiber→[q₁₁=q₁₀]∣ q₁₀ q₀₀)
      (∣fiber→[q₀₀=q₁₀=q₁₁]∣ q₁₀)

  fiber→ :
      {x₁ : X}{y₀ : Y}(q₁₀ : Q x₁ y₀)
    → {x₀ : X}(q₀₀ : Q x₀ y₀) → {y₁ : Y}(q₁₁ : Q x₁ y₁)
    → (r : inl x₀ ≡ inr y₁)
    → fiberSquarePush q₀₀ q₁₀ q₁₁ r → rightCode _ r
  fiber→ q₁₀ q₀₀ q₁₁ = Fiber→.extension q₁₀ (_ , q₁₁) (_ , q₀₀)

  module Fiber←
    {x₀ : X}{y₁ : Y}(q₀₁ : Q x₀ y₁) =
    WedgeConnectivity m n
      (leftFiber  x₀ , (y₁ , q₀₁)) (leftConn  x₀)
      (rightFiber y₁ , (x₀ , q₀₁)) (rightConn y₁)
      (λ (y₀ , q₀₀) (x₁ , q₁₁) →
        (((r : inl x₀ ≡ inr y₁) → push q₀₁ ≡ r → leftCodeExtended q₀₀ _ (push q₁₁) r)
        , isOfHLevelΠ2 _ (λ x y → isOfHLevelTrunc _)))
      (λ (y₀ , q₀₀) → ∣fiber←[q₁₁=q₀₁]∣ q₀₁ q₀₀)
      (λ (x₁ , q₁₁) → ∣fiber←[q₀₀=q₀₁]∣ q₀₁ q₁₁)
      (∣fiber←[q₀₀=q₀₁=q₁₁]∣ q₀₁)

  fiber← :
      {x₀ : X}{y₁ : Y}(q₀₁ : Q x₀ y₁)
    → {y₀ : Y}(q₀₀ : Q x₀ y₀) → {x₁ : X}(q₁₁ : Q x₁ y₁)
    → (r : inl x₀ ≡ inr y₁)
    → push q₀₁ ≡ r → leftCodeExtended q₀₀ _ (push q₁₁) r
  fiber← q₀₁ q₀₀ q₁₁ = Fiber←.extension q₀₁ (_ , q₀₀) (_ , q₁₁)

  module _
    {x₀ x₁ : X}{y₀ y₁ : Y}
    (q₀₀ : Q x₀ y₀)(q₁₁ : Q x₁ y₁)
    (r : inl x₀ ≡ inr y₁) where

    left→rightCodeExtended : leftCodeExtended q₀₀ _ (push q₁₁) r → rightCode _ r
    left→rightCodeExtended =
      rec (isOfHLevelTrunc _) (λ (q₁₀ , p) → fiber→ q₁₀ q₀₀ q₁₁ r p)

    right→leftCodeExtended : rightCode _ r → leftCodeExtended q₀₀ _ (push q₁₁) r
    right→leftCodeExtended =
      rec (isOfHLevelTrunc _) (λ (q₀₁ , p) → fiber← q₀₁ q₀₀ q₁₁ r p)

  {- Definition of one-side homotopy -}

  module _
    {x₁ : X}{y₀ : Y}(q₁₀ : Q x₁ y₀) where

    {- (x₀ , q₀₀) = (x₁ , q₁₀) -}
    module _
      {y₁ : Y}(q₁₁ : Q x₁ y₁)
      (r : inl x₁ ≡ inr y₁)
      (p : fiberSquarePush q₁₀ q₁₀ q₁₁ r) where

      ∣fiber→←[q₀₀=q₁₀]∣ : right→leftCodeExtended q₁₀ q₁₁ r (fiber→ q₁₀ q₁₀ q₁₁ r p) ≡ ∣ q₁₀ , p ∣ₕ
      ∣fiber→←[q₀₀=q₁₀]∣ =
          (λ i → right→leftCodeExtended q₁₀ q₁₁ r (Fiber→.left q₁₀ (_ , q₁₁) i r p))
        ∙ recUniq {n = m + n} _ _ _
        ∙ (λ i → Fiber←.left q₁₁ (_ , q₁₀) i r (fiber→[q₀₀=q₁₀] q₁₀ q₁₁ r p .snd))
        ∙ (λ i → ∣ q₁₀ , fiber→←[q₀₀=q₁₀] q₁₀ q₁₁ r p i ∣ₕ)

    {- (y₁ , q₁₁) = (y₀ , q₁₀) -}
    module _
      {x₀ : X}(q₀₀ : Q x₀ y₀)
      (r : inl x₀ ≡ inr y₀)
      (p : fiberSquarePush q₀₀ q₁₀ q₁₀ r) where

      ∣fiber→←[q₁₁=q₁₀]∣ : right→leftCodeExtended q₀₀ q₁₀ r (fiber→ q₁₀ q₀₀ q₁₀ r p) ≡ ∣ q₁₀ , p ∣ₕ
      ∣fiber→←[q₁₁=q₁₀]∣ =
          (λ i → right→leftCodeExtended q₀₀ q₁₀ r (Fiber→.right q₁₀ (_ , q₀₀) i r p))
        ∙ recUniq {n = m + n} _ _ _
        ∙ (λ i → Fiber←.right q₀₀ (_ , q₁₀) i r (fiber→[q₁₁=q₁₀] q₁₀ q₀₀ r p .snd))
        ∙ (λ i → ∣ q₁₀ , fiber→←[q₁₁=q₁₀] q₁₀ q₀₀ r p i ∣ₕ)

    {- q₀₀ = q₁₁ = q₁₀ -}
    module _
      (r : inl x₁ ≡ inr y₀)
      (p : fiberSquarePush q₁₀ q₁₀ q₁₀ r) where

      path→←Square =
           (λ i j → right→leftCodeExtended q₁₀ q₁₀ r (Fiber→.homSquare q₁₀ i j r p))
        ∙₂ (λ i → recUniq {n = m + n} _ _ _)
        ∙₂ (λ i j → Fiber←.homSquare q₁₀ i j r (fiber→[q₀₀=q₁₀=q₁₁] q₁₀ i r p .snd))
        ∙₂ (λ i j → ∣ (q₁₀ , fiber→←hypercube q₁₀ r p i j) ∣ₕ)

    ∣fiber→←[q₀₀=q₁₀=q₁₁]∣ : ∣fiber→←[q₀₀=q₁₀]∣ q₁₀ ≡ ∣fiber→←[q₁₁=q₁₀]∣ q₁₀
    ∣fiber→←[q₀₀=q₁₀=q₁₁]∣ i r p = path→←Square r p i

  fiber→← :
      {x₁ : X}{y₀ : Y}(q₁₀ : Q x₁ y₀)
    → {x₀ : X}(q₀₀ : Q x₀ y₀) → {y₁ : Y}(q₁₁ : Q x₁ y₁)
    → (r : inl x₀ ≡ inr y₁)
    → (p : fiberSquarePush q₀₀ q₁₀ q₁₁ r)
    → right→leftCodeExtended q₀₀ q₁₁ r (fiber→ q₁₀ q₀₀ q₁₁ r p) ≡ ∣ q₁₀ , p ∣ₕ
  fiber→← {x₁ = x₁} {y₀ = y₀} q₁₀ q₀₀' q₁₁' =
    WedgeConnectivity.extension m n
      (leftFiber  x₁ , (y₀ , q₁₀)) (leftConn  x₁)
      (rightFiber y₀ , (x₁ , q₁₀)) (rightConn y₀)
      (λ (y₁ , q₁₁) (x₀ , q₀₀) →
        ((  (r : inl x₀ ≡ inr y₁) → (p : fiberSquarePush q₀₀ q₁₀ q₁₁ r)
          → right→leftCodeExtended q₀₀ q₁₁ r (fiber→ q₁₀ q₀₀ q₁₁ r p) ≡ ∣ q₁₀ , p ∣ₕ )
        , isOfHLevelΠ2 _ (λ x y → isOfHLevelTruncPath)))
      (λ (y₁ , q₁₁) → ∣fiber→←[q₀₀=q₁₀]∣ q₁₀ q₁₁)
      (λ (x₀ , q₀₀) → ∣fiber→←[q₁₁=q₁₀]∣ q₁₀ q₀₀)
      (∣fiber→←[q₀₀=q₁₀=q₁₁]∣ q₁₀)
      (_ , q₁₁') (_ , q₀₀')

  {- Definition of the other side homotopy -}

  module _
    {x₀ : X}{y₁ : Y}(q₀₁ : Q x₀ y₁) where

    {- (x₁ , q₁₁) = (x₀ , q₀₁) -}
    module _
      {y₀ : Y}(q₀₀ : Q x₀ y₀)
      (r : inl x₀ ≡ inr y₁)
      (p : push q₀₁ ≡ r) where

      ∣fiber←→[q₁₁=q₀₁]∣ : left→rightCodeExtended q₀₀ q₀₁ r (fiber← q₀₁ q₀₀ q₀₁ r p) ≡ ∣ q₀₁ , p ∣ₕ
      ∣fiber←→[q₁₁=q₀₁]∣ =
          (λ i → left→rightCodeExtended q₀₀ q₀₁ r (Fiber←.left q₀₁ (_ , q₀₀) i r p))
        ∙ recUniq {n = m + n} _ _ _
        ∙ (λ i → Fiber→.left q₀₀ (_ , q₀₁) i r (fiber←[q₁₁=q₀₁] q₀₁ q₀₀ r p .snd))
        ∙ (λ i → ∣ q₀₁ , fiber←→[q₁₁=q₀₁] q₀₁ q₀₀ r p i ∣ₕ)

    {- (y₀ , q₀₀) = (y₁ , q₀₁) -}
    module _
      {x₁ : X}(q₁₁ : Q x₁ y₁)
      (r : inl x₀ ≡ inr y₁)
      (p : push q₀₁ ≡ r) where

      ∣fiber←→[q₀₀=q₀₁]∣ : left→rightCodeExtended q₀₁ q₁₁ r (fiber← q₀₁ q₀₁ q₁₁ r p) ≡ ∣ q₀₁ , p ∣ₕ
      ∣fiber←→[q₀₀=q₀₁]∣  =
          (λ i → left→rightCodeExtended q₀₁ q₁₁ r (Fiber←.right q₀₁ (_ , q₁₁) i r p))
        ∙ recUniq {n = m + n} _ _ _
        ∙ (λ i → Fiber→.right q₁₁ (_ , q₀₁) i r (fiber←[q₀₀=q₀₁] q₀₁ q₁₁ r p .snd))
        ∙ (λ i → ∣ q₀₁ , fiber←→[q₀₀=q₀₁] q₀₁ q₁₁ r p i ∣ₕ)

    {- q₀₀ = q₀₁ = q₁₁ -}
    module _
      (r : inl x₀ ≡ inr y₁)
      (p : push q₀₁ ≡ r) where

      path←→Square =
           (λ i j → left→rightCodeExtended q₀₁ q₀₁ r (Fiber←.homSquare q₀₁ i j r p))
        ∙₂ (λ i → recUniq {n = m + n} _ _ _)
        ∙₂ (λ i j → Fiber→.homSquare q₀₁ i j r (fiber←[q₀₀=q₀₁=q₁₁] q₀₁ i r p .snd))
        ∙₂ (λ i j → ∣ q₀₁ , fiber←→hypercube q₀₁ r p i j ∣ₕ)

    ∣fiber←→[q₀₀=q₀₁=q₁₁]∣ : ∣fiber←→[q₁₁=q₀₁]∣ q₀₁ ≡ ∣fiber←→[q₀₀=q₀₁]∣ q₀₁
    ∣fiber←→[q₀₀=q₀₁=q₁₁]∣ i r p = path←→Square r p i

  fiber←→ :
      {x₀ : X}{y₁ : Y}(q₀₁ : Q x₀ y₁)
    → {y₀ : Y}(q₀₀ : Q x₀ y₀) → {x₁ : X}(q₁₁ : Q x₁ y₁)
    → (r : inl x₀ ≡ inr y₁)
    → (p : push q₀₁ ≡ r)
    → left→rightCodeExtended q₀₀ q₁₁ r (fiber← q₀₁ q₀₀ q₁₁ r p) ≡ ∣ q₀₁ , p ∣ₕ
  fiber←→ {x₀ = x₀} {y₁ = y₁} q₀₁ q₀₀' q₁₁' =
    WedgeConnectivity.extension m n
      (leftFiber  x₀ , (y₁ , q₀₁)) (leftConn  x₀)
      (rightFiber y₁ , (x₀ , q₀₁)) (rightConn y₁)
      (λ (y₀ , q₀₀) (x₁ , q₁₁) →
        ((  (r : inl x₀ ≡ inr y₁) → (p : push q₀₁ ≡ r)
          → left→rightCodeExtended q₀₀ q₁₁ r (fiber← q₀₁ q₀₀ q₁₁ r p) ≡ ∣ q₀₁ , p ∣ₕ )
        , isOfHLevelΠ2 _ (λ x y → isOfHLevelTruncPath)))
      (λ (y₀ , q₀₀) → ∣fiber←→[q₁₁=q₀₁]∣ q₀₁ q₀₀)
      (λ (x₁ , q₁₁) → ∣fiber←→[q₀₀=q₀₁]∣ q₀₁ q₁₁)
      (∣fiber←→[q₀₀=q₀₁=q₁₁]∣ q₀₁)
      (_ , q₀₀') (_ , q₁₁')

  module _
    {x₀ x₁ : X}{y₀ y₁ : Y}
    (q₀₀ : Q x₀ y₀)(q₁₁ : Q x₁ y₁)
    (r : inl x₀ ≡ inr y₁) where

    left→right→leftCodeExtended :
        (a : leftCodeExtended q₀₀ _ (push q₁₁) r)
      → right→leftCodeExtended q₀₀ q₁₁ r (left→rightCodeExtended q₀₀ q₁₁ r a) ≡ a
    left→right→leftCodeExtended a =
      sym (∘rec _ _ _ (right→leftCodeExtended q₀₀ q₁₁ r) a) ∙
      (λ i → recId _ (λ (q₁₀ , p) → fiber→← q₁₀ q₀₀ q₁₁ r p) i a)

    right→left→rightCodeExtended :
        (a : rightCode _ r)
      → left→rightCodeExtended q₀₀ q₁₁ r (right→leftCodeExtended q₀₀ q₁₁ r a) ≡ a
    right→left→rightCodeExtended a =
      sym (∘rec _ _ _ (left→rightCodeExtended q₀₀ q₁₁ r) a) ∙
      (λ i → recId _ (λ (q₀₁ , p) → fiber←→ q₀₁ q₀₀ q₁₁ r p) i a)

    left≃rightCodeExtended : leftCodeExtended q₀₀ _ (push q₁₁) r ≃ rightCode y₁ r
    left≃rightCodeExtended =
      isoToEquiv (iso (left→rightCodeExtended _ _ _) (right→leftCodeExtended _ _ _)
                       right→left→rightCodeExtended left→right→leftCodeExtended)

  {- Definition and properties of Code -}

  module _ (x₀ : X)(y₀ : Y)(q₀₀ : Q x₀ y₀) where

    leftCode' : (x : X){p : Pushout} → inl x ≡ p → inl x₀ ≡ p → Type ℓ
    leftCode' x r' = leftCodeExtended q₀₀ x r'

    leftCode : (x : X) → inl x₀ ≡ inl x → Type ℓ
    leftCode x = leftCode' x refl

    fiberPath : {x : X}{y : Y} → (q : Q x y) → leftCode' x (push q) ≡ rightCode y
    fiberPath q i r = ua (left≃rightCodeExtended q₀₀ q r) i

    pushCode :
        {x : X}{y : Y} → (q : Q x y)
      → PathP (λ i → inl x₀ ≡ push q i → Type ℓ) (leftCode x) (rightCode y)
    pushCode q i =
      hcomp (λ j → λ { (i = i0) → leftCode _
                     ; (i = i1) → fiberPath q j })
            (leftCode' _ (λ j → push q (i ∧ j)))

    Code : (p : Pushout) → inl x₀ ≡ p → Type ℓ
    Code (inl x) = leftCode  x
    Code (inr y) = rightCode y
    Code (push q i) = pushCode q i

    {- Transportation rule of pushCode -}

    transpLeftCode : (y : Y) → (q : Q x₀ y) → (q' : leftCodeExtended q₀₀ _ refl refl) → leftCode' _ (push q) (push q)
    transpLeftCode y q q' =
      transport (λ i → leftCode' _ (λ j → push q (i ∧ j)) (λ j → push q (i ∧ j))) q'

    transpPushCodeβ' :
        (y : Y) → (q : Q x₀ y) → (q' : leftCodeExtended q₀₀ _ refl refl)
      → transport (λ i → pushCode q i (λ j → push q (i ∧ j))) q' ≡ left→rightCodeExtended _ _ _ (transpLeftCode y q q')
    transpPushCodeβ' y q q' i = transportRefl (left→rightCodeExtended _ _ _ (transpLeftCode y q (transportRefl q' i))) i

    module _
      {p : Pushout}(r : inl x₀ ≡ p) where

      fiber-filler : I → Type ℓ
      fiber-filler i = fiber' q₀₀ (λ j → r (i ∧ j)) (λ j → r (i ∧ j))

      module _
        (q : fiberSquare q₀₀ q₀₀ refl refl) where

        transpLeftCode-filler : (i j k : I) → Pushout
        transpLeftCode-filler i j k' =
          hfill (λ k → λ { (i = i0) → push q₀₀ (~ j)
                         ; (i = i1) → r (j ∧ k)
                         ; (j = i0) → push q₀₀ (~ i)
                         ; (j = i1) → r (i ∧ k) })
                (inS (q i j)) k'

    transpLeftCodeβ' :
        {p : Pushout} → (r : inl x₀ ≡ p) → (q : fiberSquare q₀₀ q₀₀ refl refl)
      → transport (λ i → fiber-filler r i) (q₀₀ , q) ≡ (q₀₀ , λ i j → transpLeftCode-filler r q i j i1)
    transpLeftCodeβ' r q =
      J (λ p r → transport (λ i → fiber-filler r i) (q₀₀ , q) ≡ (q₀₀ , λ i j → transpLeftCode-filler r q i j i1))
        (transportRefl _ ∙ (λ k → (q₀₀ , λ i j → transpLeftCode-filler refl q i j k))) r

    transpLeftCodeβ :
        (y : Y) → (q : Q x₀ y) → (q' : fiberSquare q₀₀ q₀₀ refl refl)
      → transpLeftCode y q ∣ q₀₀ , q' ∣ₕ ≡ ∣ q₀₀ , (λ i j → transpLeftCode-filler (push q) q' i j i1) ∣ₕ
    transpLeftCodeβ y q q' = transportTrunc _ ∙ (λ i → ∣ transpLeftCodeβ' _ q' i ∣ₕ)

    transpPushCodeβ :
        (y : Y) → (q : Q x₀ y) → (q' : fiberSquare q₀₀ q₀₀ refl refl)
      →   transport (λ i → pushCode q i (λ j → push q (i ∧ j))) ∣ q₀₀ , q' ∣ₕ
        ≡ ∣fiber→[q₀₀=q₁₀]∣ q₀₀ q (push q) (λ i j → transpLeftCode-filler (push q) q' i j i1)
    transpPushCodeβ y q q' =
        transpPushCodeβ' _ _ _
      ∙ (λ i → left→rightCodeExtended _ _ _ (transpLeftCodeβ _ _ q' i))
      ∙ recUniq {n = m + n} _ _ _
      ∙ (λ i' → Fiber→.left q₀₀ (_ , q) i' (push q) (λ i j → transpLeftCode-filler (push q) q' i j i1))

    {- The contractibility of Code -}

    centerCode : {p : Pushout} → (r : inl x₀ ≡ p) → Code p r
    centerCode r =
      transport (λ i → Code _ (λ j → r (i ∧ j))) ∣ q₀₀ , (λ i j → push q₀₀ (~ i ∧ ~ j)) ∣ₕ

    module _
      (y : Y)(q : Q x₀ y) where

      transp-filler : (i j k : I) → Pushout
      transp-filler = transpLeftCode-filler (push q) (λ i' j' → push q₀₀ (~ i' ∧ ~ j'))

      transp-square : fiberSquare q₀₀ q₀₀ (push q) (push q)
      transp-square i j = transp-filler i j i1

      contractionCodeRefl' :
        fiber→[q₀₀=q₁₀] q₀₀ q (push q) transp-square .snd ≡ refl
      contractionCodeRefl' i j k =
        hcomp (λ l → λ { (i = i0) → fiber→[q₀₀=q₁₀]-filler q₀₀ q (push q) transp-square j k l
                       ; (i = i1) → transp-square (~ j ∨ l) k
                       ; (j = i0) → push q (k ∧ (i ∨ l))
                       ; (j = i1) → transp-square l k
                       ; (k = i0) → push q₀₀ (j ∧ ~ l)
                       ; (k = i1) → push q ((i ∧ ~ j) ∨ l) })
              (transp-filler (~ j) k i)

      contractionCodeRefl : centerCode (push q) ≡ ∣ q , refl ∣ₕ
      contractionCodeRefl = transpPushCodeβ _ _ _ ∙ (λ i → ∣ q , contractionCodeRefl' i ∣ₕ)

    module _
      (y : Y)(r : inl x₀ ≡ inr y) where

      contractionCode' : (a : fiber push r) → centerCode r ≡ ∣ a ∣ₕ
      contractionCode' (q , p') = J (λ r' p → centerCode r' ≡ ∣ q , p ∣ₕ) (contractionCodeRefl _ q) p'

      contractionCode : (a : Code _ r) → centerCode r ≡ a
      contractionCode = elim (λ _ → isOfHLevelTruncPath) contractionCode'

      isContrCode : isContr (Code _ r)
      isContrCode = centerCode r , contractionCode

  excision-helper :
      (x : X) → Trunc (1 + m) (Σ[ y₀ ∈ Y ] Q x y₀)
    → (y : Y) → (r : inl x ≡ inr y) → isContr (Trunc (m + n) (fiber push r))
  excision-helper x y' y r = rec (isProp→isOfHLevelSuc m isPropIsContr) (λ (y₀ , q₀₀) → isContrCode x y₀ q₀₀ y r ) y'

  {- The Main Result : Blakers-Massey Homotopy Excision Theorem -}
  Excision : (x : X)(y : Y) → isConnectedFun (m + n) (push {x = x} {y = y})
  Excision x y = excision-helper x (leftConn x .fst) y

max_stars_repo_name: ecavallo/cubical

max_issues_repo_name: ecavallo/cubical

max_forks_repo_name: ecavallo/cubical


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

open import Agda.Primitive

postulate
  _↦_ : ∀{i j}{A : Set i}{B : Set j} → A → B → Set (i ⊔ j)

{-# BUILTIN REWRITE _↦_ #-}  -- currently fails a sanity check

postulate
  resize : ∀{i j} → Set i → Set j
  resize-id : ∀{i} {j} {A : Set i} → resize {i} {j} A ↦ A

{-# REWRITE resize-id #-}

-- Impredicative quantification

Forall : ∀{i} (F : Set i → Set) → Set
Forall {i} F = resize ((X : Set i) → F X)

-- Example: Impredicative encoding of natural numbers

Nat = Forall λ X → (X → X) → X → X

zero : Nat
zero X s z = z

suc : Nat → Nat
suc n X s z = s (n X s z)

-- requires impredicativity:

id : Nat → Nat
id n = n Nat suc zero

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module Data.Num.Increment where

open import Data.Num.Core
open import Data.Num.Bounded
open import Data.Num.Maximum
open import Data.Num.Next

open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.Properties.Simple
open import Data.Nat.Properties.Extra

open import Data.Fin as Fin
    using (Fin; fromℕ≤; inject≤)
    renaming (zero to z; suc to s)

open import Data.Fin.Properties using (toℕ-fromℕ≤; bounded)
open import Data.Product

open import Function
open import Relation.Nullary.Decidable
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

open ≡-Reasoning
open ≤-Reasoning renaming (begin_ to start_; _∎ to _□; _≡⟨_⟩_ to _≈⟨_⟩_)
open DecTotalOrder decTotalOrder using (reflexive) renaming (refl to ≤-refl)

------------------------------------------------------------------------
-- a number is incrementable if there exists some n' : Numeral b d o such that ⟦ n' ⟧ℕ ≡ suc ⟦ n ⟧ℕ

Incrementable : ∀ {b d o} → (xs : Numeral b d o) → Set
Incrementable {b} {d} {o} xs = Σ[ xs' ∈ Numeral b d o ] ⟦ xs' ⟧ ≡ suc ⟦ xs ⟧

m≡1+n⇒m>n : ∀ {m n} → m ≡ suc n → m > n
m≡1+n⇒m>n {zero}  {n}  ()
m≡1+n⇒m>n {suc m} {.m} refl = s≤s ≤-refl

Maximum⇒¬Incrementable : ∀ {b d o}
    → (xs : Numeral b d o)
    → (max : Maximum xs)
    → ¬ (Incrementable xs)
Maximum⇒¬Incrementable xs max (evidence , claim)
    = contradiction (max evidence) (>⇒≰ (m≡1+n⇒m>n claim))

Interval⇒Incrementable : ∀ {b d o}
    → (xs : Numeral (suc b) (suc d) o)
    → (¬greatest : ¬ (Greatest (lsd xs)))
    → (proper : 2 ≤ suc (d + o))
    → Incrementable xs
Interval⇒Incrementable {b} {d} {o} xs ¬greatest proper
    = (next-numeral-Proper xs proper) , (begin
            ⟦ next-numeral-Proper xs proper ⟧
        ≡⟨ cong ⟦_⟧ (next-numeral-Proper-refine xs proper (Interval b d o ¬greatest)) ⟩
            ⟦ next-numeral-Proper-Interval xs ¬greatest proper ⟧
        ≡⟨ next-numeral-Proper-Interval-lemma xs ¬greatest proper ⟩
            suc ⟦ xs ⟧
        ∎)

GappedEndpoint⇒¬Incrementable : ∀ {b d o}
    → (xs : Numeral (suc b) (suc d) o)
    → (greatest : Greatest (lsd xs))
    → (proper : 2 ≤ suc (d + o))
    → (gapped : Gapped xs proper)
    → ¬ (Incrementable xs)
GappedEndpoint⇒¬Incrementable {b} {d} {o} xs greatest proper gapped (incremented , claim)
    = contradiction ⟦next⟧>⟦incremented⟧ ⟦next⟧≯⟦incremented⟧
    where
        next : Numeral (suc b) (suc d) o
        next = next-numeral-Proper xs proper

        ⟦next⟧>⟦incremented⟧ : ⟦ next ⟧ > ⟦ incremented ⟧
        ⟦next⟧>⟦incremented⟧ =
            start
                suc ⟦ incremented ⟧
            ≈⟨ cong suc claim ⟩
                suc (suc ⟦ xs ⟧)
            ≤⟨ next-numeral-Proper-GappedEndpoint-lemma xs greatest proper gapped ⟩
                ⟦ next-numeral-Proper-GappedEndpoint xs proper gapped ⟧
            ≈⟨ cong ⟦_⟧ (sym (next-numeral-Proper-refine xs proper (GappedEndpoint b d o greatest gapped))) ⟩
                ⟦ next-numeral-Proper xs proper ⟧
            □

        ⟦next⟧≯⟦incremented⟧ : ⟦ next ⟧ ≯ ⟦ incremented ⟧
        ⟦next⟧≯⟦incremented⟧ = ≤⇒≯ $ next-numeral-is-immediate-Proper xs incremented proper (m≡1+n⇒m>n claim)

UngappedEndpoint⇒Incrementable : ∀ {b d o}
    → (xs : Numeral (suc b) (suc d) o)
    → (greatest : Greatest (lsd xs))
    → (proper : 2 ≤ suc (d + o))
    → (¬gapped : ¬ (Gapped xs proper))
    → Incrementable xs
UngappedEndpoint⇒Incrementable {b} {d} {o} xs greatest proper ¬gapped
    = (next-numeral-Proper xs proper) , (begin
            ⟦ next-numeral-Proper xs proper ⟧
        ≡⟨ cong ⟦_⟧ (next-numeral-Proper-refine xs proper (UngappedEndpoint b d o greatest ¬gapped)) ⟩
            ⟦ next-numeral-Proper-UngappedEndpoint xs greatest proper ¬gapped ⟧
        ≡⟨ next-numeral-Proper-UngappedEndpoint-lemma xs greatest proper ¬gapped ⟩
            suc ⟦ xs ⟧
        ∎)

¬Gapped⇒Incrementable : ∀ {b d o}
    → (xs : Numeral (suc b) (suc d) o)
    → (proper : 2 ≤ suc (d + o))
    → (¬gapped : ¬ (Gapped xs proper))
    → Incrementable xs
¬Gapped⇒Incrementable xs proper ¬gapped with nextView xs proper
¬Gapped⇒Incrementable xs proper ¬gapped | Interval b d o ¬greatest
    = Interval⇒Incrementable xs ¬greatest proper
¬Gapped⇒Incrementable xs proper ¬gapped | GappedEndpoint b d o greatest gapped
    = contradiction gapped ¬gapped
¬Gapped⇒Incrementable xs proper ¬gapped | UngappedEndpoint b d o greatest _
    = UngappedEndpoint⇒Incrementable xs greatest proper ¬gapped

Incrementable?-Proper : ∀ {b d o}
    → (xs : Numeral (suc b) (suc d) o)
    → (proper : 2 ≤ suc (d + o))
    → Dec (Incrementable xs)
Incrementable?-Proper xs proper with nextView xs proper
Incrementable?-Proper xs proper | Interval b d o ¬greatest
    = yes (Interval⇒Incrementable xs ¬greatest proper)
Incrementable?-Proper xs proper | GappedEndpoint b d o greatest gapped
    = no (GappedEndpoint⇒¬Incrementable xs greatest proper gapped)
Incrementable?-Proper xs proper | UngappedEndpoint b d o greatest ¬gapped
    = yes (UngappedEndpoint⇒Incrementable xs greatest proper ¬gapped)

Incrementable? : ∀ {b d o}
    → (xs : Numeral b d o)
    → Dec (Incrementable xs)
Incrementable? xs with Maximum? xs
Incrementable? xs | yes max = no (Maximum⇒¬Incrementable xs max)
Incrementable? {b} {d} {o} xs | no ¬max with numView b d o
Incrementable? xs | no ¬max | NullBase d o
    = yes ((next-numeral-NullBase xs ¬max) , (next-numeral-NullBase-lemma xs ¬max))
Incrementable? xs | no ¬max | NoDigits b o
    = yes (NoDigits-explode xs)
Incrementable? xs | no ¬max | AllZeros b
    = no (contradiction (Maximum-AllZeros xs) ¬max)
Incrementable? xs | no ¬max | Proper b d o proper
    = Incrementable?-Proper xs proper

increment : ∀ {b d o}
    → (xs : Numeral b d o)
    → (incr : True (Incrementable? xs))
    → Numeral b d o
increment xs incr = proj₁ $ toWitness incr

increment-next-numeral-Proper : ∀ {b d o}
    → (xs : Numeral (suc b) (suc d) o)
    → (proper : 2 ≤ suc (d + o))
    → (incr : True (Incrementable?-Proper xs proper))
    → proj₁ (toWitness incr) ≡ next-numeral-Proper xs proper
increment-next-numeral-Proper xs proper incr with nextView xs proper
increment-next-numeral-Proper xs proper incr | Interval b d o ¬greatest = begin
        next-numeral-Proper xs proper
    ≡⟨ next-numeral-Proper-refine xs proper (Interval b d o ¬greatest) ⟩
        next-numeral-Proper-Interval xs ¬greatest proper
    ∎
increment-next-numeral-Proper xs proper ()   | GappedEndpoint b d o greatest gapped
increment-next-numeral-Proper xs proper incr | UngappedEndpoint b d o greatest ¬gapped = begin
        next-numeral-Proper xs proper
    ≡⟨ next-numeral-Proper-refine xs proper (UngappedEndpoint b d o greatest ¬gapped) ⟩
        next-numeral-Proper-UngappedEndpoint xs greatest proper ¬gapped
    ∎

increment-next-numeral : ∀ {b d o}
    → (xs : Numeral b d o)
    → (¬max : ¬ (Maximum xs))
    → (incr : True (Incrementable? xs))
    → increment xs incr ≡ next-numeral xs ¬max
increment-next-numeral xs ¬max incr with Maximum? xs
increment-next-numeral xs ¬max () | yes max
increment-next-numeral {b} {d} {o} xs ¬max incr | no _  with numView b d o
increment-next-numeral xs _ incr | no ¬max | NullBase d o = refl
increment-next-numeral xs _ incr | no ¬max | NoDigits b o = NoDigits-explode xs
increment-next-numeral xs _ ()   | no ¬max | AllZeros b
increment-next-numeral xs _ incr | no ¬max | Proper b d o proper
    = increment-next-numeral-Proper xs proper incr

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral