text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommAlgebra.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.SIP

open import Cubical.Data.Sigma

open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.Ring
open import Cubical.Algebra.Algebra

open import Cubical.Displayed.Base
open import Cubical.Displayed.Auto
open import Cubical.Displayed.Record
open import Cubical.Displayed.Universe

open import Cubical.Reflection.RecordEquiv

private
  variable
    ℓ ℓ' : Level

record IsCommAlgebra (R : CommRing ℓ) {A : Type ℓ'}
                     (0a : A) (1a : A)
                     (_+_ : A → A → A) (_·_ : A → A → A) (-_ : A → A)
                     (_⋆_ : ⟨ R ⟩ → A → A) : Type (ℓ-max ℓ ℓ') where

  constructor iscommalgebra

  field
    isAlgebra : IsAlgebra (CommRing→Ring R) 0a 1a _+_ _·_ -_ _⋆_
    ·-comm    : (x y : A) → x · y ≡ y · x

  open IsAlgebra isAlgebra public

unquoteDecl IsCommAlgebraIsoΣ = declareRecordIsoΣ IsCommAlgebraIsoΣ (quote IsCommAlgebra)

record CommAlgebraStr (R : CommRing ℓ) (A : Type ℓ') : Type (ℓ-max ℓ ℓ') where

  constructor commalgebrastr

  field
    0a             : A
    1a             : A
    _+_            : A → A → A
    _·_            : A → A → A
    -_             : A → A
    _⋆_            : ⟨ R ⟩ → A → A
    isCommAlgebra      : IsCommAlgebra R 0a 1a _+_ _·_ -_ _⋆_

  open IsCommAlgebra isCommAlgebra public

  infix  8 -_
  infixl 7 _·_
  infixl 7 _⋆_
  infixl 6 _+_

CommAlgebra : (R : CommRing ℓ) → ∀ ℓ' → Type (ℓ-max ℓ (ℓ-suc ℓ'))
CommAlgebra R ℓ' = Σ[ A ∈ Type ℓ' ] CommAlgebraStr R A

