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

open import HoTT
open import cohomology.FunctionOver

module cohomology.TwoPushouts where

--        g     h
--     B --> C --> D    K = A ⊔^B C / (f,g)        d₁ = A <- B -> C
--    f|     |     |    L = K ⊔^C D / (left,h)     d₂ = K <- C -> D
--     v     v     v                               d  = A <- B -> D
--     A --> K --> L
--
module TwoPushoutsEquiv {i j k l} {A : Type i} {B : Type j} {C : Type k}
  {D : Type l} (f : B → A) (g : B → C) (h : C → D) where

  private
    d₁ : Span
    d₁ = span A C B f g

    d₂ : Span
    d₂ = span (Pushout d₁) D C right h

    d : Span
    d = span A D B f (h ∘ g)

  module Inner = PushoutRec {d = d₁} {D = Pushout d}
    left
    (right ∘ h)
    glue

  module Into = PushoutRec {d = d} {D = Pushout d₂}
    (left ∘ left)
    right
    (λ b → ap left (glue b) ∙ glue (g b))

  into : Pushout d -> Pushout d₂
  into = Into.f

  module Out = PushoutRec {d = d₂} {D = Pushout d}
    Inner.f
    right
    (λ _ → idp)

  out : Pushout d₂ → Pushout d
  out = Out.f

  private
    square-extend-tr : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ b : A}
      {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
      {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁} (q : a₁₀ == b)
      → Square p₀₋ p₋₀ p₋₁ p₁₋
      → Square p₀₋ (p₋₀ ∙ q) p₋₁ (! q ∙' p₁₋)
    square-extend-tr idp ids = ids

    square-corner-bl : ∀ {i} {A : Type i} {a₀ a₁ : A} (q : a₀ == a₁)
      → Square (! q) idp q idp
    square-corner-bl idp = ids

  into-inner : (k : Pushout d₁) → into (Inner.f k) == left k
  into-inner = Pushout-elim
    (λ a → idp)
    (λ c → ! (glue c))
    (λ b → ↓-='-from-square $
      (ap-∘ into Inner.f (glue b)
       ∙ ap (ap into) (Inner.glue-β b) ∙ Into.glue-β b)
      ∙v⊡ square-extend-tr (glue (g b)) vid-square)

  abstract
    into-out : (l : Pushout d₂) → into (out l) == l
    into-out = Pushout-elim
      into-inner
      (λ d → idp)
      (λ c → ↓-∘=idf-from-square into out $
        ap (ap into) (Out.glue-β c) ∙v⊡ square-corner-bl (glue c))

    out-into : (l : Pushout d) → out (into l) == l
    out-into = Pushout-elim
      (λ a → idp)
      (λ d → idp)
      (λ b → ↓-∘=idf-from-square out into $ vert-degen-square $
        ap out (ap into (glue b))
          =⟨ ap (ap out) (Into.glue-β b) ⟩
        ap out (ap left (glue b) ∙ glue (g b))
          =⟨ ap-∙ out (ap left (glue b)) (glue (g b)) ⟩
        ap out (ap left (glue b)) ∙ ap out (glue (g b))
          =⟨ ∘-ap out left (glue b) |in-ctx (λ w → w ∙ ap out (glue (g b))) ⟩
        ap Inner.f (glue b) ∙ ap out (glue (g b))
          =⟨ Out.glue-β (g b) |in-ctx (λ w → ap Inner.f (glue b) ∙ w) ⟩
        ap Inner.f (glue b) ∙ idp
          =⟨ ∙-unit-r _ ⟩
        ap Inner.f (glue b)
          =⟨ Inner.glue-β b ⟩
        glue b ∎)

  two-pushouts-equiv : Pushout d ≃ Pushout d₂
  two-pushouts-equiv = equiv into out into-out out-into

  two-pushouts : Lift {j = lmax l (lmax k (lmax j i))} (Pushout d) == Pushout d₂
  two-pushouts = ua (two-pushouts-equiv ∘e lift-equiv)

  two-pushouts-left : lift ∘ left == left ∘ left
                      [ (λ E → (A → E)) ↓ two-pushouts ]
  two-pushouts-left = codomain-over-equiv _ _

  two-pushouts-right : lift ∘ right == right [ (λ E → (D → E)) ↓ two-pushouts ]
  two-pushouts-right = codomain-over-equiv _ _

  two-pushouts-inner : lift ∘ Inner.f == left
                       [ (λ E → (Pushout d₁ → E)) ↓ two-pushouts ]
  two-pushouts-inner = codomain-over-equiv _ _ ▹ λ= into-inner

--        g     h
--     Y --> Z --> W    K = X ⊔^Y Y / (f,g)        ps₁ = X <- Y -> Z
--    f|     |     |    L = Z ⊔^Z W / (left,h)     ps₂ = K <- Z -> W
--     v     v     v                               ps = X <- Y -> W
--     X --> K --> L
--
module TwoPushoutsPtd {i j k l} {X : Ptd i} {Y : Ptd j} {Z : Ptd k} {W : Ptd l}
  (f : fst (Y ⊙→ X)) (g : fst (Y ⊙→ Z)) (h : fst (Z ⊙→ W)) where

  private
    ps₁ = ⊙span X Z Y f g
    ps₂ = ⊙span (⊙Pushout ps₁) W Z (⊙right ps₁) h
    ps = ⊙span X W Y f (h ⊙∘ g)

  open TwoPushoutsEquiv (fst f) (fst g) (fst h) public

  two-pushouts-ptd :
    ⊙Lift {j = lmax l (lmax k (lmax j i))} (⊙Pushout ps)
    == ⊙Pushout ps₂
  two-pushouts-ptd = ⊙ua (two-pushouts-equiv ∘e lift-equiv) idp

  two-pushouts-⊙left :
    ⊙lift ⊙∘ ⊙left ps == ⊙left ps₂ ⊙∘ ⊙left ps₁
    [ (λ V → fst (X ⊙→ V)) ↓ two-pushouts-ptd ]
  two-pushouts-⊙left = codomain-over-⊙equiv _ _ _

  two-pushouts-⊙right :
    ⊙lift ⊙∘ ⊙right ps == ⊙right ps₂
    [ (λ V → fst (W ⊙→ V)) ↓ two-pushouts-ptd ]
  two-pushouts-⊙right =
    codomain-over-⊙equiv _ _ _ ▹ pair= idp (lemma f g h)
    where
    lemma : {X : Ptd i} {Y : Ptd j} {Z : Ptd k} {W : Ptd l}
      (f : fst (Y ⊙→ X)) (g : fst (Y ⊙→ Z)) (h : fst (Z ⊙→ W))
      → ap (TwoPushoutsEquiv.into (fst f) (fst g) (fst h)
               ∘ lower {j = lmax l (lmax k (lmax j i))})
              (snd (⊙lift ⊙∘ ⊙right (⊙span X W Y f (h ⊙∘ g))))
        ∙ idp
        ==  ap right (! (snd h)) ∙ ! (glue (snd Z))
            ∙' ap left (snd (⊙right (⊙span X Z Y f g)))
    lemma {Y = Y} (f , idp) (g , idp) (h , idp) =
      ap (2P.into ∘ lower) (ap lift (! (glue (snd Y))) ∙ idp) ∙ idp
        =⟨ ∙-unit-r _ ⟩
      ap (2P.into ∘ lower) (ap lift (! (glue (snd Y))) ∙ idp)
        =⟨ ∙-unit-r _ |in-ctx (ap (2P.into ∘ lower)) ⟩
      ap (2P.into ∘ lower) (ap lift (! (glue (snd Y))))
        =⟨ ∘-ap (2P.into ∘ lower) lift _ ⟩
      ap 2P.into (! (glue (snd Y)))
        =⟨ ap-! 2P.into (glue (snd Y)) ⟩
      ! (ap 2P.into (glue (snd Y)))
        =⟨ 2P.Into.glue-β (snd Y) |in-ctx ! ⟩
      ! (ap left (glue (snd Y)) ∙ glue (g (snd Y)))
        =⟨ !-∙ (ap left (glue (snd Y))) (glue (g (snd Y))) ⟩
      ! (glue (g (snd Y))) ∙ ! (ap left (glue (snd Y)))
        =⟨ !-ap left (glue (snd Y)) |in-ctx (λ w → ! (glue (g (snd Y))) ∙ w) ⟩
      ! (glue (g (snd Y))) ∙ ap left (! (glue (snd Y)))
        =⟨ ∙=∙' (! (glue (g (snd Y)))) (ap left (! (glue (snd Y)))) ⟩
      ! (glue (g (snd Y))) ∙' ap left (! (glue (snd Y))) ∎
      where
      module 2P = TwoPushoutsEquiv f g h

  two-pushouts-⊙inner : ⊙lift ⊙∘ (Inner.f , idp) == ⊙left ps₂
    [ (λ V → fst (⊙Pushout ps₁ ⊙→ V)) ↓ two-pushouts-ptd ]
  two-pushouts-⊙inner =
    codomain-over-⊙equiv _ _ _ ▹ ⊙λ= into-inner idp

open TwoPushoutsEquiv
  using (two-pushouts-equiv; two-pushouts; two-pushouts-left;
         two-pushouts-right; two-pushouts-inner)

open TwoPushoutsPtd
  using (two-pushouts-ptd; two-pushouts-⊙left; two-pushouts-⊙right;
         two-pushouts-⊙inner)

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
data Foo : Set where
  foo = Foo

-- Bad error message WAS:
-- A postulate block can only contain type signatures or instance blocks

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module Definition.Typed.EqualityRelation where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Weakening using (_∷_⊆_)

-- Generic equality relation used with the logical relation

record EqRelSet : Set₁ where
  constructor eqRel
  field
    ---------------
    -- Relations --
    ---------------

    -- Equality of types
    _⊢_≅_   : Con Term → (A B : Term)   → Set

    -- Equality of terms
    _⊢_≅_∷_ : Con Term → (t u A : Term) → Set

    -- Equality of neutral terms
    _⊢_~_∷_ : Con Term → (t u A : Term) → Set

    ----------------
    -- Properties --
    ----------------

    -- Generic equality compatibility
    ~-to-≅ₜ : ∀ {k l A Γ}
            → Γ ⊢ k ~ l ∷ A
            → Γ ⊢ k ≅ l ∷ A

    -- Judgmental conversion compatibility
    ≅-eq  : ∀ {A B Γ}
          → Γ ⊢ A ≅ B
          → Γ ⊢ A ≡ B
    ≅ₜ-eq : ∀ {t u A Γ}
          → Γ ⊢ t ≅ u ∷ A
          → Γ ⊢ t ≡ u ∷ A

    -- Universe
    ≅-univ : ∀ {A B Γ}
           → Γ ⊢ A ≅ B ∷ U
           → Γ ⊢ A ≅ B

    -- Symmetry
    ≅-sym  : ∀ {A B Γ}   → Γ ⊢ A ≅ B     → Γ ⊢ B ≅ A
    ≅ₜ-sym : ∀ {t u A Γ} → Γ ⊢ t ≅ u ∷ A → Γ ⊢ u ≅ t ∷ A
    ~-sym  : ∀ {k l A Γ} → Γ ⊢ k ~ l ∷ A → Γ ⊢ l ~ k ∷ A

    -- Transitivity
    ≅-trans  : ∀ {A B C Γ}   → Γ ⊢ A ≅ B     → Γ ⊢ B ≅ C     → Γ ⊢ A ≅ C
    ≅ₜ-trans : ∀ {t u v A Γ} → Γ ⊢ t ≅ u ∷ A → Γ ⊢ u ≅ v ∷ A → Γ ⊢ t ≅ v ∷ A
    ~-trans  : ∀ {k l m A Γ} → Γ ⊢ k ~ l ∷ A → Γ ⊢ l ~ m ∷ A → Γ ⊢ k ~ m ∷ A

    -- Conversion
    ≅-conv : ∀ {t u A B Γ} → Γ ⊢ t ≅ u ∷ A → Γ ⊢ A ≡ B → Γ ⊢ t ≅ u ∷ B
    ~-conv : ∀ {k l A B Γ} → Γ ⊢ k ~ l ∷ A → Γ ⊢ A ≡ B → Γ ⊢ k ~ l ∷ B

    -- Weakening
    ≅-wk  : ∀ {A B ρ Γ Δ}
          → ρ ∷ Δ ⊆ Γ
          → ⊢ Δ
          → Γ ⊢ A ≅ B
          → Δ ⊢ wk ρ A ≅ wk ρ B
    ≅ₜ-wk : ∀ {t u A ρ Γ Δ}
          → ρ ∷ Δ ⊆ Γ
          → ⊢ Δ
          → Γ ⊢ t ≅ u ∷ A
          → Δ ⊢ wk ρ t ≅ wk ρ u ∷ wk ρ A
    ~-wk  : ∀ {k l A ρ Γ Δ}
          → ρ ∷ Δ ⊆ Γ
          → ⊢ Δ
          → Γ ⊢ k ~ l ∷ A
          → Δ ⊢ wk ρ k ~ wk ρ l ∷ wk ρ A

    -- Weak head expansion
    ≅-red : ∀ {A A′ B B′ Γ}
          → Γ ⊢ A ⇒* A′
          → Γ ⊢ B ⇒* B′
          → Whnf A′
          → Whnf B′
          → Γ ⊢ A′ ≅ B′
          → Γ ⊢ A  ≅ B

    ≅ₜ-red : ∀ {a a′ b b′ A B Γ}
           → Γ ⊢ A ⇒* B
           → Γ ⊢ a ⇒* a′ ∷ B
           → Γ ⊢ b ⇒* b′ ∷ B
           → Whnf B
           → Whnf a′
           → Whnf b′
           → Γ ⊢ a′ ≅ b′ ∷ B
           → Γ ⊢ a  ≅ b  ∷ A

    -- Universe type reflexivity
    ≅-Urefl   : ∀ {Γ} → ⊢ Γ → Γ ⊢ U ≅ U

    -- Natural number type reflexivity
    ≅-ℕrefl   : ∀ {Γ} → ⊢ Γ → Γ ⊢ ℕ ≅ ℕ
    ≅ₜ-ℕrefl  : ∀ {Γ} → ⊢ Γ → Γ ⊢ ℕ ≅ ℕ ∷ U

    -- Empty type reflexivity
    ≅-Emptyrefl   : ∀ {Γ} → ⊢ Γ → Γ ⊢ Empty ≅ Empty
    ≅ₜ-Emptyrefl  : ∀ {Γ} → ⊢ Γ → Γ ⊢ Empty ≅ Empty ∷ U

    -- Unit type reflexivity
    ≅-Unitrefl : ∀ {Γ} → ⊢ Γ → Γ ⊢ Unit ≅ Unit
    ≅ₜ-Unitrefl  : ∀ {Γ} → ⊢ Γ → Γ ⊢ Unit ≅ Unit ∷ U

    -- Unit η-equality
    ≅ₜ-η-unit : ∀ {Γ e e'}
             → Γ ⊢ e ∷ Unit
             → Γ ⊢ e' ∷ Unit
             → Γ ⊢ e ≅ e' ∷ Unit

    -- Π-congruence

    ≅-Π-cong  : ∀ {F G H E Γ}
              → Γ ⊢ F
              → Γ ⊢ F ≅ H
              → Γ ∙ F ⊢ G ≅ E
              → Γ ⊢ Π F ▹ G ≅ Π H ▹ E

    ≅ₜ-Π-cong : ∀ {F G H E Γ}
              → Γ ⊢ F
              → Γ ⊢ F ≅ H ∷ U
              → Γ ∙ F ⊢ G ≅ E ∷ U
              → Γ ⊢ Π F ▹ G ≅ Π H ▹ E ∷ U

    -- Σ-congruence

    ≅-Σ-cong  : ∀ {F G H E Γ}
              → Γ ⊢ F
              → Γ ⊢ F ≅ H
              → Γ ∙ F ⊢ G ≅ E
              → Γ ⊢ Σ F ▹ G ≅ Σ H ▹ E

    ≅ₜ-Σ-cong : ∀ {F G H E Γ}
              → Γ ⊢ F
              → Γ ⊢ F ≅ H ∷ U
              → Γ ∙ F ⊢ G ≅ E ∷ U
              → Γ ⊢ Σ F ▹ G ≅ Σ H ▹ E ∷ U

    -- Zero reflexivity
    ≅ₜ-zerorefl : ∀ {Γ} → ⊢ Γ → Γ ⊢ zero ≅ zero ∷ ℕ

    -- Successor congruence
    ≅-suc-cong : ∀ {m n Γ} → Γ ⊢ m ≅ n ∷ ℕ → Γ ⊢ suc m ≅ suc n ∷ ℕ

    -- η-equality
    ≅-η-eq : ∀ {f g F G Γ}
           → Γ ⊢ F
           → Γ ⊢ f ∷ Π F ▹ G
           → Γ ⊢ g ∷ Π F ▹ G
           → Function f
           → Function g
           → Γ ∙ F ⊢ wk1 f ∘ var 0 ≅ wk1 g ∘ var 0 ∷ G
           → Γ ⊢ f ≅ g ∷ Π F ▹ G

    -- η for product types
    ≅-Σ-η : ∀ {p r F G Γ}
          → Γ ⊢ F
          → Γ ∙ F ⊢ G
          → Γ ⊢ p ∷ Σ F ▹ G
          → Γ ⊢ r ∷ Σ F ▹ G
          → Product p
          → Product r
          → Γ ⊢ fst p ≅ fst r ∷ F
          → Γ ⊢ snd p ≅ snd r ∷ G [ fst p ]
          → Γ ⊢ p ≅ r ∷ Σ F ▹ G

    -- Variable reflexivity
    ~-var : ∀ {x A Γ} → Γ ⊢ var x ∷ A → Γ ⊢ var x ~ var x ∷ A

    -- Application congruence
    ~-app : ∀ {a b f g F G Γ}
          → Γ ⊢ f ~ g ∷ Π F ▹ G
          → Γ ⊢ a ≅ b ∷ F
          → Γ ⊢ f ∘ a ~ g ∘ b ∷ G [ a ]

    -- Product projections congruence
    ~-fst : ∀ {p r F G Γ}
          → Γ ⊢ F
          → Γ ∙ F ⊢ G
          → Γ ⊢ p ~ r ∷ Σ F ▹ G
          → Γ ⊢ fst p ~ fst r ∷ F

    ~-snd : ∀ {p r F G Γ}
          → Γ ⊢ F
          → Γ ∙ F ⊢ G
          → Γ ⊢ p ~ r ∷ Σ F ▹ G
          → Γ ⊢ snd p ~ snd r ∷ G [ fst p ]

    -- Natural recursion congruence
    ~-natrec : ∀ {z z′ s s′ n n′ F F′ Γ}
             → Γ ∙ ℕ ⊢ F ≅ F′
             → Γ     ⊢ z ≅ z′ ∷ F [ zero ]
             → Γ     ⊢ s ≅ s′ ∷ Π ℕ ▹ (F ▹▹ F [ suc (var 0) ]↑)
             → Γ     ⊢ n ~ n′ ∷ ℕ
             → Γ     ⊢ natrec F z s n ~ natrec F′ z′ s′ n′ ∷ F [ n ]

    -- Empty recursion congruence
    ~-Emptyrec : ∀ {n n′ F F′ Γ}
               → Γ ⊢ F ≅ F′
               → Γ ⊢ n ~ n′ ∷ Empty
               → Γ ⊢ Emptyrec F n ~ Emptyrec F′ n′ ∷ F

  -- Star reflexivity
  ≅ₜ-starrefl : ∀ {Γ} → ⊢ Γ → Γ ⊢ star ≅ star ∷ Unit
  ≅ₜ-starrefl [Γ] = ≅ₜ-η-unit (starⱼ [Γ]) (starⱼ [Γ])

  -- Composition of universe and generic equality compatibility
  ~-to-≅ : ∀ {k l Γ} → Γ ⊢ k ~ l ∷ U → Γ ⊢ k ≅ l
  ~-to-≅ k~l = ≅-univ (~-to-≅ₜ k~l)

  ≅-W-cong : ∀ {F G H E Γ} W
          → Γ ⊢ F
          → Γ ⊢ F ≅ H
          → Γ ∙ F ⊢ G ≅ E
          → Γ ⊢ ⟦ W ⟧ F ▹ G ≅ ⟦ W ⟧ H ▹ E
  ≅-W-cong BΠ = ≅-Π-cong
  ≅-W-cong BΣ = ≅-Σ-cong

  ≅ₜ-W-cong : ∀ {F G H E Γ} W
            → Γ ⊢ F
            → Γ ⊢ F ≅ H ∷ U
            → Γ ∙ F ⊢ G ≅ E ∷ U
            → Γ ⊢ ⟦ W ⟧ F ▹ G ≅ ⟦ W ⟧ H ▹ E ∷ U
  ≅ₜ-W-cong BΠ = ≅ₜ-Π-cong
  ≅ₜ-W-cong BΣ = ≅ₜ-Σ-cong


text:
module Oscar.Category.Morphism where

open import Oscar.Category.Setoid
open import Oscar.Level
open import Oscar.Property
open import Oscar.Data.Nat

record Morphism
  {𝔬} (⋆ : Set 𝔬) 𝔪 𝔮
  : Set (𝔬 ⊔ lsuc (𝔪 ⊔ 𝔮))
  where
  constructor #_

  field
    _⇒_ : ⋆ → ⋆ → Setoid 𝔪 𝔮

  _↦_ : ⋆ → ⋆ → Set 𝔪
  _↦_ x y = Setoid.⋆ (x ⇒ y)

  infix 4 _≞_
  _≞_ : ∀ {x y} → x ↦ y → x ↦ y → Set 𝔮
  _≞_ {x} {y} = Setoid._≋_ (x ⇒ y)

  instance IsSetoid↦ : ∀ {x y} → IsSetoid (_≞_ {x} {y})
  IsSetoid↦ {x} {y} = Setoid.isSetoid (x ⇒ y)

  -- IsSetoid↦ : ∀ {x y} → IsSetoid (x ↦ y) 𝔮
  -- IsSetoid↦ {x} {y} = Setoid.isSetoid (x ⇒ y)

  --   ⦃ isMorphism ⦄ : IsMorphism (λ {x} {y} → _≞_ {x} {y})

-- record Morphism 𝔬 𝔪 𝔮 : Set (lsuc (𝔬 ⊔ 𝔪 ⊔ 𝔮)) where
--   constructor ↑_
--   infix 4 _≞_
--   field
--     {⋆} : Set 𝔬
--     {_↦_} : ⋆ → ⋆ → Set 𝔪
--     _≞_ : ∀ {x y} → x ↦ y → x ↦ y → Set 𝔮
--     ⦃ isSetoid ⦄ : ∀ {x} {y} → IsSetoid (_≞_ {x} {y})

--   instance IsSetoid↦ : ∀ {x y} → IsSetoid (_≞_ {x} {y})
--   IsSetoid↦ {x} {y} = Setoid.isSetoid (x ⇒ y)

--   setoid : ∀ {x y} → Setoid 𝔪 𝔮
--   setoid {x} {y} = ↑ _≞_ {x} {y}


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Group.Exact where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.HITs.PropositionalTruncation renaming (rec to pRec)
open import Cubical.Algebra.Group.GroupPath

open import Cubical.Algebra.Group.Instances.Unit

-- TODO : Define exact sequences
-- (perhaps short, finite, ℕ-indexed and ℤ-indexed)

SES→isEquiv : ∀ {ℓ ℓ'} {L R : Group ℓ-zero}
  → {G : Group ℓ} {H : Group ℓ'}
  → Unit ≡ L
  → Unit ≡ R
  → (lhom : GroupHom L G) (midhom : GroupHom G H) (rhom : GroupHom H R)
  → ((x : _) → isInKer midhom x → isInIm lhom x)
  → ((x : _) → isInKer rhom x → isInIm midhom x)
  → isEquiv (fst midhom)
SES→isEquiv {R = R} {G = G} {H = H} =
  J (λ L _ → Unit ≡ R →
      (lhom : GroupHom L G) (midhom : GroupHom G H)
      (rhom : GroupHom H R) →
      ((x : fst G) → isInKer midhom x → isInIm lhom x) →
      ((x : fst H) → isInKer rhom x → isInIm midhom x) →
      isEquiv (fst midhom))
      ((J (λ R _ → (lhom : GroupHom Unit G) (midhom : GroupHom G H)
                   (rhom : GroupHom H R) →
                   ((x : fst G) → isInKer midhom x → isInIm lhom x) →
                   ((x : _) → isInKer rhom x → isInIm midhom x) →
                   isEquiv (fst midhom))
         main))
  where
  main : (lhom : GroupHom Unit G) (midhom : GroupHom G H)
         (rhom : GroupHom H Unit) →
         ((x : fst G) → isInKer midhom x → isInIm lhom x) →
         ((x : fst H) → isInKer rhom x → isInIm midhom x) →
         isEquiv (fst midhom)
  main lhom midhom rhom lexact rexact =
    BijectionIsoToGroupEquiv {G = G} {H = H}
      bijIso' .fst .snd
    where
    bijIso' : BijectionIso G H
    BijectionIso.fun bijIso' = midhom
    BijectionIso.inj bijIso' x inker =
      pRec (GroupStr.is-set (snd G) _ _)
           (λ s → sym (snd s) ∙ IsGroupHom.pres1 (snd lhom))
           (lexact _ inker)
    BijectionIso.surj bijIso' x = rexact x refl

max_stars_repo_name: FernandoLarrain/cubical

max_issues_repo_name: FernandoLarrain/cubical

max_forks_repo_name: FernandoLarrain/cubical


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

module Categories.Category.Monoidal.Construction.Minus2 where

-- Any -2-Category is Monoidal.  Of course, One is Monoidal, but
-- we don't need to shrink to do this, it can be done directly.
-- The assumptions in the construction of a -2-Category are all
-- needed to make things work properly.

open import Data.Product using (proj₁; proj₂)

open import Categories.Minus2-Category
open import Categories.Category.Monoidal
import Categories.Morphism as M

-- Doing it manually is just as easy as going through Cartesian here
-2-Monoidal : ∀ {o ℓ e} → (C : -2-Category {o} {ℓ} {e}) → Monoidal (-2-Category.cat C)
-2-Monoidal C = record
  { ⊗ = record
    { F₀ = proj₁
    ; F₁ = proj₁
    ; identity = Hom-Conn
    ; homomorphism = Hom-Conn
    ; F-resp-≈ = λ _ → Hom-Conn
    }
  ; unit = proj₁ Obj-Contr
  ; unitorˡ = λ {X} → proj₂ Obj-Contr X
  ; unitorʳ = M.≅.refl cat
  ; associator = M.≅.refl cat
  ; unitorˡ-commute-from = Hom-Conn
  ; unitorˡ-commute-to = Hom-Conn
  ; unitorʳ-commute-from = Hom-Conn
  ; unitorʳ-commute-to = Hom-Conn
  ; assoc-commute-from = Hom-Conn
  ; assoc-commute-to = Hom-Conn
  ; triangle = Hom-Conn
  ; pentagon = Hom-Conn
  }
  where
    open -2-Category C

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


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

open import Base
open import Homotopy.PushoutDef

-- Suspension is defined as a particular case of pushout

module Spaces.Suspension {i} (A : Set i) where

suspension-diag : pushout-diag i
suspension-diag = diag unit , unit , A , (λ _ → tt) , (λ _ → tt)

suspension : Set i
suspension = pushout suspension-diag

north : suspension
north = left tt

south : suspension
south = right tt

paths : A → north ≡ south
paths x = glue x

suspension-rec : ∀ {j} (P : suspension → Set j) (n : P north) (s : P south)
  (p : (x : A) → transport P (paths x) n ≡ s) → ((x : suspension) → P x)
suspension-rec P n s p = pushout-rec P (λ _ → n) (λ _ → s) p

suspension-β-paths : ∀ {j} (P : suspension → Set j) (n : P north) (s : P south)
  (p : (x : A) → transport P (paths x) n ≡ s)
  → ((x : A) → apd (suspension-rec P n s p) (paths x) ≡ p x)
suspension-β-paths P n s p =
  pushout-β-glue P (λ _ → n) (λ _ → s) p

suspension-rec-nondep : ∀ {j} (C : Set j) (n s : C) (p : A → n ≡ s)
  → (suspension → C)
suspension-rec-nondep C n s p =
  pushout-rec-nondep C (λ _ → n) (λ _ → s) p

suspension-β-paths-nondep : ∀ {j} (C : Set j) (n s : C) (p : A → n ≡ s)
  → ((x : A) → ap (suspension-rec-nondep C n s p) (paths x) ≡ p x)
suspension-β-paths-nondep C n s p =
  pushout-β-glue-nondep C (λ _ → n) (λ _ → s) p


text:
{-# OPTIONS --safe #-}
module JVM.Contexts where

open import JVM.Types

open import Relation.Ternary.Construct.List.Overlapping Ty public
  renaming
    ( overlap-rel to ctx-rel
    ; overlap-commutative to ctx-commutative
    ; overlap-semigroup to ctx-semigroup
    ; overlap-monoid to ctx-monoid)


text:
{-# OPTIONS --no-qualified-instances #-}
module JVM.Printer where

open import Function
open import Data.Bool
open import Data.Product hiding (swap)
open import Data.List as L
open import Data.List.Relation.Unary.Any
open import Data.Nat as N
open import Data.Nat.Show as Nat
open import Data.Fin
open import Data.String as S
open import Relation.Unary
open import Relation.Ternary.Core
open import Relation.Ternary.Structures
open import Relation.Ternary.Structures.Syntax hiding (_∣_)

open import Relation.Binary.PropositionalEquality
open import Relation.Ternary.Monad

open import JVM.Types
open import JVM.Contexts using (indexOf)
open import JVM.Syntax.Values
open import JVM.Syntax.Instructions as I hiding (Instr)
open import JVM.Printer.Printer StackTy
open import JVM.Printer.Jasmin as J hiding (procedure)

private
  module _ {T : Set} where
    open import JVM.Model T public

const-instr : Const a → Instr
const-instr Const.null   = aconst_null
const-instr (num x)      = sipush x
const-instr (bool false) = iconst0
const-instr (bool true)  = iconst1

load-instr : Ty → ℕ → Instr
load-instr (ref _)   = aload
load-instr (array _) = iload
load-instr int     = iload
load-instr boolean = iload
load-instr byte    = iload
load-instr short   = iload
load-instr long    = iload
load-instr char    = iload

store-instr : Ty → ℕ → Instr
store-instr (ref _)   = astore
store-instr (array _) = aastore
store-instr int     = istore
store-instr boolean = istore
store-instr byte    = istore
store-instr short   = istore
store-instr long    = istore
store-instr char    = istore

bop-instr : NativeBinOp a b c → Instr
bop-instr add = iadd
bop-instr sub = isub
bop-instr mul = imul
bop-instr div = idiv
bop-instr xor = ixor

if-instr : ∀ {as} → I.Comparator as → String → Instr
if-instr eq = if eq
if-instr ne = if ne
if-instr lt = if lt
if-instr ge = if ge
if-instr gt = if gt
if-instr le = if le
if-instr icmpge = if icmpge
if-instr icmpgt = if icmpgt
if-instr icmpeq = if icmpeq
if-instr icmpne = if icmpne
if-instr icmplt = if icmplt
if-instr icmple = if icmple

module _ {𝑭} where

  prettyᵢ : ∀ {ψ₁ ψ₂} → ∀[ Down ⟨ 𝑭 ∣ ψ₁ ↝ ψ₂ ⟩ ⇒ Printer Emp ]
  prettyᵢ (↓ noop)      = print (instr nop)
  prettyᵢ (↓ pop)       = print (instr pop)
  prettyᵢ (↓ dup)       = print (instr dup)
  prettyᵢ (↓ swap)      = print (instr swap)
  prettyᵢ (↓ (push x))  = print (instr (const-instr x))
  prettyᵢ (↓ (bop x))   = print (instr (bop-instr x))
  prettyᵢ (↓ (load {a = a} r))  = do
    print (instr (load-instr a (toℕ $ index r)))
  prettyᵢ (↓ (store {a = a} r)) = do
    print (instr (store-instr a (toℕ $ index r)))
  prettyᵢ (↓ (goto x))  = do
    emp n ← lookDown (↓ x)
    print (instr (goto (Nat.show n)))
  prettyᵢ (↓ (if c x)) = do
    emp n ← lookDown (↓ x)
    print (instr (if-instr c (Nat.show n)))

  import JVM.Syntax.Bytecode.Printer ⟨ 𝑭 ∣_↝_⟩ prettyᵢ as Printer

  pretty : ∀ {ψ₁ ψ₂ Φ} → ⟪ 𝑭 ∣ ψ₁ ↝ ψ₂ ⟫ Φ → List Stat
  pretty bc = execPrinter (Printer.pretty bc)

  procedure : ∀ {ψ₁ ψ₂ Φ} → String → ⟪ 𝑭 ∣ ψ₁ ↝ ψ₂ ⟫ Φ → Jasmin
  procedure name bc = J.procedure name (L.length 𝑭) 10 (pretty bc)


text:
module Generic.Test.Data where

open import Generic.Test.Data.Fin     public
open import Generic.Test.Data.Lift    public
open import Generic.Test.Data.Product public
open import Generic.Test.Data.List    public
open import Generic.Test.Data.Maybe   public
open import Generic.Test.Data.Vec     public
open import Generic.Test.Data.W       public

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
-- binary search trees (not balanced)

open import bool
open import bool-thms2
open import eq
open import maybe
open import product
open import product-thms
open import bool-relations using (transitive ; total)

module z05-01-bst (A : Set)                    -- type of elements
                  (_≤A_ : A → A → 𝔹)           -- ordering function
                  (≤A-trans : transitive _≤A_) -- proof of transitivity of given ordering
                  (≤A-total : total      _≤A_) -- proof of totality     of given ordering
                  where
{-
IAL
- relations.agda
  - models binary relation on A as functions from A to A to Set
- bool-relations.agda
  - models binary realtion on A as functions from A to A to 𝔹

Cannot use A→A→Set relations here because code cannot manipulate types.
But code can pattern match on values of type 𝔹, so boolean relations more useful.
-}
open import bool-relations _≤A_ hiding (transitive ; total)
open import minmax _≤A_ ≤A-trans ≤A-total

-- able to store values in bounds 'l' and 'u'
--         l(ower) bound
--         |   u(upper) bound
--         v   v
data bst : A → A → Set where
  bst-leaf : ∀ {l u : A}
           → l ≤A u ≡ tt
           → bst l u
  bst-node : ∀ {l l' u' u : A}
           → (d : A)      -- value stored in this node
           → bst l' d     -- left  subtree of values ≤ stored value
           → bst d u'     -- right subtree of values ≥ stored value
           → l ≤A l' ≡ tt
           → u' ≤A u ≡ tt
           → bst l u

------------------------------------------------------------------------------
bst-search : ∀ {l u : A}
           → (d : A)                             -- find a node that is isomorphic (_=A_) to d
           → bst l u
           → maybe (Σ A (λ d' → d iso𝔹 d' ≡ tt)) -- return that node or nothing
bst-search d (bst-leaf _) = nothing -- could return proof not in tree instead
-- compare given element with stored element
bst-search d (bst-node d' L R _ _) with keep (d ≤A d')
-- compare given element with stored element (other direction)
bst-search d (bst-node d' L R _ _) | tt , p1 with keep (d' ≤A d)
-- both are true implying iso, so return that element and proof
bst-search d (bst-node d' L R _ _) | tt , p1 | tt , p2 = just (d' , iso𝔹-intro p1 p2)
-- if either is false then search the appropriate branch
bst-search d (bst-node d' L R _ _) | tt , p1 | ff , p2 = bst-search d L -- search in left
bst-search d (bst-node d' L R _ _) | ff , p1           = bst-search d R -- search in right

------------------------------------------------------------------------------
-- change the lower bound from l' to l
bst-dec-lb : ∀ {l l' u' : A}
           → bst l' u'
           → l ≤A l' ≡ tt
           → bst l u'
bst-dec-lb (bst-leaf p)           q = bst-leaf       (≤A-trans q p)
bst-dec-lb (bst-node d L R p1 p2) q = bst-node d L R (≤A-trans q p1) p2

-- change the upper bound from u' to u
bst-inc-ub : ∀ {l' u' u : A}
           → bst l' u'
           → u' ≤A u ≡ tt
           → bst l' u
bst-inc-ub (bst-leaf p)           q = bst-leaf          (≤A-trans p q)
bst-inc-ub (bst-node d L R p1 p2) q = bst-node d L R p1 (≤A-trans p2 q)

bst-insert : ∀{l u : A}
           → (d : A)                 -- insert 'd'
           → bst l u                 -- into this 'bst'
           → bst (min d l) (max d u) -- type might change
bst-insert d (bst-leaf p) =
  bst-node d (bst-leaf ≤A-refl) (bst-leaf ≤A-refl) min-≤1 max-≤1

bst-insert d (bst-node d' L R p1 p2) with keep (d ≤A d')

bst-insert d (bst-node d' L R p1 p2) | tt , p with bst-insert d L

bst-insert d (bst-node d' L R p1 p2) | tt , p | L' rewrite p =
  bst-node d' L'                (bst-inc-ub R (≤A-trans p2 max-≤2))
           (min2-mono p1) ≤A-refl

bst-insert d (bst-node d' L R p1 p2) | ff , p with bst-insert d R

bst-insert d (bst-node d' L R p1 p2) | ff , p | R' rewrite p =
  bst-node d' (bst-dec-lb L p1) R'
           min-≤2         (max2-mono p2)

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

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

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


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of unnormalized Rational numbers
------------------------------------------------------------------------

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

module Data.Rational.Unnormalised.Properties where

open import Algebra
import Algebra.Consequences.Setoid as FC
open import Algebra.Consequences.Propositional
open import Data.Nat.Base using (suc)
import Data.Nat.Properties as ℕ
open import Data.Integer.Base as ℤ using (ℤ; +0; +[1+_]; 0ℤ; 1ℤ)
open import Data.Integer.Solver renaming (module +-*-Solver to ℤ-solver)
import Data.Integer.Properties as ℤ
import Data.Integer.Properties
open import Data.Rational.Unnormalised
open import Data.Product using (_,_)
open import Data.Sum.Base using ([_,_]′; inj₁; inj₂)
open import Function.Base using (_on_; _$_; _∘_)
open import Level using (0ℓ)
open import Relation.Nullary using (yes; no)
import Relation.Nullary.Decidable as Dec
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

open import Algebra.Properties.CommutativeSemigroup ℤ.*-commutativeSemigroup

------------------------------------------------------------------------
-- Properties of ↥_ and ↧_
------------------------------------------------------------------------

↥↧≡⇒≡ : ∀ {p q} → ↥ p ≡ ↥ q → ↧ₙ p ≡ ↧ₙ q → p ≡ q
↥↧≡⇒≡ refl refl = refl

------------------------------------------------------------------------
-- Properties of _≃_
------------------------------------------------------------------------

drop-*≡* : ∀ {p q} → p ≃ q → ↥ p ℤ.* ↧ q ≡ ↥ q ℤ.* ↧ p
drop-*≡* (*≡* eq) = eq

≃-refl : Reflexive _≃_
≃-refl = *≡* refl

≃-reflexive : _≡_ ⇒ _≃_
≃-reflexive refl = *≡* refl

≃-sym : Symmetric _≃_
≃-sym (*≡* eq) = *≡* (sym eq)

≃-trans : Transitive _≃_
≃-trans {x} {y} {z} (*≡* ad≡cb) (*≡* cf≡ed) =
  *≡* (ℤ.*-cancelʳ-≡ (↥ x ℤ.* ↧ z) (↥ z ℤ.* ↧ x) (↧ y) (λ()) (begin
     ↥ x ℤ.* ↧ z ℤ.* ↧ y ≡⟨ xy∙z≈xz∙y (↥ x) _ _ ⟩
     ↥ x ℤ.* ↧ y ℤ.* ↧ z ≡⟨ cong (ℤ._* ↧ z) ad≡cb ⟩
     ↥ y ℤ.* ↧ x ℤ.* ↧ z ≡⟨ xy∙z≈xz∙y (↥ y) _ _ ⟩
     ↥ y ℤ.* ↧ z ℤ.* ↧ x ≡⟨ cong (ℤ._* ↧ x) cf≡ed ⟩
     ↥ z ℤ.* ↧ y ℤ.* ↧ x ≡⟨ xy∙z≈xz∙y (↥ z) _ _ ⟩
     ↥ z ℤ.* ↧ x ℤ.* ↧ y ∎))
  where open ≡-Reasoning

_≃?_ : Decidable _≃_
p ≃? q = Dec.map′ *≡* drop-*≡* (↥ p ℤ.* ↧ q ℤ.≟ ↥ q ℤ.* ↧ p)

≃-isEquivalence : IsEquivalence _≃_
≃-isEquivalence = record
  { refl  = ≃-refl
  ; sym   = ≃-sym
  ; trans = ≃-trans
  }

≃-isDecEquivalence : IsDecEquivalence _≃_
≃-isDecEquivalence = record
  { isEquivalence = ≃-isEquivalence
  ; _≟_           = _≃?_
  }

≃-setoid : Setoid 0ℓ 0ℓ
≃-setoid = record
  { isEquivalence = ≃-isEquivalence
  }

≃-decSetoid : DecSetoid 0ℓ 0ℓ
≃-decSetoid = record
  { isDecEquivalence = ≃-isDecEquivalence
  }

------------------------------------------------------------------------
-- Properties of _≤_
------------------------------------------------------------------------
-- Relational properties

drop-*≤* : ∀ {p q} → p ≤ q → (↥ p ℤ.* ↧ q) ℤ.≤ (↥ q ℤ.* ↧ p)
drop-*≤* (*≤* pq≤qp) = pq≤qp

≤-reflexive : _≃_ ⇒ _≤_
≤-reflexive (*≡* eq) = *≤* (ℤ.≤-reflexive eq)

≤-refl : Reflexive _≤_
≤-refl = ≤-reflexive ≃-refl

≤-trans : Transitive _≤_
≤-trans {i = p@(mkℚᵘ n₁ d₁-1)} {j = q@(mkℚᵘ n₂ d₂-1)} {k = r@(mkℚᵘ n₃ d₃-1)} (*≤* eq₁) (*≤* eq₂)
  = let d₁ = ↧ p; d₂ = ↧ q; d₃ = ↧ r in *≤* $
  ℤ.*-cancelʳ-≤-pos (n₁ ℤ.* d₃) (n₃ ℤ.* d₁) d₂-1 $ begin
  (n₁  ℤ.* d₃) ℤ.* d₂  ≡⟨ ℤ.*-assoc n₁ d₃ d₂ ⟩
  n₁   ℤ.* (d₃ ℤ.* d₂) ≡⟨ cong (n₁ ℤ.*_) (ℤ.*-comm d₃ d₂) ⟩
  n₁   ℤ.* (d₂ ℤ.* d₃) ≡⟨ sym (ℤ.*-assoc n₁ d₂ d₃) ⟩
  (n₁  ℤ.* d₂) ℤ.* d₃  ≤⟨ ℤ.*-monoʳ-≤-pos d₃-1 eq₁ ⟩
  (n₂  ℤ.* d₁) ℤ.* d₃  ≡⟨ cong (ℤ._* d₃) (ℤ.*-comm n₂ d₁) ⟩
  (d₁ ℤ.* n₂)  ℤ.* d₃  ≡⟨ ℤ.*-assoc d₁ n₂ d₃ ⟩
  d₁  ℤ.* (n₂  ℤ.* d₃) ≤⟨ ℤ.*-monoˡ-≤-pos d₁-1 eq₂ ⟩
  d₁  ℤ.* (n₃  ℤ.* d₂) ≡⟨ sym (ℤ.*-assoc d₁ n₃ d₂) ⟩
  (d₁ ℤ.* n₃)  ℤ.* d₂  ≡⟨ cong (ℤ._* d₂) (ℤ.*-comm d₁ n₃) ⟩
  (n₃  ℤ.* d₁) ℤ.* d₂  ∎
  where open ℤ.≤-Reasoning

≤-antisym : Antisymmetric _≃_ _≤_
≤-antisym (*≤* le₁) (*≤* le₂) = *≡* (ℤ.≤-antisym le₁ le₂)

≤-total : Total _≤_
≤-total p q = [ inj₁ ∘ *≤* , inj₂ ∘ *≤* ]′ (ℤ.≤-total
  (↥ p ℤ.* ↧ q)
  (↥ q ℤ.* ↧ p))

infix 4 _≤?_
_≤?_ : Decidable _≤_
p ≤? q = Dec.map′ *≤* drop-*≤* (↥ p ℤ.* ↧ q ℤ.≤? ↥ q ℤ.* ↧ p)

≤-irrelevant : Irrelevant _≤_
≤-irrelevant (*≤* p≤q₁) (*≤* p≤q₂) = cong *≤* (ℤ.≤-irrelevant p≤q₁ p≤q₂)

------------------------------------------------------------------------
-- Structures

≤-isPreorder : IsPreorder _≃_ _≤_
≤-isPreorder = record
  { isEquivalence = ≃-isEquivalence
  ; reflexive     = ≤-reflexive
  ; trans         = ≤-trans
  }

≤-isPartialOrder : IsPartialOrder _≃_ _≤_
≤-isPartialOrder = record
  { isPreorder = ≤-isPreorder
  ; antisym    = ≤-antisym
  }

≤-isTotalOrder : IsTotalOrder _≃_ _≤_
≤-isTotalOrder = record
  { isPartialOrder = ≤-isPartialOrder
  ; total          = ≤-total
  }

≤-isDecTotalOrder : IsDecTotalOrder _≃_ _≤_
≤-isDecTotalOrder = record
  { isTotalOrder = ≤-isTotalOrder
  ; _≟_          = _≃?_
  ; _≤?_         = _≤?_
  }

------------------------------------------------------------------------
-- Bundles

≤-decTotalOrder : DecTotalOrder 0ℓ 0ℓ 0ℓ
≤-decTotalOrder = record
  { isDecTotalOrder = ≤-isDecTotalOrder
  }

------------------------------------------------------------------------
-- Properties of _+_
------------------------------------------------------------------------

------------------------------------------------------------------------
-- Raw bundles

+-rawMagma : RawMagma 0ℓ 0ℓ
+-rawMagma = record
  { _≈_ = _≃_
  ; _∙_ = _+_
  }

+-rawMonoid : RawMonoid 0ℓ 0ℓ
+-rawMonoid = record
  { _≈_ = _≃_
  ; _∙_ = _+_
  ; ε   = 0ℚᵘ
  }

+-0-rawGroup : RawGroup 0ℓ 0ℓ
+-0-rawGroup = record
  { Carrier = ℚᵘ
  ; _≈_ = _≃_
  ; _∙_ = _+_
  ; ε = 0ℚᵘ
  ; _⁻¹ = -_
  }

+-*-rawRing : RawRing 0ℓ 0ℓ
+-*-rawRing = record
  { Carrier = ℚᵘ
  ; _≈_ = _≃_
  ; _+_ = _+_
  ; _*_ = _*_
  ; -_ = -_
  ; 0# = 0ℚᵘ
  ; 1# = 1ℚᵘ
  }

------------------------------------------------------------------------
-- Algebraic properties

-- Congruence

+-cong : Congruent₂ _≃_ _+_
+-cong {x} {y} {u} {v} (*≡* ab′∼a′b) (*≡* cd′∼c′d) = *≡* (begin
  (↥x ℤ.* ↧u ℤ.+ ↥u ℤ.* ↧x) ℤ.* (↧y ℤ.* ↧v)               ≡⟨ solve 6 (λ ↥x ↧x ↧y ↥u ↧u ↧v →
                                                             (↥x :* ↧u :+ ↥u :* ↧x) :* (↧y :* ↧v) :=
                                                             (↥x :* ↧y :* (↧u :* ↧v)) :+ ↥u :* ↧v :* (↧x :* ↧y))
                                                             refl (↥ x) (↧ x) (↧ y) (↥ u) (↧ u) (↧ v) ⟩
  ↥x ℤ.* ↧y ℤ.* (↧u ℤ.* ↧v) ℤ.+ ↥u ℤ.* ↧v ℤ.* (↧x ℤ.* ↧y) ≡⟨ cong₂ ℤ._+_ (cong (ℤ._* (↧u ℤ.* ↧v)) ab′∼a′b)
                                                                         (cong (ℤ._* (↧x ℤ.* ↧y)) cd′∼c′d) ⟩
  ↥y ℤ.* ↧x ℤ.* (↧u ℤ.* ↧v) ℤ.+ ↥v ℤ.* ↧u ℤ.* (↧x ℤ.* ↧y) ≡⟨ solve 6 (λ ↧x ↥y ↧y ↧u ↥v ↧v →
                                                             (↥y :* ↧x :* (↧u :* ↧v)) :+ ↥v :* ↧u :* (↧x :* ↧y) :=
                                                             (↥y :* ↧v :+ ↥v :* ↧y) :* (↧x :* ↧u))
                                                             refl (↧ x) (↥ y) (↧ y) (↧ u) (↥ v) (↧ v) ⟩
  (↥y ℤ.* ↧v ℤ.+ ↥v ℤ.* ↧y) ℤ.* (↧x ℤ.* ↧u)               ∎)
  where
  ↥x = ↥ x; ↧x = ↧ x; ↥y = ↥ y; ↧y = ↧ y; ↥u = ↥ u; ↧u = ↧ u; ↥v = ↥ v; ↧v = ↧ v
  open ≡-Reasoning
  open ℤ-solver

-- Associativity

+-assoc-↥ : Associative (_≡_ on ↥_) _+_
+-assoc-↥ p q r = solve 6 (λ ↥p ↧p ↥q ↧q ↥r ↧r →
    (↥p :* ↧q :+ ↥q :* ↧p) :* ↧r :+ ↥r :* (↧p :* ↧q) :=
    ↥p :* (↧q :* ↧r) :+ (↥q :* ↧r :+ ↥r :* ↧q) :* ↧p)
  refl (↥ p) (↧ p) (↥ q) (↧ q) (↥ r) (↧ r)
  where open ℤ-solver

+-assoc-↧ : Associative (_≡_ on ↧ₙ_) _+_
+-assoc-↧ p q r = ℕ.*-assoc (↧ₙ p) (↧ₙ q) (↧ₙ r)

+-assoc-≡ : Associative _≡_ _+_
+-assoc-≡ p q r = ↥↧≡⇒≡ (+-assoc-↥ p q r) (+-assoc-↧ p q r)

+-assoc : Associative _≃_ _+_
+-assoc p q r = ≃-reflexive (+-assoc-≡ p q r)

-- Commutativity

+-comm-↥ : Commutative (_≡_ on ↥_) _+_
+-comm-↥ p q = ℤ.+-comm (↥ p ℤ.* ↧ q) (↥ q ℤ.* ↧ p)

+-comm-↧ : Commutative (_≡_ on ↧ₙ_) _+_
+-comm-↧ p q = ℕ.*-comm (↧ₙ p) (↧ₙ q)

+-comm-≡ : Commutative _≡_ _+_
+-comm-≡ p q = ↥↧≡⇒≡ (+-comm-↥ p q) (+-comm-↧ p q)

+-comm : Commutative _≃_ _+_
+-comm p q = ≃-reflexive (+-comm-≡ p q)

-- Identities

+-identityˡ-↥ : LeftIdentity (_≡_ on ↥_) 0ℚᵘ _+_
+-identityˡ-↥ p = begin
  0ℤ ℤ.* ↧ p ℤ.+ ↥ p ℤ.* 1ℤ ≡⟨ cong₂ ℤ._+_ (ℤ.*-zeroˡ (↧ p)) (ℤ.*-identityʳ (↥ p)) ⟩
  0ℤ ℤ.+ ↥ p                ≡⟨ ℤ.+-identityˡ (↥ p) ⟩
  ↥ p                       ∎
  where open ≡-Reasoning

+-identityˡ-↧ : LeftIdentity (_≡_ on ↧ₙ_) 0ℚᵘ _+_
+-identityˡ-↧ p = ℕ.+-identityʳ (↧ₙ p)

+-identityˡ-≡ : LeftIdentity _≡_ 0ℚᵘ _+_
+-identityˡ-≡ p = ↥↧≡⇒≡ (+-identityˡ-↥ p) (+-identityˡ-↧ p)

+-identityˡ : LeftIdentity _≃_ 0ℚᵘ _+_
+-identityˡ p = ≃-reflexive (+-identityˡ-≡ p)

+-identityʳ-≡ : RightIdentity _≡_ 0ℚᵘ _+_
+-identityʳ-≡ = comm+idˡ⇒idʳ +-comm-≡ {e = 0ℚᵘ} +-identityˡ-≡

+-identityʳ : RightIdentity _≃_ 0ℚᵘ _+_
+-identityʳ p = ≃-reflexive (+-identityʳ-≡ p)

+-identity-≡ : Identity _≡_ 0ℚᵘ _+_
+-identity-≡ = +-identityˡ-≡ , +-identityʳ-≡

+-identity : Identity _≃_ 0ℚᵘ _+_
+-identity = +-identityˡ , +-identityʳ

+-inverseˡ : LeftInverse _≃_ 0ℚᵘ -_ _+_
+-inverseˡ p = *≡* let n = ↥ p; d = ↧ p in
  ((ℤ.- n) ℤ.* d ℤ.+ n ℤ.* d) ℤ.* 1ℤ ≡⟨ ℤ.*-identityʳ ((ℤ.- n) ℤ.* d ℤ.+ n ℤ.* d) ⟩
  (ℤ.- n) ℤ.* d ℤ.+ n ℤ.* d          ≡˘⟨ cong (ℤ._+ (n ℤ.* d)) (ℤ.neg-distribˡ-* n d) ⟩
  ℤ.- (n ℤ.* d) ℤ.+ n ℤ.* d          ≡⟨ ℤ.+-inverseˡ (n ℤ.* d) ⟩
  0ℤ ∎ where open ≡-Reasoning

+-inverseʳ : RightInverse _≃_ 0ℚᵘ -_ _+_
+-inverseʳ p = *≡* let n = ↥ p; d = ↧ p in
  (n ℤ.* d ℤ.+ (ℤ.- n) ℤ.* d) ℤ.* 1ℤ ≡⟨ ℤ.*-identityʳ (n ℤ.* d ℤ.+ (ℤ.- n) ℤ.* d) ⟩
  n ℤ.* d ℤ.+ (ℤ.- n) ℤ.* d          ≡˘⟨ cong (λ n+d → n ℤ.* d ℤ.+ n+d) (ℤ.neg-distribˡ-* n d) ⟩
  n ℤ.* d ℤ.+ ℤ.- (n ℤ.* d)          ≡⟨ ℤ.+-inverseʳ (n ℤ.* d) ⟩
  0ℤ ∎ where open ≡-Reasoning

+-inverse : Inverse _≃_ 0ℚᵘ -_ _+_
+-inverse = +-inverseˡ , +-inverseʳ

-‿cong : Congruent₁ _≃_ (-_)
-‿cong {p} {q} (*≡* p≡q) = *≡* (begin
  ↥(- p) ℤ.* ↧ q             ≡˘⟨ ℤ.*-identityˡ (ℤ.-(↥ p) ℤ.* ↧ q) ⟩
  1ℤ ℤ.* (↥(- p) ℤ.* ↧ q)    ≡⟨ sym (ℤ.*-assoc 1ℤ (↥(- p)) (↧ q)) ⟩
  (1ℤ ℤ.* ℤ.-(↥ p)) ℤ.* ↧ q  ≡˘⟨ cong (ℤ._* ↧ q) (ℤ.neg-distribʳ-* 1ℤ (↥ p)) ⟩
  ℤ.-(1ℤ ℤ.* ↥ p) ℤ.* ↧ q    ≡⟨ cong (ℤ._* ↧ q) (ℤ.neg-distribˡ-* 1ℤ (↥ p)) ⟩
  ((ℤ.- 1ℤ) ℤ.* ↥ p) ℤ.* ↧ q ≡⟨ ℤ.*-assoc (ℤ.- 1ℤ) (↥ p) (↧ q) ⟩
  ℤ.- 1ℤ ℤ.* (↥ p ℤ.* ↧ q)   ≡⟨ cong (λ r → ℤ.- 1ℤ ℤ.* r) p≡q ⟩
  ℤ.- 1ℤ ℤ.* (↥ q ℤ.* ↧ p)   ≡⟨ sym (ℤ.*-assoc (ℤ.- 1ℤ) (↥ q) (↧ p)) ⟩
  (ℤ.- 1ℤ ℤ.* ↥ q) ℤ.* ↧ p   ≡˘⟨ cong (ℤ._* ↧ p) (ℤ.neg-distribˡ-* 1ℤ (↥ q)) ⟩
  ℤ.-(1ℤ ℤ.* ↥ q) ℤ.* ↧ p    ≡⟨ cong (ℤ._* ↧ p) (ℤ.neg-distribʳ-* 1ℤ (↥ q)) ⟩
  (1ℤ ℤ.* ↥(- q)) ℤ.* ↧ p    ≡⟨ ℤ.*-assoc 1ℤ (ℤ.-(↥ q)) (↧ p) ⟩
  1ℤ ℤ.* (↥(- q) ℤ.* ↧ p)    ≡⟨ ℤ.*-identityˡ (↥(- q) ℤ.* ↧ p) ⟩
  ↥(- q) ℤ.* ↧ p ∎) where open ≡-Reasoning

------------------------------------------------------------------------
-- Algebraic structures

+-isMagma : IsMagma _≃_ _+_
+-isMagma = record
  { isEquivalence = ≃-isEquivalence
  ; ∙-cong        = +-cong
  }

+-isSemigroup : IsSemigroup _≃_ _+_
+-isSemigroup = record
  { isMagma = +-isMagma
  ; assoc   = +-assoc
  }

+-0-isMonoid : IsMonoid _≃_ _+_ 0ℚᵘ
+-0-isMonoid = record
  { isSemigroup = +-isSemigroup
  ; identity    = +-identity
  }

+-0-isCommutativeMonoid : IsCommutativeMonoid _≃_ _+_ 0ℚᵘ
+-0-isCommutativeMonoid = record
  { isMonoid = +-0-isMonoid
  ; comm     = +-comm
  }

+-0-isGroup : IsGroup _≃_ _+_ 0ℚᵘ (-_)
+-0-isGroup = record
  { isMonoid = +-0-isMonoid
  ; inverse  = +-inverse
  ; ⁻¹-cong  = -‿cong
  }

+-0-isAbelianGroup : IsAbelianGroup _≃_ _+_ 0ℚᵘ (-_)
+-0-isAbelianGroup = record
  { isGroup = +-0-isGroup
  ; comm    = +-comm
  }

------------------------------------------------------------------------
-- Algebraic bundles

+-magma : Magma 0ℓ 0ℓ
+-magma = record
  { isMagma = +-isMagma
  }

+-semigroup : Semigroup 0ℓ 0ℓ
+-semigroup = record
  { isSemigroup = +-isSemigroup
  }

+-0-monoid : Monoid 0ℓ 0ℓ
+-0-monoid = record
  { isMonoid = +-0-isMonoid
  }

+-0-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
+-0-commutativeMonoid = record
  { isCommutativeMonoid = +-0-isCommutativeMonoid
  }

+-0-group : Group 0ℓ 0ℓ
+-0-group = record
  { isGroup = +-0-isGroup
  }

+-0-abelianGroup : AbelianGroup 0ℓ 0ℓ
+-0-abelianGroup = record
  { isAbelianGroup = +-0-isAbelianGroup
  }

------------------------------------------------------------------------
-- Properties of _*_
------------------------------------------------------------------------

------------------------------------------------------------------------
-- Raw bundles

*-rawMagma : RawMagma 0ℓ 0ℓ
*-rawMagma = record
  { _≈_ = _≃_
  ; _∙_ = _*_
  }

*-rawMonoid : RawMonoid 0ℓ 0ℓ
*-rawMonoid = record
  { _≈_ = _≃_
  ; _∙_ = _*_
  ; ε   = 1ℚᵘ
  }

------------------------------------------------------------------------
-- Algebraic properties

*-cong : Congruent₂ _≃_ _*_
*-cong {x} {y} {u} {v} (*≡* ↥x↧y≡↥y↧x) (*≡* ↥u↧v≡↥v↧u) = *≡* (begin
  (↥ x ℤ.* ↥ u) ℤ.* (↧ y ℤ.* ↧ v) ≡⟨ solve 4 (λ ↥x ↥u ↧y ↧v →
                                       (↥x :* ↥u) :* (↧y :* ↧v) :=
                                       (↥u :* ↧v) :* (↥x :* ↧y))
                                       refl (↥ x) (↥ u) (↧ y) (↧ v) ⟩
  (↥ u ℤ.* ↧ v) ℤ.* (↥ x ℤ.* ↧ y) ≡⟨ cong₂ ℤ._*_ ↥u↧v≡↥v↧u ↥x↧y≡↥y↧x ⟩
  (↥ v ℤ.* ↧ u) ℤ.* (↥ y ℤ.* ↧ x) ≡⟨ solve 4 (λ ↥v ↧u ↥y ↧x →
                                       (↥v :* ↧u) :* (↥y :* ↧x) :=
                                       (↥y :* ↥v) :* (↧x :* ↧u))
                                       refl (↥ v) (↧ u) (↥ y) (↧ x) ⟩
  (↥ y ℤ.* ↥ v) ℤ.* (↧ x ℤ.* ↧ u) ∎)
  where open ≡-Reasoning; open ℤ-solver

-- Associativity

*-assoc-↥ : Associative (_≡_ on ↥_) _*_
*-assoc-↥ p q r = ℤ.*-assoc (↥ p) (↥ q) (↥ r)

*-assoc-↧ : Associative (_≡_ on ↧ₙ_) _*_
*-assoc-↧ p q r = ℕ.*-assoc (↧ₙ p) (↧ₙ q) (↧ₙ r)

*-assoc-≡ : Associative _≡_ _*_
*-assoc-≡ p q r = ↥↧≡⇒≡ (*-assoc-↥ p q r) (*-assoc-↧ p q r)

*-assoc : Associative _≃_ _*_
*-assoc p q r = ≃-reflexive (*-assoc-≡ p q r)

-- Commutativity

*-comm-↥ : Commutative (_≡_ on ↥_) _*_
*-comm-↥ p q = ℤ.*-comm (↥ p) (↥ q)

*-comm-↧ : Commutative (_≡_ on ↧ₙ_) _*_
*-comm-↧ p q = ℕ.*-comm (↧ₙ p) (↧ₙ q)

*-comm-≡ : Commutative _≡_ _*_
*-comm-≡ p q = ↥↧≡⇒≡ (*-comm-↥ p q) (*-comm-↧ p q)

*-comm : Commutative _≃_ _*_
*-comm p q = ≃-reflexive (*-comm-≡ p q)

-- Identities

*-identityˡ-≡ : LeftIdentity _≡_ 1ℚᵘ _*_
*-identityˡ-≡ p = ↥↧≡⇒≡ (ℤ.*-identityˡ (↥ p)) (ℕ.+-identityʳ (↧ₙ p))

*-identityʳ-≡ : RightIdentity _≡_ 1ℚᵘ _*_
*-identityʳ-≡ = comm+idˡ⇒idʳ *-comm-≡ {e = 1ℚᵘ} *-identityˡ-≡

*-identity-≡ : Identity _≡_ 1ℚᵘ _*_
*-identity-≡ = *-identityˡ-≡ , *-identityʳ-≡

*-identityˡ : LeftIdentity _≃_ 1ℚᵘ _*_
*-identityˡ p = ≃-reflexive (*-identityˡ-≡ p)

*-identityʳ : RightIdentity _≃_ 1ℚᵘ _*_
*-identityʳ p = ≃-reflexive (*-identityʳ-≡ p)

*-identity : Identity _≃_ 1ℚᵘ _*_
*-identity = *-identityˡ , *-identityʳ

*-zeroˡ : LeftZero _≃_ 0ℚᵘ _*_
*-zeroˡ p = *≡* refl

*-zeroʳ : RightZero _≃_ 0ℚᵘ _*_
*-zeroʳ = FC.comm+zeˡ⇒zeʳ ≃-setoid *-comm *-zeroˡ

*-zero : Zero _≃_ 0ℚᵘ _*_
*-zero = *-zeroˡ , *-zeroʳ

*-distribˡ-+ : _DistributesOverˡ_ _≃_ _*_ _+_
*-distribˡ-+ p q r =
  let ↥p = ↥ p; ↧p = ↧ p
      ↥q = ↥ q; ↧q = ↧ q
      ↥r = ↥ r; ↧r = ↧ r
      eq : (↥p ℤ.* (↥q ℤ.* ↧r ℤ.+ ↥r ℤ.* ↧q)) ℤ.* (↧p ℤ.* ↧q ℤ.* (↧p ℤ.* ↧r)) ≡
           (↥p ℤ.* ↥q ℤ.* (↧p ℤ.* ↧r) ℤ.+ ↥p ℤ.* ↥r ℤ.* (↧p ℤ.* ↧q)) ℤ.* (↧p ℤ.* (↧q ℤ.* ↧r))
      eq = solve 6 (λ ↥p ↧p ↥q d e f →
           (↥p :* (↥q :* f :+ e :* d)) :* (↧p :* d :* (↧p :* f)) :=
           (↥p :* ↥q :* (↧p :* f) :+ ↥p :* e :* (↧p :* d)) :* (↧p :* (d :* f)))
           refl ↥p ↧p ↥q ↧q ↥r ↧r
  in *≡* eq where open ℤ-solver

*-distribʳ-+ : _DistributesOverʳ_ _≃_ _*_ _+_
*-distribʳ-+ = FC.comm+distrˡ⇒distrʳ ≃-setoid +-cong *-comm *-distribˡ-+

*-distrib-+ : _DistributesOver_ _≃_ _*_ _+_
*-distrib-+ = *-distribˡ-+ , *-distribʳ-+

------------------------------------------------------------------------
-- Algebraic structures

*-isMagma : IsMagma _≃_ _*_
*-isMagma = record
  { isEquivalence = ≃-isEquivalence
  ; ∙-cong        = *-cong
  }

*-isSemigroup : IsSemigroup _≃_ _*_
*-isSemigroup = record
  { isMagma = *-isMagma
  ; assoc   = *-assoc
  }

*-1-isMonoid : IsMonoid _≃_ _*_ 1ℚᵘ
*-1-isMonoid = record
  { isSemigroup = *-isSemigroup
  ; identity    = *-identity
  }

*-1-isCommutativeMonoid : IsCommutativeMonoid _≃_ _*_ 1ℚᵘ
*-1-isCommutativeMonoid = record
  { isMonoid = *-1-isMonoid
  ; comm     = *-comm
  }

+-*-isRing : IsRing _≃_ _+_ _*_ -_ 0ℚᵘ 1ℚᵘ
+-*-isRing = record
  { +-isAbelianGroup = +-0-isAbelianGroup
  ; *-isMonoid       = *-1-isMonoid
  ; distrib          = *-distrib-+
  ; zero             = *-zero
  }

+-*-isCommutativeRing : IsCommutativeRing _≃_ _+_ _*_ -_ 0ℚᵘ 1ℚᵘ
+-*-isCommutativeRing = record
  { isRing = +-*-isRing
  ; *-comm = *-comm
  }

------------------------------------------------------------------------
-- Algebraic bundles

*-magma : Magma 0ℓ 0ℓ
*-magma = record
  { isMagma = *-isMagma
  }

*-semigroup : Semigroup 0ℓ 0ℓ
*-semigroup = record
  { isSemigroup = *-isSemigroup
  }

*-1-monoid : Monoid 0ℓ 0ℓ
*-1-monoid = record
  { isMonoid = *-1-isMonoid
  }

*-1-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
*-1-commutativeMonoid = record
  { isCommutativeMonoid = *-1-isCommutativeMonoid
  }

+-*-ring : Ring 0ℓ 0ℓ
+-*-ring = record
  { isRing = +-*-isRing
  }

+-*-commutativeRing : CommutativeRing 0ℓ 0ℓ
+-*-commutativeRing = record
  { isCommutativeRing = +-*-isCommutativeRing
  }


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

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just : A → Maybe A

postulate
  String : Set

{-# BUILTIN STRING String #-}

infix 1000 ♯_

postulate
  ∞  : ∀ {a} (A : Set a) → Set a
  ♯_ : ∀ {a} {A : Set a} → A → ∞ A
  ♭  : ∀ {a} {A : Set a} → ∞ A → A

{-# BUILTIN INFINITY ∞  #-}
{-# BUILTIN SHARP    ♯_ #-}
{-# BUILTIN FLAT     ♭  #-}

infixr 5 _∷_

data Colist (A : Set) : Set where
  []  : Colist A
  _∷_ : (x : A) (xs : ∞ (Colist A)) → Colist A

postulate
  Char : Set

{-# BUILTIN CHAR Char #-}

Costring : Set
Costring = Colist Char

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

data List {a} (A : Set a) : Set a where
  []  : List A
  _∷_ : (x : A) (xs : List A) → List A

{-# BUILTIN LIST List #-}
{-# BUILTIN NIL  []   #-}
{-# BUILTIN CONS _∷_  #-}

private
 primitive
  primStringAppend   : String → String → String
  primStringToList   : String → List Char
  primStringFromList : List Char → String

infixr 5 _++_

_++_ : String → String → String
_++_ = primStringAppend

toList : String → List Char
toList = primStringToList

fromList : List Char → String
fromList = primStringFromList

fromListToColist : {A : Set} → List A → Colist A
fromListToColist []       = []
fromListToColist (x ∷ xs) = x ∷ ♯ fromListToColist xs

toCostring : String → Costring
toCostring s = fromListToColist (toList s)

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

costringToString : Costring → ℕ → Maybe String
costringToString []       _       = just ""
costringToString (x ∷ xs) 0       with ♭ xs
... | []    = just (fromList (x ∷ []))
... | _ ∷ _ = nothing
costringToString (x ∷ xs) (suc n) with costringToString (♭ xs) n
... | nothing  = nothing
... | just xs′ = just (fromList (x ∷ []) ++ xs′)

test0 : costringToString (toCostring "") 0 ≡ just ""
test0 = refl

test1 : costringToString (toCostring "apa") 3 ≡ just "apa"
test1 = refl


text:
module Everything where

import Holes.Prelude
import Holes.Term
import Holes.Cong.Limited
import Holes.Cong.General
import Holes.Cong.Propositional


text:
module Issue118Comment9 where

open import Common.Level
open import Common.Coinduction

data Box (A : Set) : Set where
  [_] : A → Box A

postulate I : Set

data P : I → Set where
  c : ∀ {i} → Box (∞ (P i)) → P i

F : ∀ {i} → P i → I
F (c x) = _

G : ∀ {i} → Box (∞ (P i)) → I
G [ x ] = _

mutual

  f : ∀ {i} (x : P i) → P (F x)
  f (c x) = c (g x)

  g : ∀ {i} (x : Box (∞ (P i))) → Box (∞ (P (G x)))
  g [ x ] = [ ♯ f (♭ x) ]

-- The code above type checks, but the termination checker should
-- complain because the inferred definitions of F and G are
-- F (c x) = G x and G [ x ] = F (♭ x), respectively.

-- 2011-04-12 freezing: now the meta-variables remain uninstantiated.
-- good.


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

module Dodo.Binary.Maximal where

-- Stdlib imports
open import Level using (Level; _⊔_)
open import Function using (_∘_)
open import Data.Product using (_,_; ∃-syntax)
open import Data.Empty using (⊥-elim)
open import Relation.Nullary using (¬_)
open import Relation.Unary using (Pred)
open import Relation.Binary using (Rel)
open import Relation.Binary using (Trichotomous; tri<; tri≈; tri>)
-- Local imports
open import Dodo.Unary.Equality
open import Dodo.Unary.Unique
open import Dodo.Binary.Equality

-- # Definitions #

maximal : ∀ {a ℓ : Level} {A : Set a}
  → Rel A ℓ
    --------------
  → Pred A (a ⊔ ℓ)
maximal r = λ x → ¬ (∃[ y ] r x y)

-- # Properties #

module _ {a ℓ₁ ℓ₂ : Level} {A : Set a} {≈ : Rel A ℓ₁} {< : Rel A ℓ₂} where

  max-unique-tri : Trichotomous ≈ < → Unique₁ ≈ (maximal <)
  max-unique-tri tri {x} {y} ¬∃z[x<z] ¬∃z[y<z] with tri x y
  ... | tri< x<y _   _   = ⊥-elim (¬∃z[x<z] (y , x<y))
  ... | tri≈ _   x≈y _   = x≈y
  ... | tri> _   _   y<x = ⊥-elim (¬∃z[y<z] (x , y<x))

module _ {a ℓ₁ ℓ₂ : Level} {A : Set a} {P : Rel A ℓ₁} {Q : Rel A ℓ₂} where

  max-flips-⊆ : P ⊆₂ Q → maximal Q ⊆₁ maximal P
  max-flips-⊆ P⊆Q = ⊆: lemma
    where
    lemma : maximal Q ⊆₁' maximal P
    lemma x ¬∃zQxz (z , Pxz) = ¬∃zQxz (z , ⊆₂-apply P⊆Q Pxz)

module _ {a ℓ₁ ℓ₂ : Level} {A : Set a} {P : Rel A ℓ₁} {Q : Rel A ℓ₂} where

  max-preserves-⇔ : P ⇔₂ Q → maximal P ⇔₁ maximal Q
  max-preserves-⇔ = ⇔₁-sym ∘ ⇔₁-compose-⇔₂ max-flips-⊆ max-flips-⊆

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


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

module Categories.NaturalTransformation.NaturalIsomorphism.Functors where

open import Level

open import Categories.Category
open import Categories.Category.Construction.Functors
open import Categories.Functor
open import Categories.NaturalTransformation.NaturalIsomorphism

import Categories.Morphism as Mor

private
  variable
    o ℓ e : Level
    C D : Category o ℓ e

-- isomorphism in Functors category is the same as natural isomorphism
module _ {F G : Functor C D} where
  open Mor (Functors C D)

  Functors-iso⇒NI : F ≅ G → NaturalIsomorphism F G
  Functors-iso⇒NI F≅G = record
    { F⇒G = from
    ; F⇐G = to
    ; iso = λ X → record
      { isoˡ = isoˡ
      ; isoʳ = isoʳ
      }
    }
    where open Mor._≅_ F≅G

  NI⇒Functors-iso : NaturalIsomorphism F G → F ≅ G
  NI⇒Functors-iso α = record
    { from = F⇒G
    ; to   = F⇐G
    ; iso  = record
      { isoˡ = isoˡ (iso _)
      ; isoʳ = isoʳ (iso _)
      }
    }
    where open NaturalIsomorphism α
          open Mor.Iso


text:
{-

Part 4: Higher inductive types

• Set quotients via HITs
• Propositional truncation
• A little synthetic homotopy theory

-}
{-# OPTIONS --cubical #-}
module Part4 where

open import Cubical.Foundations.Isomorphism
open import Cubical.Data.Int  hiding (_+_)
open import Cubical.Data.Nat  hiding (elim)
open import Cubical.Data.Prod hiding (map)

open import Part1
open import Part2
open import Part3

-- Another thing that Cubical Agda adds is the possibility to define
-- higher inductive types. These are just like normal Agda datatypes,
-- but they have also "higher" constructors specifying non-trivial
-- paths, square, cubes, etc. in the type. These give a nice way of
-- defining set quotiented types as well as higher dimensional types
-- quotiented by some arbitrary relation.

-- Let's start by looking at some set quotient examples. The following
-- definition of finite multisets is due to Vikraman Choudhury and
-- Marcelo Fiore.

infixr 5 _∷_

data FMSet (A : Type ℓ) : Type ℓ where
  [] : FMSet A
  _∷_ : (x : A) → (xs : FMSet A) → FMSet A
  comm : (x y : A) (xs : FMSet A) → x ∷ y ∷ xs ≡ y ∷ x ∷ xs
  trunc : (xs ys : FMSet A) (p q : xs ≡ ys) → p ≡ q

infixr 30 _++_

_++_ : ∀ (xs ys : FMSet A) → FMSet A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ xs ++ ys
comm x y xs i ++ ys = comm x y (xs ++ ys) i
trunc xs zs p q i j ++ ys =
  trunc (xs ++ ys) (zs ++ ys) (λ k → p k ++ ys) (λ k → q k ++ ys) i j

unitl-++ : (xs : FMSet A) → [] ++ xs ≡ xs
unitl-++ xs = refl

unitr-++ : (xs : FMSet A) → xs ++ [] ≡ xs
unitr-++ [] = refl
unitr-++ (x ∷ xs) = cong (x ∷_) (unitr-++ xs)
unitr-++ (comm x y xs i) j = comm x y (unitr-++ xs j) i
unitr-++ (trunc xs ys p q i k) j =
  trunc (unitr-++ xs j) (unitr-++ ys j)
        (λ k → unitr-++ (p k) j) (λ k → unitr-++ (q k) j) i k

-- Filling the goals for comm and trunc quickly gets tiresome and
-- useful lemmas about eliminating into propositions are proved in
-- Cubical.HITs.FiniteMultiset. As we're proving an equality of a set
-- truncated type we can prove the trunc and comm cases once and for
-- all so that we only have to give cases for [] and _∷_ when
-- constructing a family of propositions. This is a very common
-- pattern when working with set truncated HITs: first define the HIT,
-- then prove special purpose recursors and eliminators for
-- eliminating into types of different h-levels. All definitions are
-- then written using these recursors and eliminators and one get very
-- short proofs.

-- A more efficient version of finite multisets based on association
-- lists can be found in Cubical.HITs.AssocList.Base. It looks like
-- this:

data AssocList (A : Type ℓ) : Type ℓ where
  ⟨⟩ : AssocList A
  ⟨_,_⟩∷_ : (a : A) (n : ℕ) (xs : AssocList A) → AssocList A
  per : (a b : A) (m n : ℕ) (xs : AssocList A)
      → ⟨ a , m ⟩∷ ⟨ b , n ⟩∷ xs ≡ ⟨ b , n ⟩∷ ⟨ a , m ⟩∷ xs
  agg : (a : A) (m n : ℕ) (xs : AssocList A)
      → ⟨ a , m ⟩∷ ⟨ a , n ⟩∷ xs ≡ ⟨ a , m + n ⟩∷ xs
  del : (a : A) (xs : AssocList A) → ⟨ a , 0 ⟩∷ xs ≡ xs
  trunc : (xs ys : AssocList A) (p q : xs ≡ ys) → p ≡ q

-- Programming and proving is more complicated with AssocList compared
-- to FMSet. This kind of example occurs everywhere in programming and
-- mathematics: one representation is easier to work with, but not
-- efficient, while another is efficient but difficult to work with.
-- Using the SIP we can get the best of both worlds (see
-- https://arxiv.org/abs/2009.05547 for details).

-- Another nice CS example of a HIT can be found in Cubical.Data.Queue
-- where we define a queue datastructure based on two lists. These
-- examples are all special cases of set quotients and are very useful
-- for programming and set level mathematics. We can define the
-- general form as:

data _/_ (A : Type ℓ) (R : A → A → Type ℓ') : Type (ℓ-max ℓ ℓ') where
  [_] : A → A / R
  eq/ : (a b : A) → R a b → [ a ] ≡ [ b ]
  trunc : (a b : A / R) (p q : a ≡ b) → p ≡ q

-- It's sometimes easier to work directly with _/_ instead of defining
-- special HITs as one can reuse lemmas for _/_ instead of reproving
-- things. For example, general lemmas about eliminating into
-- propositions have already been proved for _/_.

-- Proving that _/_ is "effective" (for prop-valued relation), i.e. that
--
--    ((a b : A) → [ a ] ≡ [ b ] → R a b)
--
-- requires univalence for propositions (hPropExt).

-- Set quotients let us define things like in normal math:
ℤ : Type₀
ℤ = (ℕ × ℕ) / rel
  where
  rel : (ℕ × ℕ) → (ℕ × ℕ) → Type₀
  rel (x₀ , y₀) (x₁ , y₁) = x₀ + y₁ ≡ x₁ + y₀

-- Another useful class of HITs are truncations, especially
-- propositional truncation:

data ∥_∥ (A : Type ℓ) : Type ℓ where
  ∣_∣ : A → ∥ A ∥
  squash : ∀ (x y : ∥ A ∥) → x ≡ y

-- This lets us define mere existence:
∃ : ∀ {ℓ ℓ'} (A : Type ℓ) (B : A → Type ℓ') → Type (ℓ-max ℓ ℓ')
∃ A B = ∥ Σ A B ∥

-- This is very useful to specify things where existence is weaker
-- than Σ. This lets us define things like surjective functions or the
-- image of a map which we cannot define properly in pre-HoTT type
-- theory.

-- We can define the recursor by pattern-matching
rec : {P : Type ℓ} → isProp P → (A → P) → ∥ A ∥ → P
rec Pprop f ∣ x ∣ = f x
rec Pprop f (squash x y i) = Pprop (rec Pprop f x) (rec Pprop f y) i

-- And the eliminator then follows easily:
elim : {P : ∥ A ∥ → Type ℓ} → ((a : ∥ A ∥) → isProp (P a)) →
       ((x : A) → P ∣ x ∣) → (a : ∥ A ∥) → P a
elim {P = P} Pprop f a =
  rec (Pprop a) (λ x → transport (λ i → P (squash ∣ x ∣ a i)) (f x)) a

-- A very important point is that propositional truncation is proof
-- relevant, so even though the elements are all equal one can still
-- extract interesting information from them. A fun example is the
-- "cost monad" which can be found in Cubical.HITs.Cost. There we pair
-- A with ∥ ℕ ∥ and use the truncated number to count the number of
-- recursive calls in various functions. As the number is truncated it
-- doesn't affect any properties of the functions, but by running
-- concrete computations we can extract the number of calls.

-------------------------------------------------------------------------
-- Another source of HITs are inspired by topology

-- We can define the circle as the following simple data declaration:
data S¹ : Type₀ where
  base : S¹
  loop : base ≡ base

-- We can write functions on S¹ using pattern-matching:
double : S¹ → S¹
double base = base
double (loop i) = (loop ∙ loop) i

-- Note that loop takes an i : I argument. This is not very surprising
-- as it's a path base ≡ base, but it's an important difference to
-- HoTT. Having the native notion of equality be heterogeneous makes
-- it possible to quite directly define a general schema for a large
-- class of HITs (more or less all in the HoTT book, with the
-- exception for the Cauchy reals (I think?)).

-- Let's use univalence to compute some winding numbers on the
-- circle. We first define a family of types over the circle whos
-- fibers are the integers.
helix : S¹ → Type₀
helix base     = Int
helix (loop i) = sucPath i

-- The loopspace of the circle
ΩS¹ : Type₀
ΩS¹ = base ≡ base

-- We can then define a function computing how many times we've looped
-- around the circle by:
winding : ΩS¹ → Int
winding p = subst helix p (pos 0)

-- This reduces just fine:
_ : winding (λ i → double ((loop ∙ loop) i)) ≡ pos 4
_ = refl

-- This would not reduce in HoTT as univalence is an axiom. Having
-- things compute makes it possible to substantially simplify many
-- proofs from HoTT in Cubical Agda, more about this later.

-- We can in fact prove that winding is an equivalence, this relies on
-- the encode-decode method and Egbert will go through the proof in
-- detail. For details about how this proof looks in Cubical Agda see:
--
--   Cubical.HITs.S1.Base

-- Complex multiplication on S¹, used in the Hopf fibration
_⋆_ : S¹ → S¹ → S¹
base   ⋆ x = x
loop i ⋆ base = loop i
loop i ⋆ loop j =
  hcomp (λ k → λ { (i = i0) → loop (j ∨ ~ k)
                 ; (i = i1) → loop (j ∧ k)
                 ; (j = i0) → loop (i ∨ ~ k)
                 ; (j = i1) → loop (i ∧ k) })
        base

-- We can define the Torus as:
data Torus : Type₀ where
  point : Torus
  line1 : point ≡ point
  line2 : point ≡ point
  square : PathP (λ i → line1 i ≡ line1 i) line2 line2

-- The square corresponds to the usual folding diagram from topology:
--
--              line1
--         p ----------> p
--         ^             ^
--         ¦             ¦
--   line2 ¦             ¦ line2
--         ¦             ¦
--         p ----------> p
--              line1

-- Proving that it is equivalent to two circles is pretty much trivial:
t2c : Torus → S¹ × S¹
t2c point        = (base , base)
t2c (line1 i)    = (loop i , base)
t2c (line2 j)    = (base , loop j)
t2c (square i j) = (loop i , loop j)

c2t : S¹ × S¹ → Torus
c2t (base   , base)   = point
c2t (loop i , base)   = line1 i
c2t (base   , loop j) = line2 j
c2t (loop i , loop j) = square i j

c2t-t2c : (t : Torus) → c2t (t2c t) ≡ t
c2t-t2c point        = refl
c2t-t2c (line1 _)    = refl
c2t-t2c (line2 _)    = refl
c2t-t2c (square _ _) = refl

t2c-c2t : (p : S¹ × S¹) → t2c (c2t p) ≡ p
t2c-c2t (base   , base)   = refl
t2c-c2t (base   , loop _) = refl
t2c-c2t (loop _ , base)   = refl
t2c-c2t (loop _ , loop _) = refl

-- Using univalence we get the following equality:
Torus≡S¹×S¹ : Torus ≡ S¹ × S¹
Torus≡S¹×S¹ = isoToPath (iso t2c c2t t2c-c2t c2t-t2c)

-- We can also directly compute winding numbers on the torus
windingTorus : point ≡ point → Int × Int
windingTorus l = ( winding (λ i → proj₁ (t2c (l i)))
                 , winding (λ i → proj₂ (t2c (l i))))

_ : windingTorus (line1 ∙ sym line2) ≡ (pos 1 , negsuc 0)
_ = refl

-- This proof turned out to be much more complicated in HoTT as
-- eliminators out of HITs don't compute definitionally for higher
-- constructors. In Cubical Agda this is not a problem as all cases
-- reduce definitionally.

-- We have many more topological examples in the library, including
-- Klein bottle, RP^n, higher spheres, suspensions, join, wedges,
-- smash product:
-- open import Cubical.HITs.KleinBottle
-- open import Cubical.HITs.RPn
-- open import Cubical.HITs.S2
-- open import Cubical.HITs.S3
-- open import Cubical.HITs.Susp
-- open import Cubical.HITs.Join
-- open import Cubical.HITs.Wedge
-- open import Cubical.HITs.SmashProduct

-- There's also a proof of the "3x3 lemma" for pushouts in less than
-- 200LOC. In HoTT-Agda this took about 3000LOC. For details see:
-- https://github.com/HoTT/HoTT-Agda/tree/master/theorems/homotopy/3x3
-- open import Cubical.HITs.Pushout

-- We also defined the Hopf fibration and proved that its total space
-- is S³ in about 300LOC:
-- open import Cubical.HITs.Hopf

-- There is also some integer cohomology:
-- open import Cubical.ZCohomology.Everything
-- To compute cohomology groups of various spaces we need a bunch of
-- interesting theorems: Freudenthal suspension theorem,
-- Mayer-Vietoris sequence...

-- For further references about doing synthetic algebraic topology in
-- Cubical Agda see:

-- Cubical Synthetic Homotopy Theory
-- Anders Mörtberg, Loïc Pujet
-- https://staff.math.su.se/anders.mortberg/papers/cubicalsynthetic.pdf

-- Synthetic Cohomology Theory in Cubical Agda
-- Guillaume Brunerie, Anders Mörtberg, Axel Ljungström.
-- https://staff.math.su.se/anders.mortberg/papers/zcohomology.pdf

--- The end! ---


text:
data ⊤ : Set where tt : ⊤

postulate
  IndexL        : Set
  Ordered       : IndexL → Set
  ¬ho-shr-morph : IndexL → IndexL
  pres-¬ord     : ∀ ind → Ordered (¬ho-shr-morph ind)
  ¬ord-morph    : ∀ ind → Ordered ind → Set

postulate tt' : ⊤

poo : ∀ ind → ¬ord-morph (¬ho-shr-morph ind) (pres-¬ord ind)
poo ind with tt | ¬ho-shr-morph ind
... | _ | _ = {!!}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --experimental-irrelevance #-}
{-# OPTIONS --universe-polymorphism #-}
module IrrelevantLevelToSet where

open import Imports.Level

-- should fail, because Set i /= Set j for i /= j, so i is not irrelevant in Set i
MySet : .(i : Level) -> Set (suc i)
MySet i = Set i

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
module Lam where

f
  : {A : Set}
  → A
  → A
f x
  = (λ y z → z) x x

g
  : {A : Set}
  → A
  → A
g {A = A} x
  = (λ (y' : A) (z : A) → z) x x

max_stars_repo_name: msuperdock/agda-unused

max_issues_repo_name: msuperdock/agda-unused

max_forks_repo_name: msuperdock/agda-unused


text:
------------------------------------------------------------------------
-- Big-step semantics for the untyped λ-calculus
------------------------------------------------------------------------

module Lambda.Substitution.OneSemantics where

open import Codata.Musical.Notation
open import Data.Fin
open import Function
open import Data.Nat

open import Lambda.Syntax
open WHNF
open import Lambda.Substitution

-- Semantic domain. ⊥ represents non-termination.

data Sem (n : ℕ) : Set where
  ⊥   : Sem n
  val : (v : Value n) → Sem n

-- Big-step semantics.

mutual

  infix 4 _⇒_ _⇒?_

  data _⇒_ {n} : Tm n → Sem n → Set where
    val : ∀ {v} → ⌜ v ⌝ ⇒ val v
    app : ∀ {t₁ t₂ t v s}
          (t₁⇓   : t₁ ⇒? val (ƛ t))
          (t₂⇓   : t₂ ⇒? val v)
          (t₁t₂⇒ : t / sub ⌜ v ⌝ ⇒? s) →
          t₁ · t₂ ⇒ s
    ·ˡ  : ∀ {t₁ t₂}
          (t₁⇑ : t₁ ⇒? ⊥) →
          t₁ · t₂ ⇒ ⊥
    ·ʳ  : ∀ {t₁ t₂ v}
          (t₁⇓ : t₁ ⇒? val v)
          (t₂⇑ : t₂ ⇒? ⊥) →
          t₁ · t₂ ⇒ ⊥

  -- Conditional coinduction: coinduction only for diverging
  -- computations.

  _⇒?_ : ∀ {n} → Tm n → Sem n → Set
  t ⇒? ⊥     = ∞ (t ⇒ ⊥)
  t ⇒? val v = t ⇒ val v

-- Example.

Ω-loops : Ω ⇒ ⊥
Ω-loops = app val val (♯ Ω-loops)

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
-- simulating streams by Nat -> A

module Stream where

data Bool : Set where
    true  : Bool
    false : Bool

if_then_else_ : forall {A} -> Bool -> A -> A -> A
if true  then t else e = t
if false then t else e = e

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

Stream : Set -> Set
Stream A = Nat -> A

_::_ : forall {A} -> A -> Stream A -> Stream A
_::_ a as zero     = a
_::_ a as (succ n) = as n

map : forall {A B} -> (A -> B) -> Stream A -> Stream B
map f as n = f (as n)

head : forall {A} -> Stream A -> A
head as = as zero

tail : forall {A} -> Stream A -> Stream A
tail as n = as (succ n)

-- construct the stream a :: f a :: f (f a) :: ...

iterate : forall {A} -> (A -> A) -> A -> Stream A
iterate f a zero = a
iterate f a (succ n) = iterate f (f a) n

zipWith : forall {A B C} -> (A -> B -> C) -> Stream A -> Stream B -> Stream C
zipWith f as bs n = f (as n) (bs n)

-- merge with with
merge : forall {A} -> (A -> A -> Bool) -> Stream A -> Stream A -> Stream A
merge le as bs with le (head as) (head bs)
merge le as bs | true  = head as :: merge le (tail as) bs
merge le as bs | false = head bs :: merge le as (tail bs)

{-
-- without with
merge' : forall {A} -> (A -> A -> Bool) -> Stream A -> Stream A -> Stream A
merge' le as bs = if le (head as) (head bs)
                  then (head as :: merge' le (tail as) bs)
                  else (head bs :: merge' le as (tail bs))
-}

-- BOTH VARIANTS OF MERGE ARE NOT STRUCTURALLY RECURSIVE


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

open import LogicalFormulae
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Naturals
open import Numbers.Naturals.Order
open import Numbers.Naturals.EuclideanAlgorithm
open import Lists.Lists
open import Numbers.Primes.PrimeNumbers
open import Decidable.Relations
open import Numbers.BinaryNaturals.Definition
open import Numbers.BinaryNaturals.Addition
open import Numbers.BinaryNaturals.Order
open import Sequences
open import Vectors
open import Orders.Total.Definition
open import Setoids.Orders.Partial.Definition
open import Setoids.Orders.Partial.Sequences
open import Setoids.Orders.Total.Definition
open import Setoids.Setoids
open import Functions.Definition
open import Semirings.Definition

module ProjectEuler.Problem2 where

fibUnary : ℕ → ℕ
fibUnary zero = 1
fibUnary (succ zero) = 1
fibUnary (succ (succ n)) = fibUnary (succ n) +N fibUnary n

fibUnaryStrictlyPositive : (a : ℕ) → 0 <N fibUnary a
fibUnaryStrictlyPositive zero = le zero refl
fibUnaryStrictlyPositive (succ zero) = le zero refl
fibUnaryStrictlyPositive (succ (succ a)) = addStrongInequalities (fibUnaryStrictlyPositive (succ a)) (fibUnaryStrictlyPositive a)

fibUnaryIncreasing : (a : ℕ) → (fibUnary (succ a)) <N (fibUnary (succ (succ a)))
fibUnaryIncreasing zero = le zero refl
fibUnaryIncreasing (succ a) = identityOfIndiscernablesLeft _<N_ (additionPreservesInequalityOnLeft (fibUnary (succ a) +N fibUnary a) (fibUnaryStrictlyPositive (succ a))) (Semiring.sumZeroRight ℕSemiring (fibUnary (succ a) +N fibUnary a))

fibUnaryBiggerThanN : (a : ℕ) → (succ (succ (succ (succ a)))) <N fibUnary (succ (succ (succ (succ a))))
fibUnaryBiggerThanN zero = le zero refl
fibUnaryBiggerThanN (succ a) = TotalOrder.<Transitive ℕTotalOrder (succPreservesInequality (fibUnaryBiggerThanN a)) (ans ((fibUnary (succ a) +N fibUnary a) +N fibUnary (succ a)) ans')
  where
    ans : {t : ℕ} → (u : ℕ) → 1 <N u → succ t <N t +N u
    ans {t} u (le x proof) rewrite Semiring.commutative ℕSemiring x 1 = le x (transitivity (applyEquality succ (Semiring.commutative ℕSemiring x (succ t))) (transitivity (applyEquality (λ i → succ (succ i)) (Semiring.commutative ℕSemiring t x)) (transitivity (applyEquality (_+N t) proof) (Semiring.commutative ℕSemiring u t))))
    ans' : 1 <N (fibUnary (succ a) +N fibUnary a) +N fibUnary (succ a)
    ans' with fibUnaryStrictlyPositive (succ a)
    ... | fibPos with fibUnary (succ a)
    ans' | fibPos | succ bl rewrite Semiring.commutative ℕSemiring (bl +N fibUnary a) (succ bl) = succPreservesInequality (le (bl +N (bl +N fibUnary a)) (Semiring.sumZeroRight ℕSemiring _))

fibUnaryArchimedean : (a : ℕ) → Sg ℕ (λ i → a <N fibUnary i)
fibUnaryArchimedean zero = 0 , le zero refl
fibUnaryArchimedean (succ zero) = 2 , le zero refl
fibUnaryArchimedean (succ (succ zero)) = 3 , le zero refl
fibUnaryArchimedean (succ (succ (succ zero))) = 4 , le 1 refl
fibUnaryArchimedean (succ (succ (succ (succ a)))) = (succ (succ (succ (succ a)))) , fibUnaryBiggerThanN a

record FibEntry : Set where
  field
    prev : BinNat
    curr : BinNat

nextFib : FibEntry → FibEntry
nextFib record { prev = prev ; curr = curr } = record { prev = curr ; curr = prev +B curr }

fib : Sequence BinNat
fib = Sequences.map FibEntry.curr (unfold nextFib record { prev = NToBinNat 0 ; curr = NToBinNat 1 })

fibMove : (n : ℕ) → FibEntry.prev (index (unfold nextFib (record { prev = [] ; curr = one :: [] })) (succ n)) ≡ FibEntry.curr (index (unfold nextFib (record { prev = [] ; curr = one :: [] })) n)
fibMove zero = refl
fibMove (succ n) rewrite indexAndUnfold nextFib (record { prev = [] ; curr = one :: [] }) (succ n) = refl

fibAlternative : (N : ℕ) → index fib N ≡ FibEntry.curr (index (unfold nextFib (record { prev = [] ; curr = one :: [] })) N)
fibAlternative n rewrite equalityCommutative (mapAndIndex (unfold nextFib record { prev = NToBinNat 0 ; curr = NToBinNat 1 }) FibEntry.curr n) = refl

fibAlternative' : (n : ℕ) → FibEntry.curr (index (unfold nextFib (record { prev = [] ; curr = one :: [] })) (succ n)) ≡ FibEntry.prev (index (unfold nextFib (record { prev = [] ; curr = one :: [] })) n) +B FibEntry.curr (index (unfold nextFib (record { prev = [] ; curr = one :: [] })) n)
fibAlternative' zero = refl
fibAlternative' (succ n) rewrite indexAndUnfold nextFib (record { prev = [] ; curr = one :: [] }) (succ n) = refl

fibsCanonical : (n : ℕ) → canonical (index fib n) ≡ index fib n
fibsCanonical zero = refl
fibsCanonical (succ zero) = refl
fibsCanonical (succ (succ n)) = transitivity (applyEquality canonical {index fib (succ (succ n))} {FibEntry.prev (index (unfold nextFib (nextFib (record { prev = [] ; curr = one :: [] }))) n) +B FibEntry.curr (index (unfold nextFib (nextFib (record { prev = [] ; curr = one :: [] }))) n)} (transitivity (fibAlternative (succ (succ n))) (fibAlternative' (succ n)))) (transitivity (sumCanonical (FibEntry.prev (index (unfold nextFib (nextFib (record { prev = [] ; curr = one :: [] }))) n)) (FibEntry.curr (index (unfold nextFib (nextFib (record { prev = [] ; curr = one :: [] }))) n)) (transitivity (transitivity (applyEquality canonical (fibMove n)) (transitivity (applyEquality canonical (equalityCommutative (fibAlternative n))) (transitivity (fibsCanonical n) (fibAlternative n)))) (equalityCommutative (fibMove n))) (transitivity (applyEquality canonical (mapAndIndex (unfold nextFib (nextFib (record { prev = [] ; curr = one :: [] }))) FibEntry.curr n)) (transitivity (fibsCanonical (succ n)) (equalityCommutative (mapAndIndex (unfold nextFib (nextFib (record { prev = [] ; curr = one :: [] }))) FibEntry.curr n))))) (equalityCommutative (transitivity (fibAlternative (succ (succ n))) (fibAlternative' (succ n)))))

fibStart : take 5 fib ≡ vecMap NToBinNat (1 ,- 1 ,- 2 ,- 3 ,- 5 ,- [])
fibStart = refl

fibsMatch : (n : ℕ) → binNatToN (index fib n) ≡ fibUnary n
fibsMatch zero = refl
fibsMatch (succ zero) = refl
fibsMatch (succ (succ n)) rewrite equalityCommutative (fibsMatch (succ n)) | equalityCommutative (fibsMatch n) | equalityCommutative (mapAndIndex (unfold nextFib record { prev = NToBinNat 0 ; curr = NToBinNat 1 }) FibEntry.curr (succ (succ n))) | indexAndUnfold nextFib (record { prev = [] ; curr = one :: [] }) (succ n) | equalityCommutative (mapAndIndex (unfold nextFib (nextFib (record { prev = [] ; curr = one :: [] }))) FibEntry.curr n) | equalityCommutative (mapAndIndex (unfold nextFib (record { prev = [] ; curr = one :: [] })) FibEntry.curr n) | indexAndUnfold nextFib (nextFib (record { prev = [] ; curr = one :: [] })) n | indexAndUnfold nextFib (record { prev = [] ; curr = one :: [] }) n = ans
  where
    x = FibEntry.curr (index (unfold nextFib (record { prev = [] ; curr = one :: [] })) n)
    y = FibEntry.prev (index (unfold nextFib (record { prev = [] ; curr = one :: [] })) n)
    ans : binNatToN (x +B (y +B x)) ≡ binNatToN (y +B x) +N binNatToN x
    ans rewrite +BCommutative x (y +B x) = +BIsHom (y +B x) x

fibsMatch' : (n : ℕ) → NToBinNat (fibUnary n) ≡ index fib n
fibsMatch' n = transitivity (applyEquality NToBinNat (equalityCommutative (fibsMatch n))) (transitivity (binToBin (index fib n)) (fibsCanonical n))

ArchimedeanSequence : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_<_ : Rel {a} {c} A} (pOrder : SetoidPartialOrder S _<_) (S : Sequence A) → Set (a ⊔ c)
ArchimedeanSequence {A = A} {_<_ = _<_} _ S = (x : A) → Sg ℕ (λ n → x < (index S n))

archimImpliesTailArchim : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_<_ : Rel {a} {c} A} (pOrder : SetoidPartialOrder S _<_) {S : Sequence A} → ArchimedeanSequence pOrder S → (Sg ℕ (λ i → index S 0 < index S i)) → ArchimedeanSequence pOrder (Sequence.tail S)
archimImpliesTailArchim {S} pOrder arch 0small x with arch x
archimImpliesTailArchim pOrder {S} arch (zero , S0<SN) x | zero , pr = exFalso (SetoidPartialOrder.irreflexive pOrder S0<SN)
archimImpliesTailArchim pOrder {S} arch (succ N , S0<SN) x | zero , pr = N , SetoidPartialOrder.<Transitive pOrder pr S0<SN
archimImpliesTailArchim pOrder arch 0small x | succ N , pr = N , pr

takeUpTo : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_<_ : Rel {a} {c} A} {pOrder : SetoidPartialOrder S _<_} {seq : Sequence A} → (arch : ArchimedeanSequence pOrder seq) → (lim : A) → List A
takeUpTo {seq = S} arch lim with arch lim
takeUpTo {seq = S} arch lim | zero , pr = []
takeUpTo {seq = S} arch lim | succ N , pr = vecToList (take N S)

archim : ArchimedeanSequence (partialOrderToSetoidPartialOrder BinNatOrder) fib
archim x with fibUnaryArchimedean (binNatToN x)
archim x | N , pr = N , u
  where
    t : (canonical x) <B (NToBinNat (binNatToN (index (Sequences.map FibEntry.curr (unfold nextFib (record { prev = [] ; curr = one :: [] }))) N)))
    t rewrite (fibsMatch N) = identityOfIndiscernablesLeft _<B_ (translate' _ _ pr) (binToBin x)
    u : x <B (index (Sequences.map FibEntry.curr (unfold nextFib (record { prev = [] ; curr = one :: [] }))) N)
    u rewrite equalityCommutative (mapAndIndex (unfold nextFib (record { prev = [] ; curr = one :: [] })) FibEntry.curr N) with transitivity (canonicalFirst x (NToBinNat (fibUnary N)) Equal) (identityOfIndiscernablesLeft _<B_ (translate' (binNatToN x) (fibUnary N) pr) (binToBin x))
    ... | r = identityOfIndiscernablesRight {a = x} {b = NToBinNat (fibUnary N)} {c = FibEntry.curr (index (unfold nextFib (record { prev = [] ; curr = one :: [] })) N)} _<B_ r (transitivity (fibsMatch' N) (fibAlternative N))

isEven : BinNat → Set
isEven [] = True
isEven (zero :: xs) = True
isEven (one :: xs) = False

isEvenAgrees : (n : BinNat) → isEven n → 2 ∣ (binNatToN n)
isEvenAgrees [] nEven = divides (record { quot = zero ; rem = zero ; pr = refl ; remIsSmall = inl (le 1 refl) ; quotSmall = inl (le 1 refl)}) refl
isEvenAgrees (zero :: n) nEven = divides (record { quot = binNatToN n ; rem = zero ; pr = Semiring.sumZeroRight ℕSemiring _ ; remIsSmall = inl (le 1 refl) ; quotSmall = inl (le 1 refl) }) refl

isEvenIncrs : (n : BinNat) → isEven n → isEven (incr (incr n))
isEvenIncrs [] nEven = record {}
isEvenIncrs (zero :: n) nEven = record {}

isEvenAgrees' : (n : ℕ) → 2 ∣ n → isEven (NToBinNat n)
isEvenAgrees' zero nEven = record {}
isEvenAgrees' (succ zero) (divides record { quot = (succ zero) ; rem = zero ; pr = () ; remIsSmall = remIsSmall ; quotSmall = (inl x) } refl)
isEvenAgrees' (succ zero) (divides record { quot = (succ (succ quot)) ; rem = zero ; pr = () ; remIsSmall = remIsSmall ; quotSmall = (inl x) } refl)
isEvenAgrees' (succ (succ n)) (divides record { quot = succ quot ; rem = zero ; pr = pr ; remIsSmall = remIsSmall ; quotSmall = inl 0<2 } refl) with isEvenAgrees' n (divides record { quot = quot ; rem = zero ; pr = transitivity (transitivity (Semiring.sumZeroRight ℕSemiring _) (Semiring.commutative ℕSemiring quot (quot +N 0))) (succInjective (succInjective (transitivity (equalityCommutative (applyEquality succ (transitivity (Semiring.sumZeroRight ℕSemiring (quot +N succ (quot +N zero))) (Semiring.commutative ℕSemiring quot (succ (quot +N 0)))))) pr))) ; remIsSmall = remIsSmall ; quotSmall = inl 0<2 } refl)
... | bl = isEvenIncrs (NToBinNat n) bl

isEvenWellDefined : (n m : BinNat) → canonical n ≡ canonical m → isEven n → isEven m
isEvenWellDefined [] [] n=m nEven = record {}
isEvenWellDefined [] (zero :: m) n=m nEven = record {}
isEvenWellDefined (zero :: n) [] n=m nEven = record {}
isEvenWellDefined (zero :: n) (zero :: m) n=m nEven = record {}
isEvenWellDefined (zero :: n) (one :: m) n=m nEven with canonical n
isEvenWellDefined (zero :: n) (one :: m) () nEven | []
isEvenWellDefined (zero :: n) (one :: m) () nEven | x :: bl

isEvenDecidable : DecidableRelation isEven
isEvenDecidable [] = inl (record {})
isEvenDecidable (zero :: x₁) = inl (record {})
isEvenDecidable (one :: x₁) = inr (λ x → x)

increasing : StrictlyIncreasing (partialOrderToSetoidPartialOrder BinNatOrder) (Sequence.tail fib)
increasing m = SetoidPartialOrder.<WellDefined (partialOrderToSetoidPartialOrder BinNatOrder) (fibsMatch' (succ m)) (fibsMatch' (succ (succ m))) (translate' (fibUnary (succ m)) (fibUnary (succ (succ m))) (fibUnaryIncreasing m))

-- increasingNaturalsBound : (S : Sequence ℕ) → StrictlyIncreasing S → (bound : ℕ) → List ℕ
-- increasingNaturalsBound s n = {!!}

{-
fibsLessThan4Mil : List BinNat
fibsLessThan4Mil = takeUpToMonotone {tOrder = BinNatTOrder} (archimImpliesTailArchim {tOrder = BinNatTOrder} archim (2 , ordersAgree 1 2 (le zero refl))) increasing (one :: one :: one :: one :: zero :: one :: zero :: zero :: zero :: zero :: one :: zero :: zero :: one :: zero :: zero :: zero :: zero :: zero :: zero :: zero :: one :: [])

evens : List BinNat
evens = filter' isEvenDecidable fibsLessThan4Mil

ans : BinNat
ans = fold _+B_ [] evens

-}


text:
module MetaCannotDependOn where

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

postulate
  Vec : Nat -> Set -> Set
  f : (A : Set) -> ((n : Nat) -> A -> Vec n Nat) -> Nat

err : Nat
err = f _ (\ n xs -> xs)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Boring lemmas used in Data.Nat.GCD and Data.Nat.Coprimality
------------------------------------------------------------------------

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

module Data.Nat.GCD.Lemmas where

open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.Solver
open import Function
open import Relation.Binary.PropositionalEquality

open +-*-Solver
open ≡-Reasoning

private
  distrib-comm : ∀ x k n → x * k + x * n ≡ x * (n + k)
  distrib-comm =
    solve 3 (λ x k n → x :* k :+ x :* n  :=  x :* (n :+ k)) refl

  distrib-comm₂ : ∀ d x k n → d + x * (n + k) ≡ d + x * k + x * n
  distrib-comm₂ =
    solve 4 (λ d x k n → d :+ x :* (n :+ k) :=  d :+ x :* k :+ x :* n) refl

-- Other properties
-- TODO: Can this proof be simplified? An automatic solver which can
-- handle ∸ would be nice...
lem₀ : ∀ i j m n → i * m ≡ j * m + n → (i ∸ j) * m ≡ n
lem₀ i j m n eq = begin
  (i ∸ j) * m            ≡⟨ *-distribʳ-∸ m i j ⟩
  (i * m) ∸ (j * m)      ≡⟨ cong (_∸ j * m) eq ⟩
  (j * m + n) ∸ (j * m)  ≡⟨ cong (_∸ j * m) (+-comm (j * m) n) ⟩
  (n + j * m) ∸ (j * m)  ≡⟨ m+n∸n≡m n (j * m) ⟩
  n                      ∎

lem₁ : ∀ i j → 2 + i ≤′ 2 + j + i
lem₁ i j = ≤⇒≤′ $ s≤s $ s≤s $ n≤m+n j i

lem₂ : ∀ d x {k n} →
       d + x * k ≡ x * n → d + x * (n + k) ≡ 2 * x * n
lem₂ d x {k} {n} eq = begin
  d + x * (n + k)    ≡⟨ distrib-comm₂ d x k n ⟩
  d + x * k + x * n  ≡⟨ cong₂ _+_ eq refl ⟩
  x * n + x * n      ≡⟨ solve 3 (λ x n k → x :* n :+ x :* n
                                       :=  con 2 :* x :* n)
                                 refl x n k ⟩
  2 * x * n          ∎

lem₃ : ∀ d x {i k n} →
       d + (1 + x + i) * k ≡ x * n →
       d + (1 + x + i) * (n + k) ≡ (1 + 2 * x + i) * n
lem₃ d x {i} {k} {n} eq = begin
  d + y * (n + k)      ≡⟨ distrib-comm₂ d y k n ⟩
  d + y * k + y * n    ≡⟨ cong₂ _+_ eq refl ⟩
  x * n + y * n        ≡⟨ solve 3 (λ x n i → x :* n :+ (con 1 :+ x :+ i) :* n
                                         :=  (con 1 :+ con 2 :* x :+ i) :* n)
                                  refl x n i ⟩
  (1 + 2 * x + i) * n  ∎
  where y = 1 + x + i

lem₄ : ∀ d y {k i} n →
       d + y * k ≡ (1 + y + i) * n →
       d + y * (n + k) ≡ (1 + 2 * y + i) * n
lem₄ d y {k} {i} n eq = begin
  d + y * (n + k)          ≡⟨ distrib-comm₂ d y k n ⟩
  d + y * k + y * n        ≡⟨ cong₂ _+_ eq refl ⟩
  (1 + y + i) * n + y * n  ≡⟨ solve 3 (λ y i n → (con 1 :+ y :+ i) :* n :+ y :* n
                                             :=  (con 1 :+ con 2 :* y :+ i) :* n)
                                      refl y i n ⟩
  (1 + 2 * y + i) * n      ∎

lem₅ : ∀ d x {n k} →
       d + x * n ≡ x * k →
       d + 2 * x * n ≡ x * (n + k)
lem₅ d x {n} {k} eq = begin
  d + 2 * x * n      ≡⟨ solve 3 (λ d x n → d :+ con 2 :* x :* n
                                       :=  d :+ x :* n :+ x :* n)
                                refl d x n ⟩
  d + x * n + x * n  ≡⟨ cong₂ _+_ eq refl ⟩
  x * k + x * n      ≡⟨ distrib-comm x k n ⟩
  x * (n + k)        ∎

lem₆ : ∀ d x {n i k} →
       d + x * n ≡ (1 + x + i) * k →
       d + (1 + 2 * x + i) * n ≡ (1 + x + i) * (n + k)
lem₆ d x {n} {i} {k} eq = begin
  d + (1 + 2 * x + i) * n  ≡⟨ solve 4 (λ d x i n → d :+ (con 1 :+ con 2 :* x :+ i) :* n
                                               :=  d :+ x :* n :+ (con 1 :+ x :+ i) :* n)
                                      refl d x i n ⟩
  d + x * n + y * n        ≡⟨ cong₂ _+_ eq refl ⟩
  y * k + y * n            ≡⟨ distrib-comm y k n ⟩
  y * (n + k)              ∎
  where y = 1 + x + i

lem₇ : ∀ d y {i} n {k} →
       d + (1 + y + i) * n ≡ y * k →
       d + (1 + 2 * y + i) * n ≡ y * (n + k)
lem₇ d y {i} n {k} eq = begin
  d + (1 + 2 * y + i) * n      ≡⟨ solve 4 (λ d y i n → d :+ (con 1 :+ con 2 :* y :+ i) :* n
                                                   :=  d :+ (con 1 :+ y :+ i) :* n :+ y :* n)
                                          refl d y i n ⟩
  d + (1 + y + i) * n + y * n  ≡⟨ cong₂ _+_ eq refl ⟩
  y * k + y * n                ≡⟨ distrib-comm y k n ⟩
  y * (n + k)                  ∎

lem₈ : ∀ {i j k q} x y →
       1 + y * j ≡ x * i → j * k ≡ q * i →
       k ≡ (x * k ∸ y * q) * i
lem₈ {i} {j} {k} {q} x y eq eq′ =
  sym (lem₀ (x * k) (y * q) i k lemma)
  where
  lemma = begin
    x * k * i        ≡⟨ solve 3 (λ x k i → x :* k :* i
                                       :=  x :* i :* k)
                                refl x k i ⟩
    x * i * k        ≡⟨ cong (_* k) (sym eq) ⟩
    (1 + y * j) * k  ≡⟨ solve 3 (λ y j k → (con 1 :+ y :* j) :* k
                                       :=  y :* (j :* k) :+ k)
                                refl y j k ⟩
    y * (j * k) + k  ≡⟨ cong (λ n → y * n + k) eq′ ⟩
    y * (q * i) + k  ≡⟨ solve 4 (λ y q i k → y :* (q :* i) :+ k
                                         :=  y :*  q :* i  :+ k)
                                refl y q i k ⟩
    y *  q * i  + k  ∎

lem₉ : ∀ {i j k q} x y →
       1 + x * i ≡ y * j → j * k ≡ q * i →
       k ≡ (y * q ∸ x * k) * i
lem₉ {i} {j} {k} {q} x y eq eq′ =
  sym (lem₀ (y * q) (x * k) i k lemma)
  where
  lem   = solve 3 (λ a b c → a :* b :* c  :=  b :* c :* a) refl
  lemma = begin
    y * q * i        ≡⟨ lem y q i ⟩
    q * i * y        ≡⟨ cong (λ n → n * y) (sym eq′) ⟩
    j * k * y        ≡⟨ sym (lem y j k) ⟩
    y * j * k        ≡⟨ cong (λ n → n * k) (sym eq) ⟩
    (1 + x * i) * k  ≡⟨ solve 3 (λ x i k → (con 1 :+ x :* i) :* k
                                       :=  x :* k :* i :+ k)
                                refl x i k ⟩
    x * k * i + k    ∎

lem₁₀ : ∀ {a′} b c {d} e f → let a = suc a′ in
        a + b * (c * d * a) ≡ e * (f * d * a) →
        d ≡ 1
lem₁₀ {a′} b c {d} e f eq =
  i*j≡1⇒j≡1 (e * f ∸ b * c) d
    (lem₀ (e * f) (b * c) d 1
       (*-cancelʳ-≡ (e * f * d) (b * c * d + 1) (begin
          e * f * d * a        ≡⟨ solve 4 (λ e f d a → e :* f :* d :* a
                                                   :=  e :* (f :* d :* a))
                                          refl e f d a ⟩
          e * (f * d * a)      ≡⟨ sym eq ⟩
          a + b * (c * d * a)  ≡⟨ solve 4 (λ a b c d → a :+ b :* (c :* d :* a)
                                                   :=  (b :* c :* d :+ con 1) :* a)
                                          refl a b c d ⟩
          (b * c * d + 1) * a  ∎)))
  where a = suc a′

lem₁₁ : ∀ {i j m n k d} x y →
       1 + y * j ≡ x * i → i * k ≡ m * d → j * k ≡ n * d →
       k ≡ (x * m ∸ y * n) * d
lem₁₁ {i} {j} {m} {n} {k} {d} x y eq eq₁ eq₂ =
  sym (lem₀ (x * m) (y * n) d k (begin
    x * m * d        ≡⟨ *-assoc x m d ⟩
    x * (m * d)      ≡⟨ cong (x *_) (sym eq₁) ⟩
    x * (i * k)      ≡⟨ sym (*-assoc x i k) ⟩
    x * i * k        ≡⟨ cong₂ _*_ (sym eq) refl ⟩
    (1 + y * j) * k  ≡⟨ solve 3 (λ y j k → (con 1 :+ y :* j) :* k
                                       :=  y :* (j :* k) :+ k)
                                refl y j k ⟩
    y * (j * k) + k  ≡⟨ cong (λ p → y * p + k) eq₂ ⟩
    y * (n * d) + k  ≡⟨ cong₂ _+_ (sym $ *-assoc y n d) refl ⟩
    y * n * d + k    ∎))


text:
-- {-# OPTIONS -v tc.size.solve:100 #-}

open import Agda.Builtin.Size

data Cx (U : Set) : Set where
  ⌀   : Cx U
  _,_ : Cx U → U → Cx U

module _ {U : Set} where
  data _⊆_ : Cx U → Cx U → Set where
    done : ⌀ ⊆ ⌀
    skip : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊆ (Γ′ , A)
    keep : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → (Γ , A) ⊆ (Γ′ , A)

  data _∈_ (A : U) : Cx U → Set where
    top : ∀ {Γ} → A ∈ (Γ , A)
    pop : ∀ {C Γ} → A ∈ Γ → A ∈ (Γ , C)

  mono∈ : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → A ∈ Γ → A ∈ Γ′
  mono∈ done     ()
  mono∈ (skip η) i       = pop (mono∈ η i)
  mono∈ (keep η) top     = top
  mono∈ (keep η) (pop i) = pop (mono∈ η i)

  refl⊆ : ∀ {Γ} → Γ ⊆ Γ
  refl⊆ {⌀}     = done
  refl⊆ {Γ , A} = keep refl⊆

infixr 3 _⊃_
data Ty : Set where
  ι   : Ty
  _⊃_ : Ty → Ty → Ty

infix 1 _⊢⟨_⟩_
data _⊢⟨_⟩_ (Γ : Cx Ty) : Size → Ty → Set where
  var : ∀ {p A}                     → A ∈ Γ → Γ ⊢⟨ p ⟩ A
  lam : ∀ {n A B} {o : Size< n}    → Γ , A ⊢⟨ o ⟩ B → Γ ⊢⟨ n ⟩ A ⊃ B
  app : ∀ {m A B} {l k : Size< m} → Γ ⊢⟨ k ⟩ A ⊃ B → Γ ⊢⟨ l ⟩ A → Γ ⊢⟨ m ⟩ B

mono⊢ : ∀ {m A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢⟨ m ⟩ A → Γ′ ⊢⟨ m ⟩ A
mono⊢ η (var i)   = var (mono∈ η i)
mono⊢ η (lam t)   = lam (mono⊢ (keep η) t)
mono⊢ η (app t u) = app (mono⊢ η t) (mono⊢ η u)

det : ∀ {i A B Γ} {j : Size< i} → Γ ⊢⟨ j ⟩ A ⊃ B → Γ , A ⊢⟨ i ⟩ B
det t = app (mono⊢ (skip refl⊆) t) (var top)

ccont : ∀ {m A B Γ} → Γ ⊢⟨ ↑ ↑ ↑ ↑ m ⟩ (A ⊃ A ⊃ B) ⊃ A ⊃ B
ccont = lam (lam (app (app (var (pop top)) (var top)) (var top)))

cont : ∀ {m A B Γ} {m′ : Size< m} → (Γ , A) , A ⊢⟨ ↑ ↑ m′ ⟩ B → Γ , A ⊢⟨ ↑ ↑ ↑ ↑ ↑ m ⟩ B
cont t = det (app ccont (lam (lam t)))

cont′ : ∀ {q A B Γ} {r : Size< q} → (Γ , A) , A ⊢⟨ {!q!} ⟩ B → Γ , A ⊢⟨ {!!} ⟩ B
cont′ t = det (app ccont (lam (lam t)))

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda