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

--open import HoTT
open import homotopy.3x3.PushoutPushout
open import homotopy.3x3.Transpose
import homotopy.3x3.To as To
import homotopy.3x3.From as From
open import homotopy.3x3.Common

module homotopy.3x3.ToFrom3 {i} (d : Span^2 {i}) where

open Span^2 d
open M d hiding (Pushout^2)
open M (transpose d) using () renaming (A₀∙ to A∙₀; A₂∙ to A∙₂; A₄∙ to A∙₄;
                                        module F₁∙ to F∙₁; f₁∙ to f∙₁;
                                        module F₃∙ to F∙₃; f₃∙ to f∙₃;
                                        v-h-span to h-v-span)
open M using (Pushout^2)

open To d
open From d

open import homotopy.3x3.ToFromInit d
open import homotopy.3x3.ToFrom2 d

module M3 (c : A₂₂) where

  open M2 c

  lemma2-3 =
    ap□ to (E∙₂Red.coh! c (↓-='-out (apd (glue {d = v-h-span}) (glue c))
                            ∙□-i/ E∙₂Red.lhs-i c / E∙₂Red.rhs-i c /)
              ∙□-i/ E∙₂Red.lhs-o c / E∙₂Red.rhs-o c /)

         =⟨ ap□-∙□-i/ to _ (E∙₂Red.lhs-o c) (E∙₂Red.rhs-o c) ⟩

    ap□ to (E∙₂Red.coh! c (↓-='-out (apd (glue {d = v-h-span}) (glue c))
                            ∙□-i/ E∙₂Red.lhs-i c / E∙₂Red.rhs-i c /))
    ∙□-i/ ap (ap to) (E∙₂Red.lhs-o c) / ap (ap to) (E∙₂Red.rhs-o c) /

         =⟨ lemma2-4 |in-ctx (λ u → u ∙□-i/ ap (ap to) (E∙₂Red.lhs-o c) / ap (ap to) (E∙₂Red.rhs-o c) /) ⟩

    ↓-='-out (apd (glue {d = h-v-span}) (glue c))
    ∙□-i/ E₂∙Red.lhs-i c / E₂∙Red.rhs-i c /
    ∙□-o/ ∘-ap to left (glue (f₁₂ c)) ∙ I₀∙.glue-β (f₁₂ c) / ! (∘-ap to right (glue (f₃₂ c)) ∙ I₄∙.glue-β (f₃₂ c)) /
    ∙□-i/ (To.glue-β (right (f₂₃ c))) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ! (ap (right ∘ right) (H₃₃ c)))
        / (! (To.glue-β (left (f₂₁ c)))) |in-ctx (λ u → ! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (left ∘ right) (H₃₁ c)) /
    ∙□-i/ E∙₂Red.ap-ap-coh!-lhs-o c to / E∙₂Red.ap-ap-coh!-rhs-o c to /
    ∙□-i/ ap (ap to) (E∙₂Red.lhs-o c) / ap (ap to) (E∙₂Red.rhs-o c) / ∎

  lemma2'-3 =
    ap-∘ to (i∙₄ ∘ f∙₃) (glue c)
    ∙ ap (ap to) (E∙₂Red.lhs-o c)
    ∙ E∙₂Red.ap-ap-coh!-lhs-o c to
    ∙ ((To.glue-β (right (f₂₃ c))) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ! (ap (right ∘ right) (H₃₃ c))))
    ∙ E₂∙Red.lhs-i c

      =⟨ coh2 (ap to)
              (ap-∘ to (i∙₄ ∘ f∙₃) (glue c))
              (ap-∘ i∙₄ f∙₃ (glue c))
              _
              _
              _
              (ap-∙∙!'`∘`∘ to (left ∘ right) (right ∘ right) (H₁₃ c) (glue (right (f₂₃ c))) (H₃₃ c))
              ((To.glue-β (right (f₂₃ c))) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ! (ap (right ∘ right) (H₃₃ c))))
              (! (ap-∙∙!`∘`∘ right left right (H₁₃ c) (glue (f₂₃ c)) (H₃₃ c)))
              (ap-! (ap right) (F∙₃.glue-β c))
              _
              ⟩

    (ap-∘ to (i∙₄ ∘ f∙₃) (glue c)
     ∙ ap (ap to) (ap-∘ i∙₄ f∙₃ (glue c))
     ∙ ap (ap to) (F∙₃.glue-β c |in-ctx (ap i∙₄)))
    ∙ (ap (ap to) (ap-∙∙!`∘`∘ i∙₄ left right (H₁₃ c) (glue (f₂₃ c)) (H₃₃ c))
       ∙ ap (ap to) (I∙₄.glue-β (f₂₃ c) |in-ctx (λ u → ap (left ∘ right) (H₁₃ c) ∙ u ∙ ! (ap (right ∘ right) (H₃₃ c))))
       ∙ ap-∙∙!'`∘`∘ to (left ∘ right) (right ∘ right) (H₁₃ c) (glue (right (f₂₃ c))) (H₃₃ c))
    ∙ (((To.glue-β (right (f₂₃ c))) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ! (ap (right ∘ right) (H₃₃ c))))
       ∙ ! (ap-∙∙!`∘`∘ right left right (H₁₃ c) (glue (f₂₃ c)) (H₃₃ c))
       ∙ ! (ap (ap right) (F∙₃.glue-β c))
       ∙ ∘-ap right f∙₃ (glue c))

      =⟨ ap-∘-ap-∙∙!'2`∘`∘-coh to i∙₄ left right (H₁₃ c) (I∙₄.glue-β (f₂₃ c)) (H₃₃ c)
         |in-ctx (λ u → (ap-∘ to (i∙₄ ∘ f∙₃) (glue c)
                         ∙ ap (ap to) (ap-∘ i∙₄ f∙₃ (glue c))
                         ∙ ap (ap to) (F∙₃.glue-β c |in-ctx (ap i∙₄)))
                        ∙ u
                        ∙ (((To.glue-β (right (f₂₃ c))) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ! (ap (right ∘ right) (H₃₃ c))))
                           ∙ ! (ap-∙∙!`∘`∘ right left right (H₁₃ c) (glue (f₂₃ c)) (H₃₃ c))
                           ∙ ! (ap (ap right) (F∙₃.glue-β c))
                           ∙ ∘-ap right f∙₃ (glue c))) ⟩

    (ap-∘ to (i∙₄ ∘ f∙₃) (glue c)
     ∙ ap (ap to) (ap-∘ i∙₄ f∙₃ (glue c))
     ∙ ap (ap to) (F∙₃.glue-β c |in-ctx (ap i∙₄)))
    ∙ (ap (ap to) (ap-∙∙`∘`∘ i∙₄ left right (H₁₃ c) (glue (f₂₃ c)) (! (H₃₃ c)))
       ∙ ap (ap to) (I∙₄.glue-β (f₂₃ c) |in-ctx (λ u → ap (left ∘ right) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c))))
       ∙ ap-∙∙!`∘`∘ to (left ∘ right) (right ∘ right) (H₁₃ c) (glue (right (f₂₃ c))) (H₃₃ c))
    ∙ (((To.glue-β (right (f₂₃ c))) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ! (ap (right ∘ right) (H₃₃ c))))
       ∙ ! (ap-∙∙!`∘`∘ right left right (H₁₃ c) (glue (f₂₃ c)) (H₃₃ c))
       ∙ ! (ap (ap right) (F∙₃.glue-β c))
       ∙ ∘-ap right f∙₃ (glue c))

      =⟨ coh5 (ap-∘ to (i∙₄ ∘ f∙₃) (glue c)
                ∙ ap (ap to) (ap-∘ i∙₄ f∙₃ (glue c))
                ∙ ap (ap to) (F∙₃.glue-β c |in-ctx (ap i∙₄)))
               (ap (ap to) (ap-∙∙`∘`∘ i∙₄ left right (H₁₃ c) (glue (f₂₃ c)) (! (H₃₃ c))))
               (ap (ap to) (I∙₄.glue-β (f₂₃ c) |in-ctx (λ u → ap (left ∘ right) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c)))))
               (ap-∙∙!`∘`∘ to (left ∘ right) (right ∘ right) (H₁₃ c) (glue (right (f₂₃ c))) (H₃₃ c))
               ((To.glue-β (right (f₂₃ c))) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ! (ap (right ∘ right) (H₃₃ c))))
               (! (ap-∙∙!`∘`∘ right left right (H₁₃ c) (glue (f₂₃ c)) (H₃₃ c)))
               (! (ap (ap right) (F∙₃.glue-β c)) ∙ ∘-ap right f∙₃ (glue c))

               (ap-∙∙`∘`∘ to (left ∘ right) (right ∘ right) (H₁₃ c) (glue (right (f₂₃ c))) (! (H₃₃ c)))
               ((To.glue-β (right (f₂₃ c))) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c))))
               (! (ap-∙∙`∘`∘ right left right (H₁₃ c) (glue (f₂₃ c)) (! (H₃₃ c))))
               (ap-! (right ∘ right) (H₃₃ c) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ ap right (glue (f₂₃ c)) ∙ u))
               (ap-∙∙!`∘`∘-coh1 to (left ∘ right) (right ∘ right) (H₁₃ c) (To.glue-β (right (f₂₃ c))) (H₃₃ c))
               (ap-∙∙!`∘`∘-coh2 right left right (H₁₃ c) {glue (f₂₃ c)} (H₃₃ c))
          ⟩

    (ap-∘ to (i∙₄ ∘ f∙₃) (glue c)
     ∙ ap (ap to) (ap-∘ i∙₄ f∙₃ (glue c))
     ∙ ap (ap to) (F∙₃.glue-β c |in-ctx (ap i∙₄)))
    ∙ (ap (ap to) (ap-∙∙`∘`∘ i∙₄ left right (H₁₃ c) (glue (f₂₃ c)) (! (H₃₃ c)))
       ∙ ap (ap to) (I∙₄.glue-β (f₂₃ c) |in-ctx (λ u → ap (left ∘ right) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c))))
       ∙ ap-∙∙`∘`∘ to (left ∘ right) (right ∘ right) (H₁₃ c) (glue (right (f₂₃ c))) (! (H₃₃ c)))
    ∙ (((To.glue-β (right (f₂₃ c))) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c))))
       ∙ ! (ap-∙∙`∘`∘ right left right (H₁₃ c) (glue (f₂₃ c)) (! (H₃₃ c)))
       ∙ ! (ap (ap right) (F∙₃.glue-β c))
       ∙ ∘-ap right f∙₃ (glue c))

         =⟨ ap-∘-ap-∙∙`∘`∘-coh to i∙₄ left right (H₁₃ c) (I∙₄.glue-β (f₂₃ c)) (! (H₃₃ c))
            |in-ctx (λ u →
              (ap-∘ to (i∙₄ ∘ f∙₃) (glue c)
               ∙ ap (ap to) (ap-∘ i∙₄ f∙₃ (glue c))
               ∙ ap (ap to) (F∙₃.glue-β c |in-ctx (ap i∙₄)))
              ∙ u
              ∙ (((To.glue-β (right (f₂₃ c))) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c))))
                 ∙ ! (ap-∙∙`∘`∘ right left right (H₁₃ c) (glue (f₂₃ c)) (! (H₃₃ c)))
                 ∙ ! (ap (ap right) (F∙₃.glue-β c))
                 ∙ ∘-ap right f∙₃ (glue c))) ⟩

    (ap-∘ to (i∙₄ ∘ f∙₃) (glue c)
     ∙ ap (ap to) (ap-∘ i∙₄ f∙₃ (glue c))
     ∙ ap (ap to) (F∙₃.glue-β c |in-ctx (ap i∙₄)))
    ∙ (∘-ap to i∙₄ (ap left (H₁₃ c) ∙ glue (f₂₃ c) ∙ ap right (! (H₃₃ c)))
       ∙ ap-∙∙`∘`∘ (to ∘ i∙₄) left right (H₁₃ c) (glue (f₂₃ c)) (! (H₃₃ c))
       ∙ (ap-∘ to i∙₄ (glue (f₂₃ c)) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c))))
       ∙ (ap (ap to) (I∙₄.glue-β (f₂₃ c)) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c)))))
    ∙ (((To.glue-β (right (f₂₃ c))) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c))))
       ∙ (! (ap-∙∙`∘`∘ right left right (H₁₃ c) (glue (f₂₃ c)) (! (H₃₃ c))))
       ∙ ! (ap (ap right) (F∙₃.glue-β c))
       ∙ ∘-ap right f∙₃ (glue c))

         =⟨ coh3 (ap-∘ to (i∙₄ ∘ f∙₃) (glue c))
                 (ap (ap to) (ap-∘ i∙₄ f∙₃ (glue c)))
                 (ap (ap to) (F∙₃.glue-β c |in-ctx (ap i∙₄)))
                 (∘-ap to i∙₄ (ap left (H₁₃ c) ∙ glue (f₂₃ c) ∙ ap right (! (H₃₃ c))))
                 _
                 _ ⟩

    (ap-∘ to (i∙₄ ∘ f∙₃) (glue c)
     ∙ ap (ap to) (ap-∘ i∙₄ f∙₃ (glue c))
     ∙ ap (ap to) (F∙₃.glue-β c |in-ctx (ap i∙₄))
     ∙ ∘-ap to i∙₄ (ap left (H₁₃ c) ∙ glue (f₂₃ c) ∙ ap right (! (H₃₃ c))))
    ∙ (ap-∙∙`∘`∘ (to ∘ i∙₄) left right (H₁₃ c) (glue (f₂₃ c)) (! (H₃₃ c))
       ∙ (ap-∘ to i∙₄ (glue (f₂₃ c)) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c))))
       ∙ (ap (ap to) (I∙₄.glue-β (f₂₃ c)) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c)))))
    ∙ ((To.glue-β (right (f₂₃ c)) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c))))
       ∙ ! (ap-∙∙`∘`∘ right left right (H₁₃ c) (glue (f₂₃ c)) (! (H₃₃ c)))
       ∙ ! (ap (ap right) (F∙₃.glue-β c))
       ∙ ∘-ap right f∙₃ (glue c))

         =⟨ ap-∘-coh to i∙₄ f∙₃ (glue c) (F∙₃.glue-β c)
           |in-ctx (λ u → u ∙ (ap-∙∙`∘`∘ (to ∘ i∙₄) left right (H₁₃ c) (glue (f₂₃ c)) (! (H₃₃ c))
                               ∙ (ap-∘ to i∙₄ (glue (f₂₃ c)) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c))))
                               ∙ (ap (ap to) (I∙₄.glue-β (f₂₃ c)) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c)))))
                            ∙ ((To.glue-β (right (f₂₃ c)) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c))))
                               ∙ ! (ap-∙∙`∘`∘ right left right (H₁₃ c) (glue (f₂₃ c)) (! (H₃₃ c)))
                               ∙ ! (ap (ap right) (F∙₃.glue-β c))
                               ∙ ∘-ap right f∙₃ (glue c))) ⟩

    (ap-∘ (to ∘ i∙₄) f∙₃ (glue c)
     ∙ (ap (ap (to ∘ i∙₄)) (F∙₃.glue-β c)))
    ∙ (ap-∙∙`∘`∘ (to ∘ i∙₄) left right (H₁₃ c) (glue (f₂₃ c)) (! (H₃₃ c))
       ∙ (ap-∘ to i∙₄ (glue (f₂₃ c)) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c))))
       ∙ (ap (ap to) (I∙₄.glue-β (f₂₃ c)) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c)))))
    ∙ ((To.glue-β (right (f₂₃ c)) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c))))
       ∙ ! (ap-∙∙`∘`∘ right left right (H₁₃ c) (glue (f₂₃ c)) (! (H₃₃ c)))
       ∙ ! (ap (ap right) (F∙₃.glue-β c))
       ∙ ∘-ap right f∙₃ (glue c))

      =⟨ !-ap-∘-inv right f∙₃ (glue c)
          |in-ctx (λ u → (ap-∘ (to ∘ i∙₄) f∙₃ (glue c)
     ∙ (ap (ap (to ∘ i∙₄)) (F∙₃.glue-β c)))
    ∙ (ap-∙∙`∘`∘ (to ∘ i∙₄) left right (H₁₃ c) (glue (f₂₃ c)) (! (H₃₃ c))
       ∙ (ap-∘ to i∙₄ (glue (f₂₃ c)) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c))))
       ∙ (ap (ap to) (I∙₄.glue-β (f₂₃ c)) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c)))))
    ∙ ((To.glue-β (right (f₂₃ c)) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c))))
       ∙ ! (ap-∙∙`∘`∘ right left right (H₁₃ c) (glue (f₂₃ c)) (! (H₃₃ c)))
       ∙ ! (ap (ap right) (F∙₃.glue-β c))
       ∙ u)) ⟩

    (ap-∘ (to ∘ i∙₄) f∙₃ (glue c)
     ∙ (ap (ap (to ∘ i∙₄)) (F∙₃.glue-β c)))
    ∙ (ap-∙∙`∘`∘ (to ∘ i∙₄) left right (H₁₃ c) (glue (f₂₃ c)) (! (H₃₃ c))
       ∙ (ap-∘ to i∙₄ (glue (f₂₃ c)) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c))))
       ∙ (ap (ap to) (I∙₄.glue-β (f₂₃ c)) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c)))))
    ∙ ((To.glue-β (right (f₂₃ c)) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c))))
       ∙ ! (ap-∙∙`∘`∘ right left right (H₁₃ c) (glue (f₂₃ c)) (! (H₃₃ c)))
       ∙ ! (ap (ap right) (F∙₃.glue-β c))
       ∙ ! (ap-∘ right f∙₃ (glue c)))

      =⟨ !-∘-ap-inv (to ∘ i∙₄) f∙₃ (glue c)
         |in-ctx (λ u → (u
     ∙ (ap (ap (to ∘ i∙₄)) (F∙₃.glue-β c)))
    ∙ (ap-∙∙`∘`∘ (to ∘ i∙₄) left right (H₁₃ c) (glue (f₂₃ c)) (! (H₃₃ c))
       ∙ (ap-∘ to i∙₄ (glue (f₂₃ c)) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c))))
       ∙ (ap (ap to) (I∙₄.glue-β (f₂₃ c)) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c)))))
    ∙ ((To.glue-β (right (f₂₃ c)) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c))))
       ∙ ! (ap-∙∙`∘`∘ right left right (H₁₃ c) (glue (f₂₃ c)) (! (H₃₃ c)))
       ∙ ! (ap (ap right) (F∙₃.glue-β c))
       ∙ ! (ap-∘ right f∙₃ (glue c)))) ⟩

    (! (∘-ap (to ∘ i∙₄) f∙₃ (glue c))
     ∙ (ap (ap (to ∘ i∙₄)) (F∙₃.glue-β c)))
    ∙ (ap-∙∙`∘`∘ (to ∘ i∙₄) left right (H₁₃ c) (glue (f₂₃ c)) (! (H₃₃ c))
       ∙ (ap-∘ to i∙₄ (glue (f₂₃ c)) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c))))
       ∙ (ap (ap to) (I∙₄.glue-β (f₂₃ c)) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c)))))
    ∙ ((To.glue-β (right (f₂₃ c)) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c))))
       ∙ ! (ap-∙∙`∘`∘ right left right (H₁₃ c) (glue (f₂₃ c)) (! (H₃₃ c)))
       ∙ ! (ap (ap right) (F∙₃.glue-β c))
       ∙ ! (ap-∘ right f∙₃ (glue c)))

      =⟨ coh4 (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c)))
               (∘-ap (to ∘ i∙₄) f∙₃ (glue c)) _ _ _ _ _ _ _ _ ⟩

    ! end-lemma1 ∎  where

      coh2 : ∀ {i j} {A : Type i} {B : Type j} (f : A → B) {a b c d e : A} {g h k l m n : B}
        (p : g == f a) (q : a == b) (r : b == c) (s : c == d) (t : d == e) (u : f e == h) (v : h == k)
        (w : k == l) {x x' : l == m} (eq-x : x == x') (y : m == n)
        → p ∙ ap f (_ =⟨ q ⟩ _ =⟨ r ⟩ _ =⟨ s ⟩ _ =⟨ t ⟩ _ ∎) ∙ u ∙ v ∙ (_ =⟨ w ⟩ _ =⟨ x ⟩ _ =⟨ y ⟩ _ ∎)
          == (p ∙ ap f q ∙ ap f r) ∙ (ap f s ∙ ap f t ∙ u) ∙ (v ∙ w ∙ x' ∙ y)
      coh2 f p idp idp idp idp idp idp idp {x = idp} idp idp = ! (∙-unit-r (p ∙ idp))

      coh3 : ∀ {i} {A : Type i} {a b c d e f g : A} (p : a == b) (q : b == c) (r : c == d) (s : d == e)
        (t : e == f) (u : f == g)
        → (p ∙ q ∙ r) ∙ (s ∙ t) ∙ u == (p ∙ q ∙ r ∙ s) ∙ t ∙ u
      coh3 idp idp idp idp idp idp = idp

      coh4 : ∀ {i j} {A : Type i} {B : Type j} (h : A → B)
        {a b c d : A} {e f g k l m : B} (p : f == e) (q : f == g) (r : g == h a) (s : a == b) (t : b == c)
        (u : c == d) (v : k == h d) (w : l == k) (x : m == l)
        → (! p ∙ q) ∙ (r ∙ (s |in-ctx h) ∙ (t |in-ctx h)) ∙ ((u |in-ctx h) ∙ (! v) ∙ (! w) ∙ ! x)
          == ! (_ =⟨ x ⟩ _ =⟨ w ⟩ _ =⟨ v ⟩ _ =⟨ ! (_ =⟨ s ⟩ _ =⟨ t ⟩ _ =⟨ u ⟩ _ ∎) |in-ctx h ⟩ _ =⟨ ! r ⟩ _ =⟨ ! q ⟩ _ =⟨ p ⟩ _ ∎)
      coh4 h idp idp r idp idp idp v idp idp = ch r v  where

        ch : ∀ {i} {B : Type i} {a b c : B} (r : a == b) (v : c == b)
           → (r ∙ idp) ∙ ! v ∙ idp == ! (_ =⟨ idp ⟩ _ =⟨ idp ⟩ _ =⟨ v ⟩ _ =⟨ idp ⟩ _ =⟨ ! r ⟩ _ ∎)
        ch idp idp = idp

      coh5 : ∀ {i} {A : Type i} {a b c d e e' f f' g h : A} (p : a == b) (q : b == c)
        (r : c == d) (s : d == e) (t : e == f) (u : f == g) (v : g == h) (s' : d == e')
        (t' : e' == f') (u' : f' == g) (w : f' == f) (α : s ∙ t == s' ∙ t' ∙ w) (β : w ∙ u == u')
        → p ∙ (q ∙ r ∙ s) ∙ (t ∙ u ∙ v)
          == p ∙ (q ∙ r ∙ s') ∙ (t' ∙ u' ∙ v)
      coh5 idp idp idp idp idp idp idp idp idp ._ ._ idp idp = idp

  lemma2'-4 =
    E₂∙Red.rhs-i c
    ∙ ((! (To.glue-β (left (f₂₁ c)))) |in-ctx (λ u → ! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (left ∘ right) (H₃₁ c)))
    ∙ E∙₂Red.ap-ap-coh!-rhs-o c to
    ∙ ap (ap to) (E∙₂Red.rhs-o c)
    ∙ ∘-ap to (i∙₀ ∘ f∙₁) (glue c)

      =⟨ coh2 (ap to)
           (ap-∘ left f∙₁ (glue c))
           (F∙₁.glue-β c |in-ctx (ap left))
           (ap-!∙∙`∘`∘ left left right (H₁₁ c) (glue (f₂₁ c)) (H₃₁ c))
           ((! (To.glue-β (left (f₂₁ c)))) |in-ctx (λ u → ! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (left ∘ right) (H₃₁ c)))
           (ap-∘ to (i∙₀ ∘ f∙₁) (glue c))
           (ap-∘ i∙₀ f∙₁ (glue c))
           ((F∙₁.glue-β c) |in-ctx ap i∙₀)
           (ap-!∙∙`∘`∘ i∙₀ left right (H₁₁ c) (glue (f₂₁ c)) (H₃₁ c))
           ((I∙₀.glue-β (f₂₁ c)) |in-ctx (λ u → ! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (right ∘ left) (H₃₁ c)))
           (ap-!'∙∙`∘`∘ to (left ∘ left) (right ∘ left) (H₁₁ c) (glue (left (f₂₁ c))) (H₃₁ c))
           (!-ap (λ u → ! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (right ∘ left) (H₃₁ c)) (I∙₀.glue-β (f₂₁ c)))
           (!-ap (ap i∙₀) (F∙₁.glue-β c))
           (!-ap-∘ i∙₀ f∙₁ (glue c))
           (!-∘-ap to (i∙₀ ∘ f∙₁) (glue c)) ⟩

    ap-∘ left f∙₁ (glue c)
    ∙ (F∙₁.glue-β c |in-ctx (ap left))
    ∙ (ap-!∙∙`∘`∘ left left right (H₁₁ c) (glue (f₂₁ c)) (H₃₁ c))
    ∙ ((! (To.glue-β (left (f₂₁ c)))) |in-ctx (λ u → ! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (left ∘ right) (H₃₁ c)))
    ∙ ! ((ap-∘ to (i∙₀ ∘ f∙₁) (glue c)
          ∙ ap (ap to) (ap-∘ i∙₀ f∙₁ (glue c))
          ∙ ap (ap to) ((F∙₁.glue-β c) |in-ctx (λ u → ap i∙₀ u)))
         ∙ (ap (ap to) (ap-!∙∙`∘`∘ i∙₀ left right (H₁₁ c) (glue (f₂₁ c)) (H₃₁ c))
            ∙ ap (ap to) ((I∙₀.glue-β (f₂₁ c)) |in-ctx (λ u → ! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (right ∘ left) (H₃₁ c)))
            ∙ ap-!'∙∙`∘`∘ to (left ∘ left) (right ∘ left) (H₁₁ c) (glue (left (f₂₁ c))) (H₃₁ c)))

      =⟨ lm |in-ctx (λ u →
    ap-∘ left f∙₁ (glue c)
    ∙ ap (ap left) (F∙₁.glue-β c)
    ∙ ap-!∙∙`∘`∘ left left right (H₁₁ c) (glue (f₂₁ c)) (H₃₁ c)
    ∙ ((! (To.glue-β (left (f₂₁ c)))) |in-ctx (λ u → ! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (left ∘ right) (H₃₁ c)))
    ∙ ! u) ⟩

    ap-∘ left f∙₁ (glue c)
    ∙ (F∙₁.glue-β c |in-ctx (ap left))
    ∙ ap-!∙∙`∘`∘ left left right (H₁₁ c) (glue (f₂₁ c)) (H₃₁ c)
    ∙ ((! (To.glue-β (left (f₂₁ c)))) |in-ctx (λ u → ! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (left ∘ right) (H₃₁ c)))
    ∙ ! ((ap-∘ (to ∘ i∙₀) f∙₁ (glue c)
          ∙ ap (ap (to ∘ i∙₀)) (F∙₁.glue-β c))
         ∙ (ap-∙∙`∘`∘ (to ∘ i∙₀) left right (! (H₁₁ c)) (glue (f₂₁ c)) (H₃₁ c)
            ∙ (ap-∘ to i∙₀ (glue (f₂₁ c)) |in-ctx (λ u → ap (left ∘ left) (! (H₁₁ c)) ∙ u ∙ ap (left ∘ right) (H₃₁ c)))
            ∙ ((I∙₀.glue-β (f₂₁ c) |in-ctx ap to) |in-ctx (λ u → ap (left ∘ left) (! (H₁₁ c)) ∙ u ∙ ap (left ∘ right) (H₃₁ c)))
            ∙ (ap-! (left ∘ left) (H₁₁ c) |in-ctx (λ u → u ∙ ap to (glue (left (f₂₁ c))) ∙ ap (left ∘ right) (H₃₁ c)))))

      =⟨ coh3 {f = λ u → ap (left ∘ left) (! (H₁₁ c)) ∙ u ∙ ap (left ∘ right) (H₃₁ c)}
              {p = ap-∘ left f∙₁ (glue c)}
              {ap (ap left) (F∙₁.glue-β c)}
              {ap-∙∙`∘`∘ left left right (! (H₁₁ c)) (glue (f₂₁ c)) (H₃₁ c)}
              {ap-∘ to i∙₀ (glue (f₂₁ c))}
              {I∙₀.glue-β (f₂₁ c) |in-ctx ap to}
              {To.glue-β (left (f₂₁ c))}
              {ap-∙∙`∘`∘ (to ∘ i∙₀) left right (! (H₁₁ c)) (glue (f₂₁ c)) (H₃₁ c)}
              {ap (ap (to ∘ i∙₀)) (F∙₁.glue-β c)}
              {ap-∘ (to ∘ i∙₀) f∙₁ (glue c)}
              (!-ap-∘ (to ∘ i∙₀) f∙₁ (glue c))
              {ap-!∙∙`∘`∘ left left right (H₁₁ c) (glue (f₂₁ c)) (H₃₁ c)}
              {(! (To.glue-β (left (f₂₁ c)))) |in-ctx (λ u → ! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (left ∘ right) (H₃₁ c))}
              {ap-! (left ∘ left) (H₁₁ c) |in-ctx (λ u → u ∙ ap to (glue (left (f₂₁ c))) ∙ ap (left ∘ right) (H₃₁ c))}
              (ap-!∙∙`∘`∘-coh left left right (H₁₁ c) (! (To.glue-β (left (f₂₁ c)))) (H₃₁ c)) ⟩

    end-lemma3 ∎  where

      coh2 : ∀ {i j} {A : Type i} {B : Type j} (f : A → B) {a b c d e o : B} (p : a == b) (q : b == c) (r : c == d) (s : d == e)
        {g h l m n : A} (y : o == f g) (x : g == h) (w : h == l) (v : l == m) (u : m == n) (t : f n == e)
        {u' : n == m} (γ : ! u == u') {w' : l == h} (δ : ! w == w') {x' : h == g} (α : ! x == x') {y' : f g == o} (β : ! y' == y)
        →
        (_ =⟨ p ⟩ _ =⟨ q ⟩ _ =⟨ r ⟩ _ ∎) ∙ s ∙ ! t ∙ ap f (_ =⟨ u' ⟩ _ =⟨ ! v ⟩ _ =⟨ w' ⟩ _ =⟨ x' ⟩ _ ∎) ∙ y'
        == p ∙ q ∙ r ∙ s ∙ ! ((y ∙ ap f x ∙ ap f w) ∙ (ap f v ∙ ap f u ∙ t))
      coh2 f idp idp idp idp .idp idp idp idp idp idp idp idp idp {y' = idp} idp = idp

      coh3 : ∀ {i j} {A : Type i} {B : Type j} {f : A → B} {a b c d e g o o' : B} {h k l m : A}
        {p : a == b} {q : b == c} {r : c == f m} {v : h == k} {w : k == l} {x : l == m}
        {s : d == f h} {t : e == d} {u : g == e} {u' : e == g} (α : ! u == u')
        {r' : c == o} {x' : o == o'} {y : f l == o'}
        (β : (r' ∙ x' ∙ ! y) == (r ∙' (! x |in-ctx f)))
        →
        p ∙ q ∙ r' ∙ x' ∙ ! ((u ∙ t) ∙ (s ∙ (v |in-ctx f) ∙ (w |in-ctx f) ∙ y))
        ==
        (_ =⟨ p ⟩ _ =⟨ q ⟩ _ =⟨ r ⟩ _ =⟨ ! (_ =⟨ v ⟩ _ =⟨ w ⟩ _ =⟨ x ⟩ _ ∎) |in-ctx f ⟩
         _ =⟨ ! s ⟩ _ =⟨ ! t ⟩ _ =⟨ u' ⟩ _ ∎)
      coh3 {p = idp} {idp} {._} {idp} {idp} {idp} {s} {idp} {idp} idp {idp} {idp} {y} idp = coh' s y  where

        coh' : ∀ {i} {B : Type i} {a b c : B} (s : a == b) (y : b == c)
          → ! (s ∙ y) == (_ =⟨ idp ⟩ _ =⟨ idp ⟩ _ =⟨ ! y ⟩ _ =⟨ idp ⟩ _ =⟨ ! s ⟩ _ ∎)
        coh' idp idp = idp

      lm =
        (ap-∘ to (i∙₀ ∘ f∙₁) (glue c)
         ∙ ap (ap to) (ap-∘ i∙₀ f∙₁ (glue c))
         ∙ ap (ap to) ((F∙₁.glue-β c) |in-ctx (λ u → ap i∙₀ u)))
        ∙ (ap (ap to) (ap-!∙∙`∘`∘ i∙₀ left right (H₁₁ c) (glue (f₂₁ c)) (H₃₁ c))
           ∙ ap (ap to) ((I∙₀.glue-β (f₂₁ c)) |in-ctx (λ u → ! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (right ∘ left) (H₃₁ c)))
           ∙ ap-!'∙∙`∘`∘ to (left ∘ left) (right ∘ left) (H₁₁ c) (glue (left (f₂₁ c))) (H₃₁ c))

          =⟨ ap-∘-coh2 to i∙₀ f∙₁ (glue c) (F∙₁.glue-β c) |in-ctx (λ u → u ∙ (ap (ap to) (ap-!∙∙`∘`∘ i∙₀ left right (H₁₁ c) (glue (f₂₁ c)) (H₃₁ c))
           ∙ ap (ap to) ((I∙₀.glue-β (f₂₁ c)) |in-ctx (λ u → ! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (right ∘ left) (H₃₁ c)))
           ∙ ap-!'∙∙`∘`∘ to (left ∘ left) (right ∘ left) (H₁₁ c) (glue (left (f₂₁ c))) (H₃₁ c))) ⟩

        (ap-∘ (to ∘ i∙₀) f∙₁ (glue c)
         ∙ ap (ap (to ∘ i∙₀)) (F∙₁.glue-β c)
         ∙ ap-∘ to i∙₀ (ap left (! (H₁₁ c)) ∙ glue (f₂₁ c) ∙ ap right (H₃₁ c)))
        ∙ (ap (ap to) (ap-!∙∙`∘`∘ i∙₀ left right (H₁₁ c) (glue (f₂₁ c)) (H₃₁ c))
           ∙ ap (ap to) ((I∙₀.glue-β (f₂₁ c)) |in-ctx (λ u → ! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (right ∘ left) (H₃₁ c)))
           ∙ ap-!'∙∙`∘`∘ to (left ∘ left) (right ∘ left) (H₁₁ c) (glue (left (f₂₁ c))) (H₃₁ c))

          =⟨ assoc (ap-∘ (to ∘ i∙₀) f∙₁ (glue c))
                   (ap (ap (to ∘ i∙₀)) (F∙₁.glue-β c))
                   (ap-∘ to i∙₀ (ap left (! (H₁₁ c)) ∙ glue (f₂₁ c) ∙ ap right (H₃₁ c)))
                   (ap (ap to) (ap-!∙∙`∘`∘ i∙₀ left right (H₁₁ c) (glue (f₂₁ c)) (H₃₁ c)))
                   (ap (ap to) ((I∙₀.glue-β (f₂₁ c)) |in-ctx (λ u → ! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (right ∘ left) (H₃₁ c))))
                   (ap-!'∙∙`∘`∘ to (left ∘ left) (right ∘ left) (H₁₁ c) (glue (left (f₂₁ c))) (H₃₁ c)) ⟩

        (ap-∘ (to ∘ i∙₀) f∙₁ (glue c)
         ∙ ap (ap (to ∘ i∙₀)) (F∙₁.glue-β c))
        ∙ (ap-∘ to i∙₀ (ap left (! (H₁₁ c)) ∙ glue (f₂₁ c) ∙ ap right (H₃₁ c))
           ∙ ap (ap to) (ap-!∙∙`∘`∘ i∙₀ left right (H₁₁ c) (glue (f₂₁ c)) (H₃₁ c))
           ∙ ap (ap to) ((I∙₀.glue-β (f₂₁ c)) |in-ctx (λ u → ! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (right ∘ left) (H₃₁ c)))
           ∙ ap-!'∙∙`∘`∘ to (left ∘ left) (right ∘ left) (H₁₁ c) (glue (left (f₂₁ c))) (H₃₁ c))

          =⟨ ap-∘-ap-∙∙5`∘`∘-coh to i∙₀ left right (H₁₁ c) (I∙₀.glue-β (f₂₁ c)) (H₃₁ c) |in-ctx (λ u → (ap-∘ (to ∘ i∙₀) f∙₁ (glue c) ∙ ap (ap (to ∘ i∙₀)) (F∙₁.glue-β c)) ∙ u) ⟩

        (ap-∘ (to ∘ i∙₀) f∙₁ (glue c)
         ∙ ap (ap (to ∘ i∙₀)) (F∙₁.glue-β c))
        ∙ (ap-∙∙`∘`∘ (to ∘ i∙₀) left right (! (H₁₁ c)) (glue (f₂₁ c)) (H₃₁ c)
          ∙ (ap-∘ to i∙₀ (glue (f₂₁ c)) |in-ctx (λ u → ap (left ∘ left) (! (H₁₁ c)) ∙ u ∙ ap (left ∘ right) (H₃₁ c)))
          ∙ ((I∙₀.glue-β (f₂₁ c) |in-ctx ap to) |in-ctx (λ u → ap (left ∘ left) (! (H₁₁ c)) ∙ u ∙ ap (left ∘ right) (H₃₁ c)))
          ∙ (ap-! (left ∘ left) (H₁₁ c) |in-ctx (λ u → u ∙ ap to (glue (left (f₂₁ c))) ∙ ap (left ∘ right) (H₃₁ c)))) ∎ where

          assoc : ∀ {i} {A : Type i} {a b c d e f g : A} (p : a == b) (q : b == c) (r : c == d) (s : d == e) (t : e == f) (u : f == g)
            → (p ∙ q ∙ r) ∙ (s ∙ t ∙ u) == (p ∙ q) ∙ (r ∙ s ∙ t ∙ u)
          assoc idp idp idp idp idp idp = idp

  lemma2-2' =
    ap□ to (E∙₂Red.coh! c (↓-='-out (apd (glue {d = v-h-span}) (glue c))
                            ∙□-i/ E∙₂Red.lhs-i c / E∙₂Red.rhs-i c /)
              ∙□-i/ E∙₂Red.lhs-o c / E∙₂Red.rhs-o c /)
    ∙□-i/ ap-∘ to (i∙₄ ∘ f∙₃) (glue c) / ∘-ap to (i∙₀ ∘ f∙₁) (glue c) /

         =⟨ lemma2-3 |in-ctx (λ u → u ∙□-i/ ap-∘ to (i∙₄ ∘ f∙₃) (glue c) / ∘-ap to (i∙₀ ∘ f∙₁) (glue c) /) ⟩

    ↓-='-out (apd (glue {d = h-v-span}) (glue c))
    ∙□-i/ E₂∙Red.lhs-i c / E₂∙Red.rhs-i c /
    ∙□-o/ ∘-ap to left (glue (f₁₂ c)) ∙ I₀∙.glue-β (f₁₂ c) / ! (∘-ap to right (glue (f₃₂ c)) ∙ I₄∙.glue-β (f₃₂ c)) /
    ∙□-i/ (To.glue-β (right (f₂₃ c))) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ! (ap (right ∘ right) (H₃₃ c)))
        / (! (To.glue-β (left (f₂₁ c)))) |in-ctx (λ u → ! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (left ∘ right) (H₃₁ c)) /
    ∙□-i/ E∙₂Red.ap-ap-coh!-lhs-o c to / E∙₂Red.ap-ap-coh!-rhs-o c to /
    ∙□-i/ ap (ap to) (E∙₂Red.lhs-o c) / ap (ap to) (E∙₂Red.rhs-o c) /
    ∙□-i/ ap-∘ to (i∙₄ ∘ f∙₃) (glue c) / ∘-ap to (i∙₀ ∘ f∙₁) (glue c) /

         =⟨ assoc (↓-='-out (apd (glue {d = h-v-span}) (glue c))) (E₂∙Red.lhs-i c) ((To.glue-β (right (f₂₃ c))) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ! (ap (right ∘ right) (H₃₃ c)))) (E∙₂Red.ap-ap-coh!-lhs-o c to) (ap (ap to) (E∙₂Red.lhs-o c)) (ap-∘ to (i∙₄ ∘ f∙₃) (glue c)) _ _ _ _ _ (∘-ap to left (glue (f₁₂ c)) ∙ I₀∙.glue-β (f₁₂ c)) _ ⟩

    ↓-='-out (apd (glue {d = h-v-span}) (glue c))
    ∙□-o/ ∘-ap to left (glue (f₁₂ c)) ∙ I₀∙.glue-β (f₁₂ c) / ! (∘-ap to right (glue (f₃₂ c)) ∙ I₄∙.glue-β (f₃₂ c)) /
    ∙□-i/ ap-∘ to (i∙₄ ∘ f∙₃) (glue c)
          ∙ ap (ap to) (E∙₂Red.lhs-o c)
          ∙ E∙₂Red.ap-ap-coh!-lhs-o c to
          ∙ ((To.glue-β (right (f₂₃ c))) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ! (ap (right ∘ right) (H₃₃ c))))
          ∙ E₂∙Red.lhs-i c
        / E₂∙Red.rhs-i c
          ∙ ((! (To.glue-β (left (f₂₁ c)))) |in-ctx (λ u → ! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (left ∘ right) (H₃₁ c)))
          ∙ E∙₂Red.ap-ap-coh!-rhs-o c to
          ∙ ap (ap to) (E∙₂Red.rhs-o c)
          ∙ ∘-ap to (i∙₀ ∘ f∙₁) (glue c) /

         =⟨ ∙□-i/-rewrite (↓-='-out (apd (glue {d = h-v-span}) (glue c))
    ∙□-o/ ∘-ap to left (glue (f₁₂ c)) ∙ I₀∙.glue-β (f₁₂ c) / ! (∘-ap to right (glue (f₃₂ c)) ∙ I₄∙.glue-β (f₃₂ c)) /) lemma2'-3 lemma2'-4 ⟩

    ↓-='-out (apd (glue {d = h-v-span}) (glue c))
    ∙□-o/ ∘-ap to left (glue (f₁₂ c)) ∙ I₀∙.glue-β (f₁₂ c) / ! (∘-ap to right (glue (f₃₂ c)) ∙ I₄∙.glue-β (f₃₂ c)) /
    ∙□-i/ ! end-lemma1 / end-lemma3 / ∎  where

      assoc : ∀ {i} {A : Type i} {a b b' c : A} {u u' : a == b} {v v1 v2 v3 v4 v5 : b == c}
         {w w1 w2 w3 w4 w5 : a == b'} {x x' : b' == c} (α : (u , v =□ w , x))
         (p1 : v1 == v) (p2 : v2 == v1) (p3 : v3 == v2) (p4 : v4 == v3) (p5 : v5 == v4)
         (q1 : w == w1) (q2 : w1 == w2) (q3 : w2 == w3) (q4 : w3 == w4) (q5 : w4 == w5)
         (r : u' == u) (s : x == x')
         → α ∙□-i/ p1 / q1 / ∙□-o/ r / s / ∙□-i/ p2 / q2 / ∙□-i/ p3 / q3 / ∙□-i/ p4 / q4 / ∙□-i/ p5 / q5 /
         == α ∙□-o/ r / s / ∙□-i/ p5 ∙ p4 ∙ p3 ∙ p2 ∙ p1 / q1 ∙ q2 ∙ q3 ∙ q4 ∙ q5 /
      assoc α idp idp idp idp idp idp idp idp idp idp idp idp = idp

  lemma2-2 =
    ap↓ (ap to) (↓-='-in (E∙₂Red.coh! c (↓-='-out (apd (glue {d = v-h-span}) (glue c))
                                          ∙□-i/ E∙₂Red.lhs-i c / E∙₂Red.rhs-i c /)
                            ∙□-i/ E∙₂Red.lhs-o c / E∙₂Red.rhs-o c /))

         =⟨ ap↓-↓-='-in-β _ _ to (E∙₂Red.coh! c (↓-='-out (apd (glue {d = v-h-span}) (glue c))
                                                  ∙□-i/ E∙₂Red.lhs-i c / E∙₂Red.rhs-i c /)
                                    ∙□-i/ E∙₂Red.lhs-o c / E∙₂Red.rhs-o c /) ⟩

    ↓-='-in ((ap□ to (E∙₂Red.coh! c (↓-='-out (apd (glue {d = v-h-span}) (glue c))
                                      ∙□-i/ E∙₂Red.lhs-i c / E∙₂Red.rhs-i c /)
                        ∙□-i/ E∙₂Red.lhs-o c / E∙₂Red.rhs-o c /))
             ∙□-i/ ap-∘ to (i∙₄ ∘ f∙₃) (glue c) / ∘-ap to (i∙₀ ∘ f∙₁) (glue c) /)

         =⟨ lemma2-2' |in-ctx ↓-='-in ⟩

    ↓-='-in (↓-='-out (apd (glue {d = h-v-span}) (glue c))
             ∙□-o/ ∘-ap to left (glue (f₁₂ c)) ∙ I₀∙.glue-β (f₁₂ c) / ! (∘-ap to right (glue (f₃₂ c)) ∙ I₄∙.glue-β (f₃₂ c)) /
             ∙□-i/ ! end-lemma1 / end-lemma3 /) ∎

  lemma2-1 =
    apd (ap to ∘ ap from ∘ glue) (glue c)

         =⟨ apd-∘' (ap to ∘ ap from) glue (glue c) ⟩

    ap↓ (ap to ∘ ap from) (apd (glue {d = h-v-span}) (glue c))

         =⟨ ap↓-∘ (ap to) (ap from) (apd glue (glue c)) ⟩

    ap↓ (ap to) (ap↓ (ap from) (apd glue (glue c)))

         =⟨ from-glue-glue-β c |in-ctx (ap↓ (ap to)) ⟩

    ap↓ (ap to) ((↓-='-in (E∙₂Red.coh! c (↓-='-out (apd (glue {d = v-h-span}) (glue c))
                                           ∙□-i/ E∙₂Red.lhs-i c / E∙₂Red.rhs-i c /)
                             ∙□-i/ E∙₂Red.lhs-o c / E∙₂Red.rhs-o c /))
                   ◃/ From.glue-β (left (f₁₂ c)) / ! (From.glue-β (right (f₃₂ c))) /)

         =⟨ ap↓-◃/ (ap to) _ (From.glue-β (left (f₁₂ c))) _ ⟩

    ap↓ (ap to) (↓-='-in (E∙₂Red.coh! c (↓-='-out (apd (glue {d = v-h-span}) (glue c))
                                          ∙□-i/ E∙₂Red.lhs-i c / E∙₂Red.rhs-i c /)
                            ∙□-i/ E∙₂Red.lhs-o c / E∙₂Red.rhs-o c /))
    ◃/ ap (ap to) (From.glue-β (left (f₁₂ c))) / ap (ap to) (! (From.glue-β (right (f₃₂ c)))) /

         =⟨ lemma2-2 |in-ctx (λ u → u ◃/ ap (ap to) (From.glue-β (left (f₁₂ c))) / ap (ap to) (! (From.glue-β (right (f₃₂ c)))) /) ⟩

    ↓-='-in (↓-='-out (apd (glue {d = h-v-span}) (glue c))
             ∙□-o/ ∘-ap to left (glue (f₁₂ c)) ∙ I₀∙.glue-β (f₁₂ c) / ! (∘-ap to right (glue (f₃₂ c)) ∙ I₄∙.glue-β (f₃₂ c)) /
             ∙□-i/ ! end-lemma1 / end-lemma3 /)
    ◃/ ap (ap to) (From.glue-β (left (f₁₂ c))) / ap (ap to) (! (From.glue-β (right (f₃₂ c)))) / ∎

  lemma2 =
    ↓-='-out (apd (ap to ∘ ap from ∘ glue) (glue c))

         =⟨ lemma2-1 |in-ctx ↓-='-out ⟩

    ↓-='-out (↓-='-in (↓-='-out (apd (glue {d = h-v-span}) (glue c))
                       ∙□-o/ ∘-ap to left (glue (f₁₂ c)) ∙ I₀∙.glue-β (f₁₂ c)
                           / ! (∘-ap to right (glue (f₃₂ c)) ∙ I₄∙.glue-β (f₃₂ c)) /
                       ∙□-i/ ! end-lemma1
                           / end-lemma3 /)
              ◃/ ap (ap to) (From.glue-β (left (f₁₂ c))) / ap (ap to) (! (From.glue-β (right (f₃₂ c)))) /)

         =⟨ thing (↓-='-out (apd (glue {d = h-v-span}) (glue c))
                       ∙□-o/ ∘-ap to left (glue (f₁₂ c)) ∙ I₀∙.glue-β (f₁₂ c)
                           / ! (∘-ap to right (glue (f₃₂ c)) ∙ I₄∙.glue-β (f₃₂ c)) /
                       ∙□-i/ ! end-lemma1
                           / end-lemma3 /) (ap (ap to) (From.glue-β (left (f₁₂ c)))) (ap (ap to) (! (From.glue-β (right (f₃₂ c))))) ⟩

    ↓-='-out (apd (glue {d = h-v-span}) (glue c))
    ∙□-o/ ∘-ap to left (glue (f₁₂ c)) ∙ I₀∙.glue-β (f₁₂ c)
        / ! (∘-ap to right (glue (f₃₂ c)) ∙ I₄∙.glue-β (f₃₂ c)) /
    ∙□-i/ ! end-lemma1
        / end-lemma3 /
    ∙□-o/ ap (ap to) (From.glue-β (left (f₁₂ c))) / ap (ap to) (! (From.glue-β (right (f₃₂ c)))) /

         =⟨ ch (↓-='-out (apd (glue {d = h-v-span}) (glue c))) (∘-ap to left (glue (f₁₂ c)))
               (ap-∘ to left (glue (f₁₂ c))) (!-∘-ap to left (glue (f₁₂ c))) (I₀∙.glue-β (f₁₂ c)) (∘-ap to right (glue (f₃₂ c)))
               (ap-∘ to right (glue (f₃₂ c))) (!-∘-ap to right (glue (f₃₂ c))) (I₄∙.glue-β (f₃₂ c)) (! end-lemma1) end-lemma3
               (ap (ap to) (From.glue-β (left (f₁₂ c)))) (! (From.glue-β (left (f₁₂ c))) |in-ctx ap to) (!-ap (ap to) (From.glue-β (left (f₁₂ c)))) (ap (ap to) (! (From.glue-β (right (f₃₂ c))))) ⟩

    ↓-='-out (apd (glue {d = h-v-span}) (glue c))
    ∙□-i/ ! end-lemma1
        / end-lemma3 /
    ∙□-o/ ! (to-from-g-l (f₁₂ c))
        / to-from-g-r (f₃₂ c) / ∎  where

      ch : ∀ {i} {A : Type i} {a b b' c : A} {p₁ p₂ p₃ p₄ : a == b} {q₁ q₂ : b == c} {r₁ r₂ : a == b'}
           {s₁ s₂ s₃ s₄ : b' == c} (α : (p₁ , q₁ =□ r₁ , s₁)) (β₁ : p₃ == p₂) (β₁-inv : p₂ == p₃)
           (eq : ! β₁ == β₁-inv) (β₂ : p₂ == p₁) (β'₁ : s₃ == s₂)
           (β'₁-inv : s₂ == s₃) (eq' : ! β'₁ == β'₁-inv) (β'₂ : s₂ == s₁)
           (γ : q₂ == q₁) (γ' : r₁ == r₂) (β₃ : p₄ == p₃) (β₃-inv : p₃ == p₄) (eq₃ : ! β₃ == β₃-inv) (β'₃ : s₃ == s₄)
           →
           α ∙□-o/ β₁ ∙ β₂ / ! (β'₁ ∙ β'₂) /
             ∙□-i/ γ / γ' /
             ∙□-o/ β₃ / β'₃ /
           ==
           α ∙□-i/ γ / γ' /
             ∙□-o/ ! (_ =⟨ ! β₂ ⟩ _ =⟨ β₁-inv ⟩ _ =⟨ β₃-inv ⟩ _ ∎) / (_ =⟨ ! β'₂ ⟩ _ =⟨ β'₁-inv ⟩ _ =⟨ β'₃ ⟩ _ ∎) /
      ch α idp .idp idp idp idp .idp idp idp idp idp idp .idp idp idp = idp

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module calculus.properties where

open import utility

open import Esterel.Lang
open import Esterel.Lang.Binding
open import Esterel.Lang.Properties
open import Esterel.Lang.CanFunction
  using (Canθₛ ; Canθₛₕ ; [S]-env)
open import Esterel.Environment as Env
  using (Env ; Θ ; _←_ ; sig ; []env ; module SigMap ; module ShrMap ; module VarMap)
open import Esterel.Context
  using (EvaluationContext ; EvaluationContext1 ; _⟦_⟧e ; _≐_⟦_⟧e ;
         Context ; Context1 ; _⟦_⟧c ; _≐_⟦_⟧c ; dchole)
open import Esterel.Variable.Signal as Signal
  using (Signal)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar)
open import Esterel.Variable.Sequential as SeqVar
  using (SeqVar)
open import Esterel.Context.Properties

open import Relation.Nullary
  using (¬_)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl)
open import Data.Empty
  using (⊥ ; ⊥-elim)
import Data.FiniteMap
open import Data.List
  using (List ; _∷_ ; [] ; _++_)
open import Data.List.All as All
  using (All ; _∷_ ; [])
open import Data.Nat
  using (ℕ ; zero ; suc ; _+_)
open import Data.Product
  using (Σ-syntax ; Σ ; _,_ ; proj₁ ; proj₂ ; _×_ ; _,′_ ; ∃)
open import Data.Sum
  using (_⊎_ ; inj₁ ; inj₂)
open import Relation.Binary.PropositionalEquality

open import sn-calculus
open import calculus
open import par-swap
open import par-swap.union-properties using (∥R∪sn≡ₑ-consistent)

open import binding-preserve using (CB-preservation*)

⟶*-concat : ∀ {p q r} -> p ⟶* q -> q ⟶* r -> p ⟶* r
⟶*-concat [refl] q⟶*r = q⟶*r
⟶*-concat ([step] p⟶q p⟶*q) q⟶*r = [step] p⟶q (⟶*-concat p⟶*q q⟶*r)

⟶*->∥R*∪sn⟶* : ∀ {p q} -> p ⟶* q -> p ∥R*∪sn⟶* q
⟶*->∥R*∪sn⟶* = thm where

 thm : ∀ {p q} -> p ⟶* q -> p ∥R*∪sn⟶* q
 thm [refl] = ∪refl
 thm ([step] ([context] C dc p⟶₁p') p'⟶*q) with thm p'⟶*q
 thm ([step] ([context] C dc [par-swap]) p'⟶*q) | R
  = ∪∥R* (∥Rn (∥Rstep{C} dc) ∥R0) R
 thm ([step] ([context] C dc ([par-nothing] doneq)) p'⟶*q) | R
  = ∪sn⟶* (rstep (rcontext C dc (rpar-done-right hnothin doneq)) rrefl) R
 thm ([step] ([context] C dc ([par-1exit] n pausedq)) p'⟶*q) | R
  = ∪sn⟶* (rstep (rcontext C dc (rpar-done-right (hexit n) (dpaused pausedq))) rrefl) R
 thm ([step] ([context] C dc ([par-2exit] n m)) p'⟶*q) | R
  = ∪sn⟶* (rstep (rcontext C dc (rpar-done-right (hexit n) (dhalted (hexit m)))) rrefl) R
 thm ([step] ([context] C dc ([is-present] S S∈ θ[S]≡present de)) p'⟶*q) | R
  = ∪sn⟶* (rstep (rcontext C dc (ris-present{S = S} S∈ θ[S]≡present de)) rrefl) R
 thm ([step] ([context] C dc ([is-absent] S S∈ θ[S]≡absent de)) p'⟶*q) | R
  = ∪sn⟶* (rstep (rcontext C dc (ris-absent{S = S} S∈ θ[S]≡absent de)) rrefl) R
 thm ([step] ([context] C dc ([emit] S∈ ¬S≡a de)) p'⟶*q) | R
  = ∪sn⟶* (rstep (rcontext C dc (remit S∈ ¬S≡a de)) rrefl) R
 thm ([step] ([context] C dc [loop-unroll]) p'⟶*q) | R
  = ∪sn⟶* (rstep (rcontext C dc rloop-unroll) rrefl) R
 thm ([step] ([context] C dc [seq-done]) p'⟶*q) | R
  = ∪sn⟶* (rstep (rcontext C dc rseq-done) rrefl) R
 thm ([step] ([context] C dc [seq-exit]) p'⟶*q) | R
  = ∪sn⟶* (rstep (rcontext C dc rseq-exit) rrefl) R
 thm ([step] ([context] C dc [loopˢ-exit]) p'⟶*q) | R
  = ∪sn⟶* (rstep (rcontext C dc rloopˢ-exit) rrefl) R
 thm ([step] ([context] C dc ([suspend-done] haltedp)) p'⟶*q) | R
  = ∪sn⟶* (rstep (rcontext C dc (rsuspend-done haltedp)) rrefl) R
 thm ([step] ([context] C dc ([trap-done] haltedp)) p'⟶*q) | R
  = ∪sn⟶* (rstep (rcontext C dc (rtrap-done haltedp)) rrefl) R
 thm ([step] ([context] C dc [raise-signal]) p'⟶*q) | R
  = ∪sn⟶* (rstep (rcontext C dc rraise-signal) rrefl) R
 thm ([step] ([context] C dc ([raise-shared] all-readyeθ de)) p'⟶*q) | R
  = ∪sn⟶* (rstep (rcontext C dc (rraise-shared all-readyeθ de)) rrefl) R
 thm ([step] ([context] C dc ([set-shared-value-old] e' s∈ θ[s]≡old de)) p'⟶*q) | R
  = ∪sn⟶* (rstep (rcontext C dc (rset-shared-value-old e' s∈ θ[s]≡old de)) rrefl) R
 thm ([step] ([context] C dc ([set-shared-value-new] e' s∈ θ[s]≡n de)) p'⟶*q) | R
  = ∪sn⟶* (rstep (rcontext C dc (rset-shared-value-new e' s∈ θ[s]≡n de)) rrefl) R
 thm ([step] ([context] C dc ([raise-var] all-readyeθ de)) p'⟶*q) | R
  = ∪sn⟶* (rstep (rcontext C dc (rraise-var all-readyeθ de)) rrefl) R
 thm ([step] ([context] C dc ([set-var] x∈ all-readyeθ de)) p'⟶*q) | R
  = ∪sn⟶* (rstep (rcontext C dc (rset-var x∈ all-readyeθ de)) rrefl) R
 thm ([step] ([context] C dc ([if-false] x∈ θ[x]≡z de)) p'⟶*q) | R
  = ∪sn⟶* (rstep (rcontext C dc (rif-false x∈ θ[x]≡z de)) rrefl) R
 thm ([step] ([context] C dc ([if-true] x∈ θ[x]≡s de)) p'⟶*q) | R
  = ∪sn⟶* (rstep (rcontext C dc (rif-true x∈ θ[x]≡s de)) rrefl) R
 thm ([step] ([context] C dc ([absence] S S∈ θ[S]≡unknown S∉Canθₛ)) p'⟶*q) | R
  = ∪sn⟶* (rstep (rcontext C dc (rabsence{S = S} S∈ θ[S]≡unknown S∉Canθₛ)) rrefl) R
 thm ([step] ([context] C dc ([readyness] s s∈ θ[s]≡old⊎θ[s]≡new s∉Canθₛₕ)) p'⟶*q) | R
  = ∪sn⟶* (rstep (rcontext C dc (rreadyness{s = s} s∈ θ[s]≡old⊎θ[s]≡new s∉Canθₛₕ)) rrefl) R
 thm ([step] ([context] C dc ([merge] de)) p'⟶*q) | R
  = ∪sn⟶* (rstep (rcontext C dc (rmerge de)) rrefl) R

∥R*∪sn⟶*->⟶* : ∀ {p q} -> p ∥R*∪sn⟶* q -> p ⟶* q
∥R*∪sn⟶*->⟶* = thm where

  p∥R*q->p⟶*q : ∀ {p q} -> p ∥R* q -> p ⟶* q
  p∥R*q->p⟶*q ∥R0 = [refl]
  p∥R*q->p⟶*q (∥Rn (∥Rstep d≐C⟦p∥q⟧c) p∥R*q)
   = [step] ([context] _ d≐C⟦p∥q⟧c [par-swap]) (p∥R*q->p⟶*q p∥R*q)

  sn* : ∀ {p q} -> p sn⟶* q -> p ⟶* q
  sn* rrefl = [refl]
  sn* (rstep (rcontext C dc step) more) with sn* more
  sn* (rstep (rcontext C dc (rpar-done-right hnothin q')) _) | R
   = [step] ([context] C dc ([par-nothing] q')) R
  sn* (rstep (rcontext C dc (rpar-done-right (hexit n) (dhalted hnothin))) _) | R
   = [step] ([context] C dc [par-swap])
     ([step] ([context] C Crefl ([par-nothing] (dhalted (hexit n))))
      R)
  sn* (rstep (rcontext C dc (rpar-done-right (hexit n) (dhalted (hexit m)))) _) | R
   = [step] ([context] C dc ([par-2exit] n m)) R
  sn* (rstep (rcontext C dc (rpar-done-right (hexit n) (dpaused p/paused))) _) | R
   = [step] ([context] C dc ([par-1exit] n p/paused)) R
  sn* (rstep (rcontext C dc (rpar-done-left (dhalted hnothin) q')) more) | R
   = [step] ([context] C dc ([par-nothing] (dhalted q'))) R
  sn* (rstep (rcontext C dc (rpar-done-left (dhalted (hexit n)) hnothin)) more) | R
   = [step] ([context] C dc [par-swap])
     ([step] ([context] C Crefl ([par-nothing] (dhalted (hexit n))))
      R)
  sn* (rstep (rcontext C dc (rpar-done-left (dhalted (hexit n)) (hexit m))) more) | R
   = [step] ([context] C dc ([par-2exit] n m)) R
  sn* (rstep (rcontext C dc (rpar-done-left (dpaused p/paused) hnothin)) more) | R
   = [step] ([context] C dc [par-swap])
     ([step] ([context] C Crefl ([par-nothing] (dpaused p/paused)))
      R)
  sn* (rstep (rcontext C dc (rpar-done-left (dpaused p/paused) (hexit n))) more) | R
   = [step] ([context] C dc [par-swap])
     ([step] ([context] C Crefl ([par-1exit] n p/paused))
      R)
  sn* (rstep (rcontext C dc (ris-present{S = S} S∈ x x₁)) _) | R
   = [step] ([context] C dc ([is-present] S S∈ x x₁)) R
  sn* (rstep (rcontext C dc (ris-absent{S = S} S∈ x x₁)) _) | R
   = [step] ([context] C dc ([is-absent] S S∈ x x₁)) R
  sn* (rstep (rcontext C dc (remit S∈ ¬S≡a x)) _) | R
   = [step] ([context] C dc ([emit] S∈ ¬S≡a x)) R
  sn* (rstep (rcontext C dc rloop-unroll) _) | R
   = [step] ([context] C dc [loop-unroll]) R
  sn* (rstep (rcontext C dc rseq-done) _) | R
   = [step] ([context] C dc [seq-done]) R
  sn* (rstep (rcontext C dc rseq-exit) _) | R
   = [step] ([context] C dc [seq-exit]) R
  sn* (rstep (rcontext C dc rloopˢ-exit) _) | R
   = [step] ([context] C dc [loopˢ-exit]) R
  sn* (rstep (rcontext C dc (rsuspend-done x)) _) | R
   = [step] ([context] C dc ([suspend-done] x)) R
  sn* (rstep (rcontext C dc (rtrap-done p')) _) | R
   = [step] ([context] C dc ([trap-done] p')) R
  sn* (rstep (rcontext C dc rraise-signal) _) | R
   = [step] ([context] C dc [raise-signal]) R
  sn* (rstep (rcontext C dc (rraise-shared e' x)) _) | R
   = [step] ([context] C dc ([raise-shared] e' x)) R
  sn* (rstep (rcontext C dc (rset-shared-value-old e' s∈ x x₁)) _) | R
   = [step] ([context] C dc ([set-shared-value-old] e' s∈ x x₁)) R
  sn* (rstep (rcontext C dc (rset-shared-value-new e' s∈ x x₁)) _) | R
   = [step] ([context] C dc ([set-shared-value-new] e' s∈ x x₁)) R
  sn* (rstep (rcontext C dc (rraise-var e' x₁)) _) | R
   = [step] ([context] C dc ([raise-var] e' x₁)) R
  sn* (rstep (rcontext C dc (rset-var x∈ e' x₁)) _) | R
   = [step] ([context] C dc ([set-var] x∈ e' x₁)) R
  sn* (rstep (rcontext C dc (rif-false x∈ x₁ x₂)) _) | R
   = [step] ([context] C dc ([if-false] x∈ x₁ x₂)) R
  sn* (rstep (rcontext C dc (rif-true x∈ x₁ x₂)) _) | R
   = [step] ([context] C dc ([if-true] x∈ x₁ x₂)) R
  sn* (rstep (rcontext C dc (rabsence{S = S} S∈ x x₁)) _) | R
   = [step] ([context] C dc ([absence] S S∈ x x₁)) R
  sn* (rstep (rcontext C dc (rreadyness{s = s} s∈ x x₁)) _) | R
   = [step] ([context] C dc ([readyness] s s∈ x x₁)) R
  sn* (rstep (rcontext C dc (rmerge x)) _) | R
   = [step] ([context] C dc ([merge] x)) R

  thm : ∀ {p q} -> p ∥R*∪sn⟶* q -> p ⟶* q
  thm (∪∥R* p∥R*q p∥R*∪sn⟶*q)
   = ⟶*-concat (p∥R*q->p⟶*q p∥R*q) (thm p∥R*∪sn⟶*q)
  thm (∪sn⟶* psn⟶*q p∥R*∪sn⟶*q)
   = ⟶*-concat (sn* psn⟶*q)  (thm p∥R*∪sn⟶*q)
  thm ∪refl = [refl]

≡ₑ-to-∥R∪sn≡ₑ : ∀ {p q} ->
  p ≡ₑ q # [] ->
  p ∥R∪sn≡ₑ q
≡ₑ-to-∥R∪sn≡ₑ
 = λ p≡ₑq#[] → thm Crefl Crefl p≡ₑq#[] where

 lift-∥R* : ∀ {p q} ->
    p ∥R* q ->
    p ∥R∪sn≡ₑ q
 lift-∥R* ∥R0 = ∪ref
 lift-∥R* (∥Rn p∥Rr r⟶q)
  = ∪trn (∪stp∥ p∥Rr) (lift-∥R* r⟶q)

 lift-sn⟶* : ∀ {p q} ->
    p sn⟶* q ->
    p ∥R∪sn≡ₑ q
 lift-sn⟶* rrefl = ∪ref
 lift-sn⟶* (rstep psn⟶r r⟶q)
  = ∪trn (∪stpsn psn⟶r) (lift-sn⟶* r⟶q)

 lift-∪ : ∀ {p q} ->
    p ∥R*∪sn⟶* q ->
    p ∥R∪sn≡ₑ q
 lift-∪ (∪∥R* p∥R*r r⟶*q)
   = ∪trn (lift-∥R* p∥R*r) (lift-∪ r⟶*q)
 lift-∪ (∪sn⟶* psn⟶*r r⟶*q)
   = ∪trn (lift-sn⟶* psn⟶*r) (lift-∪ r⟶*q)
 lift-∪ ∪refl = ∪ref

 thm : ∀ {p′ p q′ q C} ->
   (p′C : p′ ≐ C ⟦ p ⟧c) ->
   (q′C : q′ ≐ C ⟦ q ⟧c) ->
   p ≡ₑ q # C ->
   p′ ∥R∪sn≡ₑ q′

 thm p′C q′C ≡ₑrefl
  rewrite sym (unplugc p′C) | sym (unplugc q′C)
  = ∪ref

 thm p′C q′C (≡ₑtran p≡ₑr r≡ₑq)
  with thm p′C Crefl p≡ₑr
 ... | p′∪≡r′
  with thm Crefl q′C r≡ₑq
 ... | r′∪≡q′ = ∪trn p′∪≡r′ r′∪≡q′

 thm p′C q′C (≡ₑsymm CBq p≡ₑq)
  with thm q′C p′C p≡ₑq
 ... | q∪≡p rewrite sym (unplugc q′C)
  = ∪sym q∪≡p CBq

 thm p′C q′C (≡ₑctxt pC′ qC′ C′⟦p₂⟧≡ₑC′⟦q₂⟧)
  = thm (C++ p′C pC′)
        (C++ q′C qC′)
        C′⟦p₂⟧≡ₑC′⟦q₂⟧

 thm p′C q′C (≡ₑstep p⟶₁q)
  with ⟶*->∥R*∪sn⟶* ([step] ([context] _ p′C p⟶₁q) [refl])
 ... | p′∥R*∪sn⟶*q′ rewrite sym (unplugc q′C)
  = lift-∪ p′∥R*∪sn⟶*q′

∥R∪sn≡-to-≡ₑ : ∀ {p q} ->
  p ∥R∪sn≡ₑ q ->
  p ≡ₑ q # []
∥R∪sn≡-to-≡ₑ = thm where

 lift⟶* : ∀ {p q} ->
  p ⟶* q ->
  p ≡ₑ q # []
 lift⟶* [refl] = ≡ₑrefl
 lift⟶* ([step] ([context] C dc p⟶₁p') r⟶*q) =
   ≡ₑtran (≡ₑctxt dc Crefl (≡ₑstep p⟶₁p'))
          (lift⟶* r⟶*q)

 thm  : ∀ {p q} ->
  p ∥R∪sn≡ₑ q ->
  p ≡ₑ q # []
 thm (∪stpsn psn⟶q) =
   lift⟶*
    (∥R*∪sn⟶*->⟶*
     (∪sn⟶* (rstep psn⟶q rrefl)
             ∪refl))
 thm (∪stp∥ (∥Rstep d≐C⟦p∥q⟧c))
   = ≡ₑctxt d≐C⟦p∥q⟧c Crefl
            (≡ₑstep [par-swap])
 thm (∪sym q∪≡p CBq)
  with thm q∪≡p
 ... | q≡ₑp
  = ≡ₑsymm CBq q≡ₑp
 thm ∪ref = ≡ₑrefl
 thm (∪trn p∪≡r r∪≡q)
  with thm p∪≡r
 ... | p≡ₑr
   with thm r∪≡q
 ... | r≡ₑq
  = ≡ₑtran p≡ₑr r≡ₑq

≡ₑ-consistent : ∀{p q BV FV}
                → CorrectBinding p BV FV
                → p ≡ₑ q # []
                → Σ[ r ∈ Term ] p ⟶* r × q ⟶* r
≡ₑ-consistent CB eq with ∥R∪sn≡ₑ-consistent CB (≡ₑ-to-∥R∪sn≡ₑ eq)
≡ₑ-consistent CB₁ eq | r , p∥⟶*r , q∥⟶*r
  = r , (∥R*∪sn⟶*->⟶* p∥⟶*r) , (∥R*∪sn⟶*->⟶* q∥⟶*r)

∥R*-preserve-CB : ∀ p q → (⊢C⟦p⟧ : CB p) → (p∥R*q :  p ∥R* q) → CB q
∥R*-preserve-CB p .p ⊢C⟦p⟧ ∥R0 = ⊢C⟦p⟧
∥R*-preserve-CB p q₁ ⊢C⟦p⟧ (∥Rn (∥Rstep d≐C⟦p∥q⟧c) p∥R*q) with binding-extractc' ⊢C⟦p⟧ d≐C⟦p∥q⟧c
... | (FV' , BV') , CB2 with CB2
... | (CBpar{BVp = BVp}{FVp = FVp} y y₁ BVp≠BVq FVp≠BVq BVp≠FVq Xp≠Xq) with n
  where
    n = binding-substc' ⊢C⟦p⟧ d≐C⟦p∥q⟧c CB2 (∪-comm-⊆-left BVp ⊆-refl) ((∪-comm-⊆-left FVp ⊆-refl)) ((CBpar y₁ y (distinct-sym BVp≠BVq)  (distinct-sym BVp≠FVq) (distinct-sym FVp≠BVq) (distinct'-sym Xp≠Xq)))
... | (_ , _ , cb) with BVFVcorrect _ _ _ cb
... | refl , refl = ∥R*-preserve-CB _ _ cb p∥R*q

∥R*∪sn⟶*-preserve-CB : ∀ p q → (⊢C⟦p⟧ : CB p) → (p∥R*∪sn⟶*q : p ∥R*∪sn⟶* q) → CB q
∥R*∪sn⟶*-preserve-CB p q ⊢C⟦p⟧ (∪∥R* p∥R*q p∥R*∪sn⟶*q)
  = ∥R*∪sn⟶*-preserve-CB _ _ (∥R*-preserve-CB _ _ ⊢C⟦p⟧ p∥R*q) p∥R*∪sn⟶*q
∥R*∪sn⟶*-preserve-CB p q ⊢C⟦p⟧ (∪sn⟶* psn⟶*q p∥R*∪sn⟶*q)
  = ∥R*∪sn⟶*-preserve-CB _ _ next p∥R*∪sn⟶*q
  where
    next = CB-preservation* p _ ⊢C⟦p⟧  psn⟶*q
∥R*∪sn⟶*-preserve-CB p .p ⊢C⟦p⟧ ∪refl = ⊢C⟦p⟧

⟶₁-preserve-CB : ∀ p q C → (⊢C⟦p⟧ : CB (C ⟦ p ⟧c)) → (p⟶₁q : p ⟶₁ q) → CB (C ⟦ q ⟧c)
⟶₁-preserve-CB p q C ⊢C⟦p⟧ p⟶₁q with (⟶*->∥R*∪sn⟶* ([step] ([context] C Crefl p⟶₁q) [refl]))
... | p∥R*∪sn⟶*q = ∥R*∪sn⟶*-preserve-CB (C ⟦ p ⟧c) (C ⟦ q ⟧c) ⊢C⟦p⟧ p∥R*∪sn⟶*q

ext: agda

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
------------------------------------------------------------------------
-- Groupoids
------------------------------------------------------------------------

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

open import Equality

module Groupoid
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open import Prelude hiding (id; _∘_; _^_)

open import Bijection eq hiding (id; _∘_)
open Derived-definitions-and-properties eq
open import Integer.Basics eq as Int using (ℤ; +_; -[1+_])
import Nat eq as Nat

private
  variable
    a       : Level
    A       : Type a
    w x y z : A
    n       : ℕ
    j       : ℤ

-- Groupoids using _≡_ as the underlying equality.

record Groupoid o ℓ : Type (lsuc (o ⊔ ℓ)) where
  infix  8 _⁻¹
  infixr 7 _∘_
  infix  4 _∼_
  field
    Object : Type o
    _∼_    : Object → Object → Type ℓ

    id  : x ∼ x
    _∘_ : y ∼ z → x ∼ y → x ∼ z
    _⁻¹ : x ∼ y → y ∼ x

    left-identity  : (p : x ∼ y) → id ∘ p ≡ p
    right-identity : (p : x ∼ y) → p ∘ id ≡ p
    assoc          : (p : y ∼ z) (q : x ∼ y) (r : w ∼ x) →
                     p ∘ (q ∘ r) ≡ (p ∘ q) ∘ r
    left-inverse   : (p : x ∼ y) → p ⁻¹ ∘ p ≡ id
    right-inverse  : (p : x ∼ y) → p ∘ p ⁻¹ ≡ id

  -- Note that this definition should perhaps contain more coherence
  -- properties: we have not assumed that _≡_ is proof-irrelevant.

  private
    variable
      p p₁ p₂ q q₁ q₂ r : x ∼ y

  -- Some derived properties.

  abstract

    -- The identity is an identity for the inverse operator as well.

    identity : id {x = x} ⁻¹ ≡ id
    identity =
      id ⁻¹       ≡⟨ sym $ right-identity (id ⁻¹) ⟩
      id ⁻¹ ∘ id  ≡⟨ left-inverse id ⟩∎
      id          ∎

    -- If p is idempotent with respect to _∘_, then p is equal to the
    -- identity element.

    idempotent⇒≡id : p ∘ p ≡ p → p ≡ id
    idempotent⇒≡id {p = p} p∘p≡p =
      p               ≡⟨ sym $ left-identity _ ⟩
      id ∘ p          ≡⟨ cong (_∘ _) $ sym $ left-inverse _ ⟩
      (p ⁻¹ ∘ p) ∘ p  ≡⟨ sym $ assoc _ _ _ ⟩
      p ⁻¹ ∘ (p ∘ p)  ≡⟨ cong (p ⁻¹ ∘_) p∘p≡p ⟩
      p ⁻¹ ∘ p        ≡⟨ left-inverse _ ⟩∎
      id              ∎

    -- Groupoids are left-cancellative and right-cancellative.

    left-cancellative :
      p ∘ q₁ ≡ p ∘ q₂ → q₁ ≡ q₂
    left-cancellative {p = p} {q₁ = q₁} {q₂ = q₂} p∘q₁≡p∘q₂ =
      q₁               ≡⟨ sym $ left-identity _ ⟩
      id ∘ q₁          ≡⟨ cong (_∘ _) $ sym $ left-inverse _ ⟩
      (p ⁻¹ ∘ p) ∘ q₁  ≡⟨ sym $ assoc _ _ _ ⟩
      p ⁻¹ ∘ (p ∘ q₁)  ≡⟨ cong (p ⁻¹ ∘_) p∘q₁≡p∘q₂ ⟩
      p ⁻¹ ∘ (p ∘ q₂)  ≡⟨ assoc _ _ _ ⟩
      (p ⁻¹ ∘ p) ∘ q₂  ≡⟨ cong (_∘ _) $ left-inverse _ ⟩
      id ∘ q₂          ≡⟨ left-identity _ ⟩∎
      q₂               ∎

    right-cancellative :
      p₁ ∘ q ≡ p₂ ∘ q → p₁ ≡ p₂
    right-cancellative {p₁ = p₁} {q = q} {p₂ = p₂} p₁∘q≡p₂∘q =
      p₁               ≡⟨ sym $ right-identity _ ⟩
      p₁ ∘ id          ≡⟨ cong (_ ∘_) $ sym $ right-inverse _ ⟩
      p₁ ∘ (q ∘ q ⁻¹)  ≡⟨ assoc _ _ _ ⟩
      (p₁ ∘ q) ∘ q ⁻¹  ≡⟨ cong (_∘ q ⁻¹) p₁∘q≡p₂∘q ⟩
      (p₂ ∘ q) ∘ q ⁻¹  ≡⟨ sym $ assoc _ _ _ ⟩
      p₂ ∘ (q ∘ q ⁻¹)  ≡⟨ cong (_ ∘_) $ right-inverse _ ⟩
      p₂ ∘ id          ≡⟨ right-identity _ ⟩∎
      p₂               ∎

    -- The inverse operator is involutive.

    involutive : (p : x ∼ y) → p ⁻¹ ⁻¹ ≡ p
    involutive p =
      p ⁻¹ ⁻¹               ≡⟨ sym $ right-identity (p ⁻¹ ⁻¹) ⟩
      p ⁻¹ ⁻¹ ∘ id          ≡⟨ sym $ cong (_∘_ (p ⁻¹ ⁻¹)) (left-inverse p) ⟩
      p ⁻¹ ⁻¹ ∘ (p ⁻¹ ∘ p)  ≡⟨ assoc _ _ _ ⟩
      (p ⁻¹ ⁻¹ ∘ p ⁻¹) ∘ p  ≡⟨ cong (λ q → q ∘ p) (left-inverse (p ⁻¹)) ⟩
      id ∘ p                ≡⟨ left-identity p ⟩∎
      p                     ∎

    -- A lemma that can be used to move something from one side of an
    -- equality to the other.

    ⁻¹∘≡→≡∘ : p ⁻¹ ∘ q ≡ r → q ≡ p ∘ r
    ⁻¹∘≡→≡∘ {p = p} {q = q} {r = r} hyp =
      q               ≡⟨ sym $ left-identity _ ⟩
      id ∘ q          ≡⟨ cong (_∘ _) $ sym $ right-inverse _ ⟩
      (p ∘ p ⁻¹) ∘ q  ≡⟨ sym $ assoc _ _ _ ⟩
      p ∘ (p ⁻¹ ∘ q)  ≡⟨ cong (_ ∘_) hyp ⟩∎
      p ∘ r           ∎

    -- A corollary.

    ⁻¹∘≡id→≡ : p ⁻¹ ∘ q ≡ id → q ≡ p
    ⁻¹∘≡id→≡ {p = p} {q = q} hyp =
      q       ≡⟨ ⁻¹∘≡→≡∘ hyp ⟩
      p ∘ id  ≡⟨ right-identity _ ⟩∎
      p       ∎

    -- Another lemma that can be used to move something from one side
    -- of an equality to the other.

    ∘⁻¹≡→≡∘ : p ∘ q ⁻¹ ≡ r → p ≡ r ∘ q
    ∘⁻¹≡→≡∘ {p = p} {q = q} {r = r} hyp =
      p               ≡⟨ sym $ right-identity _ ⟩
      p ∘ id          ≡⟨ cong (_ ∘_) $ sym $ left-inverse _ ⟩
      p ∘ (q ⁻¹ ∘ q)  ≡⟨ assoc _ _ _ ⟩
      (p ∘ q ⁻¹) ∘ q  ≡⟨ cong (_∘ _) hyp ⟩∎
      r ∘ q           ∎

    -- A corollary.

    ∘⁻¹≡id→≡ : p ∘ q ⁻¹ ≡ id → p ≡ q
    ∘⁻¹≡id→≡ {p = p} {q = q} hyp =
      p       ≡⟨ ∘⁻¹≡→≡∘ hyp ⟩
      id ∘ q  ≡⟨ left-identity _ ⟩∎
      q       ∎

    -- A lemma relating _∘_ and _⁻¹.

    ∘⁻¹ : (p ∘ q) ⁻¹ ≡ q ⁻¹ ∘ p ⁻¹
    ∘⁻¹ {p = p} {q = q} = right-cancellative
      ((p ∘ q) ⁻¹ ∘ (p ∘ q)     ≡⟨ left-inverse _ ⟩
       id                       ≡⟨ sym $ left-inverse _ ⟩
       q ⁻¹ ∘ q                 ≡⟨ cong (q ⁻¹ ∘_) $ sym $ left-identity _ ⟩
       q ⁻¹ ∘ (id ∘ q)          ≡⟨ cong (q ⁻¹ ∘_) $ cong (_∘ _) $ sym $ left-inverse _ ⟩
       q ⁻¹ ∘ ((p ⁻¹ ∘ p) ∘ q)  ≡⟨ cong (q ⁻¹ ∘_) $ sym $ assoc _ _ _ ⟩
       q ⁻¹ ∘ (p ⁻¹ ∘ (p ∘ q))  ≡⟨ assoc _ _ _ ⟩∎
       (q ⁻¹ ∘ p ⁻¹) ∘ (p ∘ q)  ∎)

    -- If p ∘ q is equal to id, then q is equal to p ⁻¹.

    ⁻¹-unique-right : p ∘ q ≡ id → q ≡ p ⁻¹
    ⁻¹-unique-right {p = p} {q = q} ∘≡id = ⁻¹∘≡id→≡
      (p ⁻¹ ⁻¹ ∘ q  ≡⟨ cong (_∘ _) $ involutive _ ⟩
       p ∘ q        ≡⟨ ∘≡id ⟩∎
       id           ∎)

    -- If p ∘ q is equal to id, then p is equal to q ⁻¹.

    ⁻¹-unique-left : p ∘ q ≡ id → p ≡ q ⁻¹
    ⁻¹-unique-left {p = p} {q = q} ∘≡id = ∘⁻¹≡id→≡
      (p ∘ q ⁻¹ ⁻¹  ≡⟨ cong (_ ∘_) $ involutive _ ⟩
       p ∘ q        ≡⟨ ∘≡id ⟩∎
       id           ∎)

  -- The inverse operator is a bijection.

  ⁻¹-bijection : x ∼ y ↔ y ∼ x
  ⁻¹-bijection = record
    { surjection = record
      { logical-equivalence = record
        { to   = _⁻¹
        ; from = _⁻¹
        }
      ; right-inverse-of = involutive
      }
    ; left-inverse-of = involutive
    }

  -- Exponentiation.

  infixl 8 _^+_
  infixr 8 _^_

  _^+_ : x ∼ x → ℕ → x ∼ x
  p ^+ 0     = id
  p ^+ suc n = p ∘ p ^+ n

  _^_ : x ∼ x → ℤ → x ∼ x
  p ^ + n      = p ^+ n
  p ^ -[1+ n ] = (p ⁻¹) ^+ suc n

  -- _^+_ is homomorphic with respect to _∘_/_+_.

  ^+∘^+ : ∀ m → p ^+ m ∘ p ^+ n ≡ p ^+ (m + n)
  ^+∘^+ {p = p} {n = n} zero =
    id ∘ p ^+ n  ≡⟨ left-identity _ ⟩∎
    p ^+ n       ∎
  ^+∘^+ {p = p} {n = n} (suc m) =
    (p ∘ p ^+ m) ∘ p ^+ n  ≡⟨ sym $ assoc _ _ _ ⟩
    p ∘ (p ^+ m ∘ p ^+ n)  ≡⟨ cong (_ ∘_) $ ^+∘^+ m ⟩∎
    p ∘ p ^+ (m + n)       ∎

  -- Some rearrangement lemmas for _^+_.

  ∘^+≡^+∘ :
    p ∘ q ≡ q ∘ p →
    ∀ n → p ∘ q ^+ n ≡ q ^+ n ∘ p
  ∘^+≡^+∘ {p = p} _ zero =
    p ∘ id  ≡⟨ right-identity _ ⟩
    p       ≡⟨ sym $ left-identity _ ⟩∎
    id ∘ p  ∎
  ∘^+≡^+∘ {p = p} {q = q} comm (suc n) =
    p ∘ (q ∘ q ^+ n)  ≡⟨ assoc _ _ _ ⟩
    (p ∘ q) ∘ q ^+ n  ≡⟨ cong (_∘ q ^+ n) comm ⟩
    (q ∘ p) ∘ q ^+ n  ≡⟨ sym $ assoc _ _ _ ⟩
    q ∘ (p ∘ q ^+ n)  ≡⟨ cong (q ∘_) $ ∘^+≡^+∘ comm n ⟩
    q ∘ (q ^+ n ∘ p)  ≡⟨ assoc _ _ _ ⟩∎
    (q ∘ q ^+ n) ∘ p  ∎

  ^+∘^+≡^+∘^+ : ∀ m n → p ^+ m ∘ p ^+ n ≡ p ^+ n ∘ p ^+ m
  ^+∘^+≡^+∘^+ {p = p} m n =
    p ^+ m ∘ p ^+ n  ≡⟨ ^+∘^+ m ⟩
    p ^+ (m + n)     ≡⟨ cong (p ^+_) $ Nat.+-comm m ⟩
    p ^+ (n + m)     ≡⟨ sym $ ^+∘^+ n ⟩∎
    p ^+ n ∘ p ^+ m  ∎

  private

    -- Some lemmas which are used to define ^∘^ below.

    lemma₁ : ∀ n → (p ∘ p ^+ n) ∘ (p ⁻¹ ∘ q) ≡ p ^+ n ∘ q
    lemma₁ {p = p} {q = q} n =
      (p ∘ p ^+ n) ∘ (p ⁻¹ ∘ q)  ≡⟨ cong (_∘ (p ⁻¹ ∘ q)) $ ∘^+≡^+∘ (refl _) n ⟩
      (p ^+ n ∘ p) ∘ (p ⁻¹ ∘ q)  ≡⟨ sym $ assoc _ _ _ ⟩
      p ^+ n ∘ (p ∘ (p ⁻¹ ∘ q))  ≡⟨ cong (p ^+ n ∘_) $ assoc _ _ _ ⟩
      p ^+ n ∘ ((p ∘ p ⁻¹) ∘ q)  ≡⟨ cong (p ^+ n ∘_) $ cong (_∘ q) $ right-inverse _ ⟩
      p ^+ n ∘ (id ∘ q)          ≡⟨ cong (p ^+ n ∘_) $ left-identity _ ⟩∎
      p ^+ n ∘ q                 ∎

    lemma₂ : ∀ n → (p ⁻¹ ∘ (p ⁻¹) ^+ n) ∘ (p ∘ q) ≡ (p ⁻¹) ^+ n ∘ q
    lemma₂ {p = p} {q = q} n =
      (p ⁻¹ ∘ (p ⁻¹) ^+ n) ∘ (p ∘ q)        ≡⟨ cong (λ r → (p ⁻¹ ∘ (p ⁻¹) ^+ n) ∘ (r ∘ q)) $ sym $ involutive _ ⟩
      (p ⁻¹ ∘ (p ⁻¹) ^+ n) ∘ (p ⁻¹ ⁻¹ ∘ q)  ≡⟨ lemma₁ n ⟩∎
      (p ⁻¹) ^+ n ∘ q                       ∎

    lemma₃ : ∀ m n → p ^+ m ∘ (p ⁻¹) ^+ suc n ≡ p ^ Int.+ m +-[1+ n ]
    lemma₃ {p = p} zero n =
      id ∘ (p ⁻¹) ^+ suc n  ≡⟨ left-identity _ ⟩∎
      (p ⁻¹) ^+ suc n       ∎
    lemma₃ {p = p} (suc m) zero =
      (p ∘ p ^+ m) ∘ p ⁻¹ ∘ id  ≡⟨ lemma₁ m ⟩
      p ^+ m ∘ id               ≡⟨ right-identity _ ⟩∎
      p ^+ m                    ∎
    lemma₃ {p = p} (suc m) (suc n) =
      (p ∘ p ^+ m) ∘ (p ⁻¹ ∘ (p ⁻¹) ^+ suc n)  ≡⟨ lemma₁ m ⟩
      p ^+ m ∘ (p ⁻¹) ^+ suc n                 ≡⟨ lemma₃ m n ⟩∎
      p ^ Int.+ m +-[1+ n ]                    ∎

    lemma₄ : ∀ m n → (p ⁻¹) ^+ suc m ∘ p ^+ n ≡ p ^ Int.+ n +-[1+ m ]
    lemma₄ {p = p} m zero =
      (p ⁻¹) ^+ suc m ∘ id  ≡⟨ right-identity _ ⟩∎
      (p ⁻¹) ^+ suc m       ∎
    lemma₄ {p = p} zero (suc n) =
      (p ⁻¹ ∘ id) ∘ p ∘ p ^+ n  ≡⟨ lemma₂ zero ⟩
      id ∘ p ^+ n               ≡⟨ left-identity _ ⟩∎
      p ^+ n                    ∎
    lemma₄ {p = p} (suc m) (suc n) =
      (p ⁻¹ ∘ (p ⁻¹) ^+ suc m) ∘ (p ∘ p ^+ n)  ≡⟨ lemma₂ (suc m) ⟩
      (p ⁻¹) ^+ suc m ∘ p ^+ n                 ≡⟨ lemma₄ m n ⟩∎
      p ^ Int.+ n +-[1+ m ]                    ∎

  -- _^_ is homomorphic with respect to _∘_/Int._+_.

  ^∘^ : ∀ i → p ^ i ∘ p ^ j ≡ p ^ (i Int.+ j)
  ^∘^ {j = + _}      (+ m)            = ^+∘^+ m
  ^∘^ {j = -[1+ n ]} (+ m)            = lemma₃ m n
  ^∘^ {j = + n}      -[1+ m ]         = lemma₄ m n
  ^∘^ {p = p} {j = -[1+ n ]} -[1+ m ] =
    (p ⁻¹) ^+ suc m ∘ (p ⁻¹) ^+ suc n  ≡⟨ ^+∘^+ (suc m) ⟩
    (p ⁻¹) ^+ (suc m + suc n)          ≡⟨ cong ((p ⁻¹) ^+_) $ cong suc $ sym $ Nat.suc+≡+suc m ⟩∎
    (p ⁻¹) ^+ (2 + m + n)              ∎

  -- _^+ n commutes with _⁻¹.

  ^+⁻¹ : ∀ n → (p ^+ n) ⁻¹ ≡ (p ⁻¹) ^+ n
  ^+⁻¹         zero    = identity
  ^+⁻¹ {p = p} (suc n) =
    (p ∘ p ^+ n) ⁻¹     ≡⟨ ∘⁻¹ ⟩
    (p ^+ n) ⁻¹ ∘ p ⁻¹  ≡⟨ cong (_∘ p ⁻¹) $ ^+⁻¹ n ⟩
    (p ⁻¹) ^+ n ∘ p ⁻¹  ≡⟨ sym $ ∘^+≡^+∘ (refl _) n ⟩∎
    p ⁻¹ ∘ (p ⁻¹) ^+ n  ∎

  -- _^ i commutes with _⁻¹.

  ^⁻¹ : ∀ i → (p ^ i) ⁻¹ ≡ (p ⁻¹) ^ i
  ^⁻¹ (+ n)    = ^+⁻¹ n
  ^⁻¹ -[1+ n ] = ^+⁻¹ (suc n)

  -- Any power of id is equal to id.

  id^+ : ∀ n → id ^+ n ≡ id {x = x}
  id^+ zero    = refl _
  id^+ (suc n) =
    id ∘ id ^+ n  ≡⟨ left-identity _ ⟩
    id ^+ n       ≡⟨ id^+ n ⟩∎
    id            ∎

  id^ : ∀ i → id ^ i ≡ id {x = x}
  id^ (+ n) = id^+ n
  id^ -[1+ n ] =
    (id ⁻¹) ^+ suc n  ≡⟨ sym $ ^+⁻¹ (suc n) ⟩
    (id ^+ suc n) ⁻¹  ≡⟨ cong _⁻¹ $ id^+ (suc n) ⟩
    id ⁻¹             ≡⟨ identity ⟩∎
    id                ∎

  private

    lemma₅ : ∀ m n → p ^+ suc m ^+ n ≡ p ^+ n ∘ p ^+ m ^+ n
    lemma₅ _ zero =
      id       ≡⟨ sym $ left-identity _ ⟩∎
      id ∘ id  ∎
    lemma₅ {p = p} m (suc n) =
      p ^+ suc m ∘ p ^+ suc m ^+ n           ≡⟨ cong (p ^+ suc m ∘_) $ lemma₅ m n ⟩
      p ^+ suc m ∘ (p ^+ n ∘ p ^+ m ^+ n)    ≡⟨ assoc _ _ _ ⟩
      (p ^+ suc m ∘ p ^+ n) ∘ p ^+ m ^+ n    ≡⟨⟩
      ((p ∘ p ^+ m) ∘ p ^+ n) ∘ p ^+ m ^+ n  ≡⟨ cong (_∘ p ^+ m ^+ n) $ sym $ assoc _ _ _ ⟩
      (p ∘ p ^+ m ∘ p ^+ n) ∘ p ^+ m ^+ n    ≡⟨ cong (_∘ p ^+ m ^+ n) $ cong (p ∘_) $ ^+∘^+≡^+∘^+ m n ⟩
      (p ∘ p ^+ n ∘ p ^+ m) ∘ p ^+ m ^+ n    ≡⟨ cong (_∘ p ^+ m ^+ n) $ assoc _ _ _ ⟩
      ((p ∘ p ^+ n) ∘ p ^+ m) ∘ p ^+ m ^+ n  ≡⟨ sym $ assoc _ _ _ ⟩∎
      (p ∘ p ^+ n) ∘ p ^+ m ∘ p ^+ m ^+ n    ∎

  -- More rearrangement lemmas for _^+_.

  ^+^+≡^+* : ∀ m → p ^+ m ^+ n ≡ p ^+ (m * n)
  ^+^+≡^+* {n = n} zero =
    id ^+ n  ≡⟨ id^+ n ⟩∎
    id       ∎
  ^+^+≡^+* {p = p} {n = n} (suc m) =
    p ^+ suc m ^+ n        ≡⟨ lemma₅ m n ⟩
    p ^+ n ∘ p ^+ m ^+ n   ≡⟨ cong (p ^+ n ∘_) $ ^+^+≡^+* m ⟩
    p ^+ n ∘ p ^+ (m * n)  ≡⟨ ^+∘^+ n ⟩
    p ^+ (n + m * n)       ≡⟨⟩
    p ^+ (suc m * n)       ∎

  ∘^+≡^+∘^+ :
    p ∘ q ≡ q ∘ p →
    ∀ n →
    (p ∘ q) ^+ n ≡ p ^+ n ∘ q ^+ n
  ∘^+≡^+∘^+ _ zero =
    id       ≡⟨ sym $ left-identity _ ⟩∎
    id ∘ id  ∎
  ∘^+≡^+∘^+ {p = p} {q = q} comm (suc n) =
    (p ∘ q) ^+ suc n             ≡⟨⟩
    (p ∘ q) ∘ (p ∘ q) ^+ n       ≡⟨ cong ((p ∘ q) ∘_) $ ∘^+≡^+∘^+ comm n ⟩
    (p ∘ q) ∘ (p ^+ n ∘ q ^+ n)  ≡⟨ sym $ assoc _ _ _ ⟩
    p ∘ (q ∘ p ^+ n ∘ q ^+ n)    ≡⟨ cong (p ∘_) $ assoc _ _ _ ⟩
    p ∘ ((q ∘ p ^+ n) ∘ q ^+ n)  ≡⟨ cong (p ∘_) $ cong (_∘ (q ^+ n)) $ ∘^+≡^+∘ (sym comm) n ⟩
    p ∘ ((p ^+ n ∘ q) ∘ q ^+ n)  ≡⟨ cong (p ∘_) $ sym $ assoc _ _ _ ⟩
    p ∘ (p ^+ n ∘ q ∘ q ^+ n)    ≡⟨ assoc _ _ _ ⟩
    (p ∘ p ^+ n) ∘ q ∘ q ^+ n    ≡⟨⟩
    p ^+ suc n ∘ q ^+ suc n      ∎

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties connecting left-scaling and right-scaling
------------------------------------------------------------------------

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

open import Relation.Binary

-- The properties are parameterised by the three carriers and
-- the result equality.

module Algebra.Module.Definitions.Bi
  {a a′ b ℓb} (A : Set a) (A′ : Set a′) {B : Set b} (_≈_ : Rel B ℓb)
  where

  open import Algebra.Core

  Associative : Opₗ A B → Opᵣ A′ B → Set _
  Associative _∙ₗ_ _∙ᵣ_ = ∀ x m y → ((x ∙ₗ m) ∙ᵣ y) ≈ (x ∙ₗ (m ∙ᵣ y))


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

module Categories.Category.Complete where

open import Level

open import Categories.Category
open import Categories.Category.Construction.Cones
open import Categories.Functor
open import Categories.Diagram.Cone.Properties
open import Categories.Diagram.Limit using (Limit)

Complete : (o ℓ e : Level) {o′ ℓ′ e′ : Level} (C : Category o′ ℓ′ e′) → Set _
Complete o ℓ e C = ∀ {J : Category o ℓ e} (F : Functor J C) → Limit F

-- a functor between diagrams corresponds to a morphism between limits
module _ {o ℓ e o′ ℓ′ e′} {C : Category o′ ℓ′ e′} (Com : Complete o ℓ e C)
  {J J′ : Category o ℓ e} (F : Functor J′ J) (G : Functor J C) where

  private
    module C  = Category C
    module J  = Category J
    module J′ = Category J′
    module F  = Functor F
    module G  = Functor G

  F⇒arr : Cones (G ∘F F) [ F-map-Coneʳ F (Limit.limit (Com G)) , Limit.limit (Com (G ∘F F)) ]
  F⇒arr = Limit.rep-cone (Com (G ∘F F)) (F-map-Coneʳ F (Limit.limit (Com G)))

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


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

open import HoTT
open import homotopy.EilenbergMacLane
open import homotopy.EilenbergMacLane1
open import homotopy.EilenbergMacLaneFunctor
open import homotopy.SmashFmapConn
open import homotopy.IterSuspSmash
open import cohomology.CupProduct.OnEM.InLowDegrees2

module cohomology.CupProduct.OnEM.InAllDegrees where

module _ {i} (A : AbGroup i) where

  private
    module A = AbGroup A
  open EMExplicit

  inv-path : A == A
  inv-path = uaᴬᴳ A A (inv-iso A)

  ⊙cond-neg : ∀ (k : ℕ) → Bool
    → ⊙EM A k ⊙→ ⊙EM A k
  ⊙cond-neg k b =
    ⊙transport (λ G → ⊙EM G k) {x = A} {y = A} (Bool-elim inv-path idp b)

  ⊙cond-neg-∘ : ∀ (k : ℕ) (b c : Bool)
    → ⊙cond-neg k b ◃⊙∘ ⊙cond-neg k c ◃⊙idf
      =⊙∘
      ⊙cond-neg k (xor b c) ◃⊙idf
  ⊙cond-neg-∘ k true true =
    ⊙transport (λ G → ⊙EM G k) {x = A} {y = A} inv-path ◃⊙∘
    ⊙transport (λ G → ⊙EM G k) {x = A} {y = A} inv-path ◃⊙idf
      =⊙∘₁⟨ 0 & 1 & ⊙transport-⊙EM-uaᴬᴳ A A (inv-iso A) k ⟩
    ⊙EM-fmap A A (–>ᴳ (inv-iso A)) k ◃⊙∘
    ⊙transport (λ G → ⊙EM G k) {x = A} {y = A} inv-path ◃⊙idf
      =⊙∘₁⟨ 1 & 1 & ⊙transport-⊙EM-uaᴬᴳ A A (inv-iso A) k ⟩
    ⊙EM-fmap A A (–>ᴳ (inv-iso A)) k ◃⊙∘
    ⊙EM-fmap A A (–>ᴳ (inv-iso A)) k ◃⊙idf
      =⊙∘₁⟨ ! $ ⊙EM-fmap-∘ A A A (–>ᴳ (inv-iso A)) (–>ᴳ (inv-iso A)) k ⟩
    ⊙EM-fmap A A (–>ᴳ (inv-iso A) ∘ᴳ –>ᴳ (inv-iso A)) k ◃⊙idf
      =⊙∘₁⟨ ap (λ φ → ⊙EM-fmap A A φ k) $
            group-hom= {ψ = idhom _} (λ= A.inv-inv) ⟩
    ⊙EM-fmap A A (idhom _) k ◃⊙idf
      =⊙∘₁⟨ ⊙EM-fmap-idhom A k ⟩
    ⊙idf _ ◃⊙idf ∎⊙∘
  ⊙cond-neg-∘ k true  false = =⊙∘-in idp
  ⊙cond-neg-∘ k false true  = =⊙∘-in (⊙λ= (⊙∘-unit-l (⊙cond-neg k true)))
  ⊙cond-neg-∘ k false false = =⊙∘-in idp

  ⊙maybe-Susp^-flip-⊙cond-neg : ∀ (k : ℕ) (b : Bool)
    → (k == 0 → b == false)
    → ⊙Trunc-fmap (⊙maybe-Susp^-flip k b) == ⊙cond-neg (S k) b
  ⊙maybe-Susp^-flip-⊙cond-neg O b h =
    ⊙Trunc-fmap (⊙idf (⊙EM₁ A.grp))
      =⟨ ⊙λ= ⊙Trunc-fmap-⊙idf ⟩
    ⊙idf (⊙EM A 1)
      =⟨ ap (⊙cond-neg 1) (! (h idp)) ⟩
    ⊙cond-neg 1 b =∎
  ⊙maybe-Susp^-flip-⊙cond-neg (S k) true h =
    ⊙Trunc-fmap (⊙Susp-flip (⊙Susp^ k (⊙EM₁ A.grp)))
      =⟨ ! (⊙EM-neg=⊙Trunc-fmap-⊙Susp-flip A k) ⟩
    ⊙EM-neg A (S (S k))
      =⟨ ! (⊙transport-⊙EM-uaᴬᴳ A A (inv-iso A) (S (S k))) ⟩
    ⊙transport (λ G → ⊙EM G (S (S k))) {x = A} {y = A} inv-path =∎
  ⊙maybe-Susp^-flip-⊙cond-neg (S k) false h = ⊙λ= (⊙Trunc-fmap-⊙idf)

  ⊙EM2-Susp-seq : ∀ (k : ℕ)
    → ⊙Susp^ k (⊙EM A 2) ⊙–→ ⊙EM A (S (S k))
  ⊙EM2-Susp-seq k =
    ⊙transport (λ l → ⊙Trunc l (⊙Susp^ (S k) (⊙EM₁ A.grp))) (+2+-comm ⟨ k ⟩₋₂ 2) ◃⊙∘
    ⊙Trunc-fmap (⊙Susp^-swap k 1 {⊙EM₁ A.grp}) ◃⊙∘
    ⊙Susp^-Trunc-swap (⊙Susp (EM₁ A.grp)) 2 k ◃⊙idf

  ⊙EM2-Susp : ∀ (k : ℕ)
    → ⊙Susp^ k (⊙EM A 2) ⊙→ ⊙EM A (S (S k))
  ⊙EM2-Susp k = ⊙compose (⊙EM2-Susp-seq k)

  ⊙EM2-Susp-⊙maybe-Susp^-flip : ∀ (k : ℕ) (b : Bool)
    → (k == 0 → b == false)
    → ⊙EM2-Susp k ◃⊙∘
      ⊙maybe-Susp^-flip k b ◃⊙idf
      =⊙∘
      ⊙Trunc-fmap (⊙maybe-Susp^-flip {X = ⊙EM₁ A.grp} (S k) b) ◃⊙∘
      ⊙EM2-Susp k ◃⊙idf
  ⊙EM2-Susp-⊙maybe-Susp^-flip k b h =
    ⊙EM2-Susp k ◃⊙∘
    ⊙maybe-Susp^-flip k b ◃⊙idf
      =⊙∘⟨ 0 & 1 & ⊙expand (⊙EM2-Susp-seq k) ⟩
    ⊙transport (λ l → ⊙Trunc l (⊙Susp^ (S k) (⊙EM₁ A.grp))) (+2+-comm ⟨ k ⟩₋₂ 2) ◃⊙∘
    ⊙Trunc-fmap (⊙Susp^-swap k 1 {⊙EM₁ A.grp}) ◃⊙∘
    ⊙Susp^-Trunc-swap (⊙Susp (EM₁ A.grp)) 2 k ◃⊙∘
    ⊙maybe-Susp^-flip k b ◃⊙idf
      =⊙∘⟨ 2 & 2 & ⊙Susp^-Trunc-swap-⊙maybe-Susp^-flip (⊙Susp (EM₁ A.grp)) 2 k b ⟩
    ⊙transport (λ l → ⊙Trunc l (⊙Susp^ (S k) (⊙EM₁ A.grp))) (+2+-comm ⟨ k ⟩₋₂ 2) ◃⊙∘
    ⊙Trunc-fmap (⊙Susp^-swap k 1 {⊙EM₁ A.grp}) ◃⊙∘
    ⊙Trunc-fmap (⊙maybe-Susp^-flip k b) ◃⊙∘
    ⊙Susp^-Trunc-swap (⊙Susp (EM₁ A.grp)) 2 k ◃⊙idf
      =⊙∘⟨ 1 & 2 & ⊙Trunc-fmap-seq-=⊙∘ p ⟩
    ⊙transport (λ l → ⊙Trunc l (⊙Susp^ (S k) (⊙EM₁ A.grp))) (+2+-comm ⟨ k ⟩₋₂ 2) ◃⊙∘
    ⊙Trunc-fmap (⊙maybe-Susp-flip (⊙Susp^ k (⊙EM₁ A.grp)) b) ◃⊙∘
    ⊙Trunc-fmap (⊙Susp^-swap k 1 {⊙EM₁ A.grp}) ◃⊙∘
    ⊙Susp^-Trunc-swap (⊙Susp (EM₁ A.grp)) 2 k ◃⊙idf
      =⊙∘⟨ 0 & 2 & !⊙∘ $
           ⊙transport-natural-=⊙∘
             (+2+-comm ⟨ k ⟩₋₂ 2)
             (λ l → ⊙Trunc-fmap {n = l} (⊙maybe-Susp^-flip (S k) b)) ⟩
    ⊙Trunc-fmap (⊙maybe-Susp-flip (⊙Susp^ k (⊙EM₁ A.grp)) b) ◃⊙∘
    ⊙transport (λ l → ⊙Trunc l (⊙Susp^ (S k) (⊙EM₁ A.grp))) (+2+-comm ⟨ k ⟩₋₂ 2) ◃⊙∘
    ⊙Trunc-fmap (⊙Susp^-swap k 1 {⊙EM₁ A.grp}) ◃⊙∘
    ⊙Susp^-Trunc-swap (⊙Susp (EM₁ A.grp)) 2 k ◃⊙idf
      =⊙∘⟨ 1 & 3 & ⊙contract ⟩
    ⊙Trunc-fmap (⊙maybe-Susp-flip (⊙Susp^ k (⊙EM₁ A.grp)) b) ◃⊙∘
    ⊙EM2-Susp k ◃⊙idf ∎⊙∘
    where
    p : ⊙Susp^-swap k 1 {⊙EM₁ A.grp} ◃⊙∘
        ⊙maybe-Susp^-flip k b ◃⊙idf
        =⊙∘
        ⊙maybe-Susp^-flip {X = ⊙EM₁ A.grp} (S k) b ◃⊙∘
        ⊙Susp^-swap k 1 {⊙EM₁ A.grp} ◃⊙idf
    p =
      ⊙Susp^-swap k 1 {⊙EM₁ A.grp} ◃⊙∘
      ⊙maybe-Susp^-flip k b ◃⊙idf
        =⊙∘⟨ !⊙∘ $ ⊙maybe-Susp^-flip-⊙Susp^-comm (⊙EM₁ A.grp) k 1 b ⟩
      ⊙Susp-fmap (fst (⊙maybe-Susp^-flip k b)) ◃⊙∘
      ⊙coe (⊙Susp^-comm k 1) ◃⊙idf
        =⊙∘₁⟨ 0 & 1 & ap ⊙Susp-fmap (de⊙-⊙maybe-Susp^-flip k b) ∙
                      ⊙Susp-fmap-maybe-Susp^-flip k b h ⟩
      ⊙maybe-Susp-flip (⊙Susp^ k (⊙EM₁ A.grp)) b ◃⊙∘
      ⊙Susp^-swap k 1 ◃⊙idf ∎⊙∘

  ⊙cpₕₕ''-seq : ∀ (m n : ℕ)
    → ⊙Susp^ (m + n) (⊙EM A 2) ⊙–→ ⊙EM A (S m + S n)
  ⊙cpₕₕ''-seq m n =
    ⊙cond-neg (S m + S n) (odd n) ◃⊙∘
    ⊙transport (⊙EM A) (! (+-βr (S m) n)) ◃⊙∘
    ⊙EM2-Susp (m + n) ◃⊙idf

  ⊙cpₕₕ'' : ∀ (m n : ℕ)
    → ⊙Susp^ (m + n) (⊙EM A 2) ⊙→ ⊙EM A (S m + S n)
  ⊙cpₕₕ'' m n = ⊙compose (⊙cpₕₕ''-seq m n)

module _ {i j} {X : Ptd i} {Y : Ptd j} where

  →-⊙→-uncurry : ∀ {k} {Z : Ptd k}
    → (de⊙ X → Y ⊙→ Z)
    → X ⊙× Y ⊙→ Z
  →-⊙→-uncurry f =
    uncurry (λ x y → fst (f x) y) , snd (f (pt X))

module _ {i} {j} (G : AbGroup i) (H : AbGroup j) where

  private
    module G = AbGroup G
    module H = AbGroup H
    module G⊗H = TensorProduct G H
  open EMExplicit

  ⊙∧-cpₕₕ'-seq : ∀ (m n : ℕ)
    → (⊙Susp^ m (⊙EM₁ G.grp) ⊙∧ ⊙Susp^ n (⊙EM₁ H.grp))
      ⊙–→
      ⊙EM G⊗H.abgroup (S m + S n)
  ⊙∧-cpₕₕ'-seq m n =
    ⊙cpₕₕ'' G⊗H.abgroup m n ◃⊙∘
    ⊙Susp^-fmap (m + n) (⊙∧-cp₁₁ G H) ◃⊙∘
    ⊙Σ^∧Σ^-out (⊙EM₁ G.grp) (⊙EM₁ H.grp) m n ◃⊙idf

  ⊙∧-cpₕₕ' : ∀ (m n : ℕ)
    → ⊙Susp^ m (⊙EM₁ G.grp) ⊙∧ ⊙Susp^ n (⊙EM₁ H.grp) ⊙→ ⊙EM G⊗H.abgroup (S m + S n)
  ⊙∧-cpₕₕ' m n = ⊙compose (⊙∧-cpₕₕ'-seq m n)

  ∧-cpₕₕ' : ∀ (m n : ℕ)
    → ⊙Susp^ m (⊙EM₁ G.grp) ∧ ⊙Susp^ n (⊙EM₁ H.grp)
    → EM G⊗H.abgroup (S m + S n)
  ∧-cpₕₕ' m n = fst (⊙∧-cpₕₕ' m n)

  ⊙smash-truncate : ∀ (m n : ℕ)
    → ⊙Susp^ m (⊙EM₁ G.grp) ⊙∧ ⊙Susp^ n (⊙EM₁ H.grp)
    ⊙→ ⊙EM G (S m) ⊙∧ ⊙EM H (S n)
  ⊙smash-truncate m n =
    ⊙∧-fmap
      ([_] {n = ⟨ S m ⟩} {A = Susp^ m (EM₁ G.grp)} , idp)
      ([_] {n = ⟨ S n ⟩} {A = Susp^ n (EM₁ H.grp)} , idp)

  smash-truncate : ∀ (m n : ℕ)
    → ⊙Susp^ m (⊙EM₁ G.grp) ∧ ⊙Susp^ n (⊙EM₁ H.grp)
    → ⊙EM G (S m) ∧ ⊙EM H (S n)
  smash-truncate m n = fst (⊙smash-truncate m n)

  smash-truncate-conn : ∀ (m n : ℕ)
    → has-conn-fibers ⟨ S m + S n ⟩ (smash-truncate m n)
  smash-truncate-conn m n =
    transport (λ k → has-conn-fibers k (smash-truncate m n)) p $
    ∧-fmap-conn
      ([_] {n = ⟨ S m ⟩} {A = Susp^ m (EM₁ G.grp)} , idp)
      ([_] {n = ⟨ S n ⟩} {A = Susp^ n (EM₁ H.grp)} , idp)
      (EM-conn G m)
      (⊙Susp^-conn' n {{EM₁-conn}})
      (trunc-proj-conn (Susp^ m (EM₁ G.grp)) ⟨ S m ⟩)
      (trunc-proj-conn (Susp^ n (EM₁ H.grp)) ⟨ S n ⟩)
    where
    p₁ : ⟨ n ⟩₋₁ +2+ ⟨ S m ⟩ == ⟨ S m + S n ⟩
    p₁ =
      ⟨ n ⟩₋₁ +2+ ⟨ S m ⟩
        =⟨ ! (+-+2+ (S n) (S (S (S m)))) ⟩
      ⟨ n + S (S (S m)) ⟩₋₁
        =⟨ ap ⟨_⟩₋₁ (+-βr n (S (S m))) ⟩
      ⟨ n + S (S m) ⟩
        =⟨ ap ⟨_⟩ (+-βr n (S m)) ⟩
      ⟨ S n + S m ⟩
        =⟨ ap ⟨_⟩ (+-comm (S n) (S m)) ⟩
      ⟨ S m + S n ⟩ =∎
    p₂ : ⟨ m ⟩₋₁ +2+ ⟨ S n ⟩ == ⟨ S m + S n ⟩
    p₂ =
      ⟨ m ⟩₋₁ +2+ ⟨ S n ⟩
        =⟨ ! (+-+2+ (S m) (S (S (S n)))) ⟩
      ⟨ m + S (S (S n)) ⟩₋₁
        =⟨ ap ⟨_⟩₋₁ (+-βr m (S (S n))) ⟩
      ⟨ m + S (S n) ⟩
        =⟨ ap ⟨_⟩ (+-βr m (S n)) ⟩
      ⟨ S m + S n ⟩ =∎
    p : minT (⟨ n ⟩₋₁ +2+ ⟨ S m ⟩) (⟨ m ⟩₋₁ +2+ ⟨ S n ⟩) == ⟨ S m + S n ⟩
    p =
      minT (⟨ n ⟩₋₁ +2+ ⟨ S m ⟩) (⟨ m ⟩₋₁ +2+ ⟨ S n ⟩)
        =⟨ ap2 minT p₁ p₂ ⟩
      minT ⟨ S m + S n ⟩ ⟨ S m + S n ⟩
        =⟨ minT-out-l ≤T-refl ⟩
      ⟨ S m + S n ⟩ =∎

  module SmashCPₕₕ (m n : ℕ) =
    ⊙ConnExtend
      {Z = ⊙EM G⊗H.abgroup (S m + S n)}
      {n = ⟨ S m + S n ⟩}
      (⊙smash-truncate m n)
      (smash-truncate-conn m n)
      (EM-level G⊗H.abgroup (S m + S n))

  ⊙∧-cpₕₕ : ∀ (m n : ℕ)
    → ⊙EM G (S m) ⊙∧ ⊙EM H (S n) ⊙→ ⊙EM G⊗H.abgroup (S m + S n)
  ⊙∧-cpₕₕ m n = SmashCPₕₕ.⊙ext m n (⊙∧-cpₕₕ' m n)

  ∧-cpₕₕ : ∀ (m n : ℕ)
    → ⊙EM G (S m) ∧ ⊙EM H (S n)
    → EM G⊗H.abgroup (S m + S n)
  ∧-cpₕₕ m n = fst (⊙∧-cpₕₕ m n)

  ⊙×-cpₕₕ-seq : ∀ (m n : ℕ)
    → ⊙EM G (S m) ⊙× ⊙EM H (S n) ⊙–→ ⊙EM G⊗H.abgroup (S m + S n)
  ⊙×-cpₕₕ-seq m n = ⊙∧-cpₕₕ m n ◃⊙∘ ×-⊙to-∧ ◃⊙idf

  ⊙×-cpₕₕ : ∀ (m n : ℕ)
    → ⊙EM G (S m) ⊙× ⊙EM H (S n) ⊙→ ⊙EM G⊗H.abgroup (S m + S n)
  ⊙×-cpₕₕ m n = ⊙compose (⊙×-cpₕₕ-seq m n)

  {-
  cp₀ₕ' : ∀ (n : ℕ) → G.El → EM H (S n) → EM G⊗H.abgroup (S n)
  cp₀ₕ' n g y = EM-fmap H G⊗H.abgroup (G⊗H.ins-r-hom g) (S n) y

  ×-cp₀ₕ' : ∀ (n : ℕ)
    → G.El × EM H (S n) → EM G⊗H.abgroup (S n)
  ×-cp₀ₕ' n = uncurry (cp₀ₕ' n)
  -}

  ⊙×-cp₀ₕ' : ∀ (n : ℕ)
    → G.⊙El ⊙× ⊙EM H (S n) ⊙→ ⊙EM G⊗H.abgroup (S n)
  ⊙×-cp₀ₕ' n =
    →-⊙→-uncurry (λ g → ⊙EM-fmap H G⊗H.abgroup (G⊗H.ins-r-hom g) (S n))
    -- ×-cp₀ₕ' n , snd (⊙EM-fmap H G⊗H.abgroup (G⊗H.ins-r-hom G.ident) (S n))

  ⊙×-cp₀ₕ-seq : ∀ (n : ℕ)
    → ⊙EM G 0 ⊙× ⊙EM H (S n) ⊙–→ ⊙EM G⊗H.abgroup (S n)
  ⊙×-cp₀ₕ-seq n =
    ⊙×-cp₀ₕ' n ◃⊙∘
    ⊙×-fmap (⊙<– (⊙emloop-equiv G.grp)) (⊙idf (⊙EM H (S n))) ◃⊙idf

  ⊙×-cp₀ₕ : ∀ (n : ℕ)
    → ⊙EM G 0 ⊙× ⊙EM H (S n) ⊙→ ⊙EM G⊗H.abgroup (S n)
  ⊙×-cp₀ₕ n = ⊙compose (⊙×-cp₀ₕ-seq n)

  ×-cp₀ₕ : ∀ (n : ℕ)
    → EM G 0 × EM H (S n) → EM G⊗H.abgroup (S n)
  ×-cp₀ₕ n = fst (⊙×-cp₀ₕ n)

  {-
  cpₕ₀' : ∀ (m : ℕ) → EM G (S m) → H.El → EM G⊗H.abgroup (S m)
  cpₕ₀' m x h = EM-fmap G G⊗H.abgroup (G⊗H.ins-l-hom h) (S m) x

  ×-cpₕ₀' : ∀ (m : ℕ)
    → EM G (S m) × H.El → EM G⊗H.abgroup (S m)
  ×-cpₕ₀' m = uncurry (cpₕ₀' m)
  -}

  ⊙×-cpₕ₀' : ∀ (m : ℕ)
    → ⊙EM G (S m) ⊙× H.⊙El ⊙→ ⊙EM G⊗H.abgroup (S m)
  ⊙×-cpₕ₀' m =
    →-⊙→-uncurry (λ h → ⊙EM-fmap G G⊗H.abgroup (G⊗H.ins-l-hom h) (S m)) ⊙∘
    ⊙×-swap
    -- ×-cpₕ₀' m , snd (⊙EM-fmap G G⊗H.abgroup (G⊗H.ins-l-hom H.ident) (S m))

  ⊙×-cpₕ₀-seq : ∀ (m : ℕ)
    → ⊙EM G (S m) ⊙× ⊙EM H 0 ⊙–→ ⊙EM G⊗H.abgroup (S m + 0)
  ⊙×-cpₕ₀-seq m =
    ⊙transport (⊙EM G⊗H.abgroup) (! (+-unit-r (S m))) ◃⊙∘
    ⊙×-cpₕ₀' m ◃⊙∘
    ⊙×-fmap (⊙idf (⊙EM G (S m))) (⊙<– (⊙emloop-equiv H.grp)) ◃⊙idf

  ⊙×-cpₕ₀ : ∀ (m : ℕ)
    → ⊙EM G (S m) ⊙× ⊙EM H 0 ⊙→ ⊙EM G⊗H.abgroup (S m + 0)
  ⊙×-cpₕ₀ m = ⊙compose (⊙×-cpₕ₀-seq m)

  ×-cpₕ₀ : ∀ (m : ℕ)
    → EM G (S m) × EM H 0 → EM G⊗H.abgroup (S m + 0)
  ×-cpₕ₀ m = fst (⊙×-cpₕ₀ m)

  ⊙×-cp : ∀ (m n : ℕ)
    → ⊙EM G m ⊙× ⊙EM H n
    ⊙→ ⊙EM G⊗H.abgroup (m + n)
  ⊙×-cp 0 0 = ⊙×-cp₀₀ G H
  ⊙×-cp 0 (S n) = ⊙×-cp₀ₕ n
  ⊙×-cp (S m) 0 = ⊙×-cpₕ₀ m
  ⊙×-cp (S m) (S n) = ⊙×-cpₕₕ m n

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
open import Level using (_⊔_)
open import Function using (_$_)
open import Algebra using (CommutativeRing)

module AKS.Modular.Equivalence {c ℓ} (R : CommutativeRing c ℓ) where

open CommutativeRing R using (0#; 1#; _+_; _*_; -_; _-_)
  renaming (Carrier to C)
open CommutativeRing R using (+-cong; +-congˡ; +-congʳ; +-identityʳ; +-assoc; +-comm)
open CommutativeRing R using (-‿inverseʳ; -‿inverseˡ; -‿cong)
open CommutativeRing R using (zeroˡ; distribʳ; distribˡ; *-congˡ; *-assoc; *-comm)
open CommutativeRing R using (_≈_; isEquivalence; setoid; ring)
  renaming (refl to ≈-refl; sym to ≈-sym)
open import Relation.Binary.Reasoning.Setoid setoid
open import Algebra.Properties.Ring ring using (-‿distribˡ-*; -‿+-comm; -‿involutive; -0#≈0#)

infix 4 _≈_[mod_]
record _≈_[mod_] (x : C) (y : C) (n : C) : Set (c ⊔ ℓ) where
  constructor modulo
  field
    k : C
    x-y≈k*n : x - y ≈ k * n

refl : ∀ {x} {y} {n} → x ≈ y → x ≈ y [mod n ]
refl {x} {y} {n} x≈y = modulo 0# $ begin
  x - y  ≈⟨ +-congˡ (-‿cong (≈-sym x≈y)) ⟩
  x - x  ≈⟨ -‿inverseʳ x ⟩
  0#     ≈⟨ ≈-sym (zeroˡ n) ⟩
  0# * n ∎

sym : ∀ {x y} {n} → x ≈ y [mod n ] → y ≈ x [mod n ]
sym {x} {y} {n} (modulo k x-y≈k*n) = modulo (- k) $ begin
  y - x       ≈⟨ +-congʳ (≈-sym (-‿involutive y)) ⟩
  - (- y) - x ≈⟨ -‿+-comm (- y) x ⟩
  - (- y + x) ≈⟨ -‿cong (+-comm (- y) x) ⟩
  - (x - y)   ≈⟨ -‿cong x-y≈k*n ⟩
  - (k * n)   ≈⟨ -‿distribˡ-* k n ⟩
  - k * n     ∎

trans : ∀ {x y z} {n} → x ≈ y [mod n ] → y ≈ z [mod n ] → x ≈ z [mod n ]
trans {x} {y} {z} {n} (modulo k₁ x-y≈k₁*n) (modulo k₂ y-z≈k₂*n) = modulo (k₁ + k₂) $ begin
  x - z               ≈⟨ +-congʳ (≈-sym (+-identityʳ x)) ⟩
  x + 0# - z          ≈⟨ +-congʳ (+-congˡ (≈-sym (-‿inverseˡ y))) ⟩
  x + (- y + y) - z   ≈⟨ +-congʳ (≈-sym (+-assoc x (- y) y)) ⟩
  (x - y) + y - z     ≈⟨ +-assoc (x - y) y (- z) ⟩
  (x - y) + (y - z)   ≈⟨ +-cong x-y≈k₁*n y-z≈k₂*n ⟩
  (k₁ * n) + (k₂ * n) ≈⟨ ≈-sym (distribʳ n k₁ k₂) ⟩
  (k₁ + k₂) * n   ∎

+-compat : ∀ {a₁ a₂ b₁ b₂} {n} → a₁ ≈ b₁ [mod n ] → a₂ ≈ b₂ [mod n ] → a₁ + a₂ ≈ b₁ + b₂ [mod n ]
+-compat {a₁} {a₂} {b₁} {b₂} {n} (modulo k₁ a₁-b₁≈k₁*n) (modulo k₂ a₂-b₂≈k₂*n) = modulo (k₁ + k₂) $ begin
  a₁ + a₂ - (b₁ + b₂)     ≈⟨ +-assoc a₁ a₂ (- (b₁ + b₂)) ⟩
  a₁ + (a₂ - (b₁ + b₂))   ≈⟨ +-congˡ (+-congˡ (≈-sym (-‿+-comm b₁ b₂))) ⟩
  a₁ + (a₂ + (- b₁ - b₂)) ≈⟨ +-congˡ (≈-sym (+-assoc a₂ (- b₁) (- b₂))) ⟩
  a₁ + (a₂ - b₁ - b₂)     ≈⟨ +-congˡ (+-congʳ (+-comm a₂ (- b₁))) ⟩
  a₁ + (- b₁ + a₂ - b₂)   ≈⟨ +-congˡ (+-assoc (- b₁) a₂ (- b₂)) ⟩
  a₁ + (- b₁ + (a₂ - b₂)) ≈⟨ ≈-sym (+-assoc a₁ (- b₁) (a₂ - b₂)) ⟩
  (a₁ - b₁) + (a₂ - b₂)   ≈⟨ +-cong a₁-b₁≈k₁*n a₂-b₂≈k₂*n ⟩
  (k₁ * n) + (k₂ * n)     ≈⟨ ≈-sym (distribʳ n k₁ k₂) ⟩
  (k₁ + k₂) * n           ∎

*-compat : ∀ {a₁ a₂ b₁ b₂} {n} → a₁ ≈ b₁ [mod n ] → a₂ ≈ b₂ [mod n ] → a₁ * a₂ ≈ b₁ * b₂ [mod n ]
*-compat {a₁} {a₂} {b₁} {b₂} {n} (modulo k₁ a₁-b₁≈k₁*n) (modulo k₂ a₂-b₂≈k₂*n) = modulo (a₂ * k₁ + b₁ * k₂) $ begin
  a₁ * a₂ - b₁ * b₂                                 ≈⟨ +-congˡ (-‿cong (*-comm b₁ b₂)) ⟩
  a₁ * a₂ - b₂ * b₁                                 ≈⟨ +-congʳ (≈-sym (+-identityʳ (a₁ * a₂))) ⟩
  a₁ * a₂ + 0# - b₂ * b₁                            ≈⟨ +-congʳ (+-congˡ lemma) ⟩
  a₁ * a₂ + (- (b₁ * a₂) + a₂ * b₁) - b₂ * b₁       ≈⟨ +-congʳ (≈-sym (+-assoc (a₁ * a₂) (- (b₁ * a₂)) (a₂ * b₁))) ⟩
  a₁ * a₂ - b₁ * a₂ + a₂ * b₁ - b₂ * b₁             ≈⟨ +-assoc (a₁ * a₂ - b₁ * a₂) (a₂ * b₁) (- (b₂ * b₁)) ⟩
  (a₁ * a₂ - b₁ * a₂) + (a₂ * b₁ - b₂ * b₁)         ≈⟨ +-cong (+-congˡ (-‿distribˡ-* b₁ a₂)) (+-congˡ (-‿distribˡ-* b₂ b₁)) ⟩
  (a₁ * a₂ + (- b₁) * a₂) + (a₂ * b₁ + (- b₂) * b₁) ≈⟨ +-cong (≈-sym (distribʳ a₂ a₁ (- b₁))) (≈-sym (distribʳ b₁ a₂ (- b₂))) ⟩
  (a₁ - b₁) * a₂ + (a₂ - b₂) * b₁                   ≈⟨ +-cong (*-comm (a₁ - b₁) a₂) (*-comm (a₂ - b₂) b₁) ⟩
  a₂ * (a₁ - b₁) + b₁ * (a₂ - b₂)                   ≈⟨ +-cong (*-congˡ a₁-b₁≈k₁*n) (*-congˡ a₂-b₂≈k₂*n) ⟩
  a₂ * (k₁ * n) + b₁ * (k₂ * n)                     ≈⟨ +-cong (≈-sym (*-assoc a₂ k₁ n)) (≈-sym (*-assoc b₁ k₂ n)) ⟩
  a₂ * k₁ * n + b₁ * k₂ * n                         ≈⟨ ≈-sym (distribʳ n (a₂ * k₁) (b₁ * k₂)) ⟩
  (a₂ * k₁ + b₁ * k₂) * n                           ∎
  where
  lemma : 0# ≈ - (b₁ * a₂) + a₂ * b₁
  lemma = begin
    0# ≈⟨ ≈-sym (-‿inverseˡ (b₁ * a₂)) ⟩
    - (b₁ * a₂) + b₁ * a₂ ≈⟨ +-congˡ (*-comm b₁ a₂) ⟩
    - (b₁ * a₂) + a₂ * b₁ ∎

n*x≈0 : ∀ {x} {n} → n * x ≈ 0# [mod n ]
n*x≈0 {x} {n} = modulo x $ begin
  n * x - 0# ≈⟨ +-congˡ -0#≈0# ⟩
  n * x + 0# ≈⟨ +-identityʳ (n * x) ⟩
  n * x      ≈⟨ *-comm n x ⟩
  x * n      ∎

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


text:
{-# OPTIONS --prop --rewriting --confluence-check #-}

open import Agda.Primitive
open import Agda.Builtin.Equality
open import Agda.Builtin.Nat renaming (Nat to ℕ; _+_ to _+ℕ_)

infix 4 _≐_
data _≐_ {ℓ} {A : Set ℓ} (x : A) : A → Prop ℓ where
  refl : x ≐ x

{-# BUILTIN REWRITE _≐_ #-}

variable
  ℓ : Level
  A B C : Set ℓ
  x y z : A

cong : (f : A → B) → x ≐ y → f x ≐ f y
cong f refl = refl

data ℤ : Set where
  zero : ℤ
  pred suc : ℤ → ℤ

postulate
  pred-suc : (x : ℤ) → pred (suc x) ≐ x
  suc-pred : (x : ℤ) → suc (pred x) ≐ x

{-# REWRITE pred-suc suc-pred #-}

_+_ : ℤ → ℤ → ℤ
zero   + y = y
pred x + y = pred (x + y)
suc x  + y = suc (x + y)

-_ : ℤ → ℤ
- zero = zero
- pred x = suc (- x)
- suc x = pred (- x)

data ℤ′ : Set where
  +[_]   : ℕ → ℤ′
  -[1+_] : ℕ → ℤ′

suc′ : ℤ′ → ℤ′
suc′ +[ x ] = +[ suc x ]
suc′ -[1+ zero ] = +[ zero ]
suc′ -[1+ suc x ] = -[1+ x ]

pred′ : ℤ′ → ℤ′
pred′ +[ zero ] = -[1+ zero ]
pred′ +[ suc x ] = +[ x ]
pred′ -[1+ x ] = -[1+ suc x ]

suc-pred′ : suc′ (pred′ x) ≐ x
suc-pred′ {+[ zero ]} = refl
suc-pred′ {+[ suc x ]} = refl
suc-pred′ { -[1+ x ]} = refl

pred-suc′ : pred′ (suc′ x) ≐ x
pred-suc′ {+[ x ]} = refl
pred-suc′ { -[1+ zero ]} = refl
pred-suc′ { -[1+ suc x ]} = refl

{-# REWRITE suc-pred′ pred-suc′ #-}

norm : ℤ → ℤ′
norm zero = +[ 0 ]
norm (pred x) = pred′ (norm x)
norm (suc x) = suc′ (norm x)

free : ℤ′ → ℤ
free +[ zero ] = zero
free +[ suc x ] = suc (free +[ x ])
free -[1+ zero ] = pred zero
free -[1+ suc x ] = pred (free -[1+ x ])

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Nat
open import Prelude
open import core

module judgemental-inconsistency where
  data incon : τ̇ → τ̇ → Set where
    ICNumArr1 : {t1 t2 : τ̇} → incon num (t1 ==> t2)
    ICNumArr2 : {t1 t2 : τ̇} → incon (t1 ==> t2) num
    ICArr1 : {t1 t2 t3 t4 : τ̇} →
               incon t1 t3 →
               incon (t1 ==> t2) (t3 ==> t4)
    ICArr2 : {t1 t2 t3 t4 : τ̇} →
               incon t2 t4 →
               incon (t1 ==> t2) (t3 ==> t4)

  -- inconsistency is symmetric
  inconsym : ∀ {t1 t2} → incon t1 t2 → incon t2 t1
  inconsym ICNumArr1 = ICNumArr2
  inconsym ICNumArr2 = ICNumArr1
  inconsym (ICArr1 x) = ICArr1 (inconsym x)
  inconsym (ICArr2 x) = ICArr2 (inconsym x)

  --inconsistency isn't reflexive
  incon-nrefl : ∀{t} → incon t t → ⊥
  incon-nrefl (ICArr1 x) = incon-nrefl x
  incon-nrefl (ICArr2 x) = incon-nrefl x

  -- first half of iso
  to~̸ : (t1 t2 : τ̇) → incon t1 t2 → t1 ~̸ t2
  to~̸ .num ._ ICNumArr1 ()
  to~̸ ._ .num ICNumArr2 ()
  to~̸ ._ ._ (ICArr1 incon) TCRefl = abort (incon-nrefl incon)
  to~̸ ._ ._ (ICArr1 incon) (TCArr x x₁) = to~̸ _ _ incon x
  to~̸ ._ ._ (ICArr2 incon) TCRefl = abort (incon-nrefl incon)
  to~̸ ._ ._ (ICArr2 incon) (TCArr x x₁) = (to~̸ _ _ incon x₁)

  -- second half of iso
  from~̸ : (t1 t2 : τ̇) → t1 ~̸ t2 → incon t1 t2
  from~̸ num (t2 ==> t3) ncon = ICNumArr1
  from~̸ (t1 ==> t2) num ncon = ICNumArr2
  from~̸ (t1 ==> t2) (t3 ==> t4) ncon with ~dec t1 t3
  ... | Inl qq = ICArr2 (from~̸ t2 t4 (λ x → ncon (TCArr qq x)))
  ... | Inr qq = ICArr1 (from~̸ _ _ qq)
  -- the remaining consistent types all lead to absurdities
  from~̸ num num ncon = abort (ncon TCRefl)
  from~̸ num ⦇-⦈ ncon = abort (ncon TCHole1)
  from~̸ ⦇-⦈ num ncon = abort (ncon TCHole2)
  from~̸ ⦇-⦈ ⦇-⦈ ncon = abort (ncon TCRefl)
  from~̸ ⦇-⦈ (t2 ==> t3) ncon = abort (ncon TCHole2)
  from~̸ (t1 ==> t2) ⦇-⦈ ncon = abort (ncon TCHole1)

  -- need to display that at least one of the round-trips above is stable
  -- for this to be structure preserving and really an iso.
  rt1 : (t1 t2 : τ̇) → (x : t1 ~̸ t2) → (to~̸ t1 t2 (from~̸ t1 t2 x)) == x
  rt1 num (t2 ==> t3) x         = funext (λ x₁ → abort (x x₁))
  rt1 (t1 ==> t2) num x         = funext (λ x₁ → abort (x x₁))
  rt1 (t1 ==> t2) (t3 ==> t4) x = funext (λ x₁ → abort (x x₁))
  rt1 num num x                 = abort (x TCRefl)
  rt1 num ⦇-⦈ x                  = abort (x TCHole1)
  rt1 ⦇-⦈ num x                  = abort (x TCHole2)
  rt1 ⦇-⦈ ⦇-⦈ x                   = abort (x TCRefl)
  rt1 ⦇-⦈ (t2 ==> t3) x          = abort (x TCHole2)
  rt1 (t1 ==> t2) ⦇-⦈ x          = abort (x TCHole1)

  -- if inconsistency at arrows is proof-irrelevant, then all of
  -- inconsistency is proof-irrelevant
  incon-irrelev : (arr-incon-irrelev : {t1 t2 t3 t4 : τ̇} (x y : incon (t1 ==> t2) (t3 ==> t4)) → x == y) →
                (t1 t2 : τ̇) (x y : incon t1 t2) → x == y
  incon-irrelev arr-incon-irrelev .num _ ICNumArr1 ICNumArr1 = refl
  incon-irrelev arr-incon-irrelev _ .num ICNumArr2 ICNumArr2 = refl
  incon-irrelev arr-incon-irrelev _ _ (ICArr1 x) (ICArr1 y) = ap1 ICArr1 (incon-irrelev arr-incon-irrelev _ _ x y)
  incon-irrelev arr-incon-irrelev _ _ (ICArr1 x) (ICArr2 y) = arr-incon-irrelev (ICArr1 x) (ICArr2 y)
  incon-irrelev arr-incon-irrelev _ _ (ICArr2 x) (ICArr1 y) = arr-incon-irrelev (ICArr2 x) (ICArr1 y)
  incon-irrelev arr-incon-irrelev _ _ (ICArr2 x) (ICArr2 y) = ap1 ICArr2 (incon-irrelev arr-incon-irrelev _ _ x y )

  -- if inconsistency at arrows is proof-irrelevant, then the round trip is
  -- stable up to equality
  rt2 : (arr-incon-irrelev : {t1 t2 t3 t4 : τ̇} (x y : incon (t1 ==> t2) (t3 ==> t4)) → x == y) →
        (t1 t2 : τ̇) → (x : incon t1 t2) → (from~̸ t1 t2 (to~̸ t1 t2 x)) == x
  rt2 arr-incon-irrelev .num _ ICNumArr1 = refl
  rt2 arr-incon-irrelev _ .num ICNumArr2 = refl
  rt2 arr-incon-irrelev (t1 ==> t2) (t3 ==> t4) (ICArr1 x) with ~dec t1 t3
  rt2 arr-incon-irrelev (t1 ==> t2) (t3 ==> t4) (ICArr1 x₁) | Inl x = abort (to~̸ t1 t3 x₁ x)
  rt2 arr-incon-irrelev (t1 ==> t2) (t3 ==> t4) (ICArr1 x₁) | Inr x = ap1 ICArr1 (incon-irrelev arr-incon-irrelev t1 t3 (from~̸ t1 t3 x) x₁)
  rt2 arr-incon-irrelev (t1 ==> t2) (t3 ==> t4) (ICArr2 x) with ~dec t1 t3
  rt2 arr-incon-irrelev (t1 ==> t2) (t3 ==> t4) (ICArr2 x₁) | Inl x = ap1 ICArr2 (incon-irrelev arr-incon-irrelev t2 t4 (from~̸ t2 t4 (to~̸ t2 t4 x₁)) x₁)
  rt2 arr-incon-irrelev (t1 ==> t2) (t3 ==> t4) (ICArr2 x₁) | Inr x = arr-incon-irrelev (ICArr1 (from~̸ t1 t3 x)) (ICArr2 x₁)

  -- if inconsistency at arrows is proof-irrelevant, then the two
  -- defintions of inconsistency are isomorphic
  incon-iso : (arr-incon-irrelev : {t1 t2 t3 t4 : τ̇} (x y : incon (t1 ==> t2) (t3 ==> t4)) → x == y)
                                   → (t1 t2 : τ̇) → (incon t1 t2) ≃ (t1 ~̸ t2)
  incon-iso arr-incon-irrelev t1 t2 = (to~̸ t1 t2) , (from~̸ t1 t2) , (rt2 arr-incon-irrelev t1 t2) , (rt1 t1 t2)


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

open import HoTT

open import stash.modalities.Orthogonality

module stash.modalities.NullifyFamily where

  module _ {ℓ} {I : Type ℓ} (X : I → Type ℓ) (A : Type ℓ) where

    private

      data #NullifyAll : Type ℓ where
        #inj : A → #NullifyAll
        #apex : (i : I) → (X i → #NullifyAll) → #NullifyAll

    NullifyAll : Type ℓ
    NullifyAll = #NullifyAll

    inj : A → NullifyAll
    inj = #inj

    apex : (i : I) → (X i → #NullifyAll) → #NullifyAll
    apex = #apex

    postulate
      apex-path : (i : I) (α : X i → NullifyAll) (x : X i) → apex i α == α x
      apex-cst : (i : I) (n : NullifyAll) → apex i (λ _ → n) == n
      apex-adj : (i : I) (n : NullifyAll) → ap (Δ NullifyAll (X i)) (apex-cst i n) == λ= (apex-path i (Δ NullifyAll (X i) n))

    module NullifyAllElim (Q : NullifyAll → Type ℓ) (is-null : ⟦ X ⊥ Q ⟧) (φ : Π A (Q ∘ inj)) where

      f : Π NullifyAll Q
      f (#inj a) = φ a
      f (#apex i α) = is-equiv.g (is-null i (#apex i α)) α'

         where α' : X i → Q (#apex i α)
               α' x = transport! Q (apex-path i α x) (f (α x))

  module _ {ℓ} {I : Type ℓ} (X : I → Type ℓ) where

    nullify-is-null : (A : Type ℓ) → ⟦ X ⊥ NullifyAll X A ⟧ₗ
    is-equiv.g (nullify-is-null A i) = apex X A i
    is-equiv.f-g (nullify-is-null A i) α = λ= (λ x → apex-path X A i α x)
    is-equiv.g-f (nullify-is-null A i) = apex-cst X A i
    is-equiv.adj (nullify-is-null A i) = apex-adj X A i

    open Modality

    NullifyAllModality : Modality ℓ
    is-local NullifyAllModality A = ⟦ X ⊥ A ⟧ₗ
    is-local-is-prop NullifyAllModality {A} = Π-level (λ i → is-equiv-is-prop)
    ◯ NullifyAllModality A = NullifyAll X A
    ◯-is-local NullifyAllModality {A} = nullify-is-null A
    η NullifyAllModality {A} = inj X A
    ◯-elim NullifyAllModality Q Q-is-null φ = NullifyAllElim.f X _ Q (λ i n → Q-is-null n i) φ
    ◯-elim-β NullifyAllModality Q Q-is-null φ a = idp
    ◯-== NullifyAllModality {A} a₀ a₁ i = is-eq _ squash inv-l inv-r

      where a₀' : NullifyAll X A
            a₀' = apex X A i (λ _ → a₀)

            a₁' : NullifyAll X A
            a₁' = apex X A i (λ _ → a₁)

            squash : (X i → a₀ == a₁) → a₀ == a₁
            squash φ = ! (apex-cst X A i a₀) ∙ cyl ∙ apex-cst X A i a₁

              where cyl : a₀' == a₁'
                    cyl = ap (apex X A i) (λ= φ)

            inv-l : (φ : X i → a₀ == a₁) → (λ _ → squash φ) == φ
            inv-l φ = {!!}

            inv-r : (p : a₀ == a₁) → squash (λ _ → p) == p
            inv-r p = {!!}

            -- Main idea is to use this coherence ... (and possibly the other adjoint as well)
            -- apex-adj : (i : I) (n : NullifyAll) → ap (Δ NullifyAll (X i)) (apex-cst i n) == λ= (apex-path i (Δ NullifyAll (X i) n))

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
open import Data.Bool using ( Bool ; true ; false ; if_then_else_ )
open import Data.Empty using ( ⊥-elim )
open import Data.Product using ( _×_ ; _,_ )
open import Data.Sum using ( inj₁ ; inj₂ )
open import Relation.Unary using ( _∈_ ; _∉_ )
open import Web.Semantic.DL.Concept using ( neg )
open import Web.Semantic.DL.Concept.Model using ( _⟦_⟧₁ ; neg-sound )
open import Web.Semantic.DL.Concept.Skolemization using
  ( CSkolems ; cskolem ; cskolem-sound )
open import Web.Semantic.DL.FOL using
  ( Formula ; true ; false ; _∧_ ; _∈₁_ ; _∈₂_ ; _∼_ ; ∀₁ )
open import Web.Semantic.DL.FOL.Model using ( _⊨f_ )
open import Web.Semantic.DL.Role.Skolemization using
  ( rskolem ; rskolem⇒ ; rskolem-sound ; rskolem⇒-sound )
open import Web.Semantic.DL.Role.Model using ( _⟦_⟧₂ )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using
  ( TBox ; ε ; _,_ ;_⊑₁_ ; _⊑₂_ ; Dis ; Ref ; Irr ; Tra )
open import Web.Semantic.DL.TBox.Model using ( _⊨t_ )
open import Web.Semantic.Util using ( True ; tt )

module Web.Semantic.DL.TBox.Skolemization {Σ : Signature} where

TSkolems : Set → TBox Σ → Set
TSkolems Δ ε = True
TSkolems Δ (T , U) = (TSkolems Δ T) × (TSkolems Δ U)
TSkolems Δ (C ⊑₁ D) = (Δ → Bool) × (CSkolems Δ (neg C)) × (CSkolems Δ D)
TSkolems Δ (Q ⊑₂ R) = True
TSkolems Δ (Dis Q R) = True
TSkolems Δ (Ref R) = True
TSkolems Δ (Irr R) = True
TSkolems Δ (Tra R) = True

tskolem : ∀ {Δ} T → (TSkolems Δ T) → Formula Σ Δ
tskolem ε Φ = true
tskolem (T , U) (Φ , Ψ) = (tskolem T Φ) ∧ (tskolem U Ψ)
tskolem (C ⊑₁ D) (φ , Φ , Ψ) = ∀₁ λ x →
  if (φ x) then (cskolem (neg C) Φ x) else (cskolem D Ψ x)
tskolem (Q ⊑₂ R) Φ = ∀₁ λ x → ∀₁ λ y →
  rskolem⇒ Q x y (rskolem R x y)
tskolem (Dis Q R) Φ = ∀₁ λ x → ∀₁ λ y →
  rskolem⇒ Q x y (rskolem⇒ R x y false)
tskolem (Ref R) Φ = ∀₁ λ x →
  rskolem R x x
tskolem (Irr R) Φ = ∀₁ λ x →
  rskolem⇒ R x x false
tskolem (Tra R) Φ = ∀₁ λ x → ∀₁ λ y → ∀₁ λ z →
  rskolem⇒ R x y (rskolem⇒ R y z (rskolem R x z))

tskolem-sound : ∀ I T Φ → (I ⊨f tskolem T Φ) → (I ⊨t T)
tskolem-sound I ε Φ _ = tt
tskolem-sound I (T , U) (Φ , Ψ) (I⊨T , I⊨U) =
  (tskolem-sound I T Φ I⊨T , tskolem-sound I U Ψ I⊨U)
tskolem-sound I (C ⊑₁ D) (φ , Φ , Ψ) I⊨C⊑D = lemma where
  lemma : ∀ {x} → (x ∈ I ⟦ C ⟧₁) → (x ∈ I ⟦ D ⟧₁)
  lemma {x} x∈⟦C⟧ with φ x | I⊨C⊑D x
  lemma {x} x∈⟦C⟧ | true  | x∈⟦¬C⟧ =
    ⊥-elim (neg-sound I C (cskolem-sound I (neg C) Φ x x∈⟦¬C⟧) x∈⟦C⟧)
  lemma {x} x∈⟦C⟧ | false | x∈⟦D⟧  =
    cskolem-sound I D Ψ x x∈⟦D⟧
tskolem-sound I (Q ⊑₂ R) Φ I⊨Q⊑R = lemma where
  lemma : ∀ {xy} → (xy ∈ I ⟦ Q ⟧₂) → (xy ∈ I ⟦ R ⟧₂)
  lemma {x , y} xy∈⟦Q⟧ =
    rskolem-sound I R x y (rskolem⇒-sound I Q x y _ (I⊨Q⊑R x y) xy∈⟦Q⟧)
tskolem-sound I (Dis Q R) Φ I⊨DisQR = lemma where
  lemma : ∀ {xy} → (xy ∈ I ⟦ Q ⟧₂) → (xy ∉ I ⟦ R ⟧₂)
  lemma {x , y} xy∈⟦Q⟧ =
    rskolem⇒-sound I R x y _ (rskolem⇒-sound I Q x y _ (I⊨DisQR x y) xy∈⟦Q⟧)
tskolem-sound I (Ref R) Φ I⊨RefR = λ x → rskolem-sound I R x x (I⊨RefR x)
tskolem-sound I (Irr R) Φ I⊨IrrR = λ x → rskolem⇒-sound I R x x _ (I⊨IrrR x)
tskolem-sound I (Tra R) Φ I⊨TraR =
  λ {x} {y} {z} xy∈⟦R⟧ yz∈⟦R⟧ → rskolem-sound I R x z
    (rskolem⇒-sound I R y z _ (rskolem⇒-sound I R x y _ (I⊨TraR x y z) xy∈⟦R⟧) yz∈⟦R⟧)

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


text:
module examplesPaperJFP.CatTerm where

open import examplesPaperJFP.BasicIO hiding (main)
open import examplesPaperJFP.Console hiding (main)
open import examplesPaperJFP.NativeIOSafe

cat : IO ConsoleInterface Unit
force cat =
  exec′ getLine          λ{ nothing → return unit ; (just line) → delay (
  exec′ (putStrLn line)  λ _     →
  cat                  )}

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda