text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.ZCohomology.MayerVietorisUnreduced where

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.Properties
open import Cubical.ZCohomology.KcompPrelims

open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Data.Sigma
open import Cubical.HITs.Pushout
open import Cubical.HITs.Sn
open import Cubical.HITs.S1
open import Cubical.HITs.Susp
open import Cubical.HITs.SetTruncation renaming (rec to sRec ; rec2 to sRec2 ; elim to sElim ; elim2 to sElim2)
open import Cubical.HITs.PropositionalTruncation renaming (rec to pRec ; elim to pElim ; elim2 to pElim2 ; ∥_∥ to ∥_∥₁ ; ∣_∣ to ∣_∣₁)
open import Cubical.Data.Nat
open import Cubical.Data.Prod hiding (_×_)
open import Cubical.Algebra.Group
open import Cubical.HITs.Truncation renaming (elim to trElim ; map to trMap ; rec to trRec ; elim3 to trElim3)

open GroupHom

module MV {ℓ ℓ' ℓ''} (A : Type ℓ) (B : Type ℓ') (C : Type ℓ'') (f : C → A) (g : C → B) where
  -- Proof from Brunerie 2016.
  -- We first define the three morphisms involved: i, Δ and d.

  private
    i* : (n : ℕ) → coHom n (Pushout f g) → coHom n A × coHom n B
    i* _ = sRec (isSet× setTruncIsSet setTruncIsSet) λ δ → ∣ (λ x → δ (inl x)) ∣₂ , ∣ (λ x → δ (inr x)) ∣₂

  iIsHom : (n : ℕ) → isGroupHom (coHomGr n (Pushout f g)) (×coHomGr n A B) (i* n)
  iIsHom _ = sElim2 (λ _ _ → isOfHLevelPath 2 (isSet× setTruncIsSet setTruncIsSet) _ _) λ _ _ → refl

  i : (n : ℕ) → GroupHom (coHomGr n (Pushout f g)) (×coHomGr n A B)
  GroupHom.fun (i n) = i* n
  GroupHom.isHom (i n) = iIsHom n

  private
    distrLem : (n : ℕ) (x y z w : coHomK n) → (x +[ n ]ₖ y) -[ n ]ₖ (z +[ n ]ₖ w) ≡ (x -[ n ]ₖ z) +[ n ]ₖ (y -[ n ]ₖ w)
    distrLem n x y z w =
         cong (ΩKn+1→Kn n) (cong₂ (λ q p → q ∙ sym p) (+ₖ→∙ n x y) (+ₖ→∙ n z w)
                        ∙∙ cong ((Kn→ΩKn+1 n x ∙ Kn→ΩKn+1 n y) ∙_) (symDistr (Kn→ΩKn+1 n z) (Kn→ΩKn+1 n w))
                        ∙∙ ((sym (assoc (Kn→ΩKn+1 n x) (Kn→ΩKn+1 n y) _))
                        ∙∙ cong (Kn→ΩKn+1 n x ∙_) (assoc (Kn→ΩKn+1 n y) (sym (Kn→ΩKn+1 n w)) (sym (Kn→ΩKn+1 n z)))
                        ∙∙ (cong (Kn→ΩKn+1 n x ∙_) (isCommΩK (suc n) _ _)
                        ∙∙ assoc _ _ _
                        ∙∙ cong₂ _∙_ (sym (Iso.rightInv (Iso-Kn-ΩKn+1 n) (Kn→ΩKn+1 n x ∙ sym (Kn→ΩKn+1 n z))))
                                     (sym (Iso.rightInv (Iso-Kn-ΩKn+1 n) (Kn→ΩKn+1 n y ∙ sym (Kn→ΩKn+1 n w)))))))

    Δ' : (n : ℕ) → ⟨ ×coHomGr n A B ⟩ → ⟨ coHomGr n C ⟩
    Δ' n (α , β) = coHomFun n f α -[ n ]ₕ coHomFun n g β

    Δ'-isMorph : (n : ℕ) → isGroupHom (×coHomGr n A B) (coHomGr n C) (Δ' n)
    Δ'-isMorph n =
      prodElim2 (λ _ _ → isOfHLevelPath 2 setTruncIsSet _ _ )
        λ f' x1 g' x2 i → ∣ (λ x → distrLem n (f' (f x)) (g' (f x)) (x1 (g x)) (x2 (g x)) i) ∣₂

  Δ : (n : ℕ) → GroupHom (×coHomGr n A B) (coHomGr n C)
  GroupHom.fun (Δ n) = Δ' n
  GroupHom.isHom (Δ n) = Δ'-isMorph n

  d-pre : (n : ℕ) → (C → coHomK n) → Pushout f g → coHomK (suc n)
  d-pre n γ (inl x) = 0ₖ (suc n)
  d-pre n γ (inr x) = 0ₖ (suc n)
  d-pre zero γ (push a i) = Kn→ΩKn+1 zero (γ a) i
  d-pre (suc n) γ (push a i) = Kn→ΩKn+1 (suc n) (γ a) i

  dHomHelperPath : (n : ℕ) (h l : C → coHomK n) (a : C) → I → I → coHomK (suc n)
  dHomHelperPath zero h l a i j =
    hcomp (λ k → λ { (i = i0) → lUnitₖ 1 (0ₖ 1) (~ j)
                   ; (i = i1) → lUnitₖ 1 (0ₖ 1) (~ j)
                   ; (j = i0) → +ₖ→∙ 0 (h a) (l a) (~ k) i
                   ; (j = i1) → cong₂Funct (λ x y → x +[ 1 ]ₖ y)
                                           (Kn→ΩKn+1 0 (h a)) (Kn→ΩKn+1 0 (l a)) (~ k) i})
          (bottom i j)
       where
       bottom : I → I → coHomK 1
       bottom i j = hcomp (λ k → λ { (i = i0) → lUnitₖ 1 (0ₖ 1) (~ j)
                                   ; (i = i1) → lUnitₖ 1 (Kn→ΩKn+1 0 (l a) k) (~ j) })
                          (anotherbottom i j)

         where
         anotherbottom : I → I → coHomK 1
         anotherbottom i j =  hcomp (λ k → λ { (i = i0) → rUnitlUnit0 1 k (~ j)
                                             ; (i = i1) → rUnitlUnit0 1 k (~ j)
                                             ; (j = i0) → Kn→ΩKn+1 0 (h a) i
                                             ; (j = i1) → Kn→ΩKn+1 0 (h a) i +[ 1 ]ₖ 0ₖ 1 })
                                    (rUnitₖ 1 (Kn→ΩKn+1 0 (h a) i) (~ j))
  dHomHelperPath (suc n) h l a i j =
    hcomp (λ k → λ { (i = i0) → lUnitₖ (2 + n) (0ₖ (2 + n)) (~ j)
                   ; (i = i1) → lUnitₖ (2 + n) (0ₖ (2 + n)) (~ j)
                   ; (j = i0) → +ₖ→∙ (suc n) (h a) (l a) (~ k) i
                   ; (j = i1) → cong₂Funct (λ x y → x +[ 2 + n ]ₖ y)
                                           (Kn→ΩKn+1 (suc n) (h a)) (Kn→ΩKn+1 (suc n) (l a)) (~ k) i})
          (bottom i j)
      where
      bottom : I → I → coHomK (2 + n)
      bottom i j = hcomp (λ k → λ { (i = i0) → lUnitₖ (2 + n) (0ₖ (2 + n)) (~ j)
                                  ; (i = i1) → lUnitₖ (2 + n) (Kn→ΩKn+1 (suc n) (l a) k) (~ j) })
                         (anotherbottom i j)

        where
        anotherbottom : I → I → coHomK (2 + n)
        anotherbottom i j = hcomp (λ k → λ { (i = i0) → rUnitlUnit0 (2 + n) k (~ j)
                                           ; (i = i1) → rUnitlUnit0 (2 + n) k (~ j)
                                           ; (j = i0) → Kn→ΩKn+1 (suc n) (h a) i
                                           ; (j = i1) → Kn→ΩKn+1 (suc n) (h a) i +[ 2 + n ]ₖ (0ₖ (2 + n)) })
                                  (rUnitₖ (2 + n) (Kn→ΩKn+1 (suc n) (h a) i) (~ j))

  dHomHelper : (n : ℕ) (h l : C → coHomK n) (x : Pushout f g)
             → d-pre n (λ x → h x +[ n ]ₖ l x) x ≡ d-pre n h x +[ suc n ]ₖ d-pre n l x
  dHomHelper n h l (inl x) = sym (lUnitₖ (suc n) (0ₖ (suc n)))
  dHomHelper n h l (inr x) = sym (lUnitₖ (suc n) (0ₖ (suc n)))
  dHomHelper zero h l (push a i) j = dHomHelperPath zero h l a i j
  dHomHelper (suc n) h l (push a i) j = dHomHelperPath (suc n) h l a i j

  dIsHom : (n : ℕ) → isGroupHom (coHomGr n C) (coHomGr (suc n) (Pushout f g)) (sRec setTruncIsSet λ a → ∣ d-pre n a ∣₂)
  dIsHom zero = sElim2 (λ _ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                   λ f g i → ∣ funExt (λ x → dHomHelper zero f g x) i ∣₂
  dIsHom (suc n) = sElim2 (λ _ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                   λ f g i → ∣ funExt (λ x → dHomHelper (suc n) f g x) i ∣₂

  d : (n : ℕ) → GroupHom (coHomGr n C) (coHomGr (suc n) (Pushout f g))
  GroupHom.fun (d n) = sRec setTruncIsSet λ a → ∣ d-pre n a ∣₂
  GroupHom.isHom (d n) = dIsHom n

  -- The long exact sequence
  Im-d⊂Ker-i : (n : ℕ) (x : ⟨ (coHomGr (suc n) (Pushout f g)) ⟩)
            → isInIm (coHomGr n C) (coHomGr (suc n) (Pushout f g)) (d n) x
            → isInKer (coHomGr (suc n) (Pushout f g)) (×coHomGr (suc n) A B) (i (suc n)) x
  Im-d⊂Ker-i n = sElim (λ _ → isSetΠ λ _ → isOfHLevelPath 2 (isSet× setTruncIsSet setTruncIsSet) _ _)
                       λ a → pRec (isOfHLevelPath' 1 (isSet× setTruncIsSet setTruncIsSet) _ _)
                               (sigmaElim (λ _ → isOfHLevelPath 2 (isSet× setTruncIsSet setTruncIsSet) _ _)
                                λ δ b i → sRec (isSet× setTruncIsSet setTruncIsSet)
                                               (λ δ → ∣ (λ x → δ (inl x)) ∣₂ , ∣ (λ x → δ (inr x)) ∣₂ ) (b (~ i)))

  Ker-i⊂Im-d : (n : ℕ) (x : ⟨ coHomGr (suc n) (Pushout f g) ⟩)
             → isInKer (coHomGr (suc n) (Pushout f g)) (×coHomGr (suc n) A B) (i (suc n)) x
             → isInIm (coHomGr n C) (coHomGr (suc n) (Pushout f g)) (d n) x
  Ker-i⊂Im-d zero =
     sElim (λ _ → isSetΠ λ _ → isProp→isSet propTruncIsProp)
           λ a p → pRec {A = (λ x → a (inl x)) ≡ λ _ → 0ₖ 1}
                        (isProp→ propTruncIsProp)
                        (λ p1 → pRec propTruncIsProp λ p2 → ∣ ∣ (λ c → ΩKn+1→Kn 0 (sym (cong (λ F → F (f c)) p1)
                                                                                ∙∙ cong a (push c)
                                                                                ∙∙ cong (λ F → F (g c)) p2)) ∣₂
                                                                             , cong ∣_∣₂ (funExt (λ δ → helper a p1 p2 δ)) ∣₁)
                                       (Iso.fun PathIdTrunc₀Iso (cong fst p))
                                       (Iso.fun PathIdTrunc₀Iso (cong snd p))

      where
      helper : (F : (Pushout f g) → hLevelTrunc 3 (S₊ 1))
               (p1 : Path (_ → hLevelTrunc 3 (S₊ 1)) (λ a₁ → F (inl a₁)) (λ _ → ∣ base ∣))
               (p2 : Path (_ → hLevelTrunc 3 (S₊ 1)) (λ a₁ → F (inr a₁)) (λ _ → ∣ base ∣))
             → (δ : Pushout f g)
             → d-pre 0 (λ c → ΩKn+1→Kn 0 ((λ i₁ → p1 (~ i₁) (f c))
                                                     ∙∙ cong F (push c)
                                                     ∙∙ cong (λ F → F (g c)) p2)) δ
              ≡ F δ
      helper F p1 p2 (inl x) = sym (cong (λ f → f x) p1)
      helper F p1 p2 (inr x) = sym (cong (λ f → f x) p2)
      helper F p1 p2 (push a i) j =
        hcomp (λ k → λ { (i = i0) → p1 (~ j) (f a)
                       ; (i = i1) → p2 (~ j) (g a)
                       ; (j = i0) → Iso.rightInv (Iso-Kn-ΩKn+1 0) ((λ i₁ → p1 (~ i₁) (f a))
                                                                       ∙∙ cong F (push a)
                                                                       ∙∙ cong (λ F₁ → F₁ (g a)) p2) (~ k) i
                        ; (j = i1) → F (push a i)})
              (doubleCompPath-filler (sym (cong (λ F → F (f a)) p1)) (cong F (push a)) (cong (λ F → F (g a)) p2) (~ j) i)
  Ker-i⊂Im-d (suc n) =
    sElim (λ _ → isSetΠ λ _ → isProp→isSet propTruncIsProp)
           λ a p → pRec {A = (λ x → a (inl x)) ≡ λ _ → 0ₖ (2 + n)} (isProp→ propTruncIsProp)
                        (λ p1 → pRec propTruncIsProp λ p2 → ∣ ∣ (λ c → ΩKn+1→Kn (suc n) (sym (cong (λ F → F (f c)) p1)
                                                                                ∙∙ cong a (push c)
                                                                                ∙∙ cong (λ F → F (g c)) p2)) ∣₂
                                                                             , cong ∣_∣₂ (funExt (λ δ → helper a p1 p2 δ)) ∣₁)
                                       (Iso.fun PathIdTrunc₀Iso (cong fst p))
                                       (Iso.fun PathIdTrunc₀Iso (cong snd p))

      where
      helper : (F : (Pushout f g) → hLevelTrunc (4 + n) (S₊ (2 + n)))
               (p1 : Path (_ → hLevelTrunc (4 + n) (S₊ (2 + n))) (λ a₁ → F (inl a₁)) (λ _ → ∣ north ∣))
               (p2 : Path (_ → hLevelTrunc (4 + n) (S₊ (2 + n))) (λ a₁ → F (inr a₁)) (λ _ → ∣ north ∣))
             → (δ : (Pushout f g))
             → d-pre (suc n) (λ c → ΩKn+1→Kn (suc n) ((λ i₁ → p1 (~ i₁) (f c))
                                                     ∙∙ cong F (push c)
                                                     ∙∙ cong (λ F → F (g c)) p2)) δ
              ≡ F δ
      helper F p1 p2 (inl x) = sym (cong (λ f → f x) p1)
      helper F p1 p2 (inr x) = sym (cong (λ f → f x) p2)
      helper F p1 p2 (push a i) j =
        hcomp (λ k → λ { (i = i0) → p1 (~ j) (f a)
                       ; (i = i1) → p2 (~ j) (g a)
                       ; (j = i0) → Iso.rightInv (Iso-Kn-ΩKn+1 (suc n)) ((λ i₁ → p1 (~ i₁) (f a))
                                                                           ∙∙ cong F (push a)
                                                                           ∙∙ cong (λ F₁ → F₁ (g a)) p2) (~ k) i
                       ; (j = i1) → F (push a i)})
              (doubleCompPath-filler (sym (cong (λ F → F (f a)) p1)) (cong F (push a)) (cong (λ F → F (g a)) p2) (~ j) i)

  open GroupHom

  Im-i⊂Ker-Δ : (n : ℕ) (x : ⟨ ×coHomGr n A B ⟩)
            → isInIm (coHomGr n (Pushout f g)) (×coHomGr n A B) (i n) x
            → isInKer (×coHomGr n A B) (coHomGr n C) (Δ n) x
  Im-i⊂Ker-Δ n (Fa , Fb) =
    sElim {B = λ Fa → (Fb : _) → isInIm (coHomGr n (Pushout f g)) (×coHomGr n A B) (i n) (Fa , Fb)
                               → isInKer (×coHomGr n A B) (coHomGr n C) (Δ n) (Fa , Fb)}
          (λ _ → isSetΠ2 λ _ _ → isOfHLevelPath 2 setTruncIsSet _ _)
          (λ Fa → sElim (λ _ → isSetΠ λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                        λ Fb → pRec (setTruncIsSet _ _)
                                     (sigmaElim (λ x → isProp→isSet (setTruncIsSet _ _))
                                                λ Fd p → helper n Fa Fb Fd p))
          Fa
          Fb
    where
    helper : (n : ℕ) (Fa : A → coHomK n) (Fb : B → coHomK n) (Fd : (Pushout f g) → coHomK n)
          → (fun (i n) ∣ Fd ∣₂ ≡ (∣ Fa ∣₂ , ∣ Fb ∣₂))
          → (fun (Δ n)) (∣ Fa ∣₂ , ∣ Fb ∣₂) ≡ 0ₕ n
    helper zero Fa Fb Fd p = cong (fun (Δ zero)) (sym p)
                           ∙∙ (λ i → ∣ (λ x → Fd (inl (f x))) ∣₂ -[ 0 ]ₕ ∣ (λ x → Fd (push x (~ i))) ∣₂ )
                           ∙∙ cancelₕ 0 ∣ (λ x → Fd (inl (f x))) ∣₂
    helper (suc n) Fa Fb Fd p = cong (fun (Δ (suc n))) (sym p)
                              ∙∙ (λ i → ∣ (λ x → Fd (inl (f x))) ∣₂ -[ (suc n) ]ₕ ∣ (λ x → Fd (push x (~ i))) ∣₂)
                              ∙∙ cancelₕ (suc n) ∣ (λ x → Fd (inl (f x))) ∣₂

  Ker-Δ⊂Im-i : (n : ℕ) (a : ⟨ ×coHomGr n A B ⟩)
            → isInKer (×coHomGr n A B) (coHomGr n C) (Δ n) a
            → isInIm (coHomGr n (Pushout f g)) (×coHomGr n A B) (i n) a
  Ker-Δ⊂Im-i n = prodElim (λ _ → isSetΠ (λ _ → isProp→isSet propTruncIsProp))
                          (λ Fa Fb p → pRec propTruncIsProp
                                            (λ q → ∣ ∣ helpFun Fa Fb q ∣₂ , refl ∣₁)
                                            (helper Fa Fb p))
    where
    helper : (Fa : A → coHomK n) (Fb : B → coHomK n)
           → fun (Δ n) (∣ Fa ∣₂ , ∣ Fb ∣₂) ≡ 0ₕ n
           → ∥ Path (_ → _) (λ c → Fa (f c)) (λ c → Fb (g c)) ∥₁
    helper Fa Fb p = Iso.fun PathIdTrunc₀Iso
                               (sym (-+cancelₕ n ∣ (λ c → Fa (f c)) ∣₂ ∣ (λ c → Fb (g c)) ∣₂)
                               ∙∙ cong (λ x → x +[ n ]ₕ ∣ (λ c → Fb (g c)) ∣₂) p
                               ∙∙ lUnitₕ n _)

    helpFun : (Fa : A → coHomK n) (Fb : B → coHomK n)
            → ((λ c → Fa (f c)) ≡ (λ c → Fb (g c)))
            → Pushout f g → coHomK n
    helpFun Fa Fb p (inl x) = Fa x
    helpFun Fa Fb p (inr x) = Fb x
    helpFun Fa Fb p (push a i) = p i a

  private
    distrHelper : (n : ℕ) (p q : _)
                → ΩKn+1→Kn n p +[ n ]ₖ (-[ n ]ₖ ΩKn+1→Kn n q) ≡ ΩKn+1→Kn n (p ∙ sym q)
    distrHelper n p q i =
        ΩKn+1→Kn n (Iso.rightInv (Iso-Kn-ΩKn+1 n) p i
      ∙ Iso.rightInv (Iso-Kn-ΩKn+1 n) (sym (Iso.rightInv (Iso-Kn-ΩKn+1 n) q i)) i)

  Ker-d⊂Im-Δ : (n : ℕ) (a : coHom n C)
             → isInKer (coHomGr n C) (coHomGr (suc n) (Pushout f g)) (d n) a
             → isInIm (×coHomGr n A B) (coHomGr n C) (Δ n) a
  Ker-d⊂Im-Δ zero =
    sElim (λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelSuc 1 propTruncIsProp)
          λ Fc p → pRec propTruncIsProp (λ p → ∣ (∣ (λ a → ΩKn+1→Kn 0 (cong (λ f → f (inl a)) p)) ∣₂ ,
                                                     ∣ (λ b → ΩKn+1→Kn 0 (cong (λ f → f (inr b)) p)) ∣₂) ,
                                                  Iso.inv (PathIdTrunc₀Iso) ∣ funExt (λ c → helper2 Fc p c) ∣₁ ∣₁)
                                         (Iso.fun (PathIdTrunc₀Iso) p)

    where

    helper2 : (Fc : C → coHomK 0)
              (p : d-pre 0 Fc ≡ (λ _ → ∣ base ∣)) (c : C)
            → ΩKn+1→Kn 0 (λ i₁ → p i₁ (inl (f c))) -[ 0 ]ₖ (ΩKn+1→Kn 0 (λ i₁ → p i₁ (inr (g c)))) ≡ Fc c
    helper2 Fc p c = cong₂ (λ x y → ΩKn+1→Kn 0 (x ∙ sym y)) (Iso.rightInv (Iso-Kn-ΩKn+1 0) (λ i₁ → p i₁ (inl (f c))))
                                                            (Iso.rightInv (Iso-Kn-ΩKn+1 0) (λ i₁ → p i₁ (inr (g c))))
                  ∙∙ cong (ΩKn+1→Kn 0) (sym ((PathP→compPathR (cong (λ f → cong f (push c)) p))
                              ∙ (λ i → (λ i₁ → p i₁ (inl (f c)))
                                      ∙ (lUnit (sym (λ i₁ → p i₁ (inr (g c)))) (~ i)))))
                  ∙∙ Iso.leftInv (Iso-Kn-ΩKn+1 zero) (Fc c)
  Ker-d⊂Im-Δ (suc n) =
    sElim (λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelSuc 1 propTruncIsProp)
          λ Fc p → pRec propTruncIsProp (λ p → ∣ (∣ (λ a → ΩKn+1→Kn (suc n) (cong (λ f → f (inl a)) p)) ∣₂ ,
                                                     ∣ (λ b → ΩKn+1→Kn (suc n) (cong (λ f → f (inr b)) p)) ∣₂) ,
                                                  Iso.inv (PathIdTrunc₀Iso) ∣ funExt (λ c → helper2 Fc p c) ∣₁ ∣₁)
                                         (Iso.fun (PathIdTrunc₀Iso) p)

    where

    helper2 : (Fc : C → coHomK (suc n))
              (p : d-pre (suc n) Fc ≡ (λ _ → ∣ north ∣)) (c : C)
            → ΩKn+1→Kn (suc n) (λ i₁ → p i₁ (inl (f c))) -[ (suc n) ]ₖ (ΩKn+1→Kn (suc n) (λ i₁ → p i₁ (inr (g c)))) ≡ Fc c
    helper2 Fc p c = cong₂ (λ x y → ΩKn+1→Kn (suc n) (x ∙ sym y)) (Iso.rightInv (Iso-Kn-ΩKn+1 (suc n)) (λ i₁ → p i₁ (inl (f c))))
                                                                   (Iso.rightInv (Iso-Kn-ΩKn+1 (suc n)) (λ i₁ → p i₁ (inr (g c))))
                  ∙∙ cong (ΩKn+1→Kn (suc n)) (sym ((PathP→compPathR (cong (λ f → cong f (push c)) p))
                              ∙ (λ i → (λ i₁ → p i₁ (inl (f c)))
                                      ∙ (lUnit (sym (λ i₁ → p i₁ (inr (g c)))) (~ i)))))
                  ∙∙ Iso.leftInv (Iso-Kn-ΩKn+1 (suc n)) (Fc c)

  Im-Δ⊂Ker-d : (n : ℕ) (a : coHom n C)
             → isInIm (×coHomGr n A B) (coHomGr n C) (Δ n) a
             → isInKer (coHomGr n C) (coHomGr (suc n) (Pushout f g)) (d n) a
  Im-Δ⊂Ker-d n =
    sElim (λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
          λ Fc → pRec (isOfHLevelPath' 1 setTruncIsSet _ _)
                       (sigmaProdElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                                      λ Fa Fb p → pRec (isOfHLevelPath' 1 setTruncIsSet _ _)
                                                        (λ q → ((λ i → fun (d n) ∣ (q (~ i)) ∣₂) ∙ dΔ-Id n Fa Fb))
                                                        (Iso.fun (PathIdTrunc₀Iso) p))

    where
    d-preLeftId : (n : ℕ) (Fa : A → coHomK n)(d : (Pushout f g))
                → d-pre n (Fa ∘ f) d ≡ 0ₖ (suc n)
    d-preLeftId zero Fa (inl x) = Kn→ΩKn+1 0 (Fa x)
    d-preLeftId (suc n) Fa (inl x) = Kn→ΩKn+1 (suc n) (Fa x)
    d-preLeftId zero Fa (inr x) = refl
    d-preLeftId (suc n) Fa (inr x) = refl
    d-preLeftId zero Fa (push a i) j = Kn→ΩKn+1 zero (Fa (f a)) (j ∨ i)
    d-preLeftId (suc n) Fa (push a i) j = Kn→ΩKn+1 (suc n) (Fa (f a)) (j ∨ i)

    d-preRightId : (n : ℕ) (Fb : B → coHomK n) (d : (Pushout f g))
                → d-pre n (Fb ∘ g) d ≡ 0ₖ (suc n)
    d-preRightId n Fb (inl x) = refl
    d-preRightId zero Fb (inr x) = sym (Kn→ΩKn+1 0 (Fb x))
    d-preRightId (suc n) Fb (inr x) = sym (Kn→ΩKn+1 (suc n) (Fb x))
    d-preRightId zero Fb (push a i) j = Kn→ΩKn+1 zero (Fb (g a)) (~ j ∧ i)
    d-preRightId (suc n) Fb (push a i) j = Kn→ΩKn+1 (suc n) (Fb (g a)) (~ j ∧ i)

    dΔ-Id : (n : ℕ) (Fa : A → coHomK n) (Fb : B → coHomK n)
            → fun (d n) (fun (Δ n) (∣ Fa ∣₂ , ∣ Fb ∣₂)) ≡ 0ₕ (suc n)
    dΔ-Id zero Fa Fb = -distrLemma 0 1 (d zero) ∣ Fa ∘ f ∣₂ ∣ Fb ∘ g ∣₂
                    ∙∙ (λ i → ∣ (λ x → d-preLeftId zero Fa x i) ∣₂ -[ 1 ]ₕ ∣ (λ x → d-preRightId zero Fb x i) ∣₂)
                    ∙∙ cancelₕ 1 (0ₕ 1)
    dΔ-Id (suc n) Fa Fb = -distrLemma (suc n) (2 + n) (d (suc n)) ∣ Fa ∘ f ∣₂ ∣ Fb ∘ g ∣₂
                    ∙∙ (λ i → ∣ (λ x → d-preLeftId (suc n) Fa x i) ∣₂ -[ (2 + n) ]ₕ ∣ (λ x → d-preRightId (suc n) Fb x i) ∣₂)
                    ∙∙ cancelₕ (2 + n) (0ₕ (2 + n))

max_stars_repo_name: ayberkt/cubical

max_issues_repo_name: ayberkt/cubical

max_forks_repo_name: ayberkt/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The basic code for equational reasoning with three relations:
-- equality, strict ordering and non-strict ordering.
------------------------------------------------------------------------
--
-- See `Data.Nat.Properties` or `Relation.Binary.Reasoning.PartialOrder`
-- for examples of how to instantiate this module.

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

open import Relation.Binary

module Relation.Binary.Reasoning.Base.Triple {a ℓ₁ ℓ₂ ℓ₃} {A : Set a}
  {_≈_ : Rel A ℓ₁} {_≤_ : Rel A ℓ₂} {_<_ : Rel A ℓ₃}
  (isPreorder : IsPreorder _≈_ _≤_)
  (<-trans : Transitive _<_) (<-resp-≈ : _<_ Respects₂ _≈_) (<⇒≤ : _<_ ⇒ _≤_)
  (<-≤-trans : Trans _<_ _≤_ _<_) (≤-<-trans : Trans _≤_ _<_ _<_)
  where

open import Data.Product using (proj₁; proj₂)
open import Function using (case_of_; id)
open import Level using (Level; _⊔_; Lift; lift)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Nullary.Decidable using (True; toWitness)

open IsPreorder isPreorder
  renaming
  ( reflexive to ≤-reflexive
  ; trans     to ≤-trans
  ; ∼-resp-≈  to ≤-resp-≈
  )

------------------------------------------------------------------------
-- A datatype to hide the current relation type

data _IsRelatedTo_ (x y : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃) where
  strict    : (x<y : x < y) → x IsRelatedTo y
  nonstrict : (x≤y : x ≤ y) → x IsRelatedTo y
  equals    : (x≈y : x ≈ y) → x IsRelatedTo y

------------------------------------------------------------------------
-- Types that are used to ensure that the final relation proved by the
-- chain of reasoning can be converted into the required relation.

data IsStrict {x y} : x IsRelatedTo y → Set (a ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃) where
  isStrict : ∀ x<y → IsStrict (strict x<y)

IsStrict? : ∀ {x y} (x≲y : x IsRelatedTo y) → Dec (IsStrict x≲y)
IsStrict? (strict    x<y) = yes (isStrict x<y)
IsStrict? (nonstrict _)   = no λ()
IsStrict? (equals    _)   = no λ()

extractStrict : ∀ {x y} {x≲y : x IsRelatedTo y} → IsStrict x≲y → x < y
extractStrict (isStrict x<y) = x<y

data IsEquality {x y} : x IsRelatedTo y → Set (a ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃) where
  isEquality : ∀ x≈y → IsEquality (equals x≈y)

IsEquality? : ∀ {x y} (x≲y : x IsRelatedTo y) → Dec (IsEquality x≲y)
IsEquality? (strict    _) = no λ()
IsEquality? (nonstrict _) = no λ()
IsEquality? (equals x≈y)  = yes (isEquality x≈y)

extractEquality : ∀ {x y} {x≲y : x IsRelatedTo y} → IsEquality x≲y → x ≈ y
extractEquality (isEquality x≈y) = x≈y

------------------------------------------------------------------------
-- Reasoning combinators

infix -1 begin_ begin-strict_ begin-equality_
infixr 0 _<⟨_⟩_ _≤⟨_⟩_ _≈⟨_⟩_ _≈˘⟨_⟩_ _≡⟨_⟩_ _≡˘⟨_⟩_ _≡⟨⟩_
infix  1 _∎

begin_ : ∀ {x y} (r : x IsRelatedTo y) → x ≤ y
begin (strict    x<y) = <⇒≤ x<y
begin (nonstrict x≤y) = x≤y
begin (equals    x≈y) = ≤-reflexive x≈y

begin-strict_ : ∀ {x y} (r : x IsRelatedTo y) → {s : True (IsStrict? r)} → x < y
begin-strict_ r {s} = extractStrict (toWitness s)

begin-equality_ : ∀ {x y} (r : x IsRelatedTo y) → {s : True (IsEquality? r)} → x ≈ y
begin-equality_ r {s} = extractEquality (toWitness s)

_<⟨_⟩_ : ∀ (x : A) {y z} → x < y → y IsRelatedTo z → x IsRelatedTo z
x <⟨ x<y ⟩ strict    y<z = strict (<-trans x<y y<z)
x <⟨ x<y ⟩ nonstrict y≤z = strict (<-≤-trans x<y y≤z)
x <⟨ x<y ⟩ equals    y≈z = strict (proj₁ <-resp-≈ y≈z x<y)

_≤⟨_⟩_ : ∀ (x : A) {y z} → x ≤ y → y IsRelatedTo z → x IsRelatedTo z
x ≤⟨ x≤y ⟩ strict    y<z = strict    (≤-<-trans x≤y y<z)
x ≤⟨ x≤y ⟩ nonstrict y≤z = nonstrict (≤-trans x≤y y≤z)
x ≤⟨ x≤y ⟩ equals    y≈z = nonstrict (proj₁ ≤-resp-≈ y≈z x≤y)

_≈⟨_⟩_ : ∀ (x : A) {y z} → x ≈ y → y IsRelatedTo z → x IsRelatedTo z
x ≈⟨ x≈y ⟩ strict    y<z = strict    (proj₂ <-resp-≈ (Eq.sym x≈y) y<z)
x ≈⟨ x≈y ⟩ nonstrict y≤z = nonstrict (proj₂ ≤-resp-≈ (Eq.sym x≈y) y≤z)
x ≈⟨ x≈y ⟩ equals    y≈z = equals    (Eq.trans x≈y y≈z)

_≈˘⟨_⟩_ : ∀ x {y z} → y ≈ x → y IsRelatedTo z → x IsRelatedTo z
x ≈˘⟨ x≈y ⟩ y∼z = x ≈⟨ Eq.sym x≈y ⟩ y∼z

_≡⟨_⟩_ : ∀ (x : A) {y z} → x ≡ y → y IsRelatedTo z → x IsRelatedTo z
x ≡⟨ x≡y ⟩ strict    y<z = strict    (case x≡y of λ where refl → y<z)
x ≡⟨ x≡y ⟩ nonstrict y≤z = nonstrict (case x≡y of λ where refl → y≤z)
x ≡⟨ x≡y ⟩ equals    y≈z = equals    (case x≡y of λ where refl → y≈z)

_≡˘⟨_⟩_ : ∀ x {y z} → y ≡ x → y IsRelatedTo z → x IsRelatedTo z
x ≡˘⟨ x≡y ⟩ y∼z = x ≡⟨ sym x≡y ⟩ y∼z

_≡⟨⟩_ : ∀ (x : A) {y} → x IsRelatedTo y → x IsRelatedTo y
x ≡⟨⟩ x≲y = x≲y

_∎ : ∀ x → x IsRelatedTo x
x ∎ = equals Eq.refl

ext: agda


text:
open import Everything

module Test.Test0 where

  test-functor-surjidentity : ∀
    {𝔬₁ 𝔯₁ ℓ₁ 𝔬₂ 𝔯₂ ℓ₂}
    ⦃ functor : Functor 𝔬₁ 𝔯₁ ℓ₁ 𝔬₂ 𝔯₂ ℓ₂ ⦄
    (open Functor functor)
    → Surjidentity.type _∼₁_ _∼₂_ _∼̇₂_ functor-smap ε₁ ε₂
  test-functor-surjidentity = surjidentity

  -- test-functor-transextensionality ⦃ functor ⦄ = let open Functor ⦃ … ⦄ in transextensionality1


text:
module tree where

open import bool
open import eq
open import level
open import list
open import list-to-string
open import nat
open import nat-thms
open import string

----------------------------------------------------------------------
-- datatype
----------------------------------------------------------------------

-- nonempty trees
data 𝕋 {ℓ} (A : Set ℓ) : Set ℓ where
  node : A → 𝕃 (𝕋 A) → 𝕋 A

----------------------------------------------------------------------
-- tree operations
----------------------------------------------------------------------

leaf : ∀ {ℓ}{A : Set ℓ} → A → 𝕋 A
leaf a = node a []

𝕋-to-string : ∀ {ℓ}{A : Set ℓ} → (f : A → string) → (t : 𝕋 A) → string
𝕋s-to-string : ∀ {ℓ}{A : Set ℓ} → (f : A → string) → (ts : 𝕃 (𝕋 A)) → string
𝕋-to-string f (node a []) = f a
𝕋-to-string f (node a ts) = "(" ^ (f a) ^ (𝕋s-to-string f ts) ^ ")"
𝕋s-to-string f [] = ""
𝕋s-to-string f (t :: ts) = " " ^ (𝕋-to-string f t) ^ (𝕋s-to-string f ts)

perfect-binary-tree : ∀ {ℓ}{A : Set ℓ} → ℕ → A → 𝕋 A
perfect-binary-tree 0 a = (node a [])
perfect-binary-tree (suc n) a = let t = perfect-binary-tree n a in
                                  (node a (t :: t :: []))

size𝕋 : ∀ {ℓ}{A : Set ℓ} → 𝕋 A → ℕ
size𝕋s : ∀ {ℓ}{A : Set ℓ} → 𝕃 (𝕋 A) → ℕ
size𝕋 (node a ts) = suc (size𝕋s ts)
size𝕋s [] = 0
size𝕋s (t :: ts) = size𝕋 t + size𝕋s ts

size-perfect : ∀ {ℓ}{A : Set ℓ}(n : ℕ)(a : A) → (size𝕋 (perfect-binary-tree n a)) ≡ pred (2 pow (suc n))
size-perfect 0 a = refl
size-perfect (suc n) a with (size𝕋 (perfect-binary-tree n a)) | size-perfect n a
... | s | ps rewrite ps with 2 pow n | nonzero-pow 2 n refl
... | x | px rewrite +0 x with x + x | (iszerosum2 x x px)
... | x2 | q rewrite +0 x2 | +0 (pred x2) | sym (+suc (pred x2) (pred x2)) | sucpred q | pred+ x2 x2 q = refl

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
{-# OPTIONS --safe #-}
module Cubical.Categories.Monad.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Categories.Category
open import Cubical.Categories.Functor renaming (𝟙⟨_⟩ to funcId)
open import Cubical.Categories.NaturalTransformation.Base
open import Cubical.Categories.NaturalTransformation.Properties
open import Cubical.Categories.Functors.HomFunctor

private
  variable
    ℓ ℓ' : Level

module _ {C : Category ℓ ℓ'} (M : Functor C C) where
  open Category C
  open Functor
  open NatTrans

  IsPointed : Type (ℓ-max ℓ ℓ')
  IsPointed = NatTrans (funcId C) M

  record IsMonad : Type (ℓ-max ℓ ℓ') where
    field
      η : IsPointed
      μ : NatTrans (funcComp M M) M
      idl-μ : PathP (λ i → NatTrans (F-rUnit {F = M} i) M) (compTrans μ (η ∘ˡ M)) (idTrans M)
      idr-μ : PathP (λ i → NatTrans (F-lUnit {F = M} i) M) (compTrans μ (M ∘ʳ η)) (idTrans M)
      assoc-μ : PathP (λ i → NatTrans (F-assoc {F = M} {G = M} {H = M} i) M)
        (compTrans μ (M ∘ʳ μ))
        (compTrans μ (μ ∘ˡ M))

    -- bind : Hom[-,M-] -> Hom[M-,M-]
    bind : NatTrans (funcComp (HomFunctor C) ((funcId C ^opF) ×F M)) (funcComp (HomFunctor C) ((M ^opF) ×F M))
    N-ob bind (x , y) f = N-ob μ y ∘ F-hom M f
    N-hom bind {x , y} {x' , y'} (f , h) = funExt λ g →
      (F-hom M ((f ⋆ g) ⋆ F-hom M h) ⋆ N-ob μ y')
        ≡⟨ cong (_⋆ N-ob μ y') (F-seq M (f ⋆ g) (F-hom M h)) ⟩
      ((F-hom M (f ⋆ g) ⋆ F-hom M (F-hom M h)) ⋆ N-ob μ y')
        ≡⟨ ⋆Assoc (F-hom M (f ⋆ g)) (F-hom M (F-hom M h)) (N-ob μ y') ⟩
      (F-hom M (f ⋆ g) ⋆ (F-hom M (F-hom M h) ⋆ N-ob μ y'))
        ≡⟨ cong (F-hom M (f ⋆ g) ⋆_) (N-hom μ h) ⟩
      (F-hom M (f ⋆ g) ⋆ (N-ob μ y ⋆ F-hom M h))
        ≡⟨ sym (⋆Assoc (F-hom M (f ⋆ g)) (N-ob μ y) (F-hom M h)) ⟩
      ((F-hom M (f ⋆ g) ⋆ N-ob μ y) ⋆ F-hom M h)
        ≡⟨ cong (_⋆ F-hom M h) (cong (_⋆ N-ob μ y) (F-seq M f g)) ⟩
      (((F-hom M f ⋆ F-hom M g) ⋆ N-ob μ y) ⋆ F-hom M h)
        ≡⟨ cong (_⋆ F-hom M h) (⋆Assoc (F-hom M f) (F-hom M g) (N-ob μ y)) ⟩
      ((M .F-hom f ⋆ (F-hom M g ⋆ N-ob μ y)) ⋆ F-hom M h) ∎

  -- Define comonads as monads on the opposite category?

module _ (C : Category ℓ ℓ') where
  Monad : Type (ℓ-max ℓ ℓ')
  Monad = Σ[ M ∈ Functor C C ] IsMonad M

module _ {C : Category ℓ ℓ'} (monadM monadN : Monad C) (ν : NatTrans (fst monadM) (fst monadN)) where

  private
    M N : Functor C C
    M = fst monadM
    N = fst monadN
    module M = IsMonad (snd monadM)
    module N = IsMonad (snd monadN)

  record IsMonadHom : Type (ℓ-max ℓ ℓ') where
    constructor proveMonadHom
    field
      N-η : compTrans ν M.η ≡ N.η
      N-μ : compTrans ν M.μ ≡ compTrans N.μ (whiskerTrans ν ν)
  open IsMonadHom

  isProp-IsMonadHom : isProp (IsMonadHom)
  N-η (isProp-IsMonadHom (proveMonadHom N-η1 N-μ1) (proveMonadHom N-η2 N-μ2) i) = isSetNatTrans _ _ N-η1 N-η2 i
  N-μ (isProp-IsMonadHom (proveMonadHom N-η1 N-μ1) (proveMonadHom N-η2 N-μ2) i) = isSetNatTrans _ _ N-μ1 N-μ2 i

module _ {C : Category ℓ ℓ'} (monadM monadN : Monad C) where
  MonadHom : Type (ℓ-max ℓ ℓ')
  MonadHom = Σ[ ν ∈ NatTrans (fst monadM) (fst monadN) ] IsMonadHom monadM monadN ν

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- Non-deterministic insert and permutation with choose oracle
-- The oracle is passed through the individual functions.

open import bool

module even-double-eo
  (Choice : Set)
  (choose : Choice → 𝔹)
  (lchoice : Choice → Choice)
  (rchoice : Choice → Choice)
 where

open import eq
open import bool-thms
open import nat
open import nat-thms
open import list

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

-- double is deterministic:
double : ℕ → ℕ
double x = x + x

-- even is a deterministic predicate:
even : ℕ → 𝔹
even zero = tt
even (suc 0) = ff
even (suc (suc x)) = even x

-- eo yields an even and odd number close to the input value:
eo : Choice → ℕ → ℕ
eo ch n = if choose ch then n else (suc n)

-- auxiliary property for x+x instead of double:
even-x+x : ∀ (x : ℕ) → even (x + x) ≡ tt
even-x+x zero = refl
even-x+x (suc x) rewrite +suc x x | even-x+x x = refl

-- (even (double x)) is always true:
even-double-is-true : ∀ (x : ℕ) → even (double x) ≡ tt
even-double-is-true x rewrite even-x+x x = refl

-- (even (double (eo n))) is always true:
even-double-eo-is-true : ∀ (ch : Choice) (n : ℕ)
                        → even (double (eo ch n)) ≡ tt
even-double-eo-is-true ch n = even-double-is-true (eo ch n)

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

max_stars_repo_name: mihanus/curry-agda

max_issues_repo_name: mihanus/curry-agda

max_forks_repo_name: mihanus/curry-agda


text:
module _ where

module G where
  module H where

module A where
  module B where
    module C where
      open G public

module I = A.B.C.H

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import HoTT

-- This file contains a helper module for FinSet,
-- proving the finite pigeonhole principle
module homotopy.Pigeonhole where

{-
  loosely based on code by copumpkin and xplat via byorgey
-}

incl : ∀ {m n} (m<n : m < n) → Fin m → Fin n
incl m<n (k , k<m) = k , <-trans k<m m<n

incl-ne : ∀ {n} (i : Fin n) → ¬ (incl ltS i == n , ltS)
incl-ne {n} (k , k<n) p = <-to-≠ k<n (ap fst p)

Dec-Σ-Fin : ∀ {ℓ} {n} (P : Fin n → Type ℓ) (dec-P : (i : Fin n) → Dec (P i))
             → Dec (Σ (Fin n) λ i → P i)
Dec-Σ-Fin {ℓ} {O} P dec-P = inr λ z → –> Fin-equiv-Empty (fst z)
Dec-Σ-Fin {ℓ} {S n} P dec-P with Dec-Σ-Fin {ℓ} {n} (P ∘ (incl ltS)) (dec-P ∘ (incl ltS))
Dec-Σ-Fin {ℓ} {S n} P dec-P | inl z = inl (incl ltS (fst z) , snd z)
Dec-Σ-Fin {ℓ} {S n} P dec-P | inr ¬z with dec-P (n , ltS)
Dec-Σ-Fin {ℓ} {S n} P dec-P | inr ¬z | (inl p)  = inl ((n , ltS) , p)
Dec-Σ-Fin {ℓ} {S n} P dec-P | inr ¬z | (inr ¬p) = inr ¬w
  where
    ¬w : Σ (Fin (S n)) P → ⊥
    ¬w ((_ , ltS) , p) = ¬p p
    ¬w ((k , ltSR k<n) , p) = ¬z ((k , k<n) , p)

<-trans-S : {m n k : ℕ} → m < n → n < (S k) → m < k
<-trans-S m<n ltS = m<n
<-trans-S m<n (ltSR n<k) = <-trans m<n n<k

ℕ-dichotomy : {m n : ℕ} → m ≠ n → (m < n) ⊔ (n < m)
ℕ-dichotomy {m} {n} m≠n with ℕ-trichotomy m n
ℕ-dichotomy {m} {n} m≠n | inl p = ⊥-rec (m≠n p)
ℕ-dichotomy {m} {n} m≠n | inr x = x

Fin-fst-= : ∀ {n} {i j : Fin n} → fst i == fst j → i == j
Fin-fst-= {n} {i , i<n} {j , j<n} = Subtype=-out (Fin-prop n)

punchout : ∀ {n} (i j : Fin (S n)) → i ≠ j → Fin n
punchout {n} (i , i<Sn) (j , j<Sn) i≠j with ℕ-dichotomy (i≠j ∘ Fin-fst-=)
punchout {n} (i , i<Sn) (.(S i) , Si<Sn) i≠j | inl ltS = i , <-trans-S ltS Si<Sn
punchout {n} (i , i<Sn) (S j , Sj<Sn) i≠j | inl (ltSR i<j) = j , <-cancel-S Sj<Sn
punchout {n} (i , i<Sn) (j , j<Sn) i≠j | inr j<i = j , <-trans-S j<i i<Sn

punchout-inj : ∀ {n} (i j k : Fin (S n)) (i≠j : i ≠ j) (i≠k : i ≠ k)
               → punchout i j i≠j == punchout i k i≠k → j == k
punchout-inj {n} (i , i<Sn) (j , j<Sn) (k , k<Sn) i≠j i≠k q with ℕ-dichotomy (i≠j ∘ Fin-fst-=)
punchout-inj {n} (i , i<Sn) (.(S i) , Si<Sn) (k , k<Sn) i≠j i≠k q | inl ltS with ℕ-dichotomy (i≠k ∘ Fin-fst-=)
punchout-inj {n} (i , i<Sn) (.(S i) , Si<Sn) (.(S i) , _) i≠j i≠k q | inl ltS | inl ltS = Fin-fst-= idp
punchout-inj {n} (i , i<Sn) (.(S i) , Si<Sn) (S k , Sk<Sn) i≠j i≠k q | inl ltS | inl (ltSR i<k) = ⊥-rec (<-to-≠ i<k (ap fst q))
punchout-inj {n} (i , i<Sn) (.(S i) , Si<Sn) (k , k<Sn) i≠j i≠k q | inl ltS | inr k<i = ⊥-rec (i≠k (Fin-fst-= (ap fst q)))
punchout-inj {n} (i , i<Sn) (S j , Sj<Sn) (k , k<Sn) i≠j i≠k q | inl (ltSR i<j) with ℕ-dichotomy (i≠k ∘ Fin-fst-=)
punchout-inj {n} (i , i<Sn) (S j , Sj<Sn) (.(S i) , Si<Sn) i≠j i≠k q | inl (ltSR i<j) | inl ltS = ⊥-rec (<-to-≠ i<j (! (ap fst q)))
punchout-inj {n} (i , i<Sn) (S j , Sj<Sn) (S k , Sk<Sn) i≠j i≠k q | inl (ltSR i<j) | inl (ltSR i<k) = Fin-fst-= (ap S (ap fst q))
punchout-inj {n} (i , i<Sn) (S j , Sj<Sn) (k , k<Sn) i≠j i≠k q | inl (ltSR i<j) | inr k<i = ⊥-rec (<-to-≠ (<-trans k<i i<j) (! (ap fst q)))
punchout-inj {n} (i , i<Sn) (j , j<Sn) (k , k<Sn) i≠j i≠k q | inr j<i with ℕ-dichotomy (i≠k ∘ Fin-fst-=)
punchout-inj {n} (i , i<Sn) (j , j<Sn) (.(S i) , Si<Sn) i≠j i≠k q | inr j<i | (inl ltS) = ⊥-rec (i≠j (Fin-fst-= (! (ap fst q))))
punchout-inj {n} (i , i<Sn) (j , j<Sn) (S k , Sk<Sn) i≠j i≠k q | inr j<i | (inl (ltSR i<k)) = ⊥-rec (<-to-≠ (<-trans j<i i<k) (ap fst q))
punchout-inj {n} (i , i<Sn) (j , j<Sn) (k , k<Sn) i≠j i≠k q | inr j<i | (inr k<i) = Fin-fst-= (ap fst q)

pigeonhole-special : ∀ {n} (f : Fin (S n) → Fin n)
                     → Σ (Fin (S n)) λ i → Σ (Fin (S n)) λ j → (i ≠ j) × (f i == f j)
pigeonhole-special {O} f = ⊥-rec (–> Fin-equiv-Empty (f (O , ltS)))
pigeonhole-special {S n} f with Dec-Σ-Fin (λ i → f (incl ltS i) == f (S n , ltS))
                                          (λ i → Fin-has-dec-eq (f (incl ltS i)) (f (S n , ltS)))
pigeonhole-special {S n} f | inl (i , p) = incl ltS i , (S n , ltS) , incl-ne i , p
pigeonhole-special {S n} f | inr h = incl ltS i , incl ltS j , (λ q → i≠j (Fin-fst-= (ap fst q))) ,
     punchout-inj (f (S n , ltS)) (f (incl ltS i)) (f (incl ltS j))
     (λ q → h (i , Fin-fst-= (! (ap fst q))))
     (λ q → h (j , Fin-fst-= (! (ap fst q))))
     (Fin-fst-= (ap fst p))
  where
    g : Fin (S n) → Fin n
    g k = punchout (f (S n , ltS)) (f (incl ltS k)) λ p → h (k , Fin-fst-= (! (ap fst p)))

    i : Fin (S n)
    i = fst (pigeonhole-special g)

    j : Fin (S n)
    j = fst (snd (pigeonhole-special g))

    i≠j : i ≠ j
    i≠j = fst (snd (snd (pigeonhole-special g)))

    p : g i == g j
    p = snd (snd (snd (pigeonhole-special g)))

pigeonhole : ∀ {m n} (m<n : m < n) (f : Fin n → Fin m)
             → Σ (Fin n) λ i → Σ (Fin n) λ j → (i ≠ j) × (f i == f j)
pigeonhole {m} {.(S m)} ltS f = pigeonhole-special f
pigeonhole {m} {(S n)} (ltSR p) f = i , j , ¬q , Subtype=-out (Fin-prop m) (ap fst r)
  where
    g : Fin (S n) → Fin n
    g k = fst (f k) , <-trans (snd (f k)) p

    i : Fin (S n)
    i = fst (pigeonhole-special g)

    j : Fin (S n)
    j = fst (snd (pigeonhole-special g))

    ¬q : i == j → ⊥
    ¬q = fst (snd (snd (pigeonhole-special g)))

    r : g i == g j
    r = snd (snd (snd (pigeonhole-special g)))

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
open import Data.Unit using ( ⊤ )
open import FRP.LTL.RSet.Core using ( RSet )

module FRP.LTL.RSet.Unit where

T : RSet
T t = ⊤

max_stars_repo_name: agda/agda-frp-ltl

max_issues_repo_name: agda/agda-frp-ltl

max_forks_repo_name: agda/agda-frp-ltl


text:
-- Andreas, 2017-07-13, issue #2642

record R : Set₁ where
  field
    F : Set
    F : Set  -- duplicate field, should be rejected

-- Otherwise, this gives an internal error:

test : Set → R
test A = record{ F = A }

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Vectors defined in terms of the reflexive-transitive closure, Star
------------------------------------------------------------------------

{-# OPTIONS --with-K --safe #-}

module Data.Star.Vec where

open import Data.Star.Nat
open import Data.Star.Fin using (Fin)
open import Data.Star.Decoration
open import Data.Star.Pointer as Pointer hiding (lookup)
open import Data.Star.List using (List)
open import Relation.Binary
open import Relation.Binary.Consequences
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
open import Function
open import Data.Unit

-- The vector type. Vectors are natural numbers decorated with extra
-- information (i.e. elements).

Vec : Set → ℕ → Set
Vec A = All (λ _ → A)

-- Nil and cons.

[] : ∀ {A} → Vec A zero
[] = ε

infixr 5 _∷_

_∷_ : ∀ {A n} → A → Vec A n → Vec A (suc n)
x ∷ xs = ↦ x ◅ xs

-- Projections.

head : ∀ {A n} → Vec A (1# + n) → A
head (↦ x ◅ _) = x

tail : ∀ {A n} → Vec A (1# + n) → Vec A n
tail (↦ _ ◅ xs) = xs

-- Append.

infixr 5 _++_

_++_ : ∀ {A m n} → Vec A m → Vec A n → Vec A (m + n)
_++_ = _◅◅◅_

-- Safe lookup.

lookup : ∀ {A n} → Fin n → Vec A n → A
lookup i xs with Pointer.lookup i xs
... | result _ x = x

------------------------------------------------------------------------
-- Conversions

fromList : ∀ {A} → (xs : List A) → Vec A (length xs)
fromList ε        = []
fromList (x ◅ xs) = x ∷ fromList xs

toList : ∀ {A n} → Vec A n → List A
toList = gmap (const tt) decoration


text:
-- Andreas, 2017-04-11, Issue 2543
-- Printing of second non-trivial with-pattern

-- {-# OPTIONS -v interaction.case:100 #-}

data D : Set where
  c : D → D

f : D → D
f y with c y
... | c z with c y
... | q = {!q!}  -- C-c C-c q

-- Was:
-- f y | c z | (c q) = ?

-- Expected:
-- f y | c z | c q = ?

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Showing natural numbers
------------------------------------------------------------------------

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

module Data.Nat.Show where

open import Data.Char as Char using (Char)
open import Data.Digit using (showDigit; toDigits; toNatDigits)
open import Function using (_∘_; _$_)
open import Data.List.Base using (List; []; _∷_; map; reverse)
open import Data.Nat
open import Data.Product using (proj₁)
open import Data.String as String using (String)
open import Relation.Nullary.Decidable using (True)

------------------------------------------------------------------------
-- Conversion from unary representation to the representation by the
-- given base.

toDigitChar : (n : ℕ) → Char
toDigitChar n = Char.fromℕ (n + (Char.toℕ '0'))

toDecimalChars : ℕ → List Char
toDecimalChars = map toDigitChar ∘ toNatDigits 10

------------------------------------------------------------------------
-- Show

-- Time complexity is O(log₁₀(n))

show : ℕ → String
show = String.fromList ∘ toDecimalChars

-- Warning: when compiled the time complexity of `showInBase b n` is
-- O(n) instead of the expected O(log(n)).

showInBase : (base : ℕ)
             {base≥2 : True (2 ≤? base)}
             {base≤16 : True (base ≤? 16)} →
             ℕ → String
showInBase base {base≥2} {base≤16} n =
  String.fromList $
  map (showDigit {base≤16 = base≤16}) $
  reverse $
  proj₁ $ toDigits base {base≥2 = base≥2} n


text:
module Issue892b where

record R : Set₁ where
  field A : Set
        B : A → Set

-- The type of R.B should print as (r : R) → R.A r → Set
-- rather than ( : R) → R.A  → Set.
bad : R.B
bad = ?


text:
------------------------------------------------------------------------
-- Programs used to define and specify breadth-first manipulations of
-- trees
------------------------------------------------------------------------

module BreadthFirst.Programs where

open import Codata.Musical.Notation
open import Codata.Musical.Colist hiding ([_])
open import Data.List.NonEmpty using (List⁺; [_]; _⁺++⁺_)
open import Data.Product

open import BreadthFirst.Universe
open import Stream hiding (zipWith)
open import Tree

infixr 5 _≺_ _∷_
infixr 4 _,_
infix  3 ↓_

mutual

  -- The term WHNF is a bit of a misnomer here; only recursive
  -- /coinductive/ arguments are suspended (in the form of programs).

  data ElW : U → Set₁ where
    leaf : ∀ {a} → ElW (tree a)
    node : ∀ {a}
           (l : ∞ (ElP (tree a))) (x : ElW a) (r : ∞ (ElP (tree a))) →
           ElW (tree a)
    _≺_  : ∀ {a} (x : ElW a) (xs : ∞ (ElP (stream a))) → ElW (stream a)
    []   : ∀ {a} → ElW (colist a)
    _∷_  : ∀ {a} (x : ElW a) (xs : ∞ (ElP (colist a))) → ElW (colist a)
    _,_  : ∀ {a b} (x : ElW a) (y : ElW b) → ElW (a ⊗ b)
    ⌈_⌉  : ∀ {A} (x : A) → ElW ⌈ A ⌉

  -- Note that higher-order functions are not handled well (see
  -- longZipWith): the arguments cannot be programs, since this would
  -- make the type negative.

  -- The tree arguments to lab and flatten used to be tree programs,
  -- but a number of lemmas could be removed when they were turned
  -- into "actual" trees.

  data ElP : U → Set₁ where
    ↓_          : ∀ {a} (w : ElW a) → ElP a
    fst         : ∀ {a b} (p : ElP (a ⊗ b)) → ElP a
    snd         : ∀ {a b} (p : ElP (a ⊗ b)) → ElP b
    lab         : ∀ {A B}
                  (t : Tree A) (lss : ElP (stream ⌈ Stream B ⌉)) →
                  ElP (tree ⌈ B ⌉ ⊗ stream ⌈ Stream B ⌉)
    longZipWith : ∀ {A} (f : A → A → A) (xs ys : ElP (colist ⌈ A ⌉)) →
                  ElP (colist ⌈ A ⌉)
    flatten     : ∀ {A} (t : Tree A) → ElP (colist ⌈ List⁺ A ⌉)

infixl 9 _·_ _⊛_

_·_ : ∀ {A B} → (A → B) → ElW ⌈ A ⌉ → ElW ⌈ B ⌉
f · ⌈ x ⌉ = ⌈ f x ⌉

_⊛_ : ∀ {A B} → ElW ⌈ (A → B) ⌉ → ElW ⌈ A ⌉ → ElW ⌈ B ⌉
⌈ f ⌉ ⊛ x = f · x

fstW : ∀ {a b} → ElW (a ⊗ b) → ElW a
fstW (x , y) = x

sndW : ∀ {a b} → ElW (a ⊗ b) → ElW b
sndW (x , y) = y

-- Uses the n-th stream to label the n-th level in the tree. Returns
-- the remaining stream elements (for every level).

labW : ∀ {A B} → Tree A → ElW (stream ⌈ Stream B ⌉) →
       ElW (tree ⌈ B ⌉ ⊗ stream ⌈ Stream B ⌉)
labW leaf         bss                = (leaf , bss)
labW (node l _ r) (⌈ b ≺ bs ⌉ ≺ bss) =
  (node (♯ fst x) ⌈ b ⌉ (♯ fst y) , ⌈ ♭ bs ⌉ ≺ ♯ snd y)
  where
  x = lab (♭ l) (♭ bss)
  y = lab (♭ r) (snd x)

longZipWithW : ∀ {A} → (A → A → A) →
               (xs ys : ElW (colist ⌈ A ⌉)) → ElW (colist ⌈ A ⌉)
longZipWithW f (x ∷ xs) (y ∷ ys) = f · x ⊛ y ∷ ♯ longZipWith f (♭ xs) (♭ ys)
longZipWithW f xs       []       = xs
longZipWithW f []       ys       = ys

flattenW : ∀ {A} → Tree A → ElW (colist ⌈ List⁺ A ⌉)
flattenW leaf         = []
flattenW (node l x r) =
  ⌈ [ x ] ⌉ ∷ ♯ longZipWith _⁺++⁺_ (flatten (♭ l)) (flatten (♭ r))

whnf : ∀ {a} → ElP a → ElW a
whnf (↓ w)                 = w
whnf (fst p)               = fstW (whnf p)
whnf (snd p)               = sndW (whnf p)
whnf (lab t bss)           = labW t (whnf bss)
whnf (longZipWith f xs ys) = longZipWithW f (whnf xs) (whnf ys)
whnf (flatten t)           = flattenW t

mutual

  ⟦_⟧W : ∀ {a} → ElW a → El a
  ⟦ leaf         ⟧W = leaf
  ⟦ (node l x r) ⟧W = node (♯ ⟦ ♭ l ⟧) ⟦ x ⟧W (♯ ⟦ ♭ r ⟧)
  ⟦ (x ≺ xs)     ⟧W = ⟦ x ⟧W ≺ ♯ ⟦ ♭ xs ⟧
  ⟦ []           ⟧W = []
  ⟦ (x ∷ xs)     ⟧W = ⟦ x ⟧W ∷ ♯ ⟦ ♭ xs ⟧
  ⟦ (x , y)      ⟧W = (⟦ x ⟧W , ⟦ y ⟧W)
  ⟦ ⌈ x ⌉        ⟧W = x

  ⟦_⟧ : ∀ {a} → ElP a → El a
  ⟦ p ⟧ = ⟦ whnf p ⟧W

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
{-# OPTIONS --allow-unsolved-metas #-}

module Real-Backup where

open import Data.Float hiding (_-_; _≈_)
open import Level using (0ℓ)
open import Algebra.Bundles using (CommutativeRing)
open import Algebra.Module.Bundles using (Module)
open import Relation.Binary.Structures using (IsStrictTotalOrder)
open import Relation.Binary.Bundles using (StrictTotalOrder)
open import Data.Sum using (_⊎_; inj₁; inj₂)
module CR = CommutativeRing
open import Relation.Binary.PropositionalEquality using (_≡_; module ≡-Reasoning)
open import Algebra.Module.Construct.TensorUnit
import Limit
open import InnerProduct
open import Relation.Nullary using (¬_)

private postulate
  todo : ∀ {a} {A : Set a} → A

+-*-commutativeRing : CommutativeRing 0ℓ 0ℓ
CR.Carrier +-*-commutativeRing = Float
CR._≈_ +-*-commutativeRing = _≡_
CR._+_ +-*-commutativeRing = _+_
CR._*_ +-*-commutativeRing = _*_
CR.- +-*-commutativeRing = -_
CR.0# +-*-commutativeRing = 0.0
CR.1# +-*-commutativeRing = 1.0
CR.isCommutativeRing +-*-commutativeRing = todo

+-*-module : Module +-*-commutativeRing 0ℓ 0ℓ
+-*-module = ⟨module⟩

<-strictTotalOrder : StrictTotalOrder _ 0ℓ 0ℓ
<-strictTotalOrder = record { Carrier = Float; _≈_ = _≡_; _<_ = todo; isStrictTotalOrder = todo }

infixl 6 _-_
_-_ : Float → Float → Float
x - y = x + (- y)

open StrictTotalOrder <-strictTotalOrder

+-*-isInnerProduct : IsInnerProduct isStrictTotalOrder (λ x → x) +-*-module _*_
+-*-isInnerProduct = todo

+-*-isNormed : IsNormed isStrictTotalOrder (λ x → x) +-*-module _*_ sqrt
+-*-isNormed =
  record
  { isInnerProduct = +-*-isInnerProduct
  ; sqrt-law = todo
  ; sqrt-concave = todo
  ; sqrt-cong = todo
  }

module _ where

  open Limit +-*-isNormed +-*-isNormed
  open IsNormed +-*-isNormed
  open Module +-*-module
  open CommutativeRing +-*-commutativeRing using (refl; +-cong)
  open import Data.Product
  open import Algebra.Module.Morphism.Structures

  _ : ∀ c → (c + x) ⟶ c as x ⟶0
  _ = λ c ε (0<ε) → ε , λ x (0<x , x<ε) →
    begin-strict
      ∥ c + x - c ∥
    ≈⟨ ∥∥-cong (y+x-y≈x c x) ⟩
      ∥ x ∥
    <⟨ x<ε ⟩
      ε
    ∎
    where
      open import Relation.Binary.Reasoning.StrictPartialOrder strictPartialOrder

      y+x-y≈x : ∀ y x → y + x - y ≈ᴹ x
      y+x-y≈x y x =
        begin-equality
          y + x - y
        ≈⟨ +ᴹ-cong (+ᴹ-comm y x) refl ⟩
          x + y - y
        ≈⟨ +ᴹ-assoc x y (- y) ⟩
          x + (y - y)
        ≈⟨ +ᴹ-cong {x = x} refl (-ᴹ‿inverseʳ y) ⟩
          x + 0.0
        ≈⟨ +ᴹ-identityʳ x ⟩
          x
        ∎

  times : Float → Float → Float
  times = _*_

  times-homo : ∀ m → IsModuleHomomorphism +-*-module +-*-module (times m)
  times-homo = todo

  _SlopeOf_At_ : (f' : MA.X → MB.X) (f : MA.X → MB.X) (x : MA.X) → Set _
  f' SlopeOf f At x = (λ y dy → f' y * dy) Differentiates f At x

  dxⁿ≈nxⁿ⁻¹
    : ∀ x n → (1.0 < n) ⊎ (¬ x ≈ 0.0)
    → (λ y → (n * (y ** (n - 1.0)))) SlopeOf (_** n) At x
  dxⁿ≈nxⁿ⁻¹ = todo

  dlogx≈1÷x : ∀ x → ¬ x ≈ 0.0 → (λ y dy → dy ÷ y) Differentiates log At x
  dlogx≈1÷x = todo

  deˣ/dx≈eˣ : ∀ x → e^_ SlopeOf e^_ At x
  deˣ/dx≈eˣ = todo

  open import Function using (_∘_)

  -- chain'
  --   : ∀ f f' g g' x
  --   → (λ dx → dx * f' x) Differentiates f At x
  --   → (λ dx → dx * g' (f x)) Differentiates g At f x
  --   → (λ dx → g'fx * (f'x dx)) Differentiates (g ∘ f) At x
  -- chain' f g x (f'x , _) (g'fx , _) = (λ dx → g'fx (f'x dx)) , todo

  ∂exp : ∀ x → (λ y dy → dy * (e^ y)) Differentiates e^_ At x
  ∂exp x = todo

  open import Data.Nat using (zero; suc)
  instance
    exp-n-∂ : ∀ {n} {x} → e^_ ⟦ x , n ⟧
    exp-n-∂ {zero} = []
    exp-n-∂ {n = suc n} = todo ∹ exp-n-∂

  it : ∀ {a} {A : Set a} → {{A}} → A
  it {{x}} = x

  gradexp : ∀ {x} → e^_ ⟦ x , 0 ⟧
  gradexp = it

  chain
    : ∀ f g x {n}
    → ⦃ f ⟦ x , n ⟧ ⦄
    → ⦃ g ⟦ f x , n ⟧ ⦄
    → (g ∘ f) ⟦ x , n ⟧
  chain f g x {n = 0} = []
  chain f g x {_} ⦃ _∹_ {_} {f'} pf ff ⦄ ⦃ _∹_ {_} {g'} pg gg ⦄ =
    let h y dy = g' (f y) (f' y dy)
    -- confusion here between xs and dxs.
    in _∹_ {δf = h} todo (chain (f' x) (g' (f x)) x ⦃ ff ⦄ ⦃ {! gg  !} ⦄)

  exp : Float → Float
  exp = e^_

  asdf : ∀ x → (exp ∘ exp) ⟦ x , 1 ⟧
  asdf x = chain exp exp x

--   gradsin : ∀ {x} → sin DifferentiableAt x
--   gradsin {x} = (λ dx → dx * (cos x)) , todo

--   gradcos : ∀ {x} → cos DifferentiableAt x
--   gradcos {x} = (λ dx → dx * (- sin x)) , todo

--   grad : ∀ f x → f DifferentiableAt x → Float → Float
--   grad f x (f'x , _) = f'x

--   teste : Float → Float
--   teste x = grad e^_ x (grade^ {x}) 1.0

--   -- testsin : Float → Float
--   -- testsin x = grad sin x (gradsin x) 1.0

--   -- test : Float → Float
--   -- test x = grad (e^_ ∘ sin) x (chain' sin e^_ x (gradsin x) (grade^ (sin x))) 1.0

--   -- _ : ∀ x → test x ≡ 1.0 * cos x * (e^ sin x)
--   -- _ = λ x → refl

--   -- -- TODO
--   -- -- definitely need some helper functions here.
--   -- _ : ∀ y n → (λ x → n * y ** (n - 1.0) * x) Differentiates (λ x → x ** n) At y
--   -- _ = λ y n → todo , λ ε 0<ε → δ₀ ε y n , λ δ (0<δ , δ<ε) → proof y n ε δ 0<δ δ<ε
--   --   where
--   --     δ₀ : Float → Float → Float → Float
--   --     δ₀ = {!   !}

--   --     triangle : ∀ x y → ∥ x + y ∥ < ∥ x ∥ + ∥ y ∥
--   --     triangle = todo

--   --     ≈< : ∀ x {y z} → y < z → x + y < x + z
--   --     ≈< = todo

--   --     -- does this imply _≈_ is _≡_?
--   --     ∀-cong : ∀ {x y} (f : CR.X → CR.X) → x ≈ y → f x ≈ f y
--   --     ∀-cong = todo

--   --     proof
--   --       : ∀ y n ε Δ (0<Δ : 0.0 < ∥ Δ ∥) (Δ<ε : ∥ Δ ∥ < ε)
--   --       → ∥ (y + Δ) ** n - (y ** n +ᴹ n * y ** (n - 1.0) * Δ) ∥ < ε
--   --     proof y n ε Δ 0<Δ Δ<ε =
--   --       begin-strict
--   --         ∥ (y + Δ) ** n - (y ** n + n * y ** (n - 1.0) * Δ) ∥
--   --       <⟨ triangle ((y + Δ) ** n) _ ⟩
--   --         ∥ (y + Δ) ** n ∥ + ∥ - (y ** n + n * y ** (n - 1.0) * Δ) ∥
--   --       ≈⟨ +-cong { ∥ (y + Δ) ** n ∥ } refl (sqrt-cong (∥-x∥²≈∥x∥² ((y ** n + n * y ** (n - 1.0) * Δ)))) ⟩
--   --         ∥ (y + Δ) ** n ∥ + ∥ (y ** n + n * y ** (n - 1.0) * Δ) ∥
--   --       <⟨ ≈< ∥ (y + Δ) ** n ∥ (triangle (y ** n) _) ⟩
--   --         ∥ (y + Δ) ** n ∥ + (∥ y ** n ∥ + ∥ n * y ** (n - 1.0) * Δ ∥)
--   --       <⟨ {! +-cong refl (x→-x _) !} ⟩
--   --         ε
--   --       ∎

-- --   -- (f (x MA.+ᴹ dx) MB.+ᴹ (MB.-ᴹ (f x MB.+ᴹ f' dx))) ⟶ MB.0ᴹ as dx ⟶ MA.0ᴹ
-- --   _ : ∀ θ → (λ dθ → F.cos θ F.* dθ) Differentiates F.sin At θ
-- --   _ =
-- --     λ θ → times-homo (F.cos θ) ,
-- --       λ ε → ε ,
-- --         λ dθ (0<abs[dθ-0] , abs[dθ-0]<ε) → {!   !} -- abs[x-0]<ε→abs[c+x-c]<ε x ε {! F.sin (θ F.+ x) !} abs[x-0]<ε
-- --         -- if abs dθ < ε then abs ( sin (θ + dθ) - (sin θ + cos θ * dθ) ) < ε

-- --         -- sin x = (e^iπx - e^-iπx) / 2i
-- --         -- cos x = (e^iπx + e^-iπx) / 2
-- --         -- sin x+dx = ?

-- -- --   open Diff +-*-module +-*-module
-- -- --   open Line +-*-commutativeRing

-- -- --   dline : ∀ m b x → Differentiable _≤_ abs abs (line m b) x
-- -- --   dline m b x = (λ x' dx → m * dx) , {!   !} , λ dy → (dy F.÷ m) , {! asdf dy  !}
-- -- --     where
-- -- --       open import Relation.Binary.Reasoning.PartialOrder ≤-poset

-- -- --       diff≈0 : ∀ dx → (line m b (x + dx) - line m b x) - m * dx ≈ 0#
-- -- --       diff≈0 dx =
-- -- --         begin-equality
-- -- --           (line m b (x + dx) - line m b x - m * dx)
-- -- --         ≈⟨ +-cong (linear-diff m b x dx) refl ⟩
-- -- --           m * dx - m * dx
-- -- --         ≈⟨ proj₂ -‿inverse (m * dx) ⟩
-- -- --           0#
-- -- --         ∎

-- -- --   open import Data.Nat using (ℕ; zero; suc)

-- -- -- --
-- -- -- --   Convex : (A → A) → Set

-- -- -- -- minimize : (f : A → A) (c : Convex f) → A
-- -- -- -- minimize f c = {!   !}

-- -- -- -- gradient : (f : A → A) (Differentiable f)

-- -- -- -- gradientDescent : (f' : A → A) (n : ℕ) → A
-- -- -- -- gradientDescent = ?

-- --   -- open import Relation.Nullary using (¬_)

-- --   -- x<y→y≮x : ∀ {x y} → x < y → ¬ y < x
-- --   -- x<y→y≮x x y = post

-- --   -- <-trans : ∀ {i j k} → i < j → j < k → i < k
-- --   -- <-trans i<j j<k = post

-- --   -- open CommutativeRing +-*-commutativeRing
-- --   -- open Module +-*-module
-- --   -- open import Relation.Binary

-- --   -- ≤-antisym : Antisymmetric _≡_ _≤_
-- --   -- ≤-antisym (inj₂ i≡j) j≤i = i≡j
-- --   -- ≤-antisym (inj₁ i<j) (inj₂ j≡i) = sym j≡i
-- --   -- ≤-antisym {i} {j} (inj₁ i<j) (inj₁ j<i) with x<y→y≮x {i} {j} i<j j<i
-- --   -- ... | ()

-- --   -- ≤-trans : Transitive _≤_
-- --   -- ≤-trans {i} {j} {k} (inj₁ i<j) (inj₁ j<k) = inj₁ (<-trans {i} {j} {k} i<j j<k)
-- --   -- ≤-trans (inj₁ i<j) (inj₂ j≡k) = inj₁ {! tt  !}
-- --   -- ≤-trans (inj₂ y) (inj₁ x) = {!   !}
-- --   -- ≤-trans (inj₂ i≡j) (inj₂ j≡k) = inj₂ (trans i≡j j≡k)

max_stars_repo_name: cspollard/diff

max_issues_repo_name: cspollard/diff

max_forks_repo_name: cspollard/diff


text:
-- Andreas, 2012-05-04
-- Occurs check when unifying indices in patterns
{-# OPTIONS --allow-unsolved-metas #-}
-- The option is supplied to force a real error to pass the regression test.
module OccursCheck1 where

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

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

test :
  let X : Nat
      X = _
  in  X == suc X
test = refl
-- should fail with error message indicating no solution possible

max_stars_repo_name: dagit/agda

max_issues_repo_name: dagit/agda

max_forks_repo_name: dagit/agda


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

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Setoids.Setoids
open import Rings.Definition
open import Rings.Lemmas
open import Rings.Orders.Partial.Definition
open import Rings.Orders.Total.Definition
open import Groups.Definition
open import Groups.Groups
open import Fields.Fields
open import Sets.EquivalenceRelations
open import Sequences
open import Setoids.Orders.Partial.Definition
open import Setoids.Orders.Total.Definition
open import Functions.Definition
open import LogicalFormulae
open import Numbers.Naturals.Naturals

module Fields.CauchyCompletion.EquivalentMonotone {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder {_<_ = _<_} pOrder} {R : Ring S _+_ _*_} (order : TotallyOrderedRing R tOrder) (F : Field R) (charNot2 : Setoid._∼_ S ((Ring.1R R) + (Ring.1R R)) (Ring.0R R) → False) where

open Setoid S
open SetoidTotalOrder tOrder
open SetoidPartialOrder pOrder
open Equivalence eq
open TotallyOrderedRing order
open Field F
open Group (Ring.additiveGroup R)
open Ring R

open import Fields.Lemmas F
open import Fields.Orders.Lemmas {F = F} record { oRing = order }
open import Rings.Orders.Lemmas(order)
open import Fields.CauchyCompletion.Definition order F
open import Fields.CauchyCompletion.Multiplication order F charNot2
open import Fields.CauchyCompletion.Addition order F charNot2
open import Fields.CauchyCompletion.Setoid order F charNot2
open import Fields.CauchyCompletion.Group order F charNot2
open import Fields.CauchyCompletion.Ring order F charNot2
open import Fields.CauchyCompletion.Comparison order F charNot2
open import Fields.CauchyCompletion.Approximation order F charNot2

halvingSequence : (start : A) → Sequence A
Sequence.head (halvingSequence start) = start
Sequence.tail (halvingSequence start) with halve charNot2 start
Sequence.tail (halvingSequence start) | start/2 , _ = halvingSequence start/2

halvingSequenceMultiple : (start : A) → {n : ℕ} → index (halvingSequence start) n ∼ index (map (start *_) (halvingSequence (Ring.1R R))) n
halvingSequenceMultiple start {zero} = Equivalence.symmetric eq (Equivalence.transitive eq *Commutative identIsIdent)
halvingSequenceMultiple start {succ n} with halve charNot2 start
... | start/2 , _ with allInvertible (1R + 1R) charNot2
halvingSequenceMultiple start {succ n} | start/2 , b | 1/2 , pr1/2 rewrite equalityCommutative (mapAndIndex (halvingSequence (1R * 1/2)) (_*_ start) n) = Equivalence.transitive eq (halvingSequenceMultiple start/2 {n}) f
  where
    g : (start * (1/2 * index (halvingSequence 1R) n)) ∼ (start * index (map (_*_ (1R * 1/2)) (halvingSequence 1R)) n)
    g rewrite equalityCommutative (mapAndIndex (halvingSequence 1R) (_*_ (1R * 1/2)) n) = *WellDefined (Equivalence.reflexive eq) (*WellDefined (Equivalence.symmetric eq identIsIdent) (Equivalence.reflexive eq))
    f : index (map (_*_ start/2) (halvingSequence 1R)) n ∼ (start * index (halvingSequence (1R * 1/2)) n)
    f rewrite equalityCommutative (mapAndIndex (halvingSequence 1R) (_*_ start/2) n) = Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.transitive eq (*WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq (*WellDefined (Equivalence.symmetric eq b) (Equivalence.reflexive eq)) (halfHalves 1/2 (Equivalence.transitive eq (Equivalence.transitive eq (+WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq *Commutative identIsIdent)) (Equivalence.symmetric eq (Equivalence.transitive eq *Commutative identIsIdent))) (Equivalence.symmetric eq *DistributesOver+)) pr1/2)))) (Equivalence.reflexive eq)) (Equivalence.symmetric eq *Associative)) g) (Equivalence.symmetric eq (*WellDefined (Equivalence.reflexive eq) (halvingSequenceMultiple (1R * 1/2) {n})))

Decreasing : Sequence A → Set o
Decreasing seq = ∀ (N : ℕ) → (index seq (succ N)) < (index seq N)

halvingSequencePositive : (n : ℕ) → 0G < index (halvingSequence 1R) n
halvingSequencePositive zero = 0<1 (charNot2ImpliesNontrivial charNot2)
halvingSequencePositive (succ n) with halve charNot2 1R
halvingSequencePositive (succ n) | 1/2 , pr1/2 = <WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq (Equivalence.transitive eq (halvingSequenceMultiple 1/2 {n}) (Equivalence.transitive eq (identityOfIndiscernablesLeft _∼_ (Equivalence.reflexive eq) (mapAndIndex (halvingSequence 1R) (_*_ 1/2) n)) *Commutative))) (orderRespectsMultiplication (halvingSequencePositive n) (halvePositive 1/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq pr1/2) (0<1 (charNot2ImpliesNontrivial charNot2)))))

decreasingHalving : Decreasing (halvingSequence 1R)
decreasingHalving N with halve charNot2 1R
decreasingHalving N | 1/2 , pr1/2 with (halfLess 1/2 1R (0<1 (charNot2ImpliesNontrivial charNot2)) pr1/2)
... | 1/2<1 = <WellDefined (Equivalence.transitive eq (identityOfIndiscernablesLeft _∼_ (Equivalence.reflexive eq) (equalityCommutative (mapAndIndex (halvingSequence 1R) (_*_ 1/2) N))) (Equivalence.symmetric eq (halvingSequenceMultiple 1/2 {N}))) identIsIdent (ringCanMultiplyByPositive {c = index (halvingSequence 1R) N} (halvingSequencePositive N) 1/2<1)

imageOfN : ℕ → A
imageOfN zero = 0R
imageOfN (succ x) = 1R + imageOfN x

nextImageOfN : (a : A) → 0R < a → ℕ
nextImageOfN a 0<a = ?

halvingToZero : (a : A) → (0G < a) → Sg ℕ (λ N → (index (halvingSequence 1R) N) < a)
halvingToZero a 0<a with SetoidTotalOrder.totality tOrder a 1R
halvingToZero a 0<a | inl (inl a<1) = {!!}
halvingToZero a 0<a | inl (inr 1<a) = 0 , 1<a
halvingToZero a 0<a | inr a=1 with halve charNot2 1R
... | 1/2 , pr1/2 = 1 , <WellDefined ans (Equivalence.symmetric eq a=1) (halfLess 1/2 1R (0<1 (charNot2ImpliesNontrivial charNot2)) pr1/2)
  where
    ans : 1/2 ∼ Sequence.head (Sequence.tail (halvingSequence 1R))
    ans with halve charNot2 1R
    ans | 1/2' , pr1/2' = halvesEqual charNot2 1/2 1/2' pr1/2 pr1/2'

halvesCauchy : cauchy (halvingSequence 1R)
halvesCauchy e 0<e = {!!}

multipleOfCauchyIsCauchy : (mult : A) → (seq : Sequence A) → cauchy seq → cauchy (map (mult *_) seq)
multipleOfCauchyIsCauchy mult seq seqCauchy e 0<e with SetoidTotalOrder.totality tOrder 0R mult
multipleOfCauchyIsCauchy mult seq seqCauchy e 0<e | inl (inl x) with allInvertible mult λ pr → irreflexive (<WellDefined (Equivalence.reflexive eq) pr x)
... | 1/mult , pr1/mult = {!!}
multipleOfCauchyIsCauchy mult seq seqCauchy e 0<e | inl (inr x) with allInvertible mult λ pr → irreflexive (<WellDefined pr (Equivalence.reflexive eq) x)
... | 1/mult , pr1/mult = {!!}
multipleOfCauchyIsCauchy mult seq seqCauchy e 0<e | inr 0=mult = 0 , ans
  where
    ans : {m n : ℕ} → (0 <N m) → (0 <N n) → abs (index (map (_*_ mult) seq) m + inverse (index (map (_*_ mult) seq) n)) < e
    ans {m} {n} _ _ rewrite equalityCommutative (mapAndIndex seq (_*_ mult) m) | equalityCommutative (mapAndIndex seq (_*_ mult) n) = <WellDefined {!!} (Equivalence.reflexive eq) 0<e

halvingSequenceCauchy : (start : A) → cauchy (halvingSequence start)
halvingSequenceCauchy start = {!!}

sequenceAllAbove : (a : CauchyCompletion) → Sequence A
sequenceAllAbove a = go (Ring.1R R) (0<1 (charNot2ImpliesNontrivial charNot2))
  where
    go : (e : A) → (0G < e) → Sequence A
    Sequence.head (go e 0<e) = rationalApproximatelyAbove a e 0<e
    Sequence.tail (go e 0<e) with halve charNot2 e
    ... | e/2 , prE/2 = go e/2 (halvePositive e/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/2) 0<e))

sequenceAllAboveCauchy : (a : CauchyCompletion) → cauchy (sequenceAllAbove a)
sequenceAllAboveCauchy a e 0<e = {!!}
  -- find N such that 1/2^N < e
  -- show that this N is enough

-- show that sequenceAllAbove ∼ a
-- monotonify sequenceAllAbove
-- show that monotonify of a sequence which is all above its limit still converges to that limit


text:
module Day4 where

open import Prelude.String as String
open import Data.Maybe
open import Foreign.Haskell using (Unit)
open import Prelude.List as List
open import Data.Nat
open import Data.Nat.DivMod
open import Data.Nat.Properties
import Data.Nat.Show as ℕs
open import Prelude.Char
open import Data.Vec as Vec renaming (_>>=_ to _VV=_ ; toList to VecToList)
open import Data.Product
open import Relation.Nullary
open import Data.Nat.Properties
open import Data.Bool.Base
open import AocIO
open import AocUtil
open import AocVec
open import Relation.Binary.PropositionalEquality
open import EvenOdd

count-falsy : List Bool → ℕ
count-falsy ls = length (filter not ls)

split-line : List Char → List String
split-line ls with (words ls)
... | ls-words = List.map packString ls-words

has-following-duplicates : List String → Bool
has-following-duplicates [] = false
has-following-duplicates (x ∷ []) = false
has-following-duplicates (x ∷ y ∷ ls) with primStringEquality x y
... | false = has-following-duplicates (y ∷ ls)
... | true = true

main : IO Unit
main = mainBuilder (readFileMain process-file)
  where
    sort-word : String → String
    sort-word s with unpackString s
    ... | ls with sort ls
    ... | ls-sorted = packString ls-sorted
    is-valid-passphrase : List String → Bool
    is-valid-passphrase ls with List.map sort-word ls
    ... | sorted-words with sort sorted-words
    ... | ls-sorted = has-following-duplicates ls-sorted
    process-file : String → IO Unit
    process-file file-content with (lines (unpackString file-content))
    ... | file-lines with (List.map split-line file-lines)
    ... | lines-split-into-words with (List.map is-valid-passphrase lines-split-into-words)
    ... | lines-are-valid with count-falsy lines-are-valid
    ... | valid-count = printString (ℕs.show valid-count)

main2 : IO Unit
main2 = mainBuilder (readFileMain process-file)
  where
    is-valid-passphrase : List String → Bool
    is-valid-passphrase ls with sort ls
    ... | ls-sorted = has-following-duplicates ls-sorted
    process-file : String → IO Unit
    process-file file-content with (lines (unpackString file-content))
    ... | file-lines with (List.map split-line file-lines)
    ... | lines-split-into-words with (List.map is-valid-passphrase lines-split-into-words)
    ... | lines-are-valid with count-falsy lines-are-valid
    ... | valid-count = printString (ℕs.show valid-count)


text:
module Basics where

id : {A : Set} -> A -> A
id a = a

_o_ : {A : Set}{B : A -> Set}{C : (a : A)(b : B a) -> Set} ->
      ({a : A}(b : B a) -> C a b) -> (g : (a : A) -> B a) ->
      (a : A) -> C a (g a)
_o_ f g a = f (g a)


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

module Definition.Conversion.Whnf where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Conversion

open import Tools.Product

mutual
  -- Extraction of neutrality from algorithmic equality of neutrals.
  ne~↑ : ∀ {t u A Γ}
       → Γ ⊢ t ~ u ↑ A
       → Neutral t × Neutral u
  ne~↑ (var-refl x₁ x≡y) = var _ , var _
  ne~↑ (app-cong x x₁) = let _ , q , w = ne~↓ x
                         in  ∘ₙ q , ∘ₙ w
  ne~↑ (fst-cong x) =
    let _ , pNe , rNe = ne~↓ x
    in  fstₙ pNe , fstₙ rNe
  ne~↑ (snd-cong x) =
    let _ , pNe , rNe = ne~↓ x
    in  sndₙ pNe , sndₙ rNe
  ne~↑ (natrec-cong x x₁ x₂ x₃) = let _ , q , w = ne~↓ x₃
                                  in  natrecₙ q , natrecₙ w
  ne~↑ (Emptyrec-cong x x₁) = let _ , q , w = ne~↓ x₁
                              in Emptyrecₙ q , Emptyrecₙ w

  -- Extraction of neutrality and WHNF from algorithmic equality of neutrals
  -- with type in WHNF.
  ne~↓ : ∀ {t u A Γ}
       → Γ ⊢ t ~ u ↓ A
       → Whnf A × Neutral t × Neutral u
  ne~↓ ([~] A₁ D whnfB k~l) = whnfB , ne~↑ k~l

-- Extraction of WHNF from algorithmic equality of types in WHNF.
whnfConv↓ : ∀ {A B Γ}
          → Γ ⊢ A [conv↓] B
          → Whnf A × Whnf B
whnfConv↓ (U-refl x) = Uₙ , Uₙ
whnfConv↓ (ℕ-refl x) = ℕₙ , ℕₙ
whnfConv↓ (Empty-refl x) = Emptyₙ , Emptyₙ
whnfConv↓ (Unit-refl x) = Unitₙ , Unitₙ
whnfConv↓ (ne x) = let _ , neA , neB = ne~↓ x
                   in  ne neA , ne neB
whnfConv↓ (Π-cong x x₁ x₂) = Πₙ , Πₙ
whnfConv↓ (Σ-cong x x₁ x₂) = Σₙ , Σₙ

-- Extraction of WHNF from algorithmic equality of terms in WHNF.
whnfConv↓Term : ∀ {t u A Γ}
              → Γ ⊢ t [conv↓] u ∷ A
              → Whnf A × Whnf t × Whnf u
whnfConv↓Term (ℕ-ins x) = let _ , neT , neU = ne~↓ x
                           in ℕₙ , ne neT , ne neU
whnfConv↓Term (Empty-ins x) = let _ , neT , neU = ne~↓ x
                              in Emptyₙ , ne neT , ne neU
whnfConv↓Term (Unit-ins x) = let _ , neT , neU = ne~↓ x
                             in Unitₙ , ne neT , ne neU
whnfConv↓Term (ne-ins t u x x₁) =
  let _ , neT , neU = ne~↓ x₁
  in ne x , ne neT , ne neU
whnfConv↓Term (univ x x₁ x₂) = Uₙ , whnfConv↓ x₂
whnfConv↓Term (zero-refl x) = ℕₙ , zeroₙ , zeroₙ
whnfConv↓Term (suc-cong x) = ℕₙ , sucₙ , sucₙ
whnfConv↓Term (η-eq x₁ x₂ y y₁ x₃) = Πₙ , functionWhnf y , functionWhnf y₁
whnfConv↓Term (Σ-η _ _ pProd rProd _ _) = Σₙ , productWhnf pProd , productWhnf rProd
whnfConv↓Term (η-unit _ _ tWhnf uWhnf) = Unitₙ , tWhnf , uWhnf


text:
postulate
  A : Set
  B : A → Set

@0 T : _
T = (@0 x : A) → B x

max_forks_repo_name: shlevy/agda


text:
------------------------------------------------------------------------
-- Types used to make recursive arguments coinductive
------------------------------------------------------------------------

-- See Data.Colist for examples of how this type is used, or
-- http://article.gmane.org/gmane.comp.lang.agda/633 for a longer
-- explanation.

module Coinduction where

infix 10 ♯_ ♯₁_

codata ∞ (T : Set) : Set where
  ♯_ : (x : T) → ∞ T

♭ : ∀ {T} → ∞ T → T
♭ (♯ x) = x

-- Variant for Set₁.

codata ∞₁ (T : Set₁) : Set₁ where
  ♯₁_ : (x : T) → ∞₁ T

♭₁ : ∀ {T} → ∞₁ T → T
♭₁ (♯₁ x) = x

max_issues_repo_name: larrytheliquid/Lemmachine


text:
open import Prelude
open import Data.List.Properties
open import Data.List.Any hiding (map)
open import Extensions.Vec
open import Data.Vec
open import Data.List.All as All hiding (map; lookup)

module Implicits.Resolution.Infinite.Semantics where

open import Implicits.Syntax
open import Implicits.Resolution.Infinite.Resolution
open import Implicits.Substitutions
open import Implicits.Substitutions.Lemmas
open import Implicits.Semantics
open import Implicits.Semantics.Lemmas

open import SystemF.Everything as F using ()

module DerivationSemantics where

  ⟦_,_⟧r : ∀ {ν n} {Δ : ICtx ν} {Γ : Ctx ν n} {a} → Δ ⊢ᵣ a → Γ # Δ →
           ∃ λ t → ⟦ Γ ⟧ctx→ F.⊢ t ∈ ⟦ a ⟧tp→
  ⟦_,_⟧r {Γ = Γ} (r-simp {r = r} r∈Δ r↓τ) m with ∈⟶index (All.lookup m r∈Δ)
  ⟦_,_⟧r {Γ = Γ} (r-simp {r = r} r∈Δ r↓τ) m | i , lookup-i≡r =
    ⟦ subst (λ u → _ F.⊢ F.var i ∈ u) eq (F.var i) , r↓τ , m ⟧r↓
    where
      eq = begin
        lookup i ⟦ Γ ⟧ctx→
          ≡⟨ sym $ lookup-⟦⟧ctx→ Γ i ⟩
        ⟦ lookup i Γ ⟧tp→
            ≡⟨ cong ⟦_⟧tp→ lookup-i≡r ⟩
        ⟦ r ⟧tp→ ∎

      ⟦_,_,_⟧r↓ : ∀ {ν n} {Δ : ICtx ν} {Γ : Ctx ν n} {a ta τ} →
                ⟦ Γ ⟧ctx→ F.⊢ ta ∈ ⟦ a ⟧tp→ → Δ ⊢ a ↓ τ → Γ # Δ →
                ∃ λ tτ → ⟦ Γ ⟧ctx→ F.⊢ tτ ∈ ⟦ simpl τ ⟧tp→
      ⟦ ⊢ta , i-simp τ , m ⟧r↓ = , ⊢ta
      ⟦ ⊢ta , i-iabs {ρ₁ = a} ⊢ᵣa b↓τ , m ⟧r↓ =
        , (proj₂ ⟦ ⊢ta F.· (proj₂ ⟦ ⊢ᵣa , m ⟧r) , b↓τ , m ⟧r↓)
      ⟦ ⊢ta , i-tabs {ρ = a} b p , m ⟧r↓ =
        ⟦ subst (λ u → _ F.⊢ _ ∈ u) (sym $ ⟦a/sub⟧tp→ a b) (⊢ta F.[ ⟦ b ⟧tp→ ]) , p , m ⟧r↓

  ⟦ r-iabs {ρ₁ = a} {ρ₂ = b} ⊢b , m ⟧r = , F.λ' ⟦ a ⟧tp→ (proj₂ ⟦ ⊢b , #ivar a m ⟧r)

  ⟦_,_⟧r {Γ = Γ} (r-tabs {ρ = r} p) m with ⟦ p , #tvar m ⟧r
  ⟦_,_⟧r {Δ = Δ} {Γ = Γ} (r-tabs {ρ = r} p) m | _ , x =
    , F.Λ (subst (λ u → u F.⊢ _ ∈ ⟦ r ⟧tp→) (⟦weaken⟧ctx→ Γ) x)

open Semantics _⊢ᵣ_ DerivationSemantics.⟦_,_⟧r public


text:
module Issue846.DivModUtils where

open import Data.Nat
open import Data.Bool

open import Issue846.OldDivMod
open import Relation.Nullary
open import Data.Nat.Properties hiding (≤-antisym)
open import Data.Nat.Solver
open import Data.Fin using (Fin; toℕ; zero; suc; fromℕ≤)
open import Data.Fin.Properties using ( bounded; toℕ-fromℕ≤; toℕ-injective )
open import Relation.Binary.PropositionalEquality
open import Function
open import Data.Product
open import Relation.Binary hiding (NonEmpty)
open import Data.Empty
open import Relation.Nullary.Negation
open ≡-Reasoning
open ≤-Reasoning
  renaming (begin_ to start_; _∎ to _□; _≡⟨_⟩_ to _≡⟨_⟩'_)
open DecTotalOrder ≤-decTotalOrder using () renaming (refl to ≤-refl; antisym to ≤-antisym)

i+[j∸m]≡i+j∸m : ∀ i j m → m ≤ j → i + (j ∸ m) ≡ i + j ∸ m
i+[j∸m]≡i+j∸m i zero zero lt = refl
i+[j∸m]≡i+j∸m i zero (suc m) ()
i+[j∸m]≡i+j∸m i (suc j) zero lt = refl
i+[j∸m]≡i+j∸m i (suc j) (suc m) (s≤s m≤j) = begin
  i + (j ∸ m)             ≡⟨ i+[j∸m]≡i+j∸m i j m m≤j ⟩
  suc (i + j) ∸ suc m   ≡⟨ cong (λ y → y ∸ suc m) $ solve 2 (λ i' j' → con 1 :+ (i' :+ j') := i' :+ (con 1 :+ j')) refl i j ⟩
  (i + suc j) ∸ suc m ∎
  where
    open +-*-Solver

-- Following code taken from https://github.com/copumpkin/derpa/blob/master/REPA/Index.agda#L210

-- the next few bits are lemmas to prove uniqueness of euclidean division

-- first : for nonzero divisors, a nonzero quotient would require a larger
-- dividend than is consistent with a zero quotient, regardless of
-- remainders.

large : ∀ {d} {r : Fin (suc d)} x (r′ : Fin (suc d)) → toℕ r ≢ suc x * suc d + toℕ r′
large {d} {r} x r′ pf = irrefl pf (
    start
      suc (toℕ r)
    ≤⟨ bounded r ⟩
      suc d
    ≤⟨ m≤m+n (suc d) (x * suc d) ⟩
      suc d + x * suc d -- same as (suc x * suc d)
    ≤⟨ m≤m+n (suc x * suc d) (toℕ r′) ⟩
      suc x * suc d + toℕ r′ -- clearer in two steps, and we'd need assoc anyway
    □)
  where
  open ≤-Reasoning
  open Relation.Binary.StrictTotalOrder Data.Nat.Properties.<-strictTotalOrder

-- a raw statement of the uniqueness, in the arrangement of terms that's
-- easiest to work with computationally

addMul-lemma′ : ∀ x x′ d (r r′ : Fin (suc d)) → x * suc d + toℕ r ≡ x′ * suc d + toℕ r′ → r ≡ r′ × x ≡ x′
addMul-lemma′ zero zero d r r′ hyp = (toℕ-injective hyp) , refl
addMul-lemma′ zero (suc x′) d r r′ hyp = ⊥-elim (large x′ r′ hyp)
addMul-lemma′ (suc x) zero d r r′ hyp = ⊥-elim (large x r (sym hyp))
addMul-lemma′ (suc x) (suc x′) d r r′ hyp
                      rewrite +-assoc (suc d) (x * suc d) (toℕ r)
                            | +-assoc (suc d) (x′ * suc d) (toℕ r′)
                      with addMul-lemma′ x x′ d r r′ (+-cancelˡ-≡ (suc d) hyp)
... | pf₁ , pf₂ = pf₁ , cong suc pf₂

-- and now rearranged to the order that Data.Nat.DivMod uses

addMul-lemma : ∀ x x′ d (r r′ : Fin (suc d)) → toℕ r + x * suc d ≡ toℕ r′ + x′ * suc d → r ≡ r′ × x ≡ x′
addMul-lemma x x′ d r r′ hyp rewrite +-comm (toℕ r) (x * suc d)
                                   | +-comm (toℕ r′) (x′ * suc d)
  = addMul-lemma′ x x′ d r r′ hyp

DivMod-lemma : ∀ x d (r : Fin (suc d)) → (res : DivMod (toℕ r + x * suc d) (suc d)) → res ≡ result x r refl
DivMod-lemma x d r (result q r′ eq) with addMul-lemma x q d r r′ eq
DivMod-lemma x d r (result .x .r eq) | refl , refl = cong (result x r) (≡-irrelevance eq refl) -- holy fuck

divMod-lemma : ∀ x d (r : Fin (suc d)) → (toℕ r + x * suc d) divMod suc d ≡ result x r refl
divMod-lemma x d r with (toℕ r + x * suc d) divMod suc d
divMod-lemma x d r | q rewrite DivMod-lemma x d r q = refl

-- End of copied code

mod-lemma : ∀ x d (r : Fin (suc d)) → (toℕ r + x * suc d) mod suc d ≡ r
mod-lemma x d r rewrite divMod-lemma x d r = refl

mod-suc : ∀ n
  →     n mod 7 ≡     zero
  → suc n mod 7 ≡ suc zero
mod-suc n eq with n divMod 7
mod-suc .(q * 7) refl | result q .zero refl = mod-lemma q 6 (suc zero)

mod-pred : ∀ n
  →  suc n mod 7 ≡ suc zero
  →      n mod 7 ≡     zero
mod-pred n eq with n divMod 7
mod-pred .(toℕ r + q * 7) eq | result q r refl with toℕ r ≤? 5
mod-pred .(toℕ r + q * 7) eq | result q r refl | yes p  = toℕ-injective eq4
  where r' = fromℕ≤ {suc (toℕ r)} {7} (s≤s (s≤s p))
        r'≡r = toℕ-fromℕ≤ (s≤s (s≤s p))
        eq4 = cong pred $ begin
          suc (toℕ r)
            ≡⟨ sym r'≡r ⟩
          toℕ r'
            ≡⟨ cong toℕ $ begin
              r'                        ≡⟨ sym (mod-lemma q 6 r') ⟩
              (toℕ r' + q * 7) mod 7    ≡⟨ cong (λ y → (y + q * 7) mod 7) r'≡r ⟩
              suc (toℕ r + q * 7) mod 7 ≡⟨ eq ⟩
              suc zero ∎ ⟩
          toℕ (suc (zero {7}))
            ≡⟨ refl ⟩
          suc zero ∎
mod-pred .(toℕ r + q * 7) eq | result q r refl | no ¬p with eq3
  where eq2 = begin
          6
            ≡⟨ ≤-antisym (≰⇒> ¬p) (pred-mono (bounded r)) ⟩
          toℕ r ∎
        eq3 = begin
          zero
            ≡⟨ sym (mod-lemma (suc q) 6 zero) ⟩
          (suc q * 7) mod 7
            ≡⟨ refl ⟩
          suc (6 + q * 7) mod 7
            ≡⟨ cong (λ y → suc (y + q * 7) mod 7) $ eq2 ⟩
          suc (toℕ r + q * 7) mod 7
            ≡⟨ eq ⟩
          suc zero ∎
... | ()

∸-mono₁ : ∀ i j k → i ≤ j →  i ∸ k ≤ j ∸ k
∸-mono₁ i j zero i≤j = i≤j
∸-mono₁ zero j (suc k) i≤j = z≤n
∸-mono₁ (suc i) zero (suc k) ()
∸-mono₁ (suc i) (suc j) (suc k) (s≤s i≤j) = ∸-mono₁ i j k i≤j

∸-mono₂ : ∀ i j k → j ≤ k → i ∸ j ≥ i ∸ k
∸-mono₂ i zero k j≤k = n∸m≤n k i
∸-mono₂ i (suc j) zero ()
∸-mono₂ zero (suc j) (suc k) j≤k = z≤n
∸-mono₂ (suc n) (suc j) (suc k) (s≤s j≤k) = ∸-mono₂ n j k j≤k

1' : Fin 7
1' = suc zero

lem-sub-p : ∀ n p → (suc n mod 7 ≡ 1') → 1 ≤ p → p ≤ 6 → ((suc n ∸ p) mod 7 ≢ 1')
lem-sub-p _ 0 _ () _ _
lem-sub-p n 1 eq1 _ _ eq2 with begin zero ≡⟨ sym (mod-pred n eq1) ⟩ n mod 7 ≡⟨ eq2 ⟩ suc zero ∎
... | ()
lem-sub-p n (suc (suc p)) eq _ ≤6 eq2 with n divMod 7 | mod-pred n eq
lem-sub-p .0 (suc (suc p)) _ _ ≤6 () | result zero .zero refl | refl
lem-sub-p .(7 + (q * 7)) (suc (suc p)) _ _ (s≤s (s≤s (≤4))) eq2 | result (suc q) .zero refl | refl = ⊥-elim $ 1+n≰n 1<1
  where <7 : (6 ∸ p) < 7
        <7 = s≤s (n∸m≤n p 6)
        eq4 = begin
            toℕ (fromℕ≤ <7) + q * 7
              ≡⟨ cong (λ y → y + q * 7) (toℕ-fromℕ≤ <7 )⟩
            (6 ∸ p) + q * 7
              ≡⟨ +-comm (6 ∸ p) (q * 7) ⟩
            q * 7 + (6 ∸ p)
              ≡⟨ i+[j∸m]≡i+j∸m (q * 7) 6 p (≤-stepsˡ 2 ≤4) ⟩
            (q * 7 + 6) ∸ p
              ≡⟨ cong (λ y → y ∸ p) (+-comm (q * 7) 6)⟩
            (6 + q * 7) ∸ p ∎
        eq5 = begin
            fromℕ≤ <7
              ≡⟨ sym (mod-lemma q 6 (fromℕ≤ <7)) ⟩
            (toℕ (fromℕ≤ <7) + q * 7) mod 7
              ≡⟨ cong (λ y → y mod 7) eq4 ⟩
            ((6 + q * 7) ∸ p) mod 7
              ≡⟨ eq2 ⟩
            suc zero ∎
        1<1 = start
            2                     ≤⟨ ∸-mono₂ 6 p 4 ≤4 ⟩
            6 ∸ p                 ≡⟨ sym (toℕ-fromℕ≤ <7) ⟩'
            toℕ (fromℕ≤ <7)       ≡⟨ cong toℕ eq5 ⟩'
            toℕ (suc (zero {7}))  ≡⟨ refl ⟩'
            suc zero □

-- bla = nonEmpty

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module Oscar.Property.IsReflexive where

open import Oscar.Level

record IsReflexive {𝔬} (⋆ : Set 𝔬) {ℓ} (_≣_ : ⋆ → ⋆ → Set ℓ) : Set (𝔬 ⊔ ℓ) where
  field
    reflexivity : ∀ x → x ≣ x


text:
module Impure.LFRef.Welltyped where

open import Prelude

open import Data.List hiding ([_])
open import Data.List.All hiding (map)
open import Data.Vec as Vec hiding ([_]; map)
open import Data.Star hiding (_▻▻_; map)
open import Data.Sum hiding (map)
open import Extensions.List as L using ()

open import Impure.LFRef.Syntax hiding (subst)
open import Relation.Binary.List.Pointwise using (Rel)

Ctx : (n : ℕ) → Set
Ctx n = Vec (Type n) n

-- store typings
World : Set
World = List (Type 0)

weaken₁-tp : ∀ {n} → Type n → Type (suc n)
weaken₁-tp tp = tp tp/ wk

_:+:_ : ∀ {n} → Type n → Ctx n → Ctx (suc n)
a :+: Γ = (weaken₁-tp a) ∷ (Vec.map (flip _tp/_ wk) Γ)

weaken+-tm : ∀ {m} n → Term m → Term (n + m)
weaken+-tm n t = t / (wk⋆ n)

weaken+-tp : ∀ n → Type 0 → Type n
weaken+-tp zero t = t
weaken+-tp (suc n) t = subst Type (+-right-identity (suc n)) (t tp/ (wk⋆ (suc n)))

weaken+-tele : ∀ {m n} k → Tele n m → Tele (n + k) m
weaken+-tele k T = subst (flip Tele _) (+-comm k _) (T tele/ (wk⋆ k))

-- mutually inductive welltypedness judgments for kinds/types and terms respectively
data _,_,_⊢_teleok : ∀ {n m} → (𝕊 : Sig) → World → Ctx n → Tele n m → Set
data _,_,_⊢_::_ : ∀ {n m} (𝕊 : Sig) → World → Ctx n → Type n → Tele n m → Set
data _,_,_⊢_∶_ : ∀ {n} (𝕊 : Sig) → World → Ctx n → Term n → Type n → Set

data _,_,_⊢_teleok where
  ε : ∀ {n 𝕊 Σ} {Γ : Ctx n} → 𝕊 , Σ , Γ ⊢ ε teleok

  _⟶_ : ∀ {n m 𝕊 Σ Γ} {A : Type n} {K : Tele (suc n) m}→
        𝕊 , Σ , Γ ⊢ A :: ε →
        𝕊 , Σ , (A :+: Γ) ⊢ K teleok →
        𝕊 , Σ , Γ ⊢ (A ⟶ K) teleok

data _,_,_⊢_∶ⁿ_ {n} (𝕊 : Sig) (Σ : World) (Γ : Ctx n) :
     ∀ {m} → List (Term n) → Tele n m → Set where

  ε : 𝕊 , Σ , Γ ⊢ [] ∶ⁿ ε

  _⟶_ : ∀ {m A t ts} {B : Tele (suc n) m}→
        𝕊 , Σ , Γ ⊢ t ∶ A →
        𝕊 , Σ , Γ ⊢ ts ∶ⁿ (B tele/ (sub t)) →
        𝕊 , Σ , Γ ⊢ (t ∷ ts) ∶ⁿ (A ⟶ B)

-- specialize the returntype from a constructor from it's welltyped arguments
_con[_/_] : ∀ {n} → (C : ConType) → (ts : List (Term n)) → length ts ≡ (ConType.m C) → Type n
_con[_/_] {n} C ts p =
  (ConType.tp C) [
    map
      (flip _/_ (subst (Vec _) p (fromList ts)))
      (ConType.indices C)
  ]

-- specialize the return type of a function from it's welltyped arguments
_fun[_/_] : ∀ {n m} → Type m → (ts : List (Term n)) → length ts ≡ m → Type n
_fun[_/_] {n} {m} a ts p = a tp/ subst (Vec _) p ((fromList ts))

data _,_,_⊢_::_ where

  Ref : ∀ {n 𝕊 Σ} {Γ : Ctx n} {A} →
        𝕊 , Σ , Γ ⊢ A :: ε →
        ----------------------
        𝕊 , Σ , Γ ⊢ Ref A :: ε

  Unit : ∀ {n 𝕊 Σ} {Γ : Ctx n} →
        ---------------------
        𝕊 , Σ , Γ ⊢ Unit :: ε

  _[_] : ∀ {n 𝕊 Σ} {Γ : Ctx n} {k K ts} →
         (Sig.types 𝕊) L.[ k ]= K →
         𝕊 , [] , [] ⊢ (proj₂ K) teleok →
         𝕊 , Σ , Γ ⊢ ts ∶ⁿ (weaken+-tele n (proj₂ K)) →
         -------------------------
         𝕊 , Σ , Γ ⊢ k [ ts ] :: ε

data _,_,_⊢_∶_ where

  unit : ∀ {n 𝕊 Σ} {Γ : Ctx n} →
        -----------------------
        𝕊 , Σ , Γ ⊢ unit ∶ Unit

  var : ∀ {n 𝕊 Σ} {Γ : Ctx n} {i A} →
        Γ [ i ]= A →
        ---------------------
        𝕊 , Σ , Γ ⊢ var i ∶ A

  con : ∀ {n 𝕊 Σ} {Γ : Ctx n} {c C ts} →
        (Sig.constructors 𝕊) L.[ c ]= C →
        (p : 𝕊 , Σ , Γ ⊢ ts ∶ⁿ weaken+-tele n (ConType.args C)) →
        (q : length ts ≡ (ConType.m C)) →
        ------------------------------------
        𝕊 , Σ , Γ ⊢ con c ts ∶ (C con[ ts / q ])

  loc : ∀ {n 𝕊 Σ} {Γ : Ctx n} {i S} →
        Σ L.[ i ]= S →
        ---------------------
        𝕊 , Σ , Γ ⊢ loc i ∶ Ref (weaken+-tp n S)

data _,_,_⊢ₑ_∶_ : ∀ {n} (𝕊 : Sig) → World → Ctx n → Exp n → Type n → Set where

  tm   : ∀ {n t} {Γ : Ctx n} {𝕊 Σ A} →
         𝕊 , Σ , Γ ⊢ t ∶ A →
         ---------------------
         𝕊 , Σ , Γ ⊢ₑ tm t ∶ A

  _·★[_]_ : ∀ {n fn ts 𝕊 Σ φ} {Γ : Ctx n} →
         (Sig.funs 𝕊) L.[ fn ]= φ →
         (q : length ts ≡ (Fun.m φ)) →
         (p : 𝕊 , Σ , Γ ⊢ ts ∶ⁿ weaken+-tele n (Fun.args φ)) →
         -----------------------------------------------------
         𝕊 , Σ , Γ ⊢ₑ (fn ·★ ts) ∶ ((Fun.returntype φ) fun[ ts / q ])

  ref : ∀ {n x A 𝕊 Σ} {Γ : Ctx n} →
        𝕊 , Σ , Γ ⊢ₑ x ∶ A →
        --------------------------
        𝕊 , Σ , Γ ⊢ₑ ref x ∶ Ref A

  !_  : ∀ {n x A} {Γ : Ctx n} {𝕊 Σ} →

        𝕊 , Σ , Γ ⊢ₑ x ∶ Ref A →
        ----------------------
        𝕊 , Σ , Γ ⊢ₑ (! x) ∶ A

  _≔_ : ∀ {n i x A} {Γ : Ctx n} {𝕊 Σ} →
        𝕊 , Σ , Γ ⊢ₑ i ∶ Ref A →
        𝕊 , Σ , Γ ⊢ₑ x ∶ A →
        --------------------------
        𝕊 , Σ , Γ ⊢ₑ (i ≔ x) ∶ Unit

data _,_,_⊢ₛ_∶_ : ∀ {n} (𝕊 : Sig) → World → Ctx n → SeqExp n → Type n → Set where

  ret  : ∀ {n x A 𝕊 Σ} {Γ : Ctx n} →
         𝕊 , Σ , Γ ⊢ₑ x ∶ A →
         ---------------------
         𝕊 , Σ , Γ ⊢ₛ ret x ∶ A

  lett : ∀ {n x c A B 𝕊 Σ} {Γ : Ctx n} →
         𝕊 , Σ , Γ ⊢ₑ x ∶ A →
         𝕊 , (Σ) , (A :+: Γ) ⊢ₛ c ∶ weaken₁-tp B →
         ---------------------------------------r
         𝕊 , Σ , Γ ⊢ₛ lett x c ∶ B

-- telescopes as context transformers
_⊢⟦_⟧ : ∀ {n m} → Ctx n → Tele n m → Ctx (n + m)
Γ ⊢⟦ ε ⟧ = subst Ctx (sym $ +-right-identity _) Γ
_⊢⟦_⟧ {n} Γ (_⟶_ {m = m} x T) = subst Ctx (sym $ +-suc n m) ((x :+: Γ) ⊢⟦ T ⟧)

_⊢_fnOk : Sig → Fun → Set
_⊢_fnOk 𝕊 φ = 𝕊 , [] , ([] ⊢⟦ Fun.args φ ⟧) ⊢ₑ (Fun.body φ) ∶ (Fun.returntype φ)

-- valid signature contexts
record _,_⊢ok {n} (𝕊 : Sig) (Γ : Ctx n) : Set where
  field
    funs-ok : All (λ x → 𝕊 ⊢ x fnOk) (Sig.funs 𝕊)

-- store welltypedness relation
-- as a pointwise lifting of the welltyped relation on closed expressions between a world and a store
_,_⊢_ : Sig → World → Store → Set
_,_⊢_ 𝕊 Σ μ = Rel (λ A x → 𝕊 , Σ , [] ⊢ (proj₁ x) ∶ A) Σ μ

-- a useful lemma about telescoped terms
tele-fit-length : ∀ {n m 𝕊 Σ Γ ts} {T : Tele n m} → 𝕊 , Σ , Γ ⊢ ts ∶ⁿ T → length ts ≡ m
tele-fit-length ε = refl
tele-fit-length (x ⟶ p) with tele-fit-length p
tele-fit-length (x ⟶ p) | refl = refl


text:
------------------------------------------------------------------------
-- Lemmas related to application of substitutions
------------------------------------------------------------------------

open import Data.Universe.Indexed

module deBruijn.Substitution.Data.Application.Application221
  {i u e} {Uni : IndexedUniverse i u e}
  where

import deBruijn.Context; open deBruijn.Context Uni
open import deBruijn.Substitution.Data.Application.Application21
open import deBruijn.Substitution.Data.Basics
open import deBruijn.Substitution.Data.Map
open import deBruijn.Substitution.Data.Simple
open import Function using (_$_)
open import Level using (_⊔_)
import Relation.Binary.PropositionalEquality as P

open P.≡-Reasoning

-- Lemmas related to application.

record Application₂₂₁
  {t₁} {T₁ : Term-like t₁}
  {t₂} {T₂ : Term-like t₂}

  -- Simple substitutions for the first kind of terms.
  (simple₁ : Simple T₁)

  -- Simple substitutions for the second kind of terms.
  (simple₂ : Simple T₂)

  -- A translation from the first to the second kind of terms.
  (trans : [ T₁ ⟶⁼ T₂ ])
  : Set (i ⊔ u ⊔ e ⊔ t₁ ⊔ t₂) where

  open Term-like T₂ using ([_]) renaming (_⊢_ to _⊢₂_; _≅-⊢_ to _≅-⊢₂_)
  open Simple simple₁
    using ()
    renaming ( wk to wk₁; wk[_] to wk₁[_]; wk-subst to wk-subst₁
             ; _↑ to _↑₁; _↑_ to _↑₁_; _↑⁺_ to _↑⁺₁_; _↑⁺⋆_ to _↑⁺⋆₁_
             )
  open Simple simple₂
    using ()
    renaming ( var to var₂
             ; weaken to weaken₂; weaken[_] to weaken₂[_]
             ; wk[_] to wk₂[_]
             ; wk-subst to wk-subst₂; wk-subst[_] to wk-subst₂[_]
             ; _↑ to _↑₂
             )

  field
    application₂₁ : Application₂₁ simple₁ simple₂ trans

  open Application₂₁ application₂₁

  field
    -- Lifts equalities valid for all variables and liftings to
    -- arbitrary terms.
    var-/⊢⋆-↑⁺⋆-⇒-/⊢⋆-↑⁺⋆ :
      ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} (ρs₁ : Subs T₁ ρ̂) (ρs₂ : Subs T₁ ρ̂) →
      (∀ Γ⁺ {σ} (x : Γ ++⁺ Γ⁺ ∋ σ) →
         var₂ · x /⊢⋆ ρs₁ ↑⁺⋆₁ Γ⁺ ≅-⊢₂ var₂ · x /⊢⋆ ρs₂ ↑⁺⋆₁ Γ⁺) →
      ∀ Γ⁺ {σ} (t : Γ ++⁺ Γ⁺ ⊢₂ σ) →
      t /⊢⋆ ρs₁ ↑⁺⋆₁ Γ⁺ ≅-⊢₂ t /⊢⋆ ρs₂ ↑⁺⋆₁ Γ⁺

    -- The wk substitution and the weaken function are equivalent.
    /⊢-wk : ∀ {Γ σ τ} (t : Γ ⊢₂ τ) →
            t /⊢ wk₁[ σ ] ≅-⊢₂ weaken₂[ σ ] · t

  abstract

    -- wk-subst is equivalent to composition with wk.

    ∘-wk : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T₂ ρ̂) →
           ρ ∘ wk₁[ σ ] ≅-⇨ wk-subst₂[ σ ] ρ
    ∘-wk ρ = begin
      [ map (app wk₁) ρ ]  ≡⟨ map-cong-ext₁ P.refl /⊢-wk (P.refl {x = [ ρ ]}) ⟩
      [ map weaken₂   ρ ]  ∎

    -- The wk substitution commutes (modulo lifting etc.) with any
    -- other.
    --
    -- TODO: Prove this lemma using /⊢-/⊢-wk?

    wk-∘-↑ : ∀ {Γ Δ} σ {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T₁ ρ̂) →
             map trans ρ ∘ wk₁[ σ / ρ ] ≅-⇨ wk₂[ σ ] ∘ ρ ↑₁
    wk-∘-↑ σ ρ = extensionality P.refl λ x → begin
      [ x /∋ map trans ρ ∘ wk₁         ]  ≡⟨ /∋-cong (P.refl {x = [ x ]}) (∘-wk (map trans ρ)) ⟩
      [ x /∋ wk-subst₂ (map trans ρ)   ]  ≡⟨ P.sym $ Simple.suc-/∋-↑ simple₂ σ x (map trans ρ) ⟩
      [ suc[ σ ] x /∋ map trans ρ ↑₂   ]  ≡⟨ /∋-cong (P.refl {x = [ suc[ σ ] x ]}) (P.sym $ map-trans-↑ ρ) ⟩
      [ suc[ σ ] x /∋ map trans (ρ ↑₁) ]  ≡⟨ /∋-map (suc[ σ ] x) trans (ρ ↑₁) ⟩
      [ trans · (suc[ σ ] x /∋ ρ ↑₁)   ]  ≡⟨ P.sym $ var-/⊢ (suc[ σ ] x) (ρ ↑₁) ⟩
      [ var₂ · suc[ σ ] x /⊢ ρ ↑₁      ]  ≡⟨ /⊢-cong (P.sym $ Simple./∋-wk simple₂ {σ = σ} x) (P.refl {x = [ ρ ↑₁ ]}) ⟩
      [ x /∋ wk₂[ σ ] /⊢ ρ ↑₁          ]  ≡⟨ P.sym $ /∋-∘ x wk₂[ σ ] (ρ ↑₁) ⟩
      [ x /∋ wk₂[ σ ] ∘ ρ ↑₁           ]  ∎

    -- A variant of suc-/∋-↑.

    var-suc-/⊢-↑ :
      ∀ {Γ Δ} σ {τ} {ρ̂ : Γ ⇨̂ Δ} (x : Γ ∋ τ) (ρ : Sub T₁ ρ̂) →
      var₂ · suc[ σ ] x /⊢ ρ ↑₁ ≅-⊢₂
      var₂ · x /⊢ ρ /⊢ wk₁[ σ / ρ ]
    var-suc-/⊢-↑ σ x ρ =
      let lemma₁ = begin
            [ x /∋ map trans ρ ]  ≡⟨ /∋-map x trans ρ ⟩
            [ trans · (x /∋ ρ) ]  ≡⟨ P.sym $ var-/⊢ x ρ ⟩
            [ var₂ · x /⊢ ρ    ]  ∎

          lemma₂ = begin
            [ map trans (wk-subst₁ ρ) ]  ≡⟨ map-trans-wk-subst ρ ⟩
            [ wk-subst₂ (map trans ρ) ]  ≡⟨ P.sym $ ∘-wk (map trans ρ) ⟩
            [ map trans ρ ∘ wk₁       ]  ∎

      in begin
      [ var₂ · suc[ σ ] x /⊢ ρ ↑₁    ]  ≡⟨ var-/⊢ (suc[ σ ] x) (ρ ↑₁) ⟩
      [ trans · (suc[ σ ] x /∋ ρ ↑₁) ]  ≡⟨ trans-cong (Simple.suc-/∋-↑ simple₁ σ x ρ) ⟩
      [ trans · (x /∋ wk-subst₁ ρ)   ]  ≡⟨ P.sym $ /∋-map x trans (wk-subst₁ ρ) ⟩
      [ x /∋ map trans (wk-subst₁ ρ) ]  ≡⟨ /∋-cong (P.refl {x = [ x ]}) lemma₂ ⟩
      [ x /∋ map trans ρ ∘ wk₁       ]  ≡⟨ /∋-∘ x (map trans ρ) wk₁ ⟩
      [ x /∋ map trans ρ /⊢ wk₁      ]  ≡⟨ /⊢-cong lemma₁ (P.refl {x = [ wk₁ ]}) ⟩
      [ var₂ · x /⊢ ρ /⊢ wk₁         ]  ∎

    private

      -- wk ↑⁺ Γ⁺ and wk commute (more or less).
      --
      -- This lemma is an instance of /⊢-/⊢-wk, which is proved below
      -- using, among other things, this lemma.

      /⊢-wk-↑⁺-/⊢-wk :
        ∀ {Γ} σ Γ⁺ τ {υ} (t : Γ ++⁺ Γ⁺ ⊢₂ υ) →
        let wk-σ = wk₁[ σ ] ↑⁺₁ Γ⁺ in
        t /⊢ wk-σ /⊢ wk₁[ τ / wk-σ ] ≅-⊢₂
        t /⊢ wk₁ /⊢ wk₁[ σ ] ↑⁺₁ (Γ⁺ ▻ τ)
      /⊢-wk-↑⁺-/⊢-wk σ Γ⁺ τ t = var-/⊢⋆-↑⁺⋆-⇒-/⊢⋆-↑⁺⋆
        (ε ▻ wk₁[ σ ] ↑⁺₁ Γ⁺ ▻ wk₁[ τ / wk₁ ↑⁺₁ Γ⁺ ])
        (ε ▻ wk₁ ▻ wk₁ ↑⁺₁ (Γ⁺ ▻ τ))
        (λ Γ⁺⁺ x → begin
           [ var₂ · x /⊢⋆ (ε ▻ wk₁ ↑⁺₁ Γ⁺ ▻ wk₁) ↑⁺⋆₁ Γ⁺⁺            ]  ≡⟨ /⊢⋆-ε-▻-▻-↑⁺⋆ Γ⁺⁺ (var₂ · x) (wk₁ ↑⁺₁ Γ⁺) wk₁ ⟩
           [ var₂ · x /⊢ wk₁ ↑⁺₁ Γ⁺ ↑⁺₁ Γ⁺⁺ /⊢
               wk₁ ↑⁺₁ (Γ⁺⁺ /⁺ wk₁ ↑⁺₁ Γ⁺)                           ]  ≡⟨ /⊢-cong (var-/⊢-wk-↑⁺-↑⁺ Γ⁺ Γ⁺⁺ x) P.refl ⟩
           [ var₂ · (lift (lift weaken∋ Γ⁺) Γ⁺⁺ · x) /⊢
               wk₁ ↑⁺₁ (Γ⁺⁺ /⁺ wk₁ ↑⁺₁ Γ⁺)                           ]  ≡⟨ var-/⊢-wk-↑⁺ (Γ⁺⁺ /⁺ wk₁ ↑⁺₁ Γ⁺)
                                                                                (lift (lift weaken∋ Γ⁺) Γ⁺⁺ · x) ⟩
           [ var₂ · (lift weaken∋ (Γ⁺⁺ /⁺ wk₁ ↑⁺₁ Γ⁺) ·
                       (lift (lift weaken∋ Γ⁺) Γ⁺⁺ · x))             ]  ≡⟨ Simple.var-cong simple₂
                                                                             (lift-weaken∋-lift-lift-weaken∋ σ Γ⁺ τ Γ⁺⁺ x) ⟩
           [ var₂ · (lift (lift weaken∋ (Γ⁺ ▻ τ)) (Γ⁺⁺ /⁺ wk₁) ·
                       (lift weaken∋ Γ⁺⁺ · x))                       ]  ≡⟨ P.sym $ var-/⊢-wk-↑⁺-↑⁺ (Γ⁺ ▻ τ) (Γ⁺⁺ /⁺ wk₁)
                                                                                (lift weaken∋ Γ⁺⁺ · x) ⟩
           [ var₂ · (lift weaken∋ Γ⁺⁺ · x) /⊢
               wk₁[ σ ] ↑⁺₁ (Γ⁺ ▻ τ) ↑⁺₁ (Γ⁺⁺ /⁺ wk₁)                ]  ≡⟨ P.sym $ /⊢-cong (var-/⊢-wk-↑⁺ Γ⁺⁺ x) P.refl ⟩
           [ var₂ · x /⊢ wk₁ ↑⁺₁ Γ⁺⁺ /⊢
               wk₁[ σ ] ↑⁺₁ (Γ⁺ ▻ τ) ↑⁺₁ (Γ⁺⁺ /⁺ wk₁)                ]  ≡⟨ P.sym $ /⊢⋆-ε-▻-▻-↑⁺⋆ Γ⁺⁺ (var₂ · x) wk₁
                                                                                (wk₁[ σ ] ↑⁺₁ (Γ⁺ ▻ τ)) ⟩
           [ var₂ · x /⊢⋆ (ε ▻ wk₁ ▻ wk₁[ σ ] ↑⁺₁ (Γ⁺ ▻ τ)) ↑⁺⋆₁ Γ⁺⁺ ]  ∎)
        ε t

      -- Another lemma used in the proof of /⊢-/⊢-wk.

      var-/⊢-↑⁺-/⊢-wk-↑⁺ :
        ∀ {Γ Δ} σ {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T₁ ρ̂) Γ⁺ {υ} (x : Γ ++⁺ Γ⁺ ∋ υ) →
        var₂ · x /⊢ ρ ↑⁺₁ Γ⁺ /⊢ wk₁[ σ / ρ ] ↑⁺₁ (Γ⁺ /⁺ ρ) ≅-⊢₂
        var₂ · (lift weaken∋[ σ ] Γ⁺ · x) /⊢ ρ ↑₁ ↑⁺₁ (Γ⁺ /⁺ wk₁)
      var-/⊢-↑⁺-/⊢-wk-↑⁺ σ ρ ε        x    = P.sym $ var-suc-/⊢-↑ σ x ρ
      var-/⊢-↑⁺-/⊢-wk-↑⁺ σ ρ (Γ⁺ ▻ τ) zero = begin
        [ var₂ · zero /⊢ ρ ↑⁺₁ (Γ⁺ ▻ τ) /⊢ wk₁ ↑⁺₁ ((Γ⁺ ▻ τ) /⁺ ρ) ]  ≡⟨ /⊢-cong (zero-/⊢-↑ τ (ρ ↑⁺₁ Γ⁺))
                                                                                (P.refl {x = [ wk₁ ↑⁺₁ ((Γ⁺ ▻ τ) /⁺ ρ) ]}) ⟩
        [ var₂ · zero /⊢ wk₁ ↑⁺₁ ((Γ⁺ ▻ τ) /⁺ ρ)                   ]  ≡⟨ zero-/⊢-↑ (τ / ρ ↑⁺₁ Γ⁺) (wk₁ ↑⁺₁ (Γ⁺ /⁺ ρ)) ⟩
        [ var₂ · zero                                              ]  ≡⟨ Simple.var-cong simple₂
                                                                           (zero-cong (/̂-↑̂⁺-/̂-ŵk-↑̂⁺ σ ⟦ ρ ⟧⇨ Γ⁺ τ)) ⟩
        [ var₂ · zero                                              ]  ≡⟨ P.sym $ zero-/⊢-↑ (τ / wk₁ ↑⁺₁ Γ⁺)
                                                                                (ρ ↑₁ σ ↑⁺₁ (Γ⁺ /⁺ wk₁)) ⟩
        [ var₂ · zero /⊢ ρ ↑₁ σ ↑⁺₁ ((Γ⁺ ▻ τ) /⁺ wk₁)              ]  ∎
      var-/⊢-↑⁺-/⊢-wk-↑⁺ σ ρ (Γ⁺ ▻ τ) (suc x) = begin
        [ var₂ · suc x /⊢ ρ ↑⁺₁ (Γ⁺ ▻ τ) /⊢ wk₁ ↑⁺₁ ((Γ⁺ ▻ τ) /⁺ ρ) ]  ≡⟨ /⊢-cong (var-suc-/⊢-↑ τ x (ρ ↑⁺₁ Γ⁺))
                                                                                (P.refl {x = [ wk₁ ↑⁺₁ ((Γ⁺ ▻ τ) /⁺ ρ) ]}) ⟩
        [ var₂ · x /⊢ ρ ↑⁺₁ Γ⁺ /⊢ wk₁ /⊢ wk₁ ↑⁺₁ ((Γ⁺ ▻ τ) /⁺ ρ)    ]  ≡⟨ P.sym $ /⊢-wk-↑⁺-/⊢-wk (σ / ρ) (Γ⁺ /⁺ ρ) (τ / ρ ↑⁺₁ Γ⁺)
                                                                                (var₂ · x /⊢ ρ ↑⁺₁ Γ⁺) ⟩
        [ var₂ · x /⊢ ρ ↑⁺₁ Γ⁺ /⊢ wk₁[ σ / ρ ] ↑⁺₁ (Γ⁺ /⁺ ρ)
            /⊢ wk₁[ τ / ρ ↑⁺₁ Γ⁺ / wk₁ ↑⁺₁ (Γ⁺ /⁺ ρ) ]              ]  ≡⟨ /⊢-cong
                                                                            (var-/⊢-↑⁺-/⊢-wk-↑⁺ σ ρ Γ⁺ x)
                                                                            (Simple.wk-cong simple₁ (/̂-↑̂⁺-/̂-ŵk-↑̂⁺ σ ⟦ ρ ⟧⇨ Γ⁺ τ)) ⟩
        [ var₂ · (lift weaken∋[ σ ] Γ⁺ · x) /⊢
            ρ ↑₁ ↑⁺₁ (Γ⁺ /⁺ wk₁) /⊢ wk₁                             ]  ≡⟨ P.sym $ var-suc-/⊢-↑ (τ / wk₁ ↑⁺₁ Γ⁺)
                                                                                (lift weaken∋[ σ ] Γ⁺ · x)
                                                                                (ρ ↑₁ ↑⁺₁ (Γ⁺ /⁺ wk₁)) ⟩
        [ var₂ · suc (lift weaken∋[ σ ] Γ⁺ · x) /⊢
            ρ ↑₁ ↑⁺₁ ((Γ⁺ ▻ τ) /⁺ wk₁)                              ]  ∎

    -- The wk substitution commutes (modulo lifting etc.) with any
    -- other.

    /⊢-/⊢-wk : ∀ {Γ Δ} σ {τ} {ρ̂ : Γ ⇨̂ Δ} (t : Γ ⊢₂ τ) (ρ : Sub T₁ ρ̂) →
               t /⊢ ρ /⊢ wk₁[ σ / ρ ] ≅-⊢₂ t /⊢ wk₁[ σ ] /⊢ ρ ↑₁
    /⊢-/⊢-wk σ t ρ = var-/⊢⋆-↑⁺⋆-⇒-/⊢⋆-↑⁺⋆
      (ε ▻ ρ ▻ wk₁)
      (ε ▻ wk₁[ σ ] ▻ ρ ↑₁)
      (λ Γ⁺ x → begin
         [ var₂ · x /⊢⋆ (ε ▻ ρ ▻ wk₁) ↑⁺⋆₁ Γ⁺                        ]  ≡⟨ /⊢⋆-ε-▻-▻-↑⁺⋆ Γ⁺ (var₂ · x) ρ wk₁ ⟩
         [ var₂ · x /⊢ ρ ↑⁺₁ Γ⁺ /⊢ wk₁ ↑⁺₁ (Γ⁺ /⁺ ρ)                 ]  ≡⟨ var-/⊢-↑⁺-/⊢-wk-↑⁺ σ ρ Γ⁺ x ⟩
         [ var₂ · (lift weaken∋[ σ ] Γ⁺ · x) /⊢ ρ ↑₁ ↑⁺₁ (Γ⁺ /⁺ wk₁) ]  ≡⟨ /⊢-cong (P.sym $ var-/⊢-wk-↑⁺ {σ = σ} Γ⁺ x)
                                                                                (P.refl {x = [ ρ ↑₁ ↑⁺₁ (Γ⁺ /⁺ wk₁) ]}) ⟩
         [ var₂ · x /⊢ wk₁[ σ ] ↑⁺₁ Γ⁺ /⊢ ρ ↑₁ ↑⁺₁ (Γ⁺ /⁺ wk₁)       ]  ≡⟨ P.sym $ /⊢⋆-ε-▻-▻-↑⁺⋆ Γ⁺ (var₂ · x) wk₁[ σ ] (ρ ↑₁) ⟩
         [ var₂ · x /⊢⋆ (ε ▻ wk₁[ σ ] ▻ ρ ↑₁) ↑⁺⋆₁ Γ⁺                ]  ∎) ε t

  open Application₂₁ application₂₁ public

max_stars_repo_name: nad/dependently-typed-syntax

max_issues_repo_name: nad/dependently-typed-syntax

max_forks_repo_name: nad/dependently-typed-syntax


text:
module OverloadedConInParamModule where

data A : Set where

module M (X : Set) where
  data B : Set where
    c : B

  data C : Set where
    c : C

open M A

f : B
f = c


text:
-- Copyright:  (c) 2016 Ertugrul Söylemez
-- License:    BSD3
-- Maintainer: Ertugrul Söylemez <esz@posteo.de>

module Data.Mod where

open import Core
open import Data.Int.Core hiding (module Props)
import Data.Int.Core as ℤ
open import Data.Nat.Core using (ℕ)
import Data.Nat.Core as ℕ

private module ℤP = ℤ.Props

ModEq : ℕ → Equiv ℤ
ModEq n =
  record {
    _≈_ = _≈_;
    refl = λ {x} → 0 , ℤP.+-right-inv x;
    sym = λ {x} {y} → sym' x y;
    trans = λ {x} {y} {z} → trans' x y z
  }

  where
  infix 4 _≈_

  _≈_ : ℤ → ℤ → Set
  x ≈ y = ∃ (λ k → x - y ≡ k * pos n)

  sym' : ∀ x y → x ≈ y → y ≈ x
  sym' x y (k , p) =
    neg k ,
    (begin
      y - x           || sym (ℤP.neg-flip x y) ::
      neg (x - y)     || cong neg p ::
      neg (k * pos n) || sym (ℤP.*-assoc -1 k (pos n)) ::
      neg k * pos n
    qed)

    where
    open Equiv (PropEq ℤ)

  trans' : ∀ x y z → x ≈ y → y ≈ z → x ≈ z
  trans' x y z (k1 , p1) (k2 , p2) =
    k1 + k2 ,
    (begin
      x - z                   || cong (x +_) (sym (ℤP.+-left-id (neg z))) ::
      x + (0 - z)             || cong (λ a → x + (a - z)) (sym (ℤP.+-left-inv y)) ::
      x + (neg y + y - z)     || cong (x +_) (ℤP.+-assoc (neg y) y (neg z)) ::
      x + (neg y + (y - z))   || sym (ℤP.+-assoc x (neg y) (y + neg z)) ::
      x + neg y + (y - z)     || cong2 _+_ p1 p2 ::
      k1 * pos n + k2 * pos n || sym (ℤP.*-+-right-dist k1 k2 (pos n)) ::
      (k1 + k2) * pos n
    qed)

    where
    open Equiv (PropEq ℤ)

module Props (n : ℕ) where
  open Equiv (ModEq n) using (_≈_)
  open Equiv (PropEq ℤ) hiding (_≈_)

  +-cong : ∀ {x1 x2 y1 y2} → x1 ≈ x2 → y1 ≈ y2 → x1 + y1 ≈ x2 + y2
  +-cong {x1} {x2} {y1} {y2} (k1 , p1) (k2 , p2) =
    k1 + k2 ,
    (begin
      x1 + y1 - (x2 + y2)   || ℤP.+-assoc x1 y1 _ ::
      x1 + (y1 - (x2 + y2)) ||
      cong (x1 +_) (
        y1 - (x2 + y2)         || cong (y1 +_) (ℤP.*-+-left-dist -1 x2 y2) ::
        y1 + (neg x2 + neg y2) || sym (ℤP.+-assoc y1 (neg x2) (neg y2)) ::
        (y1 + neg x2 + neg y2) || cong (_+ neg y2) (ℤP.+-comm y1 (neg x2)) ::
        neg x2 + y1 + neg y2   || ℤP.+-assoc (neg x2) y1 _ ::
        neg x2 + (y1 + neg y2)
      qed) ::
      x1 + (neg x2 + (y1 + neg y2)) || sym (ℤP.+-assoc x1 (neg x2) _) ::
      x1 - x2 + (y1 - y2)           || cong2 _+_ p1 p2 ::
      k1 * pos n + k2 * pos n       || sym (ℤP.*-+-right-dist k1 k2 (pos n)) ::
      (k1 + k2) * pos n
    qed)

max_stars_repo_name: esoeylemez/agda-simple

max_issues_repo_name: esoeylemez/agda-simple

max_forks_repo_name: esoeylemez/agda-simple


text:
module L.Base.Sigma where

-- Reexport definitions
open import L.Base.Sigma.Core public

max_stars_repo_name: borszag/smallib

max_issues_repo_name: borszag/smallib

max_forks_repo_name: borszag/smallib