module _ {R : CommRing ℓ} where
  open CommRingStr (snd R) using (1r) renaming (_+_ to _+r_; _·_ to _·s_)

  CommAlgebraStr→AlgebraStr : {A : Type ℓ'} → CommAlgebraStr R A → AlgebraStr (CommRing→Ring R) A
  CommAlgebraStr→AlgebraStr (commalgebrastr _ _ _ _ _ _ (iscommalgebra isAlgebra ·-comm)) =
    algebrastr _ _ _ _ _ _ isAlgebra

  CommAlgebra→Algebra : (A : CommAlgebra R ℓ') → Algebra (CommRing→Ring R) ℓ'
  CommAlgebra→Algebra (_ , str) = (_ , CommAlgebraStr→AlgebraStr str)

  CommAlgebra→CommRing : (A : CommAlgebra R ℓ') → CommRing ℓ'
  CommAlgebra→CommRing (_ , commalgebrastr  _ _ _ _ _ _ (iscommalgebra isAlgebra ·-comm)) =
    _ , commringstr _ _ _ _ _ (iscommring (IsAlgebra.isRing isAlgebra) ·-comm)

  isSetCommAlgebra : (A : CommAlgebra R ℓ') → isSet ⟨ A ⟩
  isSetCommAlgebra A = isSetAlgebra (CommAlgebra→Algebra A)

  makeIsCommAlgebra : {A : Type ℓ'} {0a 1a : A}
                      {_+_ _·_ : A → A → A} { -_ : A → A} {_⋆_ : ⟨ R ⟩ → A → A}
                      (isSet-A : isSet A)
                      (+-assoc :  (x y z : A) → x + (y + z) ≡ (x + y) + z)
                      (+-rid : (x : A) → x + 0a ≡ x)
                      (+-rinv : (x : A) → x + (- x) ≡ 0a)
                      (+-comm : (x y : A) → x + y ≡ y + x)
                      (·-assoc :  (x y z : A) → x · (y · z) ≡ (x · y) · z)
                      (·-lid : (x : A) → 1a · x ≡ x)
                      (·-ldist-+ : (x y z : A) → (x + y) · z ≡ (x · z) + (y · z))
                      (·-comm : (x y : A) → x · y ≡ y · x)
                      (⋆-assoc : (r s : ⟨ R ⟩) (x : A) → (r ·s s) ⋆ x ≡ r ⋆ (s ⋆ x))
                      (⋆-ldist : (r s : ⟨ R ⟩) (x : A) → (r +r s) ⋆ x ≡ (r ⋆ x) + (s ⋆ x))
                      (⋆-rdist : (r : ⟨ R ⟩) (x y : A) → r ⋆ (x + y) ≡ (r ⋆ x) + (r ⋆ y))
                      (⋆-lid   : (x : A) → 1r ⋆ x ≡ x)
                      (⋆-lassoc : (r : ⟨ R ⟩) (x y : A) → (r ⋆ x) · y ≡ r ⋆ (x · y))
                    → IsCommAlgebra R 0a 1a _+_ _·_ -_ _⋆_
  makeIsCommAlgebra {A = A} {0a} {1a} {_+_} {_·_} { -_} {_⋆_} isSet-A
                    +-assoc +-rid +-rinv +-comm
                    ·-assoc ·-lid ·-ldist-+ ·-comm
                    ⋆-assoc ⋆-ldist ⋆-rdist ⋆-lid ⋆-lassoc
   = iscommalgebra
     (makeIsAlgebra
       isSet-A
       +-assoc +-rid +-rinv +-comm
       ·-assoc
         (λ x → x · 1a ≡⟨ ·-comm _ _ ⟩ 1a · x ≡⟨ ·-lid _ ⟩ x ∎)
         ·-lid
         (λ x y z → x · (y + z)       ≡⟨ ·-comm _ _ ⟩
                    (y + z) · x       ≡⟨ ·-ldist-+ _ _ _ ⟩
                    (y · x) + (z · x) ≡⟨ cong (λ u → (y · x) + u) (·-comm _ _) ⟩
                    (y · x) + (x · z) ≡⟨ cong (λ u → u + (x · z)) (·-comm _ _) ⟩
                    (x · y) + (x · z) ∎)
         ·-ldist-+
       ⋆-assoc
         ⋆-ldist
         ⋆-rdist
         ⋆-lid
         ⋆-lassoc
         λ r x y → r ⋆ (x · y) ≡⟨ cong (λ u → r ⋆ u) (·-comm _ _) ⟩
                   r ⋆ (y · x) ≡⟨ sym (⋆-lassoc _ _ _) ⟩
                   (r ⋆ y) · x ≡⟨ ·-comm _ _ ⟩
                   x · (r ⋆ y) ∎)
     ·-comm

  module _ (S : CommRing ℓ) where
    open CommRingStr (snd S) renaming (1r to 1S)
    open CommRingStr (snd R) using () renaming (_·_ to _·R_; _+_ to _+R_; 1r to 1R)
    commAlgebraFromCommRing :
          (_⋆_ : fst R → fst S → fst S)
        → ((r s : fst R) (x : fst S) → (r ·R s) ⋆ x ≡ r ⋆ (s ⋆ x))
        → ((r s : fst R) (x : fst S) → (r +R s) ⋆ x ≡ (r ⋆ x) + (s ⋆ x))
        → ((r : fst R) (x y : fst S) → r ⋆ (x + y) ≡ (r ⋆ x) + (r ⋆ y))
        → ((x : fst S) → 1R ⋆ x ≡ x)
        → ((r : fst R) (x y : fst S) → (r ⋆ x) · y ≡ r ⋆ (x · y))
        → CommAlgebra R ℓ
    commAlgebraFromCommRing _⋆_ ·Assoc⋆ ⋆DistR ⋆DistL ⋆Lid ⋆Assoc· = fst S ,
      commalgebrastr 0r 1S _+_ _·_  -_ _⋆_
        (makeIsCommAlgebra is-set +Assoc +Rid +Rinv +Comm ·Assoc ·Lid ·Ldist+ ·Comm
                                  ·Assoc⋆ ⋆DistR ⋆DistL ⋆Lid ⋆Assoc·)

  IsCommAlgebraEquiv : {A B : Type ℓ'}
    (M : CommAlgebraStr R A) (e : A ≃ B) (N : CommAlgebraStr R B)
    → Type (ℓ-max ℓ ℓ')
  IsCommAlgebraEquiv M e N =
    IsAlgebraHom (CommAlgebraStr→AlgebraStr M) (e .fst) (CommAlgebraStr→AlgebraStr N)

  CommAlgebraEquiv : (M N : CommAlgebra R ℓ') → Type (ℓ-max ℓ ℓ')
  CommAlgebraEquiv M N = Σ[ e ∈ ⟨ M ⟩ ≃ ⟨ N ⟩ ] IsCommAlgebraEquiv (M .snd) e (N .snd)

  IsCommAlgebraHom : {A B : Type ℓ'}
    (M : CommAlgebraStr R A) (f : A → B) (N : CommAlgebraStr R B)
    → Type (ℓ-max ℓ ℓ')
  IsCommAlgebraHom M f N =
    IsAlgebraHom (CommAlgebraStr→AlgebraStr M) f (CommAlgebraStr→AlgebraStr N)

  CommAlgebraHom : (M N : CommAlgebra R ℓ') → Type (ℓ-max ℓ ℓ')
  CommAlgebraHom M N = Σ[ f ∈ (⟨ M ⟩ → ⟨ N ⟩) ] IsCommAlgebraHom (M .snd) f (N .snd)

  module _ {M N : CommAlgebra R ℓ'} where
    open CommAlgebraStr {{...}}
    open IsAlgebraHom
    private
      instance
        _ = snd M
        _ = snd N

    makeCommAlgebraHom : (f : fst M → fst N)
                           → (fPres1 : f 1a ≡ 1a)
                           → (fPres+ : (x y : fst M) → f (x + y) ≡ f x + f y)
                           → (fPres· : (x y : fst M) → f (x · y) ≡ f x · f y)
                           → (fPres⋆ : (r : fst R) (x : fst M) → f (r ⋆ x) ≡ r ⋆ f x)
                           → CommAlgebraHom M N
    makeCommAlgebraHom f fPres1 fPres+ fPres· fPres⋆ = f , isHom
      where fPres0 =
                    f 0a                  ≡⟨ sym (+-rid _) ⟩
                    f 0a + 0a             ≡⟨ cong (λ u → f 0a + u) (sym (+-rinv (f 0a))) ⟩
                    f 0a + (f 0a - f 0a)  ≡⟨ +-assoc (f 0a) (f 0a) (- f 0a) ⟩
                    (f 0a + f 0a) - f 0a  ≡⟨ cong (λ u → u - f 0a) (sym (fPres+ 0a 0a)) ⟩
                    f (0a + 0a) - f 0a    ≡⟨ cong (λ u → f u - f 0a) (+-lid 0a) ⟩
                    f 0a - f 0a           ≡⟨ +-rinv (f 0a) ⟩
                    0a ∎

            isHom : IsCommAlgebraHom (snd M) f (snd N)
            pres0 isHom = fPres0
            pres1 isHom = fPres1
            pres+ isHom = fPres+
            pres· isHom = fPres·
            pres- isHom = (λ x →
                               f (- x) ≡⟨ sym (+-rid _) ⟩
                               (f (- x) + 0a) ≡⟨ cong (λ u → f (- x) + u) (sym (+-rinv (f x))) ⟩
                               (f (- x) + (f x - f x)) ≡⟨ +-assoc _ _ _ ⟩
                               ((f (- x) + f x) - f x) ≡⟨ cong (λ u → u - f x) (sym (fPres+ _ _)) ⟩
                               (f ((- x) + x) - f x) ≡⟨ cong (λ u → f u - f x) (+-linv x) ⟩
                               (f 0a - f x) ≡⟨ cong (λ u → u - f x) fPres0 ⟩
                               (0a - f x) ≡⟨ +-lid _ ⟩ (- f x) ∎)
            pres⋆ isHom = fPres⋆

    isPropIsCommAlgebraHom : (f : fst M → fst N) → isProp (IsCommAlgebraHom (snd M) f (snd N))
    isPropIsCommAlgebraHom f = isPropIsAlgebraHom
                                 (CommRing→Ring R)
                                 (snd (CommAlgebra→Algebra M))
                                 f
                                 (snd (CommAlgebra→Algebra N))

isPropIsCommAlgebra : (R : CommRing ℓ) {A : Type ℓ'}
  (0a 1a : A)
  (_+_ _·_ : A → A → A)
  (-_ : A → A)
  (_⋆_ : ⟨ R ⟩ → A → A)
  → isProp (IsCommAlgebra R 0a 1a _+_ _·_ -_ _⋆_)
isPropIsCommAlgebra R _ _ _ _ _ _ =
  isOfHLevelRetractFromIso 1 IsCommAlgebraIsoΣ
    (isPropΣ (isPropIsAlgebra _ _ _ _ _ _ _)
      (λ alg → isPropΠ2 λ _ _ → alg .IsAlgebra.is-set _ _))

𝒮ᴰ-CommAlgebra : (R : CommRing ℓ) → DUARel (𝒮-Univ ℓ') (CommAlgebraStr R) (ℓ-max ℓ ℓ')
𝒮ᴰ-CommAlgebra R =
  𝒮ᴰ-Record (𝒮-Univ _) (IsCommAlgebraEquiv {R = R})
    (fields:
      data[ 0a ∣ nul ∣ pres0 ]
      data[ 1a ∣ nul ∣ pres1 ]
      data[ _+_ ∣ bin ∣ pres+ ]
      data[ _·_ ∣ bin ∣ pres· ]
      data[ -_ ∣ autoDUARel _ _ ∣ pres- ]
      data[ _⋆_ ∣ autoDUARel _ _ ∣ pres⋆ ]
      prop[ isCommAlgebra ∣ (λ _ _ → isPropIsCommAlgebra _ _ _ _ _ _ _) ])
  where
  open CommAlgebraStr
  open IsAlgebraHom

  -- faster with some sharing
  nul = autoDUARel (𝒮-Univ _) (λ A → A)
  bin = autoDUARel (𝒮-Univ _) (λ A → A → A → A)

CommAlgebraPath : (R : CommRing ℓ) → (A B : CommAlgebra R ℓ') → (CommAlgebraEquiv A B) ≃ (A ≡ B)
CommAlgebraPath R = ∫ (𝒮ᴰ-CommAlgebra R) .UARel.ua

isGroupoidCommAlgebra : {R : CommRing ℓ} → isGroupoid (CommAlgebra R ℓ')
isGroupoidCommAlgebra A B = isOfHLevelRespectEquiv 2 (CommAlgebraPath _ _ _) (isSetAlgebraEquiv _ _)


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

module Definition.Conversion.EqRelInstance where

open import Definition.Untyped
open import Definition.Untyped.Properties using (wkSingleSubstId)
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.Weakening using (_∷_⊆_; wkEq; step; id)
open import Definition.Conversion
open import Definition.Conversion.Reduction
open import Definition.Conversion.Universe
open import Definition.Conversion.Stability
open import Definition.Conversion.Soundness
open import Definition.Conversion.Lift
open import Definition.Conversion.Conversion
open import Definition.Conversion.Transitivity
open import Definition.Conversion.Weakening
open import Definition.Conversion.Whnf
open import Definition.Typed.EqualityRelation
open import Definition.Typed.Consequences.Syntactic
open import Definition.Typed.Consequences.Substitution
open import Definition.Typed.Consequences.Injectivity
open import Definition.Typed.Consequences.Equality
open import Definition.Typed.Consequences.Reduction
open import Definition.Conversion.Symmetry

open import Tools.Nat
open import Tools.Product
import Tools.PropositionalEquality as PE
open import Tools.Function

-- Algorithmic equality of neutrals with injected conversion.
data _⊢_~_∷_^_ (Γ : Con Term) (k l A : Term) (r : TypeInfo) : Set where
  ↑ : ∀ {B} → Γ ⊢ A ≡ B ^ r → Γ ⊢ k ~ l ↑ B ^ r → Γ ⊢ k ~ l ∷ A ^ r

-- Properties of algorithmic equality of neutrals with injected conversion.

~-var : ∀ {x A r Γ} → Γ ⊢ var x ∷ A ^ r → Γ ⊢ var x ~ var x ∷ A ^ r
~-var x =
  let ⊢A = syntacticTerm x
  in  ↑ (refl ⊢A) (var-refl′ x)

~-app : ∀ {f g a b F G Γ rF lF lG lΠ}
      → Γ ⊢ f ~ g ∷ Π F ^ rF ° lF ▹ G ° lG ° lΠ ^ [ ! , ι lΠ ]
      → Γ ⊢ a [genconv↑] b ∷ F ^ [ rF , ι lF ]
      → Γ ⊢ f ∘ a ^ lΠ ~ g ∘ b ^ lΠ ∷ G [ a ] ^ [ ! , ι lG ]
~-app {rF = !} (↑ A≡B (~↑! x)) x₁ =
  let _ , ⊢B = syntacticEq A≡B
      B′ , whnfB′ , D = whNorm ⊢B
      ΠFG≡B′ = trans A≡B (subset* (red D))
      H , E , B≡ΠHE = Π≡A ΠFG≡B′ whnfB′
      F≡H , _ , _ , _ , G≡E = injectivity (PE.subst (λ x → _ ⊢ _ ≡ x ^ _) B≡ΠHE ΠFG≡B′)
      _ , ⊢f , _ = syntacticEqTerm (soundnessConv↑Term x₁)
  in  ↑ (substTypeEq G≡E (refl ⊢f))
        (app-cong′  (PE.subst (λ x → _ ⊢ _ ~ _ ↓! x ^ _)
                       B≡ΠHE ([~] _ (red D) whnfB′ x))
             (convConvTerm x₁ F≡H))
~-app {rF = %} (↑ A≡B (~↑! x)) x₁ =
  let _ , ⊢B = syntacticEq A≡B
      B′ , whnfB′ , D = whNorm ⊢B
      ΠFG≡B′ = trans A≡B (subset* (red D))
      H , E , B≡ΠHE = Π≡A ΠFG≡B′ whnfB′
      F≡H , _ , _ , _ , G≡E = injectivity (PE.subst (λ x → _ ⊢ _ ≡ x ^ _) B≡ΠHE ΠFG≡B′)
      _ , ⊢f , _ = syntacticEqTerm (proj₂ (proj₂ (soundness~↑% x₁)))
  in  ↑ (substTypeEq G≡E (genRefl ⊢f))
        (app-cong′ (PE.subst (λ x → _ ⊢ _ ~ _ ↓! x ^ _)
                       B≡ΠHE ([~] _ (red D) whnfB′ x))
                   (conv~↑% x₁ F≡H))
~-natrec : ∀ {z z′ s s′ n n′ F F′ Γ lF}
         → (Γ ∙ ℕ ^ [ ! , ι ⁰ ]) ⊢ F [conv↑] F′ ^ [ ! , ι lF ]  →
      Γ ⊢ z [conv↑] z′ ∷ (F [ zero ]) ^ ι lF →
      Γ ⊢ s [conv↑] s′ ∷ (Π ℕ ^ ! ° ⁰ ▹ (F ^ ! ° lF ▹▹ F [ suc (var 0) ]↑ ° lF ° lF) ° lF ° lF) ^ ι lF →
      Γ ⊢ n ~ n′ ∷ ℕ ^ [ ! , ι ⁰ ] →
      Γ ⊢ natrec lF F z s n ~ natrec lF F′ z′ s′ n′ ∷ (F [ n ]) ^ [ ! , ι lF ]
~-natrec {n = n} {n′ = n′} x x₁ x₂ (↑ A≡B (~↑! x₄)) =
  let _ , ⊢B = syntacticEq A≡B
      B′ , whnfB′ , D = whNorm ⊢B
      ℕ≡B′ = trans A≡B (subset* (red D))
      B≡ℕ = ℕ≡A ℕ≡B′ whnfB′
      k~l′ = PE.subst (λ x → _ ⊢ n ~ n′ ↓! x ^ _) B≡ℕ
                      ([~] _ (red D) whnfB′ x₄)
      ⊢F , _ = syntacticEq (soundnessConv↑ x)
      _ , ⊢n , _ = syntacticEqTerm (soundness~↓! k~l′)
  in  ↑ (refl (substType ⊢F ⊢n)) (natrec-cong′ x x₁ x₂ k~l′)

~-Emptyrec : ∀ {e e' F F′ Γ l lEmpty}
         → Γ ⊢ F [conv↑] F′ ^ [ ! , ι l ] →
         Γ ⊢ e ∷ Empty lEmpty ^ [ % , ι lEmpty ] →
         Γ ⊢ e' ∷ Empty lEmpty ^ [ % , ι lEmpty ] →
         Γ ⊢ Emptyrec l lEmpty F e ~ Emptyrec l lEmpty F′ e' ∷ F ^ [ ! , ι l ]
~-Emptyrec {e = e} {e' = e'} x ⊢e ⊢e' =
  let k~l′ = %~↑ ⊢e ⊢e'
      ⊢F , _ = syntacticEq (soundnessConv↑ x)
  in  ↑ (refl ⊢F) (Emptyrec-cong′ x k~l′)

~-IdCong : ∀ {A A' : Term} {l : Level} {t t' u u' : Term} {Γ : Con Term} →
      Γ ⊢ A ~ A' ∷ Univ ! l ^ [ ! , next l ] →
      Γ ⊢ t [conv↑] t' ∷ A ^ ι l →
      Γ ⊢ u [conv↑] u' ∷ A ^ ι l →
      Γ ⊢ Id A t u ~ Id A' t' u' ∷ SProp l ^ [ ! , next l ]
~-IdCong (↑ A≡B (~↑! x)) t~t' u~u' =
     let ⊢Γ = wfEqTerm (soundnessConv↑Term t~t')
         _ , ⊢B = syntacticEq A≡B
         B′ , whnfB′ , D = whNorm ⊢B
         U≡B′ = trans A≡B (subset* (red D))
         B≡U = U≡A-whnf U≡B′ whnfB′
         A~A′ = PE.subst (λ x → _ ⊢ _ ~ _ ↓! x ^ _) B≡U
                      ([~] _ (red D) whnfB′ x)
     in ↑ (refl (Ugenⱼ ⊢Γ)) (~↑! (Id-cong A~A′ t~t' u~u'))

~-Idℕ : ∀ {t t' u u' : Term} {Γ : Con Term} →
    ⊢ Γ →
    Γ ⊢ t ~ t' ∷ ℕ ^ [ ! , ι ⁰ ] →
    Γ ⊢ u [genconv↑] u' ∷ ℕ ^ [ ! , ι ⁰ ] →
    Γ ⊢ Id ℕ t u ~ Id ℕ t' u' ∷ SProp ⁰ ^ [ ! , next ⁰ ]
~-Idℕ ⊢Γ (↑ A≡B (~↑! x)) u~u' =
     let _ , ⊢B = syntacticEq A≡B
         B′ , whnfB′ , D = whNorm ⊢B
         ℕ≡B′ = trans A≡B (subset* (red D))
         B≡ℕ = ℕ≡A ℕ≡B′ whnfB′
         t~t′ = PE.subst (λ x → _ ⊢ _ ~ _ ↓! x ^ _) B≡ℕ
                      ([~] _ (red D) whnfB′ x)
     in ↑ (refl (Ugenⱼ ⊢Γ)) (~↑! (Id-ℕ t~t′ u~u'))

~-Idℕ0 : ∀ {u u' : Term} {Γ : Con Term} →
    ⊢ Γ →
    Γ ⊢ u ~ u' ∷ ℕ ^ [ ! , ι ⁰ ] →
    Γ ⊢ Id ℕ zero u ~ Id ℕ zero u' ∷ SProp ⁰ ^ [ ! , next ⁰ ]
~-Idℕ0 ⊢Γ (↑ A≡B (~↑! x)) =
     let _ , ⊢B = syntacticEq A≡B
         B′ , whnfB′ , D = whNorm ⊢B
         ℕ≡B′ = trans A≡B (subset* (red D))
         B≡ℕ = ℕ≡A ℕ≡B′ whnfB′
         t~t′ = PE.subst (λ x → _ ⊢ _ ~ _ ↓! x ^ _) B≡ℕ
                      ([~] _ (red D) whnfB′ x)
     in ↑ (refl (Ugenⱼ ⊢Γ)) (~↑! (Id-ℕ0 t~t′))

~-IdℕS : ∀ {t t' u u' : Term} {Γ : Con Term} →
    ⊢ Γ →
    Γ ⊢ t [genconv↑] t' ∷ ℕ ^ [ ! , ι ⁰ ] →
    Γ ⊢ u ~ u' ∷ ℕ ^ [ ! , ι ⁰ ] →
    Γ ⊢ Id ℕ (suc t) u ~ Id ℕ (suc t') u' ∷ SProp ⁰ ^ [ ! , next ⁰ ]
~-IdℕS ⊢Γ X (↑ A≡B (~↑! x)) =
     let _ , ⊢B = syntacticEq A≡B
         B′ , whnfB′ , D = whNorm ⊢B
         ℕ≡B′ = trans A≡B (subset* (red D))
         B≡ℕ = ℕ≡A ℕ≡B′ whnfB′
         t~t′ = PE.subst (λ x → _ ⊢ _ ~ _ ↓! x ^ _) B≡ℕ
                      ([~] _ (red D) whnfB′ x)
     in ↑ (refl (Ugenⱼ ⊢Γ)) (~↑! (Id-ℕS X t~t′))

~-IdU : ∀ {t t' u u' : Term} {Γ : Con Term} →
    ⊢ Γ →
    Γ ⊢ t ~ t' ∷ U ⁰ ^ [ ! , next ⁰ ] →
    Γ ⊢ u [genconv↑] u' ∷ U ⁰ ^ [ ! , next ⁰ ] →
    Γ ⊢ Id (U ⁰) t u ~ Id (U ⁰) t' u' ∷ SProp ¹ ^ [ ! , next ¹ ]
~-IdU ⊢Γ (↑ A≡B (~↑! x)) X =
     let _ , ⊢B = syntacticEq A≡B
         B′ , whnfB′ , D = whNorm ⊢B
         U≡B′ = trans A≡B (subset* (red D))
         B≡U = U≡A-whnf U≡B′ whnfB′
         t~t′ = PE.subst (λ x → _ ⊢ _ ~ _ ↓! x ^ _) B≡U
                      ([~] _ (red D) whnfB′ x)
     in ↑ (refl (Ugenⱼ ⊢Γ)) (~↑! (Id-U t~t′ X))

~-IdUℕ : ∀ {u u' : Term} {Γ : Con Term} →
    ⊢ Γ →
    Γ ⊢ u ~ u' ∷ U ⁰ ^ [ ! , next ⁰ ] →
    Γ ⊢ Id (U ⁰) ℕ u ~ Id (U ⁰) ℕ u' ∷ SProp ¹ ^ [ ! , next ¹ ]
~-IdUℕ ⊢Γ (↑ A≡B (~↑! x)) =
     let _ , ⊢B = syntacticEq A≡B
         B′ , whnfB′ , D = whNorm ⊢B
         U≡B′ = trans A≡B (subset* (red D))
         B≡U = U≡A-whnf U≡B′ whnfB′
         t~t′ = PE.subst (λ x → _ ⊢ _ ~ _ ↓! x ^ _) B≡U
                      ([~] _ (red D) whnfB′ x)
     in ↑ (refl (Ugenⱼ ⊢Γ)) (~↑! (Id-Uℕ t~t′))

~-IdUΠ : ∀ {A : Term} {rA : Relevance} {B A' B' u u' : Term}
    {Γ : Con Term} →
    Γ ⊢ Π A ^ rA ° ⁰ ▹ B ° ⁰ ° ⁰ [genconv↑] Π A' ^ rA ° ⁰ ▹ B' ° ⁰ ° ⁰ ∷ U ⁰ ^ [ ! , next ⁰ ] →
    Γ ⊢ u ~ u' ∷ U ⁰ ^ [ ! , next ⁰ ] →
    Γ ⊢ Id (U ⁰) (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° ⁰) u ~
    Id (U ⁰) (Π A' ^ rA ° ⁰ ▹ B' ° ⁰ ° ⁰) u' ∷ SProp ¹ ^ [ ! , next ¹ ]
~-IdUΠ X (↑ A≡B (~↑! x)) =
     let ⊢Γ =  wfEqTerm (soundnessConv↑Term X)
         _ , ⊢B = syntacticEq A≡B
         B′ , whnfB′ , D = whNorm ⊢B
         U≡B′ = trans A≡B (subset* (red D))
         B≡U = U≡A-whnf U≡B′ whnfB′
         t~t′ = PE.subst (λ x → _ ⊢ _ ~ _ ↓! x ^ _) B≡U
                      ([~] _ (red D) whnfB′ x)
     in ↑ (refl (Ugenⱼ ⊢Γ)) (~↑! (Id-UΠ X t~t′))

~-castcong : ∀ {A A' B B' e e' t t' : Term} {Γ : Con Term} →
    Γ ⊢ A ~ A' ∷ U ⁰ ^ [ ! , next ⁰ ] →
    Γ ⊢ B [genconv↑] B' ∷ U ⁰ ^ [ ! , next ⁰ ] →
    Γ ⊢ t [genconv↑] t' ∷ A ^ [ ! , ι ⁰ ] →
    Γ ⊢ e ∷ Id (U ⁰) A B ^ [ % , next ⁰ ] →
    Γ ⊢ e' ∷ Id (U ⁰) A' B' ^ [ % , next ⁰ ] →
    Γ ⊢ cast ⁰ A B e t ~ cast ⁰ A' B' e' t' ∷ B ^ [ ! , ι ⁰ ]
~-castcong (↑ A≡B (~↑! x)) X Y ⊢e ⊢e' =
     let _ , ⊢B , _ = syntacticEqTerm (soundnessConv↑Term X)
         _ , ⊢B' = syntacticEq A≡B
         B′ , whnfB′ , D = whNorm ⊢B'
         U≡B′ = trans A≡B (subset* (red D))
         B≡U = U≡A-whnf U≡B′ whnfB′
         t~t′ = PE.subst (λ x → _ ⊢ _ ~ _ ↓! x ^ _) B≡U
                      ([~] _ (red D) whnfB′ x)
     in ↑ (refl (univ ⊢B)) (~↑! (cast-cong t~t′ X Y ⊢e ⊢e'))

~-castℕ : ∀ {B B' e e' t t' : Term} {Γ : Con Term} →
    ⊢ Γ →
    Γ ⊢ B ~ B' ∷ U ⁰ ^ [ ! , next ⁰ ] →
    Γ ⊢ t [genconv↑] t' ∷ ℕ ^ [ ! , ι ⁰ ] →
    Γ ⊢ e ∷ Id (U ⁰) ℕ B ^ [ % , next ⁰ ] →
    Γ ⊢ e' ∷ Id (U ⁰) ℕ B' ^ [ % , next ⁰ ] →
    Γ ⊢ cast ⁰ ℕ B e t ~ cast ⁰ ℕ B' e' t' ∷ B ^ [ ! , ι ⁰ ]
~-castℕ ⊢Γ (↑ A≡B (~↑! x)) X ⊢e ⊢e' =
     let _ , ⊢B' = syntacticEq A≡B
         B′ , whnfB′ , D = whNorm ⊢B'
         U≡B′ = trans A≡B (subset* (red D))
         B≡U = U≡A-whnf U≡B′ whnfB′
         t~t′ = PE.subst (λ x → _ ⊢ _ ~ _ ↓! x ^ _) B≡U
                      ([~] _ (red D) whnfB′ x)
         _ , ⊢B , _ = syntacticEqTerm (soundness~↓! t~t′)
     in ↑ (refl (univ ⊢B)) (~↑! (cast-ℕ t~t′ X ⊢e ⊢e'))

~-castℕℕ : ∀ {e e' t t' : Term} {Γ : Con Term} →
    ⊢ Γ →
    Γ ⊢ t ~ t' ∷ ℕ ^ [ ! , ι ⁰ ] →
    Γ ⊢ e ∷ Id (U ⁰) ℕ ℕ ^ [ % , next ⁰ ] →
    Γ ⊢ e' ∷ Id (U ⁰) ℕ ℕ ^ [ % , next ⁰ ] →
    Γ ⊢ cast ⁰ ℕ ℕ e t ~ cast ⁰ ℕ ℕ e' t' ∷ ℕ ^ [ ! , ι ⁰ ]
~-castℕℕ ⊢Γ (↑ A≡B (~↑! x)) ⊢e ⊢e' =
     let _ , ⊢B' = syntacticEq A≡B
         B′ , whnfB′ , D = whNorm ⊢B'
         ℕ≡B′ = trans A≡B (subset* (red D))
         B≡ℕ = ℕ≡A ℕ≡B′ whnfB′
         t~t′ = PE.subst (λ x → _ ⊢ _ ~ _ ↓! x ^ _) B≡ℕ
                      ([~] _ (red D) whnfB′ x)
         _ , ⊢B , _ = syntacticEqTerm (soundness~↓! t~t′)
     in ↑ (refl (univ (ℕⱼ ⊢Γ))) (~↑! (cast-ℕℕ t~t′ ⊢e ⊢e'))

~-castΠ : ∀ {A A' : Term} {rA : Relevance} {P P' B B' e e' t t' : Term}
    {Γ : Con Term} →
    Γ ⊢ Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰ [genconv↑] Π A' ^ rA ° ⁰ ▹ P' ° ⁰ ° ⁰ ∷ U ⁰ ^ [ ! , next ⁰ ] →
    Γ ⊢ B ~ B' ∷ U ⁰ ^ [ ! , next ⁰ ] →
    Γ ⊢ t [genconv↑] t' ∷ Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰ ^ [ ! , ι ⁰ ] →
    Γ ⊢ e ∷ Id (U ⁰) (Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰) B ^ [ % , next ⁰ ] →
    Γ ⊢ e' ∷ Id (U ⁰) (Π A' ^ rA ° ⁰ ▹ P' ° ⁰ ° ⁰) B' ^ [ % , next ⁰ ] →
    Γ ⊢ cast ⁰ (Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰) B e t ~ cast ⁰ (Π A' ^ rA ° ⁰ ▹ P' ° ⁰ ° ⁰) B' e' t' ∷ B ^ [ ! , ι ⁰ ]
~-castΠ X (↑ A≡B (~↑! x)) Y ⊢e ⊢e' =
     let _ , ⊢B' = syntacticEq A≡B
         B′ , whnfB′ , D = whNorm ⊢B'
         U≡B′ = trans A≡B (subset* (red D))
         B≡U = U≡A-whnf U≡B′ whnfB′
         t~t′ = PE.subst (λ x → _ ⊢ _ ~ _ ↓! x ^ _) B≡U
                      ([~] _ (red D) whnfB′ x)
         _ , ⊢B , _ = syntacticEqTerm (soundness~↓! t~t′)
     in ↑ (refl (univ ⊢B)) (~↑! (cast-Π X t~t′ Y ⊢e ⊢e'))

~-castℕΠ : ∀ {A A' : Term} {rA : Relevance} {P P' e e' t t' : Term}
    {Γ : Con Term} →
    Γ ⊢ A ∷ Univ rA ⁰ ^ [ ! , next ⁰ ] →
    (Γ ∙ A ^ [ rA , ι ⁰ ]) ⊢ P ∷ U ⁰ ^ [ ! , next ⁰ ] →
    Γ ⊢ Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰ [genconv↑] Π A' ^ rA ° ⁰ ▹ P' ° ⁰ ° ⁰ ∷ U ⁰ ^ [ ! , next ⁰ ] →
    Γ ⊢ t [genconv↑] t' ∷ ℕ ^ [ ! , ι ⁰ ] →
    Γ ⊢ e ∷ Id (U ⁰) ℕ (Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰) ^ [ % , next ⁰ ] →
    Γ ⊢ e' ∷ Id (U ⁰) ℕ (Π A' ^ rA ° ⁰ ▹ P' ° ⁰ ° ⁰) ^ [ % , next ⁰ ] →
    Γ ⊢ cast ⁰ ℕ (Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰) e t ~ cast ⁰ ℕ (Π A' ^ rA ° ⁰ ▹ P' ° ⁰ ° ⁰) e' t' ∷
    Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰ ^ [ ! , ι ⁰ ]
~-castℕΠ ⊢A ⊢P X Y ⊢e ⊢e' = ↑ (refl (univ (Πⱼ ≡is≤ PE.refl ▹ ≡is≤ PE.refl ▹ ⊢A ▹ ⊢P))) (~↑! (cast-ℕΠ X Y ⊢e ⊢e'))

~-castΠℕ : ∀ {A A' : Term} {rA : Relevance} {P P' e e' t t' : Term}
    {Γ : Con Term} →
    Γ ⊢ A ∷ Univ rA ⁰ ^ [ ! , next ⁰ ] →
    (Γ ∙ A ^ [ rA , ι ⁰ ]) ⊢ P ∷ U ⁰ ^ [ ! , next ⁰ ] →
    Γ ⊢ Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰ [genconv↑] Π A' ^ rA ° ⁰ ▹ P' ° ⁰ ° ⁰
    ∷ U ⁰ ^ [ ! , next ⁰ ] →
    Γ ⊢ t [genconv↑] t' ∷ Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰ ^ [ ! , ι ⁰ ] →
    Γ ⊢ e ∷ Id (U ⁰) (Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰) ℕ ^ [ % , next ⁰ ] →
    Γ ⊢ e' ∷ Id (U ⁰) (Π A' ^ rA ° ⁰ ▹ P' ° ⁰ ° ⁰) ℕ ^ [ % , next ⁰ ] →
    Γ ⊢ cast ⁰ (Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰) ℕ e t ~
    cast ⁰ (Π A' ^ rA ° ⁰ ▹ P' ° ⁰ ° ⁰) ℕ e' t' ∷ ℕ ^ [ ! , ι ⁰ ]
~-castΠℕ ⊢A ⊢P X Y ⊢e ⊢e' = ↑ (refl (univ (ℕⱼ (wfTerm ⊢A)))) (~↑! (cast-Πℕ X Y ⊢e ⊢e'))

~-castΠΠ%! : ∀ {A A' P P' B B' Q Q' e e' t t' : Term} {Γ : Con Term} →
    Γ ⊢ A ∷ Univ % ⁰ ^ [ ! , next ⁰ ] →
    (Γ ∙ A ^ [ % , ι ⁰ ]) ⊢ P ∷ U ⁰ ^ [ ! , next ⁰ ] →
    Γ ⊢ Π A ^ % ° ⁰ ▹ P ° ⁰ ° ⁰ [genconv↑] Π A' ^ % ° ⁰ ▹ P' ° ⁰ ° ⁰ ∷ U ⁰ ^ [ ! , next ⁰ ] →
    Γ ⊢ B ∷ Univ ! ⁰ ^ [ ! , next ⁰ ] →
    (Γ ∙ B ^ [ ! , ι ⁰ ]) ⊢ Q ∷ U ⁰ ^ [ ! , next ⁰ ] →
    Γ ⊢ Π B ^ ! ° ⁰ ▹ Q ° ⁰ ° ⁰ [genconv↑] Π B' ^ ! ° ⁰ ▹ Q' ° ⁰ ° ⁰ ∷ U ⁰ ^ [ ! , next ⁰ ] →
    Γ ⊢ t [genconv↑] t' ∷ Π A ^ % ° ⁰ ▹ P ° ⁰ ° ⁰ ^ [ ! , ι ⁰ ] →
    Γ ⊢ e  ∷ Id (U ⁰) (Π A ^ % ° ⁰ ▹ P ° ⁰ ° ⁰) (Π B ^ ! ° ⁰ ▹ Q ° ⁰ ° ⁰) ^ [ % , next ⁰ ] →
    Γ ⊢ e' ∷ Id (U ⁰) (Π A' ^ % ° ⁰ ▹ P' ° ⁰ ° ⁰) (Π B' ^ ! ° ⁰ ▹ Q' ° ⁰ ° ⁰) ^ [ % , next ⁰ ] →
    Γ ⊢ cast ⁰ (Π A ^ % ° ⁰ ▹ P ° ⁰ ° ⁰) (Π B ^ ! ° ⁰ ▹ Q ° ⁰ ° ⁰) e t ~
        cast ⁰ (Π A' ^ % ° ⁰ ▹ P' ° ⁰ ° ⁰) (Π B' ^ ! ° ⁰ ▹ Q' ° ⁰ ° ⁰) e' t' ∷ Π B ^ ! ° ⁰ ▹ Q ° ⁰ ° ⁰ ^ [ ! , ι ⁰ ]
~-castΠΠ%! ⊢A ⊢P X ⊢B ⊢Q Y t~t' ⊢e ⊢e' = ↑ (refl (univ (Πⱼ ≡is≤ PE.refl ▹ ≡is≤ PE.refl ▹ ⊢B ▹ ⊢Q)))
                                           (~↑! (cast-ΠΠ%! X Y t~t' ⊢e ⊢e'))

~-castΠΠ!% : ∀ {A A' P P' B B' Q Q' e e' t t' : Term} {Γ : Con Term} →
    Γ ⊢ A ∷ Univ ! ⁰ ^ [ ! , next ⁰ ] →
    (Γ ∙ A ^ [ ! , ι ⁰ ]) ⊢ P ∷ U ⁰ ^ [ ! , next ⁰ ] →
    Γ ⊢ Π A ^ ! ° ⁰ ▹ P ° ⁰ ° ⁰ [genconv↑] Π A' ^ ! ° ⁰ ▹ P' ° ⁰ ° ⁰ ∷ U ⁰ ^ [ ! , next ⁰ ] →
    Γ ⊢ B ∷ Univ % ⁰ ^ [ ! , next ⁰ ] →
    (Γ ∙ B ^ [ % , ι ⁰ ]) ⊢ Q ∷ U ⁰ ^ [ ! , next ⁰ ] →
    Γ ⊢ Π B ^ % ° ⁰ ▹ Q ° ⁰ ° ⁰ [genconv↑] Π B' ^ % ° ⁰ ▹ Q' ° ⁰ ° ⁰ ∷ U ⁰ ^ [ ! , next ⁰ ] →
    Γ ⊢ t [genconv↑] t' ∷ Π A ^ ! ° ⁰ ▹ P ° ⁰ ° ⁰ ^ [ ! , ι ⁰ ] →
    Γ ⊢ e  ∷ Id (U ⁰) (Π A ^ ! ° ⁰ ▹ P ° ⁰ ° ⁰) (Π B ^ % ° ⁰ ▹ Q ° ⁰ ° ⁰) ^ [ % , next ⁰ ] →
    Γ ⊢ e' ∷ Id (U ⁰) (Π A' ^ ! ° ⁰ ▹ P' ° ⁰ ° ⁰) (Π B' ^ % ° ⁰ ▹ Q' ° ⁰ ° ⁰) ^ [ % , next ⁰ ] →
    Γ ⊢ cast ⁰ (Π A ^ ! ° ⁰ ▹ P ° ⁰ ° ⁰) (Π B ^ % ° ⁰ ▹ Q ° ⁰ ° ⁰) e t ~
        cast ⁰ (Π A' ^ ! ° ⁰ ▹ P' ° ⁰ ° ⁰) (Π B' ^ % ° ⁰ ▹ Q' ° ⁰ ° ⁰) e' t' ∷ Π B ^ % ° ⁰ ▹ Q ° ⁰ ° ⁰ ^ [ ! , ι ⁰ ]
~-castΠΠ!% ⊢A ⊢P X ⊢B ⊢Q Y t~t' ⊢e ⊢e' = ↑ (refl (univ (Πⱼ ≡is≤ PE.refl ▹ ≡is≤ PE.refl ▹ ⊢B ▹ ⊢Q)))
                                           (~↑! (cast-ΠΠ!% X Y t~t' ⊢e ⊢e'))

~-sym : {k l A : Term} {r : TypeInfo} {Γ : Con Term} → Γ ⊢ k ~ l ∷ A ^ r → Γ ⊢ l ~ k ∷ A ^ r
~-sym (↑ A≡B x) =
  let ⊢Γ = wfEq A≡B
      B , A≡B′ , l~k = sym~↑ (reflConEq ⊢Γ) x
  in  ↑ (trans A≡B A≡B′) l~k

~-trans : {k l m A : Term} {r : TypeInfo} {Γ : Con Term}
        → Γ ⊢ k ~ l ∷ A ^ r → Γ ⊢ l ~ m ∷ A ^ r
        → Γ ⊢ k ~ m ∷ A ^ r
~-trans (↑ x (~↑! x₁)) (↑ x₂ (~↑! x₃)) =
  let ⊢Γ = wfEq x
      k~m , _ = trans~↑! PE.refl (reflConEq ⊢Γ) x₁ x₃
  in  ↑ x (~↑! k~m)
~-trans (↑ x (~↑% x₁)) (↑ x₂ (~↑% x₃)) =
  let ⊢Γ = wfEq x
      k~m = trans~↑% (reflConEq ⊢Γ) x₁ (conv~↑% x₃ (trans (sym x₂) x))
  in  ↑ x (~↑% k~m)

~-wk : {k l A : Term} {r : TypeInfo} {ρ : Wk} {Γ Δ : Con Term} →
      ρ ∷ Δ ⊆ Γ →
      ⊢ Δ → Γ ⊢ k ~ l ∷ A ^ r → Δ ⊢ wk ρ k ~ wk ρ l ∷ wk ρ A ^ r
~-wk x x₁ (↑ x₂ x₃) = ↑ (wkEq x x₁ x₂) (wk~↑ x x₁ x₃)

~-conv : {k l A B : Term} {r : TypeInfo} {Γ : Con Term} →
      Γ ⊢ k ~ l ∷ A ^ r → Γ ⊢ A ≡ B ^ r → Γ ⊢ k ~ l ∷ B ^ r
~-conv (↑ x x₁) x₂ = ↑ (trans (sym x₂) x) x₁

~-to-conv : {k l A : Term} {Γ : Con Term} {r : TypeInfo} →
      Γ ⊢ k ~ l ∷ A ^ r →  Γ ⊢ k [genconv↑] l ∷ A ^ r
~-to-conv {r = [ ! , ll ]} (↑ x x₁) = convConvTerm (lift~toConv↑ x₁) (sym x)
~-to-conv {r = [ % , ll ]} (↑ x (~↑% x₁)) = conv~↑% x₁ (sym x)

un-univConv : ∀ {A B : Term} {r : Relevance} {l : Level} {Γ : Con Term} →
                Γ ⊢ A [conv↑] B ^ [ r , ι l ] →
                Γ ⊢ A [conv↑] B ∷ Univ r l ^ next l
un-univConv {A} {B} {r} {l} ([↑] A′ B′ D D′ whnfA′ whnfB′ (univ x)) =
            let ⊢Γ = wfEqTerm (soundnessConv↓Term x)
            in [↑]ₜ (Univ r l) A′ B′ (id (Ugenⱼ ⊢Γ)) (un-univ⇒* D) (un-univ⇒* D′) Uₙ whnfA′ whnfB′ x

Πₜ-cong : ∀ {F G H E rF rG lF lG lΠ Γ}
        → lF ≤ lΠ
        → lG ≤ lΠ
        → Γ ⊢ F ^ [ rF , ι lF ]
        → Γ ⊢ F [conv↑] H ∷ Univ rF lF ^ next lF
        → Γ ∙ F ^ [ rF , ι lF ] ⊢ G [conv↑] E ∷ Univ rG lG ^ next lG
        → Γ ⊢ Π F ^ rF ° lF ▹ G ° lG ° lΠ [conv↑] Π H ^ rF ° lF ▹ E ° lG ° lΠ ∷ Univ rG lΠ ^ next lΠ
Πₜ-cong lF< lG< x x₁ x₂ = liftConvTerm (Π-cong PE.refl PE.refl PE.refl PE.refl lF< lG< x x₁ x₂)

~-irrelevance : {k l A : Term} {Γ : Con Term} {ll : TypeLevel}
               → Γ ⊢ k ∷ A ^ [ % , ll ]
               → Γ ⊢ l ∷ A ^ [ % , ll ]
               → Γ ⊢ k ~ l ∷ A ^ [ % , ll ]
~-irrelevance ⊢k ⊢l =
  let X = ~↑% (%~↑ ⊢k ⊢l)
      ⊢A  = syntacticTerm ⊢k
  in ↑ (refl ⊢A) X

soundnessgenConv : ∀ {a b A r Γ} → Γ ⊢ a [genconv↑] b ∷ A ^ r → Γ ⊢ a ≡ b ∷ A ^ r
soundnessgenConv {r = [ ! , l ]} = soundnessConv↑Term
soundnessgenConv {r = [ % , l ]} x = proj₂ (proj₂ (soundness~↑% x))

symgenConv : ∀ {t u A r Γ} → Γ ⊢ t [genconv↑] u ∷ A ^ r → Γ ⊢ u [genconv↑] t ∷ A ^ r
symgenConv {r = [ ! , l ]} = symConvTerm
symgenConv {r = [ % , l ]} t<>u = let ⊢Γ = wfEqTerm (proj₂ (proj₂ (soundness~↑% t<>u)))
                          in  sym~↑% (reflConEq ⊢Γ) t<>u

wkgenConv↑Term : ∀ {ρ t u A Γ r Δ} ([ρ] : ρ ∷ Δ ⊆ Γ) → ⊢ Δ
             → Γ ⊢ t [genconv↑] u ∷ A ^ r
             → Δ ⊢ wk ρ t [genconv↑] wk ρ u ∷ wk ρ A ^ r
wkgenConv↑Term {r = [ ! , l ]} = wkConv↑Term
wkgenConv↑Term {r = [ % , l ]} = wk~↑%

convgenconv : ∀ {t u A B : Term} {r : TypeInfo} {Γ : Con Term} →
      Γ ⊢ t [genconv↑] u ∷ A ^ r →
      Γ ⊢ A ≡ B ^ r → Γ ⊢ t [genconv↑] u ∷ B ^ r
convgenconv {r = [ ! , l ]} = convConvTerm
convgenconv {r = [ % , l ]} = conv~↑%

transgenConv : ∀ {t u v A : Term} {r : TypeInfo} {Γ : Con Term} →
      Γ ⊢ t [genconv↑] u ∷ A ^ r →
      Γ ⊢ u [genconv↑] v ∷ A ^ r → Γ ⊢ t [genconv↑] v ∷ A ^ r
transgenConv {r = [ ! , l ]} = transConvTerm
transgenConv {r = [ % , l ]} = trans~↑!Term

-- Algorithmic equality instance of the generic equality relation.
instance eqRelInstance : EqRelSet
eqRelInstance = eqRel _⊢_[conv↑]_^_ _⊢_[genconv↑]_∷_^_ _⊢_~_∷_^_
                      ~-to-conv soundnessConv↑ soundnessgenConv
                      univConv↑ un-univConv
                      symConv symgenConv ~-sym
                      transConv transgenConv ~-trans
                      convgenconv ~-conv
                      wkConv↑ wkgenConv↑Term ~-wk
                      reductionConv↑ reductionConv↑Term
                      (liftConv ∘ᶠ (U-refl PE.refl)) ( liftConvTerm ∘ᶠ  (U-refl PE.refl))
                      (liftConvTerm ∘ᶠ ℕ-refl)
                      (liftConvTerm ∘ᶠ (Empty-refl PE.refl))
                      Πₜ-cong
                      (λ x x₁ x₂ → liftConvTerm (∃-cong PE.refl x x₁ x₂))
                      (liftConvTerm ∘ᶠ zero-refl)
                      (liftConvTerm ∘ᶠ suc-cong)
                      (λ l< l<' x x₁ x₂ x₃ x₄ x₅ → liftConvTerm (η-eq l< l<' x x₁ x₂ x₃ x₄ x₅))
                      ~-var ~-app ~-natrec ~-Emptyrec
                      ~-IdCong ~-Idℕ ~-Idℕ0 ~-IdℕS ~-IdU ~-IdUℕ ~-IdUΠ
                      ~-castcong ~-castℕ ~-castℕℕ ~-castΠ ~-castℕΠ ~-castΠℕ ~-castΠΠ%! ~-castΠΠ!%
                      ~-irrelevance

ext: agda

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
open import Array
open import Array.APL

open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.DivMod hiding (_/_)
open import Data.Fin hiding (_≤_; _<_; _+_) --using (Fin; zero; suc; toℕ)
open import Data.Vec
open import Data.Vec.Properties
open import Relation.Binary.PropositionalEquality
open import Data.Product

open import Function
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Data.Unit using (⊤)

open import Agda.Builtin.Float

-- Save some typing when selecting from index-vectors/shapes
-- converted into arrays.
pattern I0 = (zero ∷ [])
pattern I1 = (suc zero ∷ [])
pattern I2 = (suc (suc zero) ∷ [])
pattern I3 = (suc (suc (suc zero)) ∷ [])

-- Verbose facts about transitivity of <, ≤, and ≡
a≤b⇒b≡c⇒a≤c : ∀ {a b c} → a ≤ b → b ≡ c → a ≤ c
a≤b⇒b≡c⇒a≤c a≤b refl = a≤b

a≤b⇒a≡c⇒b≡d⇒c≤d : ∀ {a b c d} → a ≤ b → a ≡ c → b ≡ d → c ≤ d
a≤b⇒a≡c⇒b≡d⇒c≤d a≤b refl refl = a≤b

a<b⇒0<b : ∀ {a b} → a < b → zero < b
a<b⇒0<b {a} a<b = ≤-trans (s≤s z≤n) a<b

a<b⇒c≤a⇒c<b : ∀ {a b c} → a < b → c ≤ a → c < b
a<b⇒c≤a⇒c<b a<b z≤n = a<b⇒0<b a<b
a<b⇒c≤a⇒c<b (s≤s a<b) (s≤s c≤a) = s≤s (a<b⇒c≤a⇒c<b a<b c≤a)

a≤b⇒c≤a⇒c≤b : ∀ {a b c} → a ≤ b → c ≤ a → c ≤ b
a≤b⇒c≤a⇒c≤b {a} {b} {c} a≤b c≤a = ≤-trans c≤a a≤b

A<B⇒B≤C⇒A≤C : ∀ {n}{ix s s₁ : Ar ℕ 1 (n ∷ [])}
             → ix <a s → s₁ ≥a s → s₁ ≥a ix
A<B⇒B≤C⇒A≤C {ix = imap x} {imap x₁} {imap x₂} ix<s ix≤s₁ iv = ≤-trans (<⇒≤ $ ix<s iv) (ix≤s₁ iv)

A≥B⇒A≡C⇒C≥B : ∀ {d s}{A B C : Ar ℕ d s}
             → A ≥a B → A =a C → C ≥a B
A≥B⇒A≡C⇒C≥B {A = imap x} {imap x₁} {imap x₂} A≥B A≡C iv rewrite (sym $ A≡C iv) = A≥B iv

-- Something that could go in Stdlib.
≡⇒≤ : ∀ {a b} → a ≡ b → a ≤ b
≡⇒≤ refl = ≤-refl

a≤a*b : ∀ {a b} → a ≤ a * suc b
a≤a*b {a} {b = zero} rewrite (*-identityʳ a) = ≤-refl
a≤a*b {a} {b = suc b} = ≤-trans a≤a*b (*-monoʳ-≤ a (≤-step ≤-refl))

a-s[b]+1≡a-b : ∀ {a b} → b < a →  a ∸ suc b + 1 ≡ a ∸ b
a-s[b]+1≡a-b {a} {b} pf = begin
                     a ∸ suc (b) + 1  ≡⟨ sym $ +-∸-comm 1 pf ⟩
                     a + 1 ∸ suc b    ≡⟨ cong₂ _∸_ (+-comm a 1) (refl {x = suc b}) ⟩
                     a ∸ b
                   ∎
                   where open ≡-Reasoning

conv-ix-inb : ∀ {n}{ix s s₁ : Ar ℕ 1 (n ∷ [])}
            → (ix<s : ix <a s)
            → (s₁≥s : s₁ ≥a s)
            → (s₁ -ₙ ix) {≥ = A<B⇒B≤C⇒A≤C {s₁ = s₁} ix<s s₁≥s}
               ≥a ((s₁ -ₙ s) {≥ = s₁≥s} +ₙ (scal 1))
conv-ix-inb {ix = imap ix} {imap s} {imap s₁} ix<s s₁≥s iv =
       let
         s₁-[1+ix]≥s₁-s = ∸-monoʳ-≤ (s₁ iv) (ix<s iv)
         s₁-[1+ix]+1≥s₁-s+1 = +-monoˡ-≤ 1 s₁-[1+ix]≥s₁-s
       in a≤b⇒b≡c⇒a≤c s₁-[1+ix]+1≥s₁-s+1 (a-s[b]+1≡a-b {a = s₁ iv} {b = ix iv} (≤-trans (ix<s iv) (s₁≥s iv)))

undo-sa-as : ∀ {n} {s s₁ : Vec ℕ n}{ix : Ar ℕ 1 (n ∷ [])}{≥1}
     → ((imap (λ iv → lookup s₁ (ix-lookup iv zero)) -ₙ ix) {≥ = ≥1})
       =a imap (λ z → lookup (a→s ((imap (λ iv → lookup s₁ (ix-lookup iv zero)) -ₙ ix) {≥ = ≥1}))
                             (ix-lookup z zero))
undo-sa-as {s₁ = s₁} {ix = (imap ix)} {≥1} iv = sym $ s→a∘a→s ((s→a s₁ -ₙ imap ix) {≥ = ≥1}) iv

-- conv ← {a←⍵ ⋄ w←⍺ ⋄ ⊃+/,w×{(1+(⍴a)-⍴w)↑⍵↓a}¨⍳⍴w}
conv : ∀ {n s s₁}
       → Ar Float n s
       → Ar Float n s₁
       → {s₁≥s : s→a s₁ ≥a s→a s}
       → let sr = a→s $ (s→a s₁ -ₙ s→a s) {≥ = s₁≥s} +ₙ scal 1
         in Ar Float n sr
conv {n = n} {s = s} {s₁ = s₁} w a {s₁≥s} = let
               sr = (s→a s₁ -ₙ s→a s) {≥ = s₁≥s} +ₙ scal 1
               idxs = ι ρ w

               rots ix ix<s = let
                  ~ix≥ρa = A<B⇒B≤C⇒A≤C ix<s s₁≥s
                  ix↓a = (ix ↓ a) {pf = ~ix≥ρa}
                  ~ix-inb = conv-ix-inb {s₁ = s→a s₁} ix<s s₁≥s
                  ~ρix↓a≥sr = A≥B⇒A≡C⇒C≥B
                                ~ix-inb
                                (undo-sa-as {s = s} {s₁ = s₁} {≥1 = ~ix≥ρa})
                  in
                  (sr ↑ ix↓a) {pf = ~ρix↓a≥sr }

               rots-unw ix,ix<s = (let
                                     ix , ix<s = ix,ix<s
                                    in rots ix ix<s)
               r = rots-unw ̈ idxs
               mul = w ̈⟨ (λ weight arr → arr ×ᵣ scal weight) ⟩ (subst-ar (a→s∘s→a s) r)
               res = reduce-1d (, mul) _+ᵣ_ (cst 0.0)
              in res

module conv-test where
  open import Array.Repr
  cex₁ = conv (cst {s = 1 ∷ []} 2.0)
             (imap {s = 2 ∷ []} λ { (zero ∷ []) → 2.0 ; (suc zero ∷ []) → 3.0})
             {s₁≥s = λ { (zero ∷ []) → s≤s z≤n} }

  cex₂ = conv (mkempty (3 ∷ 0 ∷ []) refl)
             (cst {s = 5 ∷ 0 ∷ []} 1.0)
             {λ { (zero ∷ []) → s≤s (s≤s (s≤s z≤n)) ;
                  (suc zero ∷ []) → z≤n}}
  repex₁ = a→rt cex₁

-- blog←{⍺×⍵×1-⍵}
blog : ∀ {n s} → Ar Float n s → Ar Float n s → Ar Float n s
blog α ω = α ×ᵣ ω ×ᵣ (scal 1.0) -ᵣ ω

-- backbias←{+/,⍵}
backbias : ∀ {n s} → Ar Float n s → Scal Float
backbias ω = _+ᵣ_ / , ω

-- XXX we can define unary -ᵣ and ÷ᵣ to make it even nicer.
-- logistic←{÷1+*-⍵}
logistic : ∀ {n s} → Ar Float n s → Ar Float n s
logistic {s} ω = (scal 1.0) ÷ᵣ (scal 1.0) +ᵣ *ᵣ (scal 0.0) -ᵣ ω

-- XXX Note that even though we had to specify n-n instances
--     explicitly, we didn't truly mimic the APL expression below.
--     As per APL semantics, meansqerr accepts the combination
--     of arguments 0-n, n-n and n-0.  So the fact that we had
--     to specialise suggests that we didn't truly implement
--     the original behaviour.
-- meansqerr←{÷∘2+/,(⍺-⍵)*2}
meansqerr : ∀ {n s} → Ar Float n s → Ar Float n s → Scal Float
meansqerr α ω =
    _÷⟨ n-n ⟩ᵣ (cst 2.0) $ (_+⟨ n-n ⟩ᵣ_ / , (α -⟨ n-n ⟩ᵣ ω) ×ᵣ (α -⟨ n-n ⟩ᵣ ω))

-- backavgpool←{2⌿2/⍵÷4}⍤2
backavgpool : ∀ {s}
              → Ar Float 2 s
              → Ar Float 2 $ a→s (s→a s ×ₙ (scal 2))
backavgpool {m ∷ n ∷ []} (imap f) =
  imap (λ iv → let
    ix , ix<r = ix→a iv
    px = (ix ÷ₙ (cst 2)) {≥0 = λ _ → s≤s z≤n}
    pv = a→ix px (s→a (m ∷ n ∷ [])) λ jv →
              let
                x = a<b⇒c≤a⇒c<b (ix<r jv) (m/n*n≤m _ 2)
                y = a≤b⇒b≡c⇒a≤c x (*-lookup {jv = jv}{m = m}{n = n})
              in    *-cancelʳ-< _ _ y
    in f pv)
  ÷ᵣ (scal 4.0)
  where
    *-lookup : ∀ {jv : Ix 1 (2 ∷ [])}{m n}
             → lookup (m * 2 ∷ n * 2 ∷ []) (ix-lookup jv zero)
             ≡ lookup (m ∷ n ∷ []) (ix-lookup jv zero) * 2
    *-lookup {jv = I0} = refl
    *-lookup {jv = I1} = refl

-- This should be perfectly generaliseable --- instead of 2
-- we can use any m>0
a<b⇒k<2⇒a*2+k<b*2 : ∀ {a b k} → a < b → k < 2 → a * 2 + k < b * 2
a<b⇒k<2⇒a*2+k<b*2 {a} {b} {zero} a<b k<2
                   rewrite (+-identityʳ (a * 2))
                         | (*-comm a 2)
                         | (*-comm b 2) = *-monoʳ-< 1 a<b
a<b⇒k<2⇒a*2+k<b*2 {a} {b} {suc zero} a<b k<2 = ≤-trans (s≤s (≡⇒≤ (+-comm _ 1)))
                                                        (*-monoˡ-≤ 2 a<b)
a<b⇒k<2⇒a*2+k<b*2 {a} {b} {suc (suc k)} a<b (s≤s (s≤s ()))

A<B⇒K<2⇒A*2+K<B*2 : ∀ {n s}{a b k : Ar ℕ n s} → a <a b → k <a (cst 2) → ((a ×ₙ (scal 2)) +ₙ k) <a (b ×ₙ (scal 2))
A<B⇒K<2⇒A*2+K<B*2 {a = imap a} {imap b} {imap k} a<b k<2 = λ iv → a<b⇒k<2⇒a*2+k<b*2 (a<b iv) (k<2 iv)

-- avgpool←{÷∘4{+/,⍵}⌺(2 2⍴2)⍤2⊢⍵}
avgpool-explicit : ∀ {s}
                 → Ar Float 2 $ a→s (s→a s ×ₙ (scal 2))
                 → Ar Float 2 s
avgpool-explicit {s} (imap p) =
  imap (λ iv → let
    sh = (s→a s ×ₙ scal 2)
    ix , ix<s = ix→a iv
    bx = ix ×ₙ scal 2
    s-00 = s→a (0 ∷ 0 ∷ [])
    i1 = a→ix (bx +ₙ s-00) sh (A<B⇒K<2⇒A*2+K<B*2 {k = s-00} ix<s
                               λ { I0 → s≤s z≤n; I1 → s≤s z≤n})
    s-01 = s→a (0 ∷ 1 ∷ [])
    i2 = a→ix (bx +ₙ s-01) sh (A<B⇒K<2⇒A*2+K<B*2 {k = s-01} ix<s
                               λ { I0 → s≤s z≤n; I1 → s≤s (s≤s z≤n)})
    s-10 = s→a (1 ∷ 0 ∷ [])
    i3 = a→ix (bx +ₙ s-10) sh (A<B⇒K<2⇒A*2+K<B*2 {k = s-10} ix<s
                               λ { I0 → s≤s (s≤s z≤n); I1 → s≤s z≤n })
    s-11 = s→a (1 ∷ 1 ∷ [])
    i4 = a→ix (bx +ₙ s-11) sh (A<B⇒K<2⇒A*2+K<B*2 {k = s-11} ix<s
                               λ { I0 → s≤s (s≤s z≤n) ; I1 → s≤s (s≤s z≤n) })
    s = _÷⟨ n-n ⟩ᵣ (scal 4.0) $
        (scal $ p i1) +⟨ n-n ⟩ᵣ (scal $ p i2)
        +⟨ n-n ⟩ᵣ (scal $ p i2) +⟨ n-n ⟩ᵣ (scal $ p i3)
        +⟨ n-n ⟩ᵣ (scal $ p i4)
  in unscal s)

-- avgpool←{÷∘4{+/,⍵}⌺(2 2⍴2)⍤2⊢⍵}
avgpool : ∀ {s}
        → Ar Float 2 $ a→s (s→a s ×ₙ (scal 2))
        → Ar Float 2 s
avgpool {s} (imap p) = imap (λ iv → let
                         sh = (s→a s ×ₙ scal 2)
                         ix , ix<s = ix→a iv
                         bx = ix ×ₙ scal 2
                         ixs = ι (cst {s = 2 ∷ []} 2)
                         use-ixs i,pf = let
                            i , pf = i,pf
                            jx = bx +⟨ n-n ⟩ₙ i
                            in p (a→ix jx sh (A<B⇒K<2⇒A*2+K<B*2 ix<s pf))

                         s = _÷⟨ n-n ⟩ᵣ (scal 4.0) $ _+⟨ n-n ⟩ᵣ_ / , use-ixs ̈ ixs
                       in unscal s)

-- multiconv←{(a ws bs)←⍵⋄bs{⍺+⍵ conv a}⍤(0,(⍴⍴a))⊢ws}
multiconv : ∀ {n m s sw so} → (a : Ar Float n s)
            →  (ws : Ar (Ar Float n sw) m so)
            →  (bs : Ar Float m so)
            →  {≥ : (s→a s) ≥a (s→a sw)}
            →  Ar (Ar Float n  (a→s $ ((s→a s -ₙ s→a sw) {≥}) +ₙ (scal 1))) m so
multiconv a ws bs {≥} = bs ̈⟨ (λ b w → (scal b) +ᵣ conv w a {≥}) ⟩ ws

--look-at-avgpl : ∀ {s} → (a : Ar Float 2 $ a→s (s→a s ×ₙ (scal 2))) → avgpool {s = s} a ≡ {!!}
--look-at-avgpl {x₁ ∷ x₂ ∷ []} (imap f) = {!!}

module test-avgpool where
  test-avgp = avgpool {s = 1 ∷ 1 ∷ []} (imap λ { (zero ∷ zero ∷ []) → 1.0 ;
                                                  (zero ∷ suc zero ∷ []) → 2.0 ;
                                                  (suc zero ∷ zero ∷ []) → 3.0 ;
                                                  (suc zero ∷ suc zero ∷ []) → 4.0 })
  avgp-val = unimap test-avgp $ zero ∷ zero ∷ []

-- This should go into APL operators.
areplicate : ∀ {a}{X : Set a}{s} → (k : ℕ) → Ar X 1 s → Ar X _ _
areplicate k (imap f) = let
                          x = imap λ iv → imap {d = 1} {s = k ∷ []} λ _ → f iv
                        in , flatten x

test-repl = a→s $ areplicate 2 $ proj₁ ̈ ι (scal 5)

∸-monoˡ-< : ∀ {m n o} → m < n → o ≤ m → m ∸ o < n ∸ o
∸-monoˡ-< {o = zero}  m<n o≤m = m<n
∸-monoˡ-< {suc m} {o = suc o} (s≤s m<n) (s≤s o≤m) = ∸-monoˡ-< m<n o≤m

a+b-a≡a : ∀ {n} {s₁ : Vec ℕ n} {s : Ix 1 (n ∷ []) → ℕ}
             {jv : Ix 1 (n ∷ [])} →
           lookup (tabulate (λ i → s (i ∷ []) + lookup s₁ i))
           (ix-lookup jv zero)
           ∸ s jv
           ≡ lookup s₁ (ix-lookup jv zero)
a+b-a≡a {zero} {[]} {s} {x ∷ []} = magic-fin x
a+b-a≡a {suc n} {x ∷ s₁} {s} {I0} = m+n∸m≡n (s I0) x
a+b-a≡a {suc n} {x ∷ s₁} {s} {suc j ∷ []} = a+b-a≡a {s₁ = s₁} {s = λ { (j ∷ []) → s (suc j ∷ [])}} {jv = j ∷ []}

pre-pad : ∀ {a}{X : Set a}{n}{s₁ : Vec ℕ n}
        → (sh : Ar ℕ 1 (n ∷ []))
        → X
        → (a : Ar X n s₁)
        → Ar X n (a→s $ sh +ₙ ρ a)
pre-pad {s₁ = s₁} (imap s) e (imap f) = imap body
  where
    body : _
    body iv = let ix , ix<s = ix→a iv
              in case ix ≥a? (imap s) of λ where
                   (yes p) → let
                      fx = (ix -ₙ (imap s)) {≥ = p}
                      fv = a→ix fx (s→a s₁)
                                λ jv → a<b⇒b≡c⇒a<c
                                          (∸-monoˡ-< (ix<s jv) (p jv))
                                          (a+b-a≡a {s₁ = s₁} {s = s} {jv = jv})
                      in f (subst-ix (λ i → lookup∘tabulate _ i) fv)
                   (no ¬p) → e

arel-thm : ∀ {n s}{a b : Ar ℕ n s} → ARel _≥_ a b → a ≥a b
arel-thm {a = imap a} {imap b} pf = pf

≥a-lkup : ∀ {n s}{a b : Ar ℕ n s} → a ≥a b → (iv : Ix n s) → unimap a iv ≥ unimap b iv
≥a-lkup {a = imap a} {imap b} p iv = p iv

_↑⟨_⟩_ : ∀ {a}{X : Set a}{n}{s : Vec ℕ n}
      → (sh : Ar ℕ 1 (n ∷ []))
      → X
      → (a : Ar X n s)
      → Ar X n (a→s sh)
_↑⟨_⟩_ {s = s} (imap sh) e (imap a) = imap body
  where
    body : _
    body iv = let ix , ix<s = ix→a iv
              in case ix <a? (ρ imap a) of λ where
                (yes p) → let
                            av = a→ix ix (ρ imap a) p
                          in a (subst-ix (λ i → lookup∘tabulate _ i) av)
                (no ¬p) → e

-- backin←{(d w in)←⍵⋄⊃+/,w{(⍴in)↑(-⍵+⍴d)↑⍺×d}¨⍳⍴w}
backin : ∀ {n s s₁} → (inp : Ar Float n s)
                     → (w : Ar Float n s₁)
                     → .{≥ : s→a s ≥a s→a s₁}
                     → (d : Ar Float n $ a→s $ (s→a s -ₙ s→a s₁) {≥} +ₙ scal 1)
                     → Ar Float n s
backin {n}{s}{s₁} inp w d = let
      ixs = ι (ρ w)
      use-ixs i,pf = let
        i , pf = i,pf
        iv = (a→ix i (ρ w) pf)
        wᵢ = (unimap w) (subst-ix (λ i → lookup∘tabulate _ i) iv)
        x = pre-pad i 0.0 (d ×ᵣ scal wᵢ)
        y = (ρ inp) ↑⟨ 0.0 ⟩ x
        in y
      s = reduce-1d (, use-ixs ̈ ixs) _+ᵣ_ (cst 0.0)
  in subst-ar (λ i → lookup∘tabulate _ i) s

s-w+1≤s : ∀ {s w} → s ≥ w → s > 0 → w > 0 → s ∸ w + 1 ≤ s
s-w+1≤s {suc s} {suc w} (s≤s s≥w) s>0 w>0 rewrite (+-comm (s ∸ w) 1) = s≤s (m∸n≤m s w)

helper : ∀ {n} {sI sw : Vec ℕ n}
       → s→a sI ≥a s→a sw
       → (cst 0) <a s→a sI
       → (cst 0) <a s→a sw
       → (iv : Ix 1 (n ∷ []))
       → lookup sI (ix-lookup iv zero) ≥
         lookup (tabulate (λ i → lookup sI i ∸ lookup sw i + 1))
         (ix-lookup iv zero)
helper {sI = sI} {sw} sI≥sw sI>0 sw>0 (x ∷ [])
       rewrite (lookup∘tabulate (λ i → lookup sI i ∸ lookup sw i + 1) x) =
       s-w+1≤s (sI≥sw (x ∷ [])) (sI>0 (x ∷ [])) (sw>0 (x ∷ []))

-- sI - (sI - sw + 1) + 1 = sw
shape-same : ∀ {n} {sI sw : Vec ℕ n}
           → s→a sI ≥a s→a sw
           → (cst 0) <a s→a sI
           → (cst 0) <a s→a sw
           → (i : Fin n)
           → lookup
             (tabulate
              (λ i₁ →
                 lookup sI i₁ ∸
                 lookup (tabulate (λ i₂ → lookup sI i₂ ∸ lookup sw i₂ + 1)) i₁
                 + 1))
             i
             ≡ lookup sw i
shape-same {suc n} {x ∷ sI} {y ∷ sw} I≥w I>0 w>0 zero =
  begin
    x ∸ (x ∸ y + 1) + 1 ≡⟨ sym $ +-∸-comm  {m = x} 1 {o = (x ∸ y + 1)}  (s-w+1≤s (I≥w I0) (I>0 I0) (w>0 I0)) ⟩
    x + 1 ∸ (x ∸ y + 1) ≡⟨ cong (x + 1 ∸_) (sym $ +-∸-comm {m = x} 1 {o = y} (I≥w I0)) ⟩
    x + 1 ∸ (x + 1 ∸ y) ≡⟨ m∸[m∸n]≡n {m = x + 1} {n = y} (a≤b⇒b≡c⇒a≤c (≤-step $ I≥w I0) (+-comm 1 x)) ⟩
    y
  ∎
  where open ≡-Reasoning
shape-same {suc n} {x ∷ sI} {x₁ ∷ sw} I≥w I>0 w>0 (suc i) =
  shape-same {sI = sI} {sw = sw} (λ { (i ∷ []) → I≥w (suc i ∷ []) })
                                 (λ { (i ∷ []) → I>0 (suc i ∷ []) })
                                 (λ { (i ∷ []) → w>0 (suc i ∷ []) }) i

{-backmulticonv ← {
  (d_out weights in bias) ← ⍵
  d_in ← +⌿d_out {backin ⍺ ⍵ in} ⍤((⍴⍴in), (⍴⍴in)) ⊢ weights
  d_w ← {⍵ conv in} ⍤(⍴⍴in) ⊢ d_out
  d_bias ← backbias ⍤(⍴⍴in) ⊢ d_out
  d_in d_w d_bias
}-}
backmulticonv : ∀ {n m}{sI sw so}
              → (W : Ar (Ar Float n sw) m so)
              → (I : Ar Float n sI)
              → (B : Ar Float m so)
                -- We can get rid of these two expressions if we rewrite
                -- the convolution to accept s+1 ≥ w, and not s ≥ w.
              → {>I : (cst 0) <a s→a sI}
              → {>w : (cst 0) <a s→a sw}
              → {≥ : s→a sI ≥a s→a sw}
              → (δo : Ar (Ar Float n (a→s $ (s→a sI -ₙ s→a sw) {≥} +ₙ (scal 1))) m so)
              → (typeOf W) × (typeOf I) × (typeOf B)
backmulticonv {sI = sI} {sw} {so} W I B {sI>0} {sw>0} {sI≥sw} δo = let
    δI = reduce-1d (, (W ̈⟨ (λ x y → backin I x {sI≥sw} y) ⟩ δo)) _+ᵣ_ (cst 0.0)
    δW = (λ x → conv x I {s₁≥s = helper {sI = sI} {sw = sw} sI≥sw sI>0 sw>0}) ̈ δo
    δB = backbias ̈ δo
  in (imap (λ iv → subst-ar (shape-same {sI = sI} {sw = sw} sI≥sw sI>0 sw>0) ((unimap δW) iv)) ,
     δI ,
     imap (λ iv → unscal $ unimap δB iv))

instance
  auto≥ : ∀ {m n : ℕ} → {{_ : True (m ≥? n)}} → m ≥ n
  auto≥ {m} {n} {{c}} = toWitness c

auto≥a : ∀ {d s}{p q : Ar ℕ d s} {_ : True (p ≥a? q)} → (p ≥a q)
auto≥a {p = imap x} {imap x₁} { c } = toWitness c

auto<a : ∀ {d s}{p q : Ar ℕ d s} {{_ : True (p <a? q)}} → (p <a q)
auto<a {p = imap x} {imap x₁} ⦃ c ⦄ = toWitness c

test-zhang : (inp : Ar Float _ (28 ∷ 28 ∷ []))
           → (k₁ :  Ar Float _ (6 ∷ 5 ∷ 5 ∷ []))
           → (b₁ :  Ar Float _ (6 ∷ []))
           → (k₂ :  Ar Float _ (12 ∷ 6 ∷ 5 ∷ 5 ∷ []))
           → (b₂ :  Ar Float _ (12 ∷ []))
           → (fc : Ar Float _ (10 ∷ 12 ∷ 1 ∷ 4 ∷ 4 ∷ []))
           → (b :  Ar Float _ (10 ∷ []))
           → Ar Float _ (10 ∷ 1 ∷ 1 ∷ 1 ∷ 1 ∷ [])
test-zhang inp k₁ b₁ k₂ b₂ fc b = let
    c₁ = logistic ̈ multiconv inp (nest k₁) b₁ {auto≥a}
    s₁ = avgpool {s = 12 ∷ 12 ∷ []} ̈ c₁
    c₂ = logistic ̈ multiconv (flatten s₁) (nest k₂) b₂ {auto≥a}
    s₂ = avgpool {s = 4 ∷ 4 ∷ []} ̈ (nest {s = _ ∷ _ ∷ []} $ flatten c₂)
    r = logistic ̈ multiconv (flatten s₂) (nest fc) b {auto≥a}
  in flatten r

train-zhang :(inp : Ar Float _ (28 ∷ 28 ∷ []))
            → (k₁ :  Ar Float _ (6 ∷ 5 ∷ 5 ∷ []))
            → (b₁ :  Ar Float _ (6 ∷ []))
            → (k₂ :  Ar Float _ (12 ∷ 6 ∷ 5 ∷ 5 ∷ []))
            → (b₂ :  Ar Float _ (12 ∷ []))
            → (fc : Ar Float _ (10 ∷ 12 ∷ 1 ∷ 4 ∷ 4 ∷ []))
            → (b :  Ar Float _ (10 ∷ []))
            → (target : Ar Float _ (10 ∷ 1 ∷ 1 ∷ 1 ∷ 1 ∷ []))
            → typeOf k₁ × typeOf b₁ × typeOf k₂ × typeOf b₂ × typeOf fc × typeOf b × Scal Float
train-zhang inp k₁ b₁ k₂ b₂ fc b target = let
    c₁ = logistic ̈ multiconv inp (nest k₁) b₁ {auto≥a}
    s₁ = avgpool {s = 12 ∷ 12 ∷ []} ̈ c₁
    c₂ = logistic ̈ multiconv (flatten s₁) (nest k₂) b₂ {auto≥a}
    s₂ = avgpool {s = 4 ∷ 4 ∷ []} ̈ (nest {s = _ ∷ _ ∷ []} $ flatten c₂)
    o = flatten $ logistic ̈ multiconv (flatten s₂) (nest fc) b {auto≥a}

    δo = o -ᵣ target
    ε  = meansqerr (, o) (, target)
    δfc , δs₂ , δb  = backmulticonv (nest fc) (flatten s₂) b {>I = auto<a} {>w = auto<a} {≥ = auto≥a}
                                   (nest (blog δo o))
    δc₂ = backavgpool ̈ (nest {s = _ ∷ _ ∷ []} δs₂)
    δk₂ , δs₁ , δb₂ =  backmulticonv (nest k₂) (flatten s₁) b₂ {>I = auto<a} {>w = auto<a} {≥ = auto≥a}
                                    (nest (blog (flatten δc₂) (flatten c₂)))
    δc₁ = backavgpool ̈ (nest {s = _ ∷ []} δs₁)
    δk₁ , _ , δb₁ =  backmulticonv (nest k₁) inp b₁ {>I = auto<a} {>w = auto<a} {≥ = auto≥a}
                                  (nest (blog (flatten δc₁) (flatten c₁)))

  in (flatten δk₁) , δb₁ , (flatten δk₂) , δb₂ , (flatten δfc) , δb , ε

max_stars_repo_name: ashinkarov/agda-array

max_issues_repo_name: ashinkarov/agda-array

max_forks_repo_name: ashinkarov/agda-array


text:
data Dec (A : Set) : Set where
  yes : A → Dec A
  no  : Dec A

record ⊤ : Set where constructor tt

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

subst : ∀ {A}(P : A → Set){x y} → x ≡ y → P x → P y
subst P refl px = px

cong : ∀ {A B}(f : A → B){x y} → x ≡ y → f x ≡ f y
cong f refl = refl

postulate _≟_ : (n n' : ⊤) → Dec (n ≡ n')

record _×_ A B : Set where
  constructor _,_
  field proj₁ : A
        proj₂ : B

open _×_

data Maybe : Set where
  nothing : Maybe

data Blah (a : Maybe × ⊤) : Set where
  blah  : {b : Maybe × ⊤} → Blah b → Blah a

update : {A : Set} → ⊤ → A → A
update n m with n ≟ n
update n m | yes p  = m
update n m | no     = m

lem-upd : ∀ {A} n (m : A) → update n m ≡ m
lem-upd n m with n ≟ n
... | yes p = refl
... | no    = refl

bug : {x : Maybe × ⊤} → proj₁ x ≡ nothing → Blah x
bug ia = blah (bug (subst {⊤}
                      (λ _ → proj₁ {B = ⊤}
                                   (update tt (nothing , tt)) ≡ nothing)
                   refl (cong proj₁ (lem-upd _ _))))


text:
open import Common.Prelude
open import TestHarness
open import TestBool using ( not; _∧_ ; _↔_ )

module TestList where

_++_ : ∀ {X} → List X → List X → List X
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

revApp : ∀ {X} → List X → List X → List X
revApp []       ys = ys
revApp (x ∷ xs) ys = revApp xs (x ∷ ys)

reverse : ∀ {X} → List X → List X
reverse xs = revApp xs []

_≟_ : List Bool → List Bool → Bool
[]       ≟ []       = true
(x ∷ xs) ≟ (y ∷ ys) = (x ↔ y) ∧ (xs ≟ ys)
_        ≟ -        = false

[tt] = true ∷ []
[ff] = false ∷ []
[tt,ff] = true ∷ [ff]
[ff,tt] = false ∷ [tt]
[ff,tt,ff] = false ∷ [tt,ff]

tests : Tests
tests _ = (
    assert ([] ≟ []) "[]=[]" ,
    assert (not ([tt] ≟ [ff])) "[tt]≠[ff]" ,
    assert (([] ++ [tt]) ≟ [tt]) "[]++[tt]=[tt]" ,
    assert (([tt] ++ []) ≟ [tt]) "[tt]++[]=[tt]" ,
    assert (([tt] ++ [ff]) ≟ [tt,ff]) "[tt]++[ff]=[tt,ff]" ,
    assert (([ff,tt] ++ [ff]) ≟ [ff,tt,ff]) "[ff,tt]++[ff]=[ff,tt,ff]" ,
    assert (not (([ff] ++ [tt]) ≟ [tt,ff])) "[ff]++[tt]≠[tt,ff]" ,
    assert (not (([tt] ++ [tt]) ≟ [tt,ff])) "[tt]++[tt]≠[tt,ff]" ,
    assert (reverse [tt,ff] ≟ [ff,tt]) "rev[tt,ff]=[ff,tt]" ,
    assert (reverse (reverse [tt,ff]) ≟ [tt,ff]) "rev(rev[tt,ff])=[tt,ff]" ,
    assert (not (reverse [tt,ff] ≟ [tt,ff])) "rev[tt,ff]≠[tt,ff]"
  )


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

module Data.Vec.Sigma where

open import Prelude
open import Data.Unit.UniversePolymorphic renaming (⊤ to ⊤′)

Vec⁺ : Type a → ℕ → Type a
Vec⁺ A zero    = A
Vec⁺ A (suc n) = A × Vec⁺ A n

Vec : Type a → ℕ → Type a
Vec A 0       = ⊤′
Vec A (suc n) = Vec⁺ A n

private variable n : ℕ

open import Data.List using (List; _∷_; [])

toList⁺ : Vec⁺ A n → List A
toList⁺ {n = zero } x = x ∷ []
toList⁺ {n = suc n} (x , xs) = x ∷ toList⁺ xs

toList : Vec A n → List A
toList {n = zero } _ = []
toList {n = suc n} = toList⁺

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
-- Regression, introduced by the fix of issue 1759

module Issue1815 where

module _ (A : Set) where

  record R1 : Set where
    field f1 : A

  record R2 : Set where
    field f2 : R1
    open R1 f2 public

-- Parameter A is hidden in type of field f1 in R1 ...
test1 : ∀ A (r : R1 A) → A
test1 A r = R1.f1 r

-- ... and should be so in the type of field f1 in R2, too.
shouldFail : ∀ A (r : R2 A) → A
shouldFail A r = R2.f1 A r

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.Vec.Relation.Binary.Equality.Propositional directly.
------------------------------------------------------------------------

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

module Data.Vec.Relation.Equality.Propositional where

open import Data.Vec.Relation.Binary.Equality.Propositional public


text: open import Issue1251.NonTerminating

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Builtin.Float

data ⊥ : Set where

defNegZero : -0.0 ≡ 0.0 → ⊥
defNegZero ()

primEqNegZero : primFloatEquality -0.0 0.0 ≡ false
primEqNegZero = refl

primLtNegZero₁ : primFloatNumericalLess 0.0 -0.0 ≡ false
primLtNegZero₁ = refl

primLtNegZero₂ : primFloatNumericalLess -0.0 0.0 ≡ false
primLtNegZero₂ = refl

primShowNegZero : primShowFloat -0.0 ≡ "-0.0"
primShowNegZero = refl

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


text:
{-# OPTIONS --universe-polymorphism #-}
open import Categories.Category
open import Categories.Object.BinaryProducts
open import Categories.Object.Exponentiating

module Categories.Object.Exponentiating.Adjunction {o ℓ e}
    (C : Category o ℓ e)
    (binary : BinaryProducts C)
    (Σ : Category.Obj C)
    (exponentiating : Exponentiating C binary Σ) where

open Category C
open BinaryProducts binary
open Exponentiating exponentiating

import Categories.Object.Product
open Categories.Object.Product C

import Categories.Object.Product.Morphisms
open Categories.Object.Product.Morphisms C

open Equiv
open HomReasoning

import Categories.Object.Exponentiating.Functor
open Categories.Object.Exponentiating.Functor C binary Σ exponentiating

open import Categories.Functor
  using (Functor; Contravariant)
  renaming (id to idF; _≡_ to _≡F_; _∘_ to _∘F_)

open import Categories.Adjunction hiding (_≡_; id)
open import Categories.NaturalTransformation
  using (NaturalTransformation; module NaturalTransformation)
open import Categories.Monad
  using (Monad)

Σ↑-Self-Adjunction : Adjunction (Functor.op Σ↑-Functor) Σ↑-Functor
Σ↑-Self-Adjunction = record
  { unit    = record
      { η       = λ _ → flip id
      ; commute = unit-commute
      }
  ; counit  = record
      { η       = λ _ → flip id
      ; commute = counit-commute
      }
  ; zig     = zig-zag
  ; zag     = zig-zag
  } where
    .lem₁ : ∀{A B C D}{f : (B × C) ⇒ D}{g : A ⇒ (C × B)}
      → (f ∘ swap ∘ second id) ∘ g
      ≡ f ∘ swap ∘ g
    lem₁ {A}{B}{C}{D}{f}{g} =
      begin
        (f ∘ swap ∘ second id) ∘ g
      ↓⟨ (refl ⟩∘⟨ refl ⟩∘⟨ second-id product) ⟩∘⟨ refl ⟩
        (f ∘ swap ∘ id) ∘ g
      ↓⟨ (refl ⟩∘⟨ identityʳ) ⟩∘⟨ refl ⟩
        (f ∘ swap) ∘ g
      ↓⟨ assoc ⟩
        f ∘ swap ∘ g
      ∎

    .lem₂ : ∀ {X Y}{f : X ⇒ Y}
      → eval {Σ↑ Y} ∘ first (flip id ∘ f)
      ≡ eval {X}    ∘ swap ∘ second [Σ↑ f ]
    lem₂ {X}{Y}{f} =
      begin
        eval {Σ↑ Y} ∘ first (flip id ∘ f)
      ↑⟨ refl ⟩∘⟨ first∘first ⟩
        eval {Σ↑ Y} ∘ first (flip id) ∘ first f
      ↑⟨ assoc ⟩
        (eval {Σ↑ Y} ∘ first (flip id)) ∘ first f
      ↓⟨ β ⟩∘⟨ refl ⟩
        (eval {Y} ∘ swap ∘ second id) ∘ first f
      ↓⟨ lem₁ ⟩
        eval {Y} ∘ swap ∘ first f
      ↓⟨ refl ⟩∘⟨ swap∘⁂ ⟩
        eval {Y} ∘ second f ∘ swap
      ↑⟨ assoc ⟩
        (eval {Y} ∘ second f) ∘ swap
      ↑⟨ β ⟩∘⟨ refl ⟩
        (eval {X} ∘ first (λ-abs X (eval {Y} ∘ second f))) ∘ swap
      ↓⟨ assoc ⟩
        eval {X} ∘ first (λ-abs X (eval {Y} ∘ second f)) ∘ swap
      ↑⟨ refl ⟩∘⟨ swap∘⁂ ⟩
        eval {X} ∘ swap ∘ second (λ-abs X (eval ∘ second f))
      ∎

    .unit-commute : ∀ {X Y} (f : X ⇒ Y)
      → flip id ∘ f ≡ [Σ² f ] ∘ flip id
    unit-commute {X}{Y} f =
      begin
        flip id ∘ f
      ↓⟨ λ-unique lem₂ ⟩
        flip [Σ↑ f ]
      ↑⟨ λ-cong lem₁ ⟩
        λ-abs (Σ↑ Y) ((eval {X} ∘ swap ∘ second id) ∘ second [Σ↑ f ])
      ↓⟨ λ-distrib ⟩
        [Σ↑ [Σ↑ f ] ] ∘ flip id
      ∎

    .counit-commute : ∀ {X Y} (f : X ⇒ Y)
      → [Σ² f ] ∘ flip id ≡ flip id ∘ f
    counit-commute f = sym (unit-commute f)

    .zig-zag : ∀{X}
      → id ≡ [Σ↑ flip id ] ∘ flip id
    zig-zag {X} =
      begin
        id
      ↑⟨ flip² ⟩
        flip (flip id)
      ↑⟨ λ-cong lem₁ ⟩
        λ-abs X ((eval ∘ swap ∘ second id) ∘ second (flip id))
      ↓⟨ λ-distrib ⟩
        [Σ↑ flip id ] ∘ flip id
      ∎

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module Test where

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

module Q where
  module R where
    f : Nat -> Nat
    f n = suc n

module B (n : Nat) where
  open Q.R public
  q = f n

module Bz = B zero

postulate
  _==_ : {A : Set} -> A -> A -> Set
  refl : {A : Set}{x : A} -> x == x

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.DStructures.Equivalences.GroupSplitEpiAction where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Function
open import Cubical.Foundations.Structure

open import Cubical.Data.Sigma
open import Cubical.Data.Unit

open import Cubical.Relation.Binary

open import Cubical.Structures.Subtype
open import Cubical.Algebra.Group
open import Cubical.Structures.LeftAction
open import Cubical.Algebra.Group.Semidirect

open import Cubical.DStructures.Base
open import Cubical.DStructures.Meta.Isomorphism
open import Cubical.DStructures.Structures.Group
open import Cubical.DStructures.Structures.SplitEpi
open import Cubical.DStructures.Structures.Action

open Kernel
open GroupHom -- such .fun!
open GroupLemmas
open MorphismLemmas

{-
After associating, we have two DURGs over Grp

 Grp × LAS × isAction   Grp × (F × B) × isSecRet
                 |     |
                  \    /
                   Grp

Action gives split mono:

    α             π₂
G₀ --> H   ↦  G₀ ↔ H ⋊⟨ α ⟩ G₀
                  ι₂

Split mono gives Action:

   σ            Ad∘ι
G₀ ↔ G₁   ↦ G₀ --> ker σ
   ι

-}

module _ (ℓ ℓ' : Level) where

  𝒮ᴰ-Iso-GroupAct-SplitEpi-* : 𝒮ᴰ-♭PIso (idfun (Group {ℓ}))
                                         (𝒮ᴰ-G\GLasAction ℓ (ℓ-max ℓ ℓ'))
                                         (𝒮ᴰ-G\GFBSplitEpi ℓ (ℓ-max ℓ ℓ'))
  RelIso.fun (𝒮ᴰ-Iso-GroupAct-SplitEpi-* G₀) (H , _α_ , isAct) = H⋊G₀ , (ι₂ α , π₂ α) , π₂-hasSec α
      where
        -- combine the action structure and axioms
        α = groupaction _α_ isAct
        -- semidirect product induced by the action α
        H⋊G₀ : Group {ℓ-max ℓ ℓ'}
        H⋊G₀ = H ⋊⟨ α ⟩ G₀
  RelIso.inv (𝒮ᴰ-Iso-GroupAct-SplitEpi-* G₀) (G₁ , (ι , σ) , isSplit) = ker-σ , _α_ , isAct
      where
        open GroupNotation₀ G₀
        open GroupNotation₁ G₁
        open SplitEpiNotation ι σ isSplit
        open IsGroupAction

        -- G₀ will act on ker σ
        ker-σ : Group {ℓ-max ℓ ℓ'}
        ker-σ = ker σ

        -- notation: group operation of ker σ
        _+ₖ_ = GroupStr._+_ (snd ker-σ)

        -- the left action structure of G₀ on ker σ
        -- is given by
        -- g α h := ιg + h - ιg
        _α_ : LeftActionStructure ⟨ G₀ ⟩ ⟨ ker-σ ⟩
        g α (h , p) = (ig +₁ h) -₁ ig , q
          where
            ig = 𝒾 g
            abstract
              -- proof that (ig +₁ h) -₁ ig
              -- lies in ker-σ
              q = s ((ig +₁ h) -₁ ig)
                    ≡⟨ σ .isHom (ig +₁ h) (-₁ ig) ⟩
                  s (ig +₁ h) +₀ s (-₁ ig)
                     ≡⟨ cong (s (ig +₁ h) +₀_)
                             (mapInv σ ig) ⟩
                  s (ig +₁ h) -₀ si g
                     ≡⟨ cong (_+₀ -₀ (s ig))
                             (σ .isHom ig h) ⟩
                  (si g +₀ s h) -₀ si g
                      ≡⟨ cong (λ z → ((si g) +₀ z) -₀ (si g))
                              p ⟩
                  ((si g) +₀ 0₀) -₀ (si g)
                      ≡⟨ cong (_+₀ -₀ (s ig))
                              (rId₀ (s ig)) ⟩
                  (si g) -₀ (si g)
                     ≡⟨ rCancel₀ (si g) ⟩
                  0₀ ∎

        -- proof that the left action structure α
        -- satisfies the group action axioms
        abstract
          isAct : IsGroupAction G₀ ker-σ _α_
          -- at every g, g α_ is a homomorphism, that is
          -- g α (h + h') ≡ g α h + g α h'
          isAct .isHom g (h , p) (h' , p') = subtypeWitnessIrrelevance (sg-typeProp σ) q
            where
              ig = ι .fun g
              -ig = -₁ ig
              q = fst (g α ((h , p) +ₖ (h' , p')))
                      ≡⟨ refl ⟩
                  (ig +₁ (h +₁ h')) -₁ ig
                      ≡⟨ cong (λ z → (ig +₁ (z +₁ h')) +₁ (-₁ ig))
                              (sym (rId₁ h)
                                ∙ cong (h +₁_) (sym (lCancel₁ ig))) ⟩
                  (ig +₁ ((h +₁ (-ig +₁ ig)) +₁ h')) -₁ ig
                      ≡⟨ cong (λ z → (ig +₁ (z +₁ h')) -₁ ig)
                              (assoc₁ h -ig ig) ⟩
                  (ig +₁ (((h +₁ -ig) +₁ ig) +₁ h')) -₁ ig
                      ≡⟨ cong (λ z → (ig +₁ z) -₁ ig)
                              (sym (assoc₁ (h -₁ ig) ig h')) ⟩
                  (ig +₁ ((h +₁ -ig) +₁ (ig +₁ h'))) -₁ ig
                      ≡⟨ cong (_+₁ -ig)
                              (assoc₁ ig (h -₁ ig) (ig +₁ h')) ⟩
                  ((ig +₁ (h +₁ -ig)) +₁ (ig +₁ h')) -₁ ig
                       ≡⟨ cong (λ z → (z +₁ (ig +₁ h')) -₁ ig)
                               (assoc₁ ig h -ig) ⟩
                  (((ig +₁ h) +₁ -ig) +₁ (ig +₁ h')) -₁ ig
                    ≡⟨ sym (assoc₁ ((ig +₁ h) -₁ ig) (ig +₁ h') -ig) ⟩
                  ((ig +₁ h) +₁ -ig) +₁ ((ig +₁ h') +₁ -ig)
                       ≡⟨ refl ⟩
                  fst ((g α (h , p)) +ₖ (g α (h' , p'))) ∎
          -- α satisfies the identity law, that is
          -- 0 α h = h for every h
          isAct .identity (h , p) = subtypeWitnessIrrelevance (sg-typeProp σ) q
            where
              q = fst (0₀ α (h , p))
                      ≡⟨ cong (λ z → (z +₁ h) +₁ (-₁ z))
                              (mapId ι) ⟩
                  (0₁ +₁ h) +₁ (-₁ 0₁)
                    ≡⟨ cong ((0₁ +₁ h) +₁_)
                            (invId G₁) ∙∙
                       rId₁ (0₁ +₁ h) ∙∙
                       lId₁ h ⟩
                  h ∎
          -- α is associative in the sense that
          -- (g +₀ g') α h = g α (g' α h)
          isAct .assoc g g' (h , p) = subtypeWitnessIrrelevance (sg-typeProp σ) q
            where
              ig = ι .fun g
              ig' = ι .fun g'
              -ig = -₁ ig
              -ig' = -₁ ig'
              q = (ι .fun (g +₀ g') +₁ h) -₁ (ι .fun (g +₀ g'))
                     ≡⟨ cong (λ z → (z +₁ h) -₁ z)
                             (ι .isHom g g') ⟩
                  ((ig +₁ ig') +₁ h) -₁ (ig +₁ ig')
                    ≡⟨ cong (((ig +₁ ig') +₁ h) +₁_)
                            (invDistr G₁ ig ig') ⟩
                  ((ig +₁ ig') +₁ h) +₁ (-ig' -₁ ig)
                    ≡⟨ cong (_+₁ (-ig' +₁ -ig))
                            (sym (assoc₁ ig ig' h)) ⟩
                  (ig +₁ (ig' +₁ h)) +₁ (-ig' -₁ ig)
                    ≡⟨ assoc₁ (ig +₁ (ig' +₁ h)) -ig' -ig ⟩
                  ((ig +₁ (ig' +₁ h)) -₁ ig') -₁ ig
                    ≡⟨ cong (_+₁ -ig)
                            (sym (assoc₁ ig (ig' +₁ h) -ig')) ⟩
                  fst (g α (g' α (h , p))) ∎
        -- end of abstract
  RelIso.rightInv (𝒮ᴰ-Iso-GroupAct-SplitEpi-* G₀) (G₁ , (ι , σ) , isSplit) = G₁-≅ , (ι-≅ , σ-≅) , isSplit-≅
    where
      -- get our hands dirty with shameless reference to what we're constructing,
      -- such is the power of copatterns!
      -- back: turn the given split epi into the group action tuple ga
      ga = RelIso.inv (𝒮ᴰ-Iso-GroupAct-SplitEpi-* G₀) (G₁ , (ι , σ) , isSplit)
      -- map ga forth to the split epi tuple se'
      se' = RelIso.fun (𝒮ᴰ-Iso-GroupAct-SplitEpi-* G₀) ga

      -- notation

      -- short for (ker σ) ⋊⟨ Adᵢ ⟩ G₀
      kσ⋊G₀ = fst se'
      -- the group action ga
      _α_ = fst (snd ga)
      isAct = snd (snd ga)

      open GroupNotation₀ G₀
      open GroupNotation₁ G₁

      -- notational convention:
      -- g : ⟨ G₀ ⟩
      -- h : ⟨ G₁ ⟩
      -- p : witness that g is in ker σ

      open SplitEpiNotation ι σ isSplit

      -- (ker σ) ⋊⟨ Adᵢ ⟩ G₀ ≃ G₁
      G₁-≅ : GroupEquiv kσ⋊G₀ G₁
      GroupEquiv.eq G₁-≅ = isoToEquiv isom
        where
          isom : Iso ⟨ kσ⋊G₀ ⟩ ⟨ G₁ ⟩
          -- map forth is straight forward
          Iso.fun isom ((h , p) , g) = h +₁ 𝒾 g

          -- beginning of Iso.inv isom h

          -- G₁ part of the map
          fst (fst (Iso.inv isom h)) = h +₁ (is- h)
          -- proof that G₁ part is in ker σ
          snd (fst (Iso.inv isom h)) = q
            where
              abstract
                q = s (h +₁ is- h)
                      ≡⟨ σ .isHom h (is- h) ⟩
                    s h +₀ s (is- h)
                      ≡⟨ cong (s h +₀_)
                              (funExt⁻ (cong GroupHom.fun isSplit) (s- h)) ⟩
                    s h +₀ (s- h)
                      ≡⟨ cong (s h +₀_)
                              (mapInv σ h) ⟩
                    s h -₀ (s h)
                      ≡⟨ rCancel₀ (s h) ⟩
                    0₀ ∎
          -- G₀ part of the map
          snd (Iso.inv isom h) = s h

          -- end of Iso.inv isom h

          -- beginning of Iso.leftInv isom ((h , p) , g)

          Iso.leftInv isom ((h , p) , g) = ΣPathP (subtypeWitnessIrrelevance (sg-typeProp σ) q , q')
            where
              abstract
                q = (h +₁ 𝒾 g) +₁ is- (h +₁ 𝒾 g)
                       ≡⟨ cong (λ z → (h +₁ 𝒾 g) +₁ is z)
                               (invDistr G₁ h (𝒾 g)) ⟩
                    (h +₁ 𝒾 g) +₁ is ((-i g) -₁ h)
                      ≡⟨ cong (λ z → (h +₁ 𝒾 g) +₁ 𝒾 z)
                              (σ .isHom (-i g) (-₁ h)) ⟩
                    (h +₁ 𝒾 g) +₁ 𝒾 ((s-i g) +₀ (s- h))
                      ≡⟨ cong (λ z → (h +₁ 𝒾 g) +₁ 𝒾 ((s-i g) +₀ z))
                              (mapInv σ h ∙∙
                               cong -₀_ p ∙∙
                               invId G₀) ⟩
                    (h +₁ 𝒾 g) +₁ 𝒾 ((s-i g) +₀ 0₀)
                      ≡⟨ cong (λ z → (h +₁ 𝒾 g) +₁ 𝒾 z)
                              (rId₀ (s-i g)) ⟩
                    (h +₁ 𝒾 g) +₁ 𝒾 (s-i g)
                      ≡⟨ cong (λ z → (h +₁ 𝒾 g) +₁ 𝒾 z )
                              (mapInv σ (𝒾 g)) ⟩
                    (h +₁ 𝒾 g) +₁ 𝒾 (-si g)
                      ≡⟨ cong ((h +₁ 𝒾 g) +₁_)
                              (mapInv ι (si g)) ⟩
                    (h +₁ 𝒾 g) -₁ (isi g)
                      ≡⟨ cong (λ z → (h +₁ 𝒾 g) -₁ (𝒾 z))
                              (funExt⁻ (cong GroupHom.fun isSplit) g ) ⟩
                    (h +₁ 𝒾 g) -₁ (𝒾 g)
                      ≡⟨ sym (assoc₁ h (𝒾 g) (-i g)) ⟩
                    h +₁ (𝒾 g -₁ (𝒾 g))
                      ≡⟨ cong (h +₁_)
                              (rCancel₁ (𝒾 g)) ⟩
                    h +₁ 0₁
                      ≡⟨ rId₁ h ⟩
                    h ∎

                q' = s (h +₁ 𝒾 g)
                       ≡⟨ σ .isHom h (𝒾 g) ⟩
                     s h +₀ si g
                       ≡⟨ cong (_+₀ si g) p ⟩
                     0₀ +₀ si g
                       ≡⟨ lId₀ (si g) ⟩
                     si g
                       ≡⟨ funExt⁻ (cong GroupHom.fun isSplit) g ⟩
                     g ∎

          -- end of Iso.leftInv isom ((h , p) , g)

          Iso.rightInv isom h = q
            where
              ish = 𝒾 (s h)
              abstract
                q = (h +₁ 𝒾 (s (-₁ h))) +₁ ish
                       ≡⟨ cong (λ z → (h +₁ z) +₁ ish) (cong 𝒾 (mapInv σ h) ∙ mapInv ι (s h)) ⟩
                    (h +₁ (-₁ ish)) +₁ ish
                       ≡⟨ sym (assoc₁ h (-₁ ish) ish) ⟩
                    h +₁ ((-₁ ish) +₁ ish)
                       ≡⟨ (cong (h +₁_) (lCancel₁ ish)) ∙ (rId₁ h) ⟩
                    h ∎

          -- end of Iso.rightInv isom h

          -- end of Iso ⟨ kσ⋊G₀ ⟩ ⟨ G₁ ⟩

      GroupEquiv.isHom G₁-≅ ((h , p) , g) ((h' , p') , g') = q
        where
          abstract
            q = (h +₁ ((𝒾 g +₁ h') +₁ (-₁ 𝒾 g))) +₁ 𝒾 (g +₀ g')
                   ≡⟨ cong ((h +₁ ((𝒾 g +₁ h') +₁ (-₁ 𝒾 g))) +₁_)
                           (ι .isHom g g') ⟩
                (h +₁ ((𝒾 g +₁ h') +₁ (-₁ 𝒾 g))) +₁ (𝒾 g +₁ 𝒾 g')
                   ≡⟨ sym (assoc₁ h ((𝒾 g +₁ h') +₁ (-₁ 𝒾 g)) (𝒾 g +₁ 𝒾 g')) ⟩
                h +₁ (((𝒾 g +₁ h') +₁ (-₁ 𝒾 g)) +₁ (𝒾 g +₁ 𝒾 g'))
                   ≡⟨ cong (h +₁_)
                           (sym (assoc₁ (𝒾 g +₁ h') (-₁ 𝒾 g) (𝒾 g +₁ 𝒾 g'))) ⟩
                h +₁ ((𝒾 g +₁ h') +₁ ((-₁ 𝒾 g) +₁ (𝒾 g +₁ 𝒾 g')))
                   ≡⟨ cong (λ z → h +₁ ((𝒾 g +₁ h') +₁ z))
                           (assoc₁ (-₁ 𝒾 g) (𝒾 g) (𝒾 g')) ⟩
                h +₁ ((𝒾 g +₁ h') +₁ (((-₁ 𝒾 g) +₁ 𝒾 g) +₁ 𝒾 g'))
                   ≡⟨ cong (λ z → h +₁ ((𝒾 g +₁ h') +₁ (z +₁ 𝒾 g')))
                           (lCancel₁ (𝒾 g)) ⟩
                h +₁ ((𝒾 g +₁ h') +₁ (0₁ +₁ 𝒾 g'))
                   ≡⟨ cong (λ z → h +₁ ((𝒾 g +₁ h') +₁ z))
                           (lId₁ (𝒾 g')) ⟩
                h +₁ ((𝒾 g +₁ h') +₁ 𝒾 g')
                   ≡⟨ cong (h +₁_)
                           (sym (assoc₁ (𝒾 g) h' (𝒾 g'))) ⟩
                h +₁ (𝒾 g +₁ (h' +₁ 𝒾 g'))
                   ≡⟨ assoc₁ h (𝒾 g) (h' +₁ 𝒾 g') ⟩
                (h +₁ 𝒾 g) +₁ (h' +₁ 𝒾 g') ∎

      -- end of GroupEquiv kσ⋊G₀ G₁

      ι-≅ : (g : ⟨ G₀ ⟩) → 0₁ +₁ (𝒾 g) ≡ 𝒾 g
      ι-≅ g = lId₁ (𝒾 g)

      σ-≅ : (((h , _) , g) : ⟨ kσ⋊G₀ ⟩) → g ≡ s (h +₁ 𝒾 g)
      σ-≅ ((h , p) , g) = q
        where
          abstract
            q = g
                  ≡⟨ funExt⁻ (cong fun (sym isSplit)) g ⟩
                s (𝒾 g)
                  ≡⟨ sym (lId₀ (s (𝒾 g))) ⟩
                0₀ +₀ s (𝒾 g)
                  ≡⟨ cong (_+₀ s (𝒾 g)) (sym p) ⟩
                s h +₀ s (𝒾 g)
                  ≡⟨ sym (σ .isHom h (𝒾 g)) ⟩
                s (h +₁ 𝒾 g) ∎

      isSplit-≅ : Unit
      isSplit-≅ = tt
  RelIso.leftInv (𝒮ᴰ-Iso-GroupAct-SplitEpi-* G₀) (H , _α_ , isAct) =  H-≅ , α-≅ , isAct-≅
    where
      -- import notation
      open GroupNotation₀ G₀
      open GroupNotationᴴ H
      open ActionNotationα (groupaction _α_ isAct) using (α-id)

      se = RelIso.fun (𝒮ᴰ-Iso-GroupAct-SplitEpi-* G₀) (H , _α_ , isAct)
      ga' = RelIso.inv (𝒮ᴰ-Iso-GroupAct-SplitEpi-* G₀) se

      -- H under fun and then inv
      ker-π₂ = fst ga'
      -- the adjoint action w.t.r. ι₂
      _β_ = fst (snd ga')
      β-isAct = snd (snd ga')
      -- inclusion of G₀ into H ⋊⟨ α ⟩ G₀
      ι = ι₂ (groupaction _α_ isAct)
      𝒾 = ι .fun

      G₀-≅ : GroupEquiv G₀ G₀
      G₀-≅ = idGroupEquiv G₀

      H-≅ : GroupEquiv ker-π₂ H
      GroupEquiv.eq H-≅ = isoToEquiv isom
        where
          isom : Iso ⟨ ker-π₂ ⟩ ⟨ H ⟩
          Iso.fun isom ((h , g) , p) = h
          Iso.inv isom h = (h , 0₀) , refl
          Iso.leftInv isom ((h , g) , p) = q
            where
              abstract
                r : (h , 0₀) ≡ (h , g)
                r = ΣPathP (refl , sym p)
                q : ((h , 0₀) , refl) ≡ ((h , g) , p)
                q = ΣPathP (r , isProp→PathP (λ i → set₀ (snd (r i)) 0₀) refl p)
          Iso.rightInv isom h = refl

      GroupEquiv.isHom H-≅ ((h , g) , p) ((h' , g') , p') = q
        where
          abstract
            q : h +ᴴ (g α h') ≡ h +ᴴ h'
            q = h +ᴴ (g α h')
                  ≡⟨ cong (λ z → h +ᴴ (z α h')) p ⟩
                h +ᴴ (0₀ α h')
                  ≡⟨ cong (h +ᴴ_) (α-id h') ⟩
                h +ᴴ h' ∎

      α-≅ : (g : ⟨ G₀ ⟩) (((h , g') , p) : ⟨ ker-π₂ ⟩)
            → GroupEquiv.eq H-≅ .fst (g β ((h , g') , p)) ≡ g α h
      α-≅ g ((h , g') , p) = q
        where
          open ActionLemmas (groupaction _α_ isAct)
          abstract
            q = (0ᴴ +ᴴ (g α h)) +ᴴ ((g +₀ g') α ((-₀ g) α (-ᴴ 0ᴴ)))
                  ≡⟨ cong (_+ᴴ ((g +₀ g') α ((-₀ g) α (-ᴴ 0ᴴ))))
                          (lIdᴴ (g α h)) ⟩
                (g α h) +ᴴ ((g +₀ g') α ((-₀ g) α (-ᴴ 0ᴴ)))
                  ≡⟨ cong (λ z → (g α h) +ᴴ ((g +₀ g') α ((-₀ g) α z)))
                          (invId H) ⟩
                (g α h) +ᴴ ((g +₀ g') α ((-₀ g) α 0ᴴ))
                  ≡⟨ cong (λ z → (g α h) +ᴴ ((g +₀ g') α z))
                          (actOnUnit (-₀ g)) ⟩
                (g α h) +ᴴ ((g +₀ g') α 0ᴴ)
                  ≡⟨ cong ((g α h) +ᴴ_)
                          (actOnUnit (g +₀ g')) ⟩
                (g α h) +ᴴ 0ᴴ
                  ≡⟨ rIdᴴ (g α h) ⟩
                g α h ∎

      isAct-≅ : Unit
      isAct-≅ = tt

  IsoActionSplitEpi-* : Iso (GGLasAct ℓ (ℓ-max ℓ ℓ')) (SplitEpi' ℓ (ℓ-max ℓ ℓ'))
  IsoActionSplitEpi-* =
    𝒮ᴰ-♭PIso-Over→TotalIso idIso
                            (𝒮ᴰ-G\GLasAction ℓ (ℓ-max ℓ ℓ'))
                            (𝒮ᴰ-G\GFBSplitEpi ℓ (ℓ-max ℓ ℓ'))
                            𝒮ᴰ-Iso-GroupAct-SplitEpi-*

  IsoActionSplitEpi : Iso (Action ℓ (ℓ-max ℓ ℓ')) (SplitEpi ℓ (ℓ-max ℓ ℓ'))
  IsoActionSplitEpi = compIso (IsoAction ℓ (ℓ-max ℓ ℓ'))
                              (compIso IsoActionSplitEpi-* (IsoSplitEpi' ℓ (ℓ-max ℓ ℓ')))

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


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

open import lib.Base

module lib.PathGroupoid where

module _ {i} {A : Type i} where

  {- Concatenation of paths

  There are two different definitions of concatenation of paths, [_∙_] and [_∙'_],
  with different definitionnal behaviour. Maybe we should have only one but it’s
  sometimes useful to have both (in particular in lib.types.Paths).
  -}

  infixr 80 _∙_ _∙'_

  _∙_ : {x y z : A}
    → (x == y → y == z → x == z)
  idp ∙ q = q

  _∙'_ : {x y z : A}
    → (x == y → y == z → x == z)
  q ∙' idp = q

  ∙=∙' : {x y z : A} (p : x == y) (q : y == z)
    → p ∙ q == p ∙' q
  ∙=∙' idp idp = idp

  ∙'=∙ : {x y z : A} (p : x == y) (q : y == z)
    → p ∙' q == p ∙ q
  ∙'=∙ idp idp = idp

  ∙-assoc : {x y z t : A} (p : x == y) (q : y == z) (r : z == t)
    → (p ∙ q) ∙ r == p ∙ (q ∙ r)
  ∙-assoc idp _ _ = idp

  ∙'-assoc : {x y z t : A} (p : x == y) (q : y == z) (r : z == t)
    → (p ∙' q) ∙' r == p ∙' (q ∙' r)
  ∙'-assoc _ _ idp = idp

  -- [∙-unit-l] and [∙'-unit-r] are definitional

  ∙-unit-r : {x y : A} (q : x == y) → q ∙ idp == q
  ∙-unit-r idp = idp

  ∙'-unit-l : {x y : A} (q : x == y) → idp ∙' q == q
  ∙'-unit-l idp = idp

  {- Reversal of paths -}

  ! : {x y : A} → (x == y → y == x)
  ! idp = idp

  !-inv-l : {x y : A} (p : x == y) → (! p) ∙ p == idp
  !-inv-l idp = idp

  !-inv'-l : {x y : A} (p : x == y) → (! p) ∙' p == idp
  !-inv'-l idp = idp

  !-inv-r : {x y : A} (p : x == y) → p ∙ (! p) == idp
  !-inv-r idp = idp

  !-inv'-r : {x y : A} (p : x == y) → p ∙' (! p) == idp
  !-inv'-r idp = idp

  {- Interactions between operations

  A lemma of the form [!-∙ …] gives a result of the form [! (_∙_ …) == …],
  and so on.
  -}

  !-∙ : {x y z : A} (p : x == y) (q : y == z) → ! (p ∙ q) == ! q ∙ ! p
  !-∙ idp idp = idp

  ∙-! : {x y z : A} (q : y == z) (p : x == y) → ! q ∙ ! p == ! (p ∙ q)
  ∙-! idp idp = idp

  !-∙' : {x y z : A} (p : x == y) (q : y == z) → ! (p ∙' q) == ! q ∙' ! p
  !-∙' idp idp = idp

  ∙'-! : {x y z : A} (q : y == z) (p : x == y) → ! q ∙' ! p == ! (p ∙' q)
  ∙'-! idp idp = idp

  !-! : {x y : A} (p : x == y) → ! (! p) == p
  !-! idp = idp

  {- Horizontal compositions -}

  infixr 80 _∙2_ _∙'2_

  _∙2_ : {x y z : A} {p p' : x == y} {q q' : y == z} (α : p == p') (β : q == q')
    → p ∙ q == p' ∙ q'
  _∙2_ {p = idp} idp β = β

  _∙'2_ : {x y z : A} {p p' : x == y} {q q' : y == z} (α : p == p') (β : q == q')
    → p ∙' q == p' ∙' q'
  _∙'2_ {q = idp} α idp = α

  idp∙2idp : {x y z : A} (p : x == y) (q : y == z)
    → (idp {a = p}) ∙2 (idp {a = q}) == idp
  idp∙2idp idp idp = idp

  idp∙'2idp : {x y z : A} (p : x == y) (q : y == z)
    → (idp {a = p}) ∙'2 (idp {a = q}) == idp
  idp∙'2idp idp idp = idp

{-
Sometimes we need to restart a new section in order to have everything in the
previous one generalized.
-}
module _ {i} {A : Type i} where
  {- Whisker and horizontal composition for Eckmann-Hilton argument -}

  infixr 80 _∙ᵣ_ _⋆2_ _⋆'2_
  infixl 80 _∙ₗ_

  _∙ᵣ_ : {x y z : A} {p p' : x == y} (α : p == p') (q : y == z)
    → p ∙ q == p' ∙ q
  _∙ᵣ_ {p = p} {p' = p'} α idp = ∙-unit-r p ∙ α ∙ ! (∙-unit-r p')

  _∙ₗ_ : {x y z : A} {q q' : y == z} (p : x == y) (β : q == q')
    → p ∙ q == p ∙ q'
  _∙ₗ_ {q = q} {q' = q'} idp β = β

  _⋆2_ : {x y z : A} {p p' : x == y} {q q' : y == z}
         (α : p == p') (β : q == q')
    → p ∙ q == p' ∙ q'
  _⋆2_ {p' = p'} {q = q} α β = (α ∙ᵣ q) ∙ (p' ∙ₗ β)

  _⋆'2_ : {x y z : A} {p p' : x == y} {q q' : y == z}
          (α : p == p') (β : q == q')
    → p ∙ q == p' ∙ q'
  _⋆'2_ {p = p} {q' = q'} α β = (p ∙ₗ β) ∙ (α ∙ᵣ q')

  ⋆2=⋆'2 : {x y z : A} {p p' : x == y} {q q' : y == z}
           (α : p == p') (β : q == q')
    → α ⋆2 β == α ⋆'2 β
  ⋆2=⋆'2 {p = idp} {q = idp} idp idp = idp

module _ {i} {A : Type i} where

  anti-whisker-right : {x y z : A} (p : y == z) {q r : x == y}
    → (q ∙ p == r ∙ p → q == r)
  anti-whisker-right idp {q} {r} h =
    ! (∙-unit-r q) ∙ (h ∙ ∙-unit-r r)

  anti-whisker-left : {x y z : A} (p : x == y) {q r : y == z}
    → (p ∙ q == p ∙ r → q == r)
  anti-whisker-left idp h = h

{- Dependent stuff -}
module _ {i j} {A : Type i} {B : A → Type j} where

  {- Dependent constant path -}

  idpᵈ : {x : A} {u : B x} → u == u [ B ↓ idp ]
  idpᵈ = idp

  {- Dependent opposite path -}

  !ᵈ : {x y : A} {p : x == y} {u : B x} {v : B y}
    → (u == v [ B ↓ p ] → v == u [ B ↓ (! p)])
  !ᵈ {p = idp} = !

  !ᵈ' : {x y : A} {p : x == y} {u : B y} {v : B x}
    → (u == v [ B ↓ (! p) ] → v == u [ B ↓ p ])
  !ᵈ' {p = idp} = !

  !ᵈ-!ᵈ' : {x y : A} {p : x == y} {u : B y} {v : B x}
    → (q : u == v [ B ↓ (! p) ])
    → !ᵈ (!ᵈ' q) == q
  !ᵈ-!ᵈ' {p = idp} idp = idp

  {- Dependent concatenation -}

  infixr 80 _∙ᵈ_ _∙'ᵈ_ _◃_ _▹_ _!◃_ _▹!_

  _∙ᵈ_ : {x y z : A} {p : x == y} {p' : y == z}
    {u : B x} {v : B y} {w : B z}
    → (u == v [ B ↓ p ]
    → v == w [ B ↓ p' ]
    → u == w [ B ↓ (p ∙ p') ])
  _∙ᵈ_ {p = idp} {p' = idp} q r = q ∙ r

  _◃_ = _∙ᵈ_

  ◃idp : {x : A} {v w : B x} (q : w == v)
    → q ◃ idp == q
  ◃idp idp = idp

  idp◃ : {x y : A} {p : x == y}
    {u : B x} {v : B y} (r : u == v [ B ↓ p ])
    → idp ◃ r == r
  idp◃ {p = idp} r = idp

  _∙'ᵈ_ : {x y z : A} {p : x == y} {p' : y == z}
    {u : B x} {v : B y} {w : B z}
    → (u == v [ B ↓ p ]
    → v == w [ B ↓ p' ]
    → u == w [ B ↓ (p ∙' p') ])
  _∙'ᵈ_ {p = idp} {p' = idp} q r = q ∙' r

  _▹_ = _∙'ᵈ_

  {- That’s not perfect, because [q] could be a dependent path. But in that case
     this is not well typed… -}
  idp▹ : {x : A} {v w : B x} (q : v == w)
    → idp ▹ q == q
  idp▹ idp = idp

  ▹idp : {x y : A} {p : x == y}
    {u : B x} {v : B y} (q : u == v [ B ↓ p ])
    → q ▹ idp == q
  ▹idp {p = idp} idp = idp

  _▹!_ : {x y z : A} {p : x == y} {p' : z == y}
    {u : B x} {v : B y} {w : B z}
    → u == v [ B ↓ p ]
    → w == v [ B ↓ p' ]
    → u == w [ B ↓ p ∙' (! p') ]
  _▹!_ {p' = idp} q idp = q

  idp▹! : {x : A} {v w : B x} (q : w == v)
    → idp ▹! q == ! q
  idp▹! idp = idp

  _!◃_ : {x y z : A} {p : y == x} {p' : y == z}
    {u : B x} {v : B y} {w : B z}
    → v == u [ B ↓ p ]
    → v == w [ B ↓ p' ]
    → u == w [ B ↓ (! p) ∙ p' ]
  _!◃_ {p = idp} idp q = q

  !◃idp :{x : A} {v w : B x} (q : v == w)
    → q !◃ idp == ! q
  !◃idp idp = idp

  {-
  This is some kind of dependent horizontal composition (used in [apd∙]).
  -}

  infixr 80 _∙2ᵈ_ _∙'2ᵈ_

  _∙2ᵈ_ : {x y z : Π A B}
    {a a' : A} {p : a == a'} {q : x a == y a} {q' : x a' == y a'}
    {r : y a == z a} {r' : y a' == z a'}
    → (q == q'            [ (λ a → x a == y a) ↓ p ])
    → (r == r'            [ (λ a → y a == z a) ↓ p ])
    → (q ∙ r == q' ∙ r' [ (λ a → x a == z a) ↓ p ])
  _∙2ᵈ_ {p = idp} α β = α ∙2 β

  _∙'2ᵈ_ : {x y z : Π A B}
    {a a' : A} {p : a == a'} {q : x a == y a} {q' : x a' == y a'}
    {r : y a == z a} {r' : y a' == z a'}
    → (q == q'            [ (λ a → x a == y a) ↓ p ])
    → (r == r'            [ (λ a → y a == z a) ↓ p ])
    → (q ∙' r == q' ∙' r' [ (λ a → x a == z a) ↓ p ])
  _∙'2ᵈ_ {p = idp} α β = α ∙'2 β

  {-
  [apd∙] reduces a term of the form [apd (λ a → q a ∙ r a) p], do not confuse it
  with [apd-∙] which reduces a term of the form [apd f (p ∙ q)].
  -}

  apd∙ : {a a' : A} {x y z : Π A B}
    (q : (a : A) → x a == y a) (r : (a : A) → y a == z a)
    (p : a == a')
    → apd (λ a → q a ∙ r a) p == apd q p ∙2ᵈ apd r p
  apd∙ q r idp = ! (idp∙2idp (q _) (r _))

  apd∙' : {a a' : A} {x y z : Π A B}
    (q : (a : A) → x a == y a) (r : (a : A) → y a == z a)
    (p : a == a')
    → apd (λ a → q a ∙' r a) p == apd q p ∙'2ᵈ apd r p
  apd∙' q r idp = ! (idp∙'2idp (q _) (r _))

module _ {i j} {A : Type i} {B : A → Type j} where

  {- Exchange -}

  ▹-∙'2ᵈ : {x y z : Π A B}
    {a a' a'' : A} {p : a == a'} {p' : a' == a''}
    {q0 : x a == y a} {q0' : x a' == y a'}
    {r0 : y a == z a} {r0' : y a' == z a'}
    {q0'' : x a'' == y a''} {r0'' : y a'' == z a''}
    (q : q0 == q0' [ (λ a → x a == y a) ↓ p ])
    (r : r0 == r0' [ (λ a → y a == z a) ↓ p ])
    (s : q0' == q0'' [ (λ a → x a == y a) ↓ p' ])
    (t : r0' == r0'' [ (λ a → y a == z a) ↓ p' ])
    → (q ∙'2ᵈ r) ▹ (s ∙'2ᵈ t) == (q ▹ s) ∙'2ᵈ (r ▹ t)
  ▹-∙'2ᵈ {p = idp} {p' = idp} {q0} {.q0} {r0} {.r0} idp idp idp idp =
    ap (λ u → (idp {a = q0} ∙'2 idp {a = r0}) ∙' u) (idp∙'2idp q0 r0)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module Lec2Start where

open import Lec1Done

------------------------------------------------------------------------------
-- Vectors  -- the star of exercise 1
------------------------------------------------------------------------------

data Vec (X : Set) : Nat -> Set where  -- like lists, but length-indexed
  []   :                              Vec X zero
  _,-_ : {n : Nat} -> X -> Vec X n -> Vec X (suc n)
infixr 4 _,-_   -- the "cons" operator associates to the right

------------------------------------------------------------------------------
-- Taking a Prefix of a Vector
------------------------------------------------------------------------------

{-+}
vTake : (m n : Nat) -> m >= n -> {X : Set} -> Vec X m -> Vec X n
vTake m       n    m>=n xs = {!!}
{+-}

------------------------------------------------------------------------------
-- Things to Prove
------------------------------------------------------------------------------

{-+}
vTakeIdFact : (n : Nat){X : Set}(xs : Vec X n) ->
              vTake n n (refl->= n) xs == xs
vTakeIdFact n xs = {!!}

vTakeCpFact : (m n p : Nat)(m>=n : m >= n)(n>=p : n >= p)
              {X : Set}(xs : Vec X m) ->
              vTake m p (trans->= m n p m>=n n>=p) xs ==
                vTake n p n>=p (vTake m n m>=n xs)
{- hit p first: why? -}
vTakeCpFact m n p m>=n n>=p xs = {!!}
{+-}

------------------------------------------------------------------------------
-- Splittings (which bear some relationship to <= from ex1)
------------------------------------------------------------------------------

data _<[_]>_ : Nat -> Nat -> Nat -> Set where
  zzz : zero <[ zero ]> zero
  lll : {l m r : Nat} ->      l <[     m ]> r
                      ->  suc l <[ suc m ]> r
  rrr : {l m r : Nat} ->      l <[     m ]>     r
                      ->      l <[ suc m ]> suc r

{-+}
_>[_]<_ : {X : Set}{l m r : Nat} ->
          Vec X l -> l <[ m ]> r -> Vec X r ->
          Vec X m
xl >[ nnn ]< xr = {!!}
{+-}

{-+}
data FindSplit {X : Set}{l m r : Nat}(nnn : l <[ m ]> r)
     : (xs : Vec X m) -> Set where
  splitBits : (xl : Vec X l)(xr : Vec X r) -> FindSplit nnn (xl >[ nnn ]< xr)
{+-}

{-+}
findSplit : {X : Set}{l m r : Nat}(nnn : l <[ m ]> r)(xs : Vec X m) ->
            FindSplit nnn xs
findSplit nnn xs = {!!}
{+-}

------------------------------------------------------------------------------
-- what I should remember to say
------------------------------------------------------------------------------

-- What's the difference between m>=n and m >= n ?
   {- m>=n (without spaces) is just an identifier; it could be anything,
      but it has been chosen to be suggestive of its *type* which is
      m >= n (with spaces) which is the proposition that m is at least n.
      By "proposition", I mean "type with at most one inhabitant", where
      we care more about whether there is an inhabitant or not than which
      one (because there's never a choice). Finished code does not show
      us the types of its components, and that's not always a good thing.
      Here, by picking nice names, we get something of an aide-memoire. -}

-- What does (x ,-_) mean?
   {- It's a "left section". Right sections (_,- xs) also exist sometimes.
      Why only sometimes? -}

-- "Why is it stuck?"
   {- Proof by induction isn't just flailing about, you know? The trick is
      to pick the case analysis that provokes the "stuck" programs to do a
      step of computation. Then the same reasoning that justifies the
      termination of the program will justify the induction in a proof
      about it. -}

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

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

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


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

open import lib.Basics
open import lib.types.Group
open import lib.types.CommutingSquare
open import lib.groups.Homomorphism
open import lib.groups.Isomorphism

module lib.groups.CommutingSquare where

-- A new type to keep the parameters.
record CommSquareᴳ {i₀ i₁ j₀ j₁}
  {G₀ : Group i₀} {G₁ : Group i₁} {H₀ : Group j₀} {H₁ : Group j₁}
  (φ₀ : G₀ →ᴳ H₀) (φ₁ : G₁ →ᴳ H₁) (ξG : G₀ →ᴳ G₁) (ξH : H₀ →ᴳ H₁)
  : Type (lmax (lmax i₀ i₁) (lmax j₀ j₁)) where
  constructor comm-sqrᴳ
  field
    commutesᴳ : ∀ g₀ → GroupHom.f (ξH ∘ᴳ φ₀) g₀ == GroupHom.f (φ₁ ∘ᴳ ξG) g₀

infix 0 _□$ᴳ_
_□$ᴳ_ = CommSquareᴳ.commutesᴳ

CommSquareᴳ-∘v : ∀ {i₀ i₁ i₂ j₀ j₁ j₂}
  {G₀ : Group i₀} {G₁ : Group i₁} {G₂ : Group i₂}
  {H₀ : Group j₀} {H₁ : Group j₁} {H₂ : Group j₂}
  {φ : G₀ →ᴳ H₀} {ψ : G₁ →ᴳ H₁} {χ : G₂ →ᴳ H₂}
  {ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁}
  {μA : G₁ →ᴳ G₂} {μB : H₁ →ᴳ H₂}
  → CommSquareᴳ ψ χ μA μB
  → CommSquareᴳ φ ψ ξG ξH
  → CommSquareᴳ φ χ (μA ∘ᴳ ξG) (μB ∘ᴳ ξH)
CommSquareᴳ-∘v {ξG = ξG} {μB = μB} (comm-sqrᴳ □₁₂) (comm-sqrᴳ □₀₁) =
  comm-sqrᴳ λ g₀ → ap (GroupHom.f μB) (□₀₁ g₀) ∙ □₁₂ (GroupHom.f ξG g₀)

CommSquareᴳ-inverse-v : ∀ {i₀ i₁ j₀ j₁}
  {G₀ : Group i₀} {G₁ : Group i₁} {H₀ : Group j₀} {H₁ : Group j₁}
  {φ₀ : G₀ →ᴳ H₀} {φ₁ : G₁ →ᴳ H₁} {ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁}
  → CommSquareᴳ φ₀ φ₁ ξG ξH
  → (ξG-ise : is-equiv (GroupHom.f ξG)) (ξH-ise : is-equiv (GroupHom.f ξH))
  → CommSquareᴳ φ₁ φ₀ (GroupIso.g-hom (ξG , ξG-ise)) (GroupIso.g-hom (ξH , ξH-ise))
CommSquareᴳ-inverse-v (comm-sqrᴳ □) ξG-ise ξH-ise =
  comm-sqrᴳ (commutes (CommSquare-inverse-v (comm-sqr □) ξG-ise ξH-ise))

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
module Control.SimplePar where

open import Prelude
open import Builtin.Float
open import Builtin.Coinduction

Val : Set
Val = Float

data IVar (A : Set) : Set where
  ivar : Int → IVar A

data Trace : Set where
  Get  : IVar Val → (Val -> Trace) → Trace
  Put  : IVar Val → Val → Trace → Trace
  New  : (IVar Val -> Trace) → Trace
  Fork : Trace → Trace → Trace
  Done : Trace

record Par (A : Set) : Set where
  constructor par
  field
    runCont : (A → Trace) → Trace

instance
  FunctorPar : Functor Par
  fmap {{FunctorPar}} f (par runCont) = par λ c → runCont (c ∘ f)

  ApplicativePar : Applicative Par
  pure  {{ApplicativePar}} a = par λ c → c a
  _<*>_ {{ApplicativePar}} (par runCont₁) (par runCont₂) =
    par λ bcont → runCont₁ λ a → runCont₂ λ ab → bcont (a ab)

  MonadPar : Monad Par
  _>>=_ {{MonadPar}} (par runCont') k =
    par λ c → runCont' λ a → Par.runCont (k a) c

data Stream (A : Set) : Set where
  _∷_ : (a : A) (as : ∞ (Stream A)) → Stream A

instance
  FunctorStream : Functor Stream
  fmap {{FunctorStream}} f (a ∷ as) = f a ∷ ♯ fmap f (♭ as)

data IntMap (A : Set) : Set where
  ε      : IntMap A
  _↦_,_ : Int → A → IntMap A → IntMap A

find : {A : Set} → Int → IntMap A → Maybe A
find x ε = nothing
find x (y ↦ a , m) =
  ifYes x == y then just a else find x m

remove : {A : Set} → Int → IntMap A → IntMap A
remove x ε = ε
remove x (y ↦ a , m) =
  ifYes x == y
    then remove x m
    else y ↦ a , remove x m

insertWith : {A : Set} → (A → A → A) → Int → A → IntMap A → IntMap A
insertWith f x a ε = x ↦ a , ε
insertWith f x a (y ↦ b , m) =
  ifYes x == y
    then y ↦ f a b , insertWith f x a m
    else x ↦ a     , insertWith f x a m

infix 2 _∌_
infix 3 _↦ε,_ _↦_,_

data Heap : Set
data _∌_ : Heap → Int → Set

data Heap where
  ∅ : Heap
  _↦ε,_ : (ix : Int) → (h : Heap) → ⦃ p : h ∌ ix ⦄ → Heap
  _↦_,_ : (ix : Int) → (v : Val) → (h : Heap) → ⦃ p : h ∌ ix ⦄ → Heap

data _∌_ where
  ∅∌ : {ix : Int} → ∅ ∌ ix
  ε∌ : {ix ix' : Int} {h : Heap}
     → ⦃ p : h ∌ ix ⦄ → ¬ (ix' ≡ ix) → ix ↦ε, h ∌ ix'
  v∌ : {ix ix' : Int} {h : Heap} {v : Val}
     → ⦃ p : h ∌ ix ⦄ → ¬ (ix' ≡ ix) → ix ↦ v , h ∌ ix'

-- data Lookup (ix : Int) (h : Heap) : Maybe Val → Dec (h ∌ ix) → Set where
--   isn : ⦃ p : h ∌ ix ⦄ → Lookup ix h nothing (yes p)
--   isε : ⦃ p : ¬ (h ∌ ix) ⦄ → Lookup ix h nothing (no p)
--   isval : (v : Val) → ⦃ p : ¬ (h ∌ ix) ⦄ → Lookup ix h (just v) (no p)

-- lookupHeap : (ix : Int) → (h : Heap) → Σ (Maybe Val) (λ v → Σ (Dec (h ∌ ix)) (λ p → Lookup ix h v p))
-- lookupHeap ix ∅ = nothing , yes ∅∌ , isn
-- lookupHeap ix (ix' ↦ε, h) with ix == ix'
-- ... | yes refl = nothing , no (λ { (ε∌ p) → p refl }) , isε
-- ... | no p with lookupHeap ix h
-- ... | (.nothing , .(yes _) , isn) = nothing , yes (ε∌ p) , isn
-- ... | (.nothing , .(no _) , isε) = nothing , yes (ε∌ p) , isn
-- ... | (.(just v) , .(no _) , isval v) = just v , no (λ { (ε∌ q) → {!!} }) , {!isval!}
-- lookupHeap ix (ix' ↦ v , h) = {!!}

lookupHeap : (ix : Int) → (h : Heap) → Maybe Val × Dec (h ∌ ix)
lookupHeap ix ∅ = nothing , yes ∅∌
lookupHeap ix (ix' ↦ε, h) with ix == ix'
... | yes refl = nothing , no λ { (ε∌ p) → p refl }
... | no p = fst (lookupHeap ix h) , yes (ε∌ p)
lookupHeap ix (ix' ↦ v , h) with ix == ix'
... | yes refl = just v , no λ { (v∌ p) → p refl }
... | no p = fst (lookupHeap ix h) , yes (v∌ p)

infix 2 _≤ₕ_

data _≤ₕ_ : Heap → Heap → Set where
  h≤h : {h : Heap} → h ≤ₕ h
  h≤ε : {h : Heap} {ix : Int} ⦃ p : h ∌ ix ⦄
      → h ≤ₕ ix ↦ε, h
  h≤v : {h : Heap} {ix : Int} {v : Val} ⦃ p : h ∌ ix ⦄
      → h ≤ₕ ix ↦ v , h
  ε≤v : {h : Heap} {ix : Int} {v : Val} ⦃ p : h ∌ ix ⦄
      → ix ↦ε, h ≤ₕ ix ↦ v , h
  h≤s : {h₁ h₂ : Heap} {ix : Int} {v w : Val} ⦃ p₁ : h₁ ∌ ix ⦄ ⦃ p₂ : h₂ ∌ ix ⦄
      → h₁ ≤ₕ h₂ → v ≤ w → ix ↦ v , h₁ ≤ₕ ix ↦ w , h₂

Blkd = IntMap (List (Val → Trace))

data Exn : Set where
  Deadlock : Blkd → Exn
  MultiplePut : Val → Int → Val → Exn

yank : {A : Set} → Nat → A → List A → A × List A
yank n x xs =
  case splitAt (natMod (length (x ∷ xs)) n) (x ∷ xs) of
    λ { (hd , []) → x , hd
      ; (hd , x ∷ tl) → x , hd ++ tl
      }

step : (Trace × List Trace) → Blkd → Int → Heap → Either Exn (List Trace × Blkd × Int × Heap)
sched : Stream Nat → List Trace → Blkd → Int → Heap → Either Exn Heap

{-# TERMINATING #-}
sched randoms [] ε cntr heap =
  return heap
sched randoms [] blkd cntr heap =
  left (Deadlock blkd)
sched (rnd ∷ rs) (t ∷ ts) blkd cntr heap =
  caseM step (yank rnd t ts) blkd cntr heap of
    λ { (threads' , blkd' , cntr' , heap') →
          sched (♭ rs) threads' blkd' cntr' heap' }
step (Get (ivar ix) k , others) blkd cntr heap =
  case lookupHeap ix heap of
    λ { (nothing , p) → return (others , insertWith _++_ ix [ k ] blkd , cntr , heap)
      ; (just v  , p) → return (k v ∷ others , blkd , cntr , heap) }
step (Put (ivar ix) v t₂ , others) blkd cntr heap =
  case lookupHeap ix heap of
    λ { (nothing , yes p) → case find ix blkd of
        λ { nothing → return (t₂ ∷ others , blkd , cntr , (ix ↦ v , heap) ⦃ p = p ⦄)
          ; (just ls) → return (t₂ ∷ map (λ k → k v) ls ++ others , remove ix blkd , cntr , heap) }
      ; (nothing , no p) → case find ix blkd of
        λ { nothing → return {!!}
          ; (just ls) → return (t₂ ∷ map (λ k → k v) ls ++ others , remove ix blkd , cntr , heap) }
      ; (just v₀ , _) → left (MultiplePut v ix v₀) }

    -- λ { nothing → case find ix blkd of
    --     λ { nothing → return (t₂ ∷ others , blkd , cntr , ix ↦ v , {!!})
    --       ; (just ls) → {!!} }
    --   ; (just v) → {!!} }
  -- let heap' = ix ↦ v , heap
  -- in case (lookupHeap ix heap) of
  --     λ { nothing → case find ix blkd of
  --       λ { nothing → return (t₂ ∷ others , blkd , cntr , heap')
  --         ; (just ls) → return (t₂ ∷ map (λ k → k v) ls ++ others , remove ix blkd , cntr , heap) }
  --       ; (just v₀) → left (MultiplePut v ix v₀) }
step (New k , others) blkd cntr heap =
  return (k (ivar cntr) ∷ others , blkd , cntr + 1 , {!!})
  -- return (k (ivar cntr) ∷ others , blkd , cntr + 1 , cntr ↦ε, heap)
step (Fork t₁ t₂ , others) blkd cntr heap =
  return (t₁ ∷ t₂ ∷ others , blkd , cntr , heap)
step (Done , others) blkd cntr heap =
  return (others , blkd , cntr , heap)

monotonicity : ∀ {threads} {blkd} {cntr} {heap}
             → ∀ {threads'} {blkd'} {cntr'} {heap'}
             → step threads blkd cntr heap ≡ right (threads' , blkd' , cntr' , heap')
             → heap ≤ₕ heap'
monotonicity {Get (ivar ix) k , others} {heap = heap} p with (lookupHeap ix heap)
monotonicity {Get (ivar ix) k , others} p | q = {!!}
monotonicity {Put (ivar ix) v t₂ , others} {heap = heap} p with (lookupHeap ix heap)
monotonicity {Put (ivar ix) v t₂ , others} {blkd = blkd} p | q = {!!}
monotonicity {New k , others} p = {!!}
monotonicity {Fork t₁ t₂ , others} p = {!!}
monotonicity {Done , others} p = {!!}

max_stars_repo_name: lkuper/verified-instances

max_issues_repo_name: ranjitjhala/verified-instances

max_forks_repo_name: ranjitjhala/verified-instances


text:
-- Andreas, 2019-05-03, issue #3732
--
-- Do not erase constructor arguments when bound to Haskell data type.
-- Otherwise, it is not predictable how the Haskell constructors should look like.

-- {-# OPTIONS -v compile:100 #-}

open import Agda.Builtin.IO
open import Agda.Builtin.Unit

{-# FOREIGN GHC data I = Bar #-}
{-# FOREIGN GHC data S = Foo I #-}

module NonMutual where

  data I : Set where
    bar : I

  {-# COMPILE GHC I = data I (Bar) #-}

  data S : Set where
    foo :  (i : I) → S

  {-# COMPILE GHC S = data S (Foo) #-}

-- It could be that an earlier type embeds a later type, by virtue of mutual blocks:

{-# FOREIGN GHC data I2 = Bar2 #-}
{-# FOREIGN GHC data S2 = Foo2 I2 #-}

module Mutual where

 mutual

  data S : Set where
    foo :  (i : I) → S

  {-# COMPILE GHC S = data S2 (Foo2) #-}

  data I : Set where
    bar : I

  {-# COMPILE GHC I = data I2 (Bar2) #-}

postulate
  main : IO ⊤

{-# COMPILE GHC main = return () #-}


text: module Metalogic.Linear.SequentCalculus {ℓₚ} (Proposition : Set(ℓₚ)) where

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

open import lib.Base
open import lib.Function
open import lib.PathFunctor
open import lib.PathGroupoid

module lib.path-seq.Concat {i} {A : Type i} where

infixr 80 _∙∙_
_∙∙_ : {a a' a'' : A}
  → a =-= a' → a' =-= a'' → a =-= a''
_∙∙_ [] t = t
_∙∙_ (p ◃∙ s) t = p ◃∙ (s ∙∙ t)

∙∙-assoc : {a a' a'' a''' : A}
  (s : a =-= a') (t : a' =-= a'') (u : a'' =-= a''')
  → (s ∙∙ t) ∙∙ u == s ∙∙ (t ∙∙ u)
∙∙-assoc [] t u = idp
∙∙-assoc (p ◃∙ s) t u = ap (p ◃∙_) (∙∙-assoc s t u)

∙∙-unit-r : {a a' : A} (s : a =-= a')
  → s ∙∙ [] == s
∙∙-unit-r [] = idp
∙∙-unit-r (p ◃∙ s) = ap (p ◃∙_) (∙∙-unit-r s)

infixl 80 _∙▹_
_∙▹_ : {a a' a'' : A}
  → a =-= a' → a' == a'' → a =-= a''
_∙▹_ {a} {a'} {a''} s p = s ∙∙ (p ◃∙ [])

↯-∙∙ : {a a' a'' : A} (s : a =-= a') (t : a' =-= a'')
  → ↯ (s ∙∙ t) == ↯ s ∙ ↯ t
↯-∙∙ [] t = idp
↯-∙∙ (p ◃∙ []) [] = ! (∙-unit-r p)
↯-∙∙ (p ◃∙ []) (p' ◃∙ t) = idp
↯-∙∙ (p ◃∙ s@(_ ◃∙ _)) t =
  ap (λ y → p ∙ y) (↯-∙∙ s t) ∙
  ! (∙-assoc p (↯ s) (↯ t))

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda