text:
module Cats.Limit where

open import Level

open import Cats.Category.Base
open import Cats.Category.Cones using
  (Cone ; Cones ; HasObj-Cone ; HasArrow-⇒ ; cone-iso→obj-iso ; apFunctor)
open import Cats.Functor using (Functor)
open import Cats.Util.Conv

import Cats.Category.Constructions.Terminal as Terminal
import Cats.Category.Constructions.Iso as Iso

module _ {lo la l≈ lo′ la′ l≈′}
  {J : Category lo la l≈}
  {Z : Category lo′ la′ l≈′}
  where

  IsLimit : {D : Functor J Z} → Cone D → Set (lo ⊔ la ⊔ lo′ ⊔ la′ ⊔ l≈′)
  IsLimit {D} = Terminal.Build.IsTerminal (Cones D)

  record Limit (D : Functor J Z) : Set (lo ⊔ la ⊔ lo′ ⊔ la′ ⊔ l≈′) where
    field
      cone : Cone D
      isLimit : IsLimit cone

  instance
    HasObj-Limit : ∀ D → HasObj (Limit D) _ _ _
    HasObj-Limit D = record { Cat = Cones D ; _ᴼ = Limit.cone }

  module _ {D : Functor J Z} where

    open Iso.Build (Cones D) using (_≅_)
    open Iso.Build Z using () renaming (_≅_ to _≅Z_)
    open Limit using (isLimit)

    unique : (l m : Limit D) → l ᴼ ≅ m ᴼ
    unique l m = Terminal.Build.terminal-unique (Cones D) (isLimit l) (isLimit m)

    obj-unique : (l m : Limit D) → l ᴼ ᴼ ≅Z m ᴼ ᴼ
    obj-unique l m = cone-iso→obj-iso _ (unique l m)

module _ {lo la l≈ lo′ la′ l≈′}
  {C : Category lo la l≈}
  {D : Category lo′ la′ l≈′}
  where

  preservesLimits : (lo″ la″ l≈″ : Level) → (F : Functor C D) → Set _
  preservesLimits lo″ la″ l≈″ F
      = {J : Category lo″ la″ l≈″}
      → {D : Functor J C}
      → {c : Cone D}
      → IsLimit c
      → IsLimit (apFunctor F c)

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


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

open import HoTT

module groups.CoefficientExtensionality {i} {A : Type i} where

module _ (dec : has-dec-eq A) where

  Word-coef : Word A → (A → ℤ)
  Word-coef nil a = 0
  Word-coef (inl a' :: w) a with dec a' a
  Word-coef (inl a' :: w) a | inl a'=a = succ $ Word-coef w a
  Word-coef (inl a' :: w) a | inr a'≠a = Word-coef w a
  Word-coef (inr a' :: w) a with dec a' a
  Word-coef (inr a' :: w) a | inl a'=a = pred $ Word-coef w a
  Word-coef (inr a' :: w) a | inr a'≠a = Word-coef w a

  abstract
    Word-coef-++ : ∀ w₁ w₂ a → Word-coef (w₁ ++ w₂) a
      == Word-coef w₁ a ℤ+ Word-coef w₂ a
    Word-coef-++ nil w₂ a = idp
    Word-coef-++ (inl a' :: w₁) w₂ a with dec a' a
    Word-coef-++ (inl a' :: w₁) w₂ a | inl a'=a =
        ap succ (Word-coef-++ w₁ w₂ a)
      ∙ ! (succ-+ (Word-coef w₁ a) (Word-coef w₂ a))
    Word-coef-++ (inl a' :: w₁) w₂ a | inr a'≠a = Word-coef-++ w₁ w₂ a
    Word-coef-++ (inr a' :: w₁) w₂ a with dec a' a
    Word-coef-++ (inr a' :: w₁) w₂ a | inl a'=a =
        ap pred (Word-coef-++ w₁ w₂ a)
      ∙ ! (pred-+ (Word-coef w₁ a) (Word-coef w₂ a))
    Word-coef-++ (inr a' :: w₁) w₂ a | inr a'≠a = Word-coef-++ w₁ w₂ a

    Word-coef-flip : ∀ w a → Word-coef (Word-flip w) a == ℤ~ (Word-coef w a)
    Word-coef-flip nil a = idp
    Word-coef-flip (inl a' :: w) a with dec a' a
    Word-coef-flip (inl a' :: w) a | inl a'=a =
        ap pred (Word-coef-flip w a) ∙ ! (ℤ~-succ (Word-coef w a))
    Word-coef-flip (inl a' :: w) a | inr a'≠a = Word-coef-flip w a
    Word-coef-flip (inr a' :: w) a with dec a' a
    Word-coef-flip (inr a' :: w) a | inl a'=a =
        ap succ (Word-coef-flip w a) ∙ ! (ℤ~-pred (Word-coef w a))
    Word-coef-flip (inr a' :: w) a | inr a'≠a = Word-coef-flip w a

  private
    abstract
      FormalSum-coef-rel : {w₁ w₂ : Word A} → FormalSumRel w₁ w₂
        → ∀ a → Word-coef w₁ a == Word-coef w₂ a
      FormalSum-coef-rel (fsr-refl p) a = ap (λ w → Word-coef w a) p
      FormalSum-coef-rel (fsr-trans fwr₁ fwr₂) a = (FormalSum-coef-rel fwr₁ a) ∙ (FormalSum-coef-rel fwr₂ a)
      FormalSum-coef-rel (fsr-sym fsr) a = ! $ FormalSum-coef-rel fsr a
      FormalSum-coef-rel (fsr-cons x fwr) a =
          Word-coef-++ (x :: nil) _ a
        ∙ ap (Word-coef (x :: nil) a ℤ+_) (FormalSum-coef-rel fwr a)
        ∙ ! (Word-coef-++ (x :: nil) _ a)
      FormalSum-coef-rel (fsr-swap x y w) a =
          Word-coef-++ (x :: y :: nil) _ a
        ∙ ap (_ℤ+ Word-coef w a)
            ( Word-coef-++ (x :: nil) (y :: nil) a
            ∙ ℤ+-comm (Word-coef (x :: nil) a) (Word-coef (y :: nil) a)
            ∙ ! (Word-coef-++ (y :: nil) (x :: nil) a))
        ∙ ! (Word-coef-++ (y :: x :: nil) _ a)
      FormalSum-coef-rel (fsr-flip x w) a =
          Word-coef-++ (x :: flip x :: nil) w a
        ∙ ap (_ℤ+ Word-coef w a)
            ( Word-coef-++ (x :: nil) (flip x :: nil) a
            ∙ ap (Word-coef (x :: nil) a ℤ+_) (Word-coef-flip (x :: nil) a)
            ∙ ℤ~-inv-r (Word-coef (x :: nil) a) )
        ∙ ℤ+-unit-l (Word-coef w a)

  FormalSum-coef : FormalSum A → (A → ℤ)
  FormalSum-coef = FormalSum-rec (→-is-set ℤ-is-set) Word-coef (λ r → λ= $ FormalSum-coef-rel r)

  -- Theorem : if coef w a == 0 then FormalSumRel w nil

  private
    exp : A → ℤ → Word A
    exp a (pos 0) = nil
    exp a (pos (S n)) = inl a :: exp a (pos n)
    exp a (negsucc 0) = inr a :: nil
    exp a (negsucc (S n)) = inr a :: exp a (negsucc n)

    abstract
      exp-succ : ∀ a z → FormalSumRel (inl a :: exp a z) (exp a (succ z))
      exp-succ a (pos _) = fsr-refl idp
      exp-succ a (negsucc 0) = fsr-flip (inl a) nil
      exp-succ a (negsucc (S n)) = fsr-flip (inl a) (exp a (negsucc n))

      exp-pred : ∀ a z → FormalSumRel (inr a :: exp a z) (exp a (pred z))
      exp-pred a (pos 0) = fsr-refl idp
      exp-pred a (pos (S n)) = fsr-flip (inr a) (exp a (pos n))
      exp-pred a (negsucc _) = fsr-refl idp

      Word-coef-inl-eq : ∀ {a b} (p : b == a) w
        → Word-coef (inl b :: w) a == succ (Word-coef w a)
      Word-coef-inl-eq {a} {b} p w with dec b a
      Word-coef-inl-eq {a} {b} p w | inl _ = idp
      Word-coef-inl-eq {a} {b} p w | inr ¬p = ⊥-rec (¬p p)

      Word-coef-inr-eq : ∀ {a b} (p : b == a) w
        → Word-coef (inr b :: w) a == pred (Word-coef w a)
      Word-coef-inr-eq {a} {b} p w with dec b a
      Word-coef-inr-eq {a} {b} p w | inl _ = idp
      Word-coef-inr-eq {a} {b} p w | inr ¬p = ⊥-rec (¬p p)

      Word-coef-inl-neq : ∀ {a b} (p : b ≠ a) w
        → Word-coef (inl b :: w) a == Word-coef w a
      Word-coef-inl-neq {a} {b} ¬p w with dec b a
      Word-coef-inl-neq {a} {b} ¬p w | inl p = ⊥-rec (¬p p)
      Word-coef-inl-neq {a} {b} ¬p w | inr _ = idp

      Word-coef-inr-neq : ∀ {a b} (p : b ≠ a) w
        → Word-coef (inr b :: w) a == Word-coef w a
      Word-coef-inr-neq {a} {b} ¬p w with dec b a
      Word-coef-inr-neq {a} {b} ¬p w | inl p = ⊥-rec (¬p p)
      Word-coef-inr-neq {a} {b} ¬p w | inr _ = idp

    -- TODO maybe there is a better way to prove the final theorem?
    -- Here we are collecting all elements [inl a] and [inr a], and recurse on the rest.
    -- The [right-shorter] field makes sure that it is terminating.
    record CollectSplitIH (a : A) {n : ℕ} (w : Word A) (len : length w == n) : Type i where
      field
        left-exponent : ℤ
        left-captures-all : Word-coef w a == left-exponent
        right-list : Word A
        right-shorter : length right-list ≤ n
        fsr : FormalSumRel w (exp a left-exponent ++ right-list)

    abstract
      collect-split : ∀ a {n} w (len=n : length w == n) → CollectSplitIH a w len=n
      collect-split a nil idp = record {
        left-exponent = 0;
        left-captures-all = idp;
        right-list = nil;
        right-shorter = inl idp;
        fsr = fsr-refl idp}
      collect-split a (inl b :: w) idp with dec b a
      ... | inl b=a = record {
        left-exponent = succ left-exponent;
        left-captures-all = Word-coef-inl-eq b=a w ∙ ap succ left-captures-all;
        right-list = right-list;
        right-shorter = ≤-trans right-shorter (inr ltS);
        fsr = fsr-trans (fsr-refl (ap (λ a → inl a :: w) b=a)) $
              fsr-trans (fsr-cons (inl a) fsr) $
                        (FormalSumRel-cong-++-l (exp-succ a left-exponent) right-list)}
        where open CollectSplitIH (collect-split a w idp)
      ... | inr b≠a = record {
        left-exponent = left-exponent;
        left-captures-all = Word-coef-inl-neq b≠a w ∙ left-captures-all;
        right-list = inl b :: right-list;
        right-shorter = ≤-ap-S right-shorter;
        fsr = fsr-trans (fsr-cons (inl b) fsr) $
          fsr-sym (FormalSumRel-swap1 (inl b) (exp a left-exponent) right-list)}
        where open CollectSplitIH (collect-split a w idp)
      collect-split a (inr b :: w) idp with dec b a
      ... | inl b=a = record {
        left-exponent = pred left-exponent;
        left-captures-all = Word-coef-inr-eq b=a w ∙ ap pred left-captures-all;
        right-list = right-list;
        right-shorter = ≤-trans right-shorter (inr ltS);
        fsr = fsr-trans (fsr-refl (ap (λ a → inr a :: w) b=a)) $
              fsr-trans (fsr-cons (inr a) fsr) $
                        (FormalSumRel-cong-++-l (exp-pred a left-exponent) right-list)}
        where open CollectSplitIH (collect-split a w idp)
      ... | inr b≠a = record {
        left-exponent = left-exponent;
        left-captures-all = Word-coef-inr-neq b≠a w ∙ left-captures-all;
        right-list = inr b :: right-list;
        right-shorter = ≤-ap-S right-shorter;
        fsr = fsr-trans (fsr-cons (inr b) fsr) $
          fsr-sym (FormalSumRel-swap1 (inr b) (exp a left-exponent) right-list)}
        where open CollectSplitIH (collect-split a w idp)

      -- We simulate strong induction by recursing on both [m] and [n≤m].
      -- We could develop a general framework for strong induction but I am lazy. -Favonia
      zero-coef-is-ident' : ∀ {m n} (n≤m : n ≤ m) (w : Word A) (len : length w == n)
        → (∀ a → Word-coef w a == 0) → FormalSumRel w nil
      zero-coef-is-ident' (inr ltS) w len zero-coef
        = zero-coef-is-ident' (inl idp) w len zero-coef
      zero-coef-is-ident' (inr (ltSR lt)) w len zero-coef
        = zero-coef-is-ident' (inr lt) w len zero-coef
      zero-coef-is-ident' {m = O} (inl idp) nil _ _ = fsr-refl idp
      zero-coef-is-ident' {m = O} (inl idp) (_ :: _) len _ = ⊥-rec $ ℕ-S≠O _ len
      zero-coef-is-ident' {m = S m} (inl idp) nil len _ = ⊥-rec $ ℕ-S≠O _ (! len)
      zero-coef-is-ident' {m = S m} (inl idp) (inl a :: w) len zero-coef =
        fsr-trans whole-is-right (zero-coef-is-ident' right-shorter right-list idp right-zero-coef)
        where
          open CollectSplitIH (collect-split a w (ℕ-S-is-inj _ _ len))
          left-exponent-is-minus-one : left-exponent == -1
          left-exponent-is-minus-one = succ-is-inj left-exponent -1 $
            ap succ (! left-captures-all) ∙ ! (Word-coef-inl-eq idp w) ∙ zero-coef a

          whole-is-right : FormalSumRel (inl a :: w) right-list
          whole-is-right =
            fsr-trans (fsr-cons (inl a) fsr) $
            fsr-trans (fsr-refl (ap (λ e → inl a :: exp a e ++ right-list) left-exponent-is-minus-one)) $
                      fsr-flip (inl a) right-list

          right-zero-coef : ∀ a' → Word-coef right-list a' == 0
          right-zero-coef a' = ! (FormalSum-coef-rel whole-is-right a') ∙ zero-coef a'
      zero-coef-is-ident' {m = S m} (inl idp) (inr a :: w) len zero-coef =
        fsr-trans whole-is-right (zero-coef-is-ident' right-shorter right-list idp right-zero-coef)
        where
          open CollectSplitIH (collect-split a w (ℕ-S-is-inj _ _ len))
          left-exponent-is-one : left-exponent == 1
          left-exponent-is-one = pred-is-inj left-exponent 1 $
            ap pred (! left-captures-all) ∙ ! (Word-coef-inr-eq idp w) ∙ zero-coef a

          whole-is-right : FormalSumRel (inr a :: w) right-list
          whole-is-right =
            fsr-trans (fsr-cons (inr a) fsr) $
            fsr-trans (fsr-refl (ap (λ e → inr a :: exp a e ++ right-list) left-exponent-is-one)) $
                      fsr-flip (inr a) right-list

          right-zero-coef : ∀ a' → Word-coef right-list a' == 0
          right-zero-coef a' = ! (FormalSum-coef-rel whole-is-right a') ∙ zero-coef a'

      zero-coef-is-ident : ∀ (w : Word A)
        → (∀ a → Word-coef w a == 0)
        → FormalSumRel w nil
      zero-coef-is-ident w = zero-coef-is-ident' (inl idp) w idp

  abstract
    FormalSum-coef-ext' : ∀ w₁ w₂
      → (∀ a → Word-coef w₁ a == Word-coef w₂ a)
      → fs[ w₁ ] == fs[ w₂ ]
    FormalSum-coef-ext' w₁ w₂ same-coef = G.inv-is-inj fs[ w₁ ] fs[ w₂ ] $
      G.inv-unique-l (G.inv fs[ w₂ ]) fs[ w₁ ] $ quot-rel $
      zero-coef-is-ident (Word-flip w₂ ++ w₁)
        (λ a → Word-coef-++ (Word-flip w₂) w₁ a
             ∙ ap2 _ℤ+_ (Word-coef-flip w₂ a) (same-coef a)
             ∙ ℤ~-inv-l (Word-coef w₂ a))
      where module G = FreeAbGroup A

    FormalSum-coef-ext : ∀ fs₁ fs₂
      → (∀ a → FormalSum-coef fs₁ a == FormalSum-coef fs₂ a)
      → fs₁ == fs₂
    FormalSum-coef-ext = FormalSum-elim
      (λ fs₁ → Π-is-set λ fs₂ → →-is-set $ =-preserves-set FormalSum-is-set)
      (λ w₁ → FormalSum-elim
        (λ fs₂ → →-is-set $ =-preserves-set FormalSum-is-set)
        (λ w₂ → FormalSum-coef-ext' w₁ w₂)
        (λ _ → prop-has-all-paths-↓ (→-is-prop $ FormalSum-is-set _ _)))
      (λ _ → prop-has-all-paths-↓ (Π-is-prop λ _ → →-is-prop $ FormalSum-is-set _ _))

  has-finite-support : (A → ℤ) → Type i
  has-finite-support f = Σ (FormalSum A) λ fs → ∀ a → f a == FormalSum-coef fs a

module _ {dec : has-dec-eq A} where

  abstract
    has-finite-support-is-prop : ∀ f → is-prop (has-finite-support dec f)
    has-finite-support-is-prop f = all-paths-is-prop
      λ{(fs₁ , match₁) (fs₂ , match₂) → pair=
        (FormalSum-coef-ext dec fs₁ fs₂ λ a → ! (match₁ a) ∙ match₂ a)
        (prop-has-all-paths-↓ $ Π-is-prop λ _ → ℤ-is-set _ _)}

ext: agda

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


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

open import lib.Basics
open import lib.NConnected
open import lib.types.Bool
open import lib.types.Nat
open import lib.types.TLevel
open import lib.types.Suspension

module lib.types.IteratedSuspension where

⊙Susp^ : ∀ {i} (n : ℕ) → Ptd i → Ptd i
⊙Susp^ O X = X
⊙Susp^ (S n) X = ⊙Susp (⊙Susp^ n X)

abstract
  ⊙Susp^-conn : ∀ {i} (n : ℕ) {X : Ptd i} {m : ℕ₋₂}
    {{_ : is-connected m (de⊙ X)}} → is-connected (⟨ n ⟩₋₂ +2+ m) (de⊙ (⊙Susp^ n X))
  ⊙Susp^-conn O = ⟨⟩
  ⊙Susp^-conn (S n) = Susp-conn (⊙Susp^-conn n)

  ⊙Susp^-conn' : ∀ {i} (n : ℕ) {X : Ptd i}
    {{_ : is-connected 0 (de⊙ X)}} → is-connected ⟨ n ⟩ (de⊙ (⊙Susp^ n X))
  ⊙Susp^-conn' O = ⟨⟩
  ⊙Susp^-conn' (S n) = Susp-conn (⊙Susp^-conn' n)

⊙Susp^-+ : ∀ {i} (m n : ℕ) {X : Ptd i}
  → ⊙Susp^ m (⊙Susp^ n X) == ⊙Susp^ (m + n) X
⊙Susp^-+ O n = idp
⊙Susp^-+ (S m) n = ap ⊙Susp (⊙Susp^-+ m n)

⊙Susp^-fmap : ∀ {i j} (n : ℕ) {X : Ptd i} {Y : Ptd j}
  → X ⊙→ Y → ⊙Susp^ n X ⊙→ ⊙Susp^ n Y
⊙Susp^-fmap O f = f
⊙Susp^-fmap (S n) f = ⊙Susp-fmap (⊙Susp^-fmap n f)

⊙Susp^-fmap-idf : ∀ {i} (n : ℕ) (X : Ptd i)
  → ⊙Susp^-fmap n (⊙idf X) == ⊙idf (⊙Susp^ n X)
⊙Susp^-fmap-idf O X = idp
⊙Susp^-fmap-idf (S n) X =
  ap ⊙Susp-fmap (⊙Susp^-fmap-idf n X) ∙ ⊙Susp-fmap-idf (⊙Susp^ n X)

⊙Susp^-fmap-cst : ∀ {i j} (n : ℕ) {X : Ptd i} {Y : Ptd j}
  → ⊙Susp^-fmap n (⊙cst {X = X} {Y = Y}) == ⊙cst
⊙Susp^-fmap-cst O = idp
⊙Susp^-fmap-cst (S n) = ap ⊙Susp-fmap (⊙Susp^-fmap-cst n)
                           ∙ (⊙Susp-fmap-cst {X = ⊙Susp^ n _})

⊙Susp^-fmap-∘ : ∀ {i j k} (n : ℕ) {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  (g : Y ⊙→ Z) (f : X ⊙→ Y)
  → ⊙Susp^-fmap n (g ⊙∘ f) == ⊙Susp^-fmap n g ⊙∘ ⊙Susp^-fmap n f
⊙Susp^-fmap-∘ O g f = idp
⊙Susp^-fmap-∘ (S n) g f =
  ap ⊙Susp-fmap (⊙Susp^-fmap-∘ n g f)
  ∙ ⊙Susp-fmap-∘ (⊙Susp^-fmap n g) (⊙Susp^-fmap n f)

⊙Susp^-Susp-split-iso : ∀ {i} (n : ℕ) (X : Ptd i)
  → ⊙Susp^ (S n) X ⊙≃ ⊙Susp^ n (⊙Susp X)
⊙Susp^-Susp-split-iso O     X = ⊙ide _
⊙Susp^-Susp-split-iso (S n) X = ⊙Susp-emap (⊙Susp^-Susp-split-iso n X)

⊙Sphere : (n : ℕ) → Ptd₀
⊙Sphere n = ⊙Susp^ n ⊙Bool

Sphere : (n : ℕ) → Type₀
Sphere n = de⊙ (⊙Sphere n)

abstract
  instance
    Sphere-conn : ∀ (n : ℕ) → is-connected ⟨ n ⟩₋₁ (Sphere n)
    Sphere-conn 0 = inhab-conn true
    Sphere-conn (S n) = Susp-conn (Sphere-conn n)

-- favonia: [S¹] has its own elim rules in Circle.agda.
⊙S⁰ = ⊙Sphere 0
⊙S¹ = ⊙Sphere 1
⊙S² = ⊙Sphere 2
⊙S³ = ⊙Sphere 3
S⁰ = Sphere 0
S¹ = Sphere 1
S² = Sphere 2
S³ = Sphere 3

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
{-

Basic theory about h-levels/n-types:

- Basic properties of isContr, isProp and isSet (definitions are in Prelude)

- Hedberg's theorem can be found in Cubical/Relation/Nullary/DecidableEq

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.Foundations.HLevels where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.FunExtEquiv
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Transport
open import Cubical.Foundations.HAEquiv      using (congEquiv)
open import Cubical.Foundations.Equiv        using (isoToEquiv; isPropIsEquiv; retEq; invEquiv)
open import Cubical.Foundations.Univalence   using (ua; univalence)

open import Cubical.Data.Sigma  using (ΣPathP; sigmaPath→pathSigma; pathSigma≡sigmaPath; _Σ≡T_)
open import Cubical.Data.Nat    using (ℕ; zero; suc; _+_; +-comm)

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ
    B : A → Type ℓ
    x y : A
    n : ℕ

hProp : Type (ℓ-suc ℓ)
hProp {ℓ} = Σ (Type ℓ) isProp

isOfHLevel : ℕ → Type ℓ → Type ℓ
isOfHLevel 0 A = isContr A
isOfHLevel 1 A = isProp A
isOfHLevel (suc (suc n)) A = (x y : A) → isOfHLevel (suc n) (x ≡ y)

isOfHLevelDep : ℕ → {A : Type ℓ} (B : A → Type ℓ') → Type (ℓ-max ℓ ℓ')
isOfHLevelDep 0 {A = A} B = {a : A} → B a
isOfHLevelDep 1 {A = A} B = {a0 a1 : A} (b0 : B a0) (b1 : B a1) (p : a0 ≡ a1)  → PathP (λ i → B (p i)) b0 b1
isOfHLevelDep (suc (suc  n)) {A = A} B = {a0 a1 : A} (b0 : B a0) (b1 : B a1) → isOfHLevelDep (suc n) {A = a0 ≡ a1} (λ p → PathP (λ i → B (p i)) b0 b1)

isOfHLevel→isOfHLevelDep : {n : ℕ} → {A : Type ℓ} {B : A → Type ℓ'} (h : (a : A) → isOfHLevel n (B a)) → isOfHLevelDep n {A = A} B
isOfHLevel→isOfHLevelDep {n = 0} {A = A} {B} h {a} = h a .fst
isOfHLevel→isOfHLevelDep {n = 1} {A = A} {B} h = λ b0 b1 p → isProp→PathP h p b0 b1
isOfHLevel→isOfHLevelDep {n = suc (suc n)} {A = A} {B} h {a0} {a1} b0 b1 =
  isOfHLevel→isOfHLevelDep {n = suc n}
    {B = λ p → PathP (λ i → B (p i)) b0 b1} λ p → helper a1 p b1
    where
      helper : (a1 : A) (p : a0 ≡ a1) (b1 : B a1) →
        isOfHLevel (suc n) (PathP (λ i → B (p i)) b0 b1)
      helper a1 p b1 = J
                         (λ a1 p → ∀ b1 → isOfHLevel (suc n) (PathP (λ i → B (p i)) b0 b1))
                         (λ _ → h _ _ _) p b1

HLevel : ℕ → Type (ℓ-suc ℓ)
HLevel {ℓ} n = Σ[ A ∈ Type ℓ ] (isOfHLevel n A)

inhProp→isContr : A → isProp A → isContr A
inhProp→isContr x h = x , h x

isPropIsProp : isProp (isProp A)
isPropIsProp f g i a b = isProp→isSet f a b (f a b) (g a b) i

-- A retract of a contractible type is contractible
retractIsContr
  : ∀ {B : Type ℓ}
  → (f : A → B) (g : B → A)
  → (h : (x : A) → g (f x) ≡ x)
  → (v : isContr B) → isContr A
retractIsContr f g h (b , p) = (g b , λ x → (cong g (p (f x))) ∙ (h x))

retractIsProp
  : {B : Type ℓ}
  (f : A → B) (g : B → A)
  (h : (x : A) → g (f x) ≡ x)
  → isProp B → isProp A
retractIsProp f g h p x y i =
  hcomp
    (λ j → λ
      { (i = i0) → h x j
      ; (i = i1) → h y j})
    (g (p (f x) (f y) i))

retractIsOfHLevel
  : (n : ℕ) {B : Type ℓ}
  (f : A → B) (g : B → A)
  (h : (x : A) → g (f x) ≡ x)
  → isOfHLevel n B → isOfHLevel n A
retractIsOfHLevel 0 = retractIsContr
retractIsOfHLevel 1 = retractIsProp
retractIsOfHLevel (suc (suc n)) f g h ofLevel x y =
  retractIsOfHLevel (suc n)
    (cong f)
    (λ q i →
      hcomp
        (λ j → λ
          { (i = i0) → h x j
          ; (i = i1) → h y j})
        (g (q i)))
    (λ p k i →
      hcomp
        (λ j → λ
          { (i = i0) → h x (j ∨ k)
          ; (i = i1) → h y (j ∨ k)
          ; (k = i1) → p i})
        (h (p i) k))
    (ofLevel (f x) (f y))

isContrSigma
  : isContr A
  → ((x : A) → isContr (B x))
  → isContr (Σ[ x ∈ A ] B x)
isContrSigma {A = A} {B = B} (a , p) q =
  let h : (x : A) (y : B x) → (q x) .fst ≡ y
      h x y = (q x) .snd y
  in (( a , q a .fst)
     , ( λ x i → p (x .fst) i
       , h (p (x .fst) i) (transp (λ j → B (p (x .fst) (i ∨ ~ j))) i (x .snd)) i))

isProp→isPropPathP : (∀ a → isProp (B a))
                   → (m : x ≡ y) (g : B x) (h : B y)
                   → isProp (PathP (λ i → B (m i)) g h)
isProp→isPropPathP {B = B} {x = x} isPropB m = J P d m where
  P : ∀ σc → x ≡ σc → _
  P _ m = ∀ g h → isProp (PathP (λ i → B (m i)) g h)
  d : P x refl
  d = isProp→isSet (isPropB x)

isProp→isContrPathP : (∀ a → isProp (B a))
                    → (m : x ≡ y) (g : B x) (h : B y)
                    → isContr (PathP (λ i → B (m i)) g h)
isProp→isContrPathP isPropB m g h =
  inhProp→isContr (isProp→PathP isPropB m g h) (isProp→isPropPathP isPropB m g h)

isProp→isContr≡ : isProp A → (x y : A) → isContr (x ≡ y)
isProp→isContr≡ isPropA x y = inhProp→isContr (isPropA x y) (isProp→isSet isPropA x y)

isContrPath : isContr A → (x y : A) → isContr (x ≡ y)
isContrPath cA = isProp→isContr≡ (isContr→isProp cA)

-- Π preserves propositionality in the following sense:
propPi : (h : (x : A) → isProp (B x)) → isProp ((x : A) → B x)
propPi h f0 f1 i x = h x (f0 x) (f1 x) i

ΣProp≡
  : ((x : A) → isProp (B x)) → {u v : Σ[ a ∈ A ] B a}
  → (p : u .fst ≡ v .fst) → u ≡ v
ΣProp≡ pB {u} {v} p i = (p i) , isProp→PathP pB p (u .snd) (v .snd) i

isPropSigma : isProp A → ((x : A) → isProp (B x)) → isProp (Σ[ x ∈ A ] B x)
isPropSigma pA pB t u = ΣProp≡ pB (pA (t .fst) (u .fst))

hLevelPi
  : ∀ n
  → ((x : A) → isOfHLevel n (B x))
  → isOfHLevel n ((x : A) → B x)
hLevelPi 0 h = (λ x → fst (h x)) , λ f i y → snd (h y) (f y) i
hLevelPi {B = B} 1 h f g i x = (h x) (f x) (g x) i
hLevelPi (suc (suc n)) h f g =
  subst (isOfHLevel (suc n)) funExtPath (hLevelPi (suc n) λ x → h x (f x) (g x))

isSetPi : ((x : A) → isSet (B x)) → isSet ((x : A) → B x)
isSetPi Bset = hLevelPi 2 (λ a → Bset a)

isSet→isSet' : isSet A → isSet' A
isSet→isSet' {A = A} Aset {x} {y} {z} {w} p q r s
  = transport (squeezeSq≡ r p q s) (Aset _ _ p (r ∙∙ q ∙∙ sym s))

isSet'→isSet : isSet' A → isSet A
isSet'→isSet {A = A} Aset' x y p q = Aset' p q refl refl

squeezeCu≡
  : ∀{w x y z w' x' y' z' : A}
  → {p : w ≡ y} {q : w ≡ x} {r : y ≡ z} {s : x ≡ z}
  → {p' : w' ≡ y'} {q' : w' ≡ x'} {r' : y' ≡ z'} {s' : x' ≡ z'}
  → {a : w ≡ w'} {b : x ≡ x'} {c : y ≡ y'} {d : z ≡ z'}
  → (ps : Square a p p' c) (qs : Square a q q' b)
  → (rs : Square c r r' d) (ss : Square b s s' d)
  → (f0 : Square p q r s) (f1 : Square p' q' r' s')
  → (f0 ≡ transport⁻ (λ k → Square (ps k) (qs k) (rs k) (ss k)) f1)
  ≡ Cube ps qs rs ss f0 f1
squeezeCu≡ ps qs rs ss f0 f1 τ
  = Cube
      (λ j → ps (j ∧ τ))
      (λ j → qs (j ∧ τ))
      (λ j → rs (j ∧ τ))
      (λ j → ss (j ∧ τ))
      f0
      (toPathP {A = λ k → Square (ps k) (qs k) (rs k) (ss k)}
         (transportTransport⁻ (λ k → Square (ps k) (qs k) (rs k) (ss k)) f1) τ)

isGroupoid→isGroupoid' : isGroupoid A → isGroupoid' A
isGroupoid→isGroupoid' Agpd ps qs rs ss f0 f1
  = transport
      ( squeezeCu≡ (λ _ → refl) f0 f1' (λ _ → refl) (λ _ → f0 i0) (λ _ → f1' i1)
      ∙ transpose≡
      ∙ squeezeCu≡ ps qs rs ss f0 f1
      ) (Agpd (ps i0 i0) (ss i0 i0) (f0 i0) (f1' i0) refl rs')
  where
  Sq = λ k → Square (ps k) (qs k) (rs k) (ss k)
  f1' = transport⁻ Sq f1
  rs' = transport⁻ (λ k → Square refl (f0 k) (f1' k) refl) (λ _ → f1' i1)
  transpose≡
    : Cube (λ i _ → ps i0 i) f0 f1' (λ i _ → ss i0 i) refl refl
    ≡ Cube refl refl refl refl f0 f1'
  transpose≡
    = ua ((λ cu i j → cu j i)
    , λ where
        .equiv-proof cu
          → ((λ i j → cu j i) , refl)
          , (λ{ (cu' , p) → λ k → (λ j i → p (~ k) i j) , λ τ → p (~ k ∨ τ) }))

isGroupoid'→isGroupoid : isGroupoid' A → isGroupoid A
isGroupoid'→isGroupoid Agpd' w x p q r s
  = Agpd' {q = p} {r = q} {q' = p} {r' = q} refl refl refl refl r s

hLevelSuc : (n : ℕ) (A : Type ℓ) → isOfHLevel n A → isOfHLevel (suc n) A
hLevelSuc 0 A = isContr→isProp
hLevelSuc 1 A = isProp→isSet
hLevelSuc (suc (suc n)) A h a b = hLevelSuc (suc n) (a ≡ b) (h a b)

hLevelLift : (m : ℕ) (hA : isOfHLevel n A) → isOfHLevel (m + n) A
hLevelLift zero hA = hA
hLevelLift {A = A} (suc m) hA = hLevelSuc _ A (hLevelLift m hA)

isPropIsOfHLevel : (n : ℕ) (A : Type ℓ) → isProp (isOfHLevel n A)
isPropIsOfHLevel 0 A = isPropIsContr
isPropIsOfHLevel 1 A = isPropIsProp
isPropIsOfHLevel (suc (suc n)) A f g i a b =
  isPropIsOfHLevel (suc n) (a ≡ b) (f a b) (g a b) i

isPropIsSet : isProp (isSet A)
isPropIsSet {A = A} = isPropIsOfHLevel 2 A

HLevel≡ : ∀ {A B : Type ℓ} {hA : isOfHLevel n A} {hB : isOfHLevel n B} →
          (A ≡ B) ≡ ((A , hA) ≡ (B , hB))
HLevel≡ {n = n} {A = A} {B = B} {hA} {hB} =
 isoToPath (iso intro elim intro-elim elim-intro)
  where
    intro : A ≡ B → (A , hA) ≡ (B , hB)
    intro eq = ΣProp≡ (λ A → isPropIsOfHLevel n _) eq

    elim : (A , hA) ≡ (B , hB) → A ≡ B
    elim = cong fst

    intro-elim : ∀ x → intro (elim x) ≡ x
    intro-elim eq = cong ΣPathP (ΣProp≡ (λ e →
      J (λ B e →
           ∀ k → (x y : PathP (λ i → isOfHLevel n (e i)) hA k) → x ≡ y)
        (λ k → isProp→isSet (isPropIsOfHLevel n _) _ _) e hB) refl)

    elim-intro : ∀ x → elim (intro x) ≡ x
    elim-intro eq = refl

-- H-level for Σ-types

isOfHLevelΣ : ∀ n → isOfHLevel n A → ((x : A) → isOfHLevel n (B x))
  → isOfHLevel n (Σ A B)
isOfHLevelΣ zero h1 h2 =
  let center = (fst h1 , fst (h2 (fst h1))) in
  let p : ∀ x → center ≡ x
      p = λ x → sym (sigmaPath→pathSigma _ _ (sym (snd h1 (fst x)) , sym (snd (h2 (fst h1)) _)))
  in (center , p)
isOfHLevelΣ 1 h1 h2 x y = sigmaPath→pathSigma x y ((h1 _ _) , (h2 _ _ _))
isOfHLevelΣ {B = B} (suc (suc n)) h1 h2 x y =
  let h3 : isOfHLevel (suc n) (x Σ≡T y)
      h3 = isOfHLevelΣ (suc n) (h1 (fst x) (fst y)) λ p → h2 (p i1)
                       (subst B p (snd x)) (snd y)
  in transport (λ i → isOfHLevel (suc n) (pathSigma≡sigmaPath x y (~ i))) h3

hLevel≃ : ∀ n → {A B : Type ℓ} (hA : isOfHLevel n A) (hB : isOfHLevel n B) → isOfHLevel n (A ≃ B)
hLevel≃ zero {A = A} {B = B} hA hB = A≃B , contr
  where
  A≃B : A ≃ B
  A≃B = isoToEquiv (iso (λ _ → fst hB) (λ _ → fst hA) (snd hB ) (snd hA))

  contr : (y : A ≃ B) → A≃B ≡ y
  contr y = ΣProp≡ isPropIsEquiv (funExt (λ a → snd hB (fst y a)))

hLevel≃ (suc n) hA hB =
  isOfHLevelΣ (suc n) (hLevelPi (suc n) (λ _ → hB))
              (λ a → subst (λ n → isOfHLevel n (isEquiv a)) (+-comm n 1) (hLevelLift n (isPropIsEquiv a)))

hLevelRespectEquiv : {A : Type ℓ} {B : Type ℓ'} → (n : ℕ) → A ≃ B → isOfHLevel n A → isOfHLevel n B
hLevelRespectEquiv 0 eq hA =
  ( fst eq (fst hA)
  , λ b → cong (fst eq) (snd hA (eq .snd .equiv-proof b .fst .fst)) ∙ eq .snd .equiv-proof b .fst .snd)
hLevelRespectEquiv 1 eq hA x y i =
  hcomp (λ j → λ { (i = i0) → retEq eq x j ; (i = i1) → retEq eq y j })
        (cong (eq .fst) (hA (invEquiv eq .fst x) (invEquiv eq .fst y)) i)
hLevelRespectEquiv {A = A} {B = B} (suc (suc n)) eq hA x y =
  hLevelRespectEquiv (suc n) (invEquiv (congEquiv (invEquiv eq))) (hA _ _)

hLevel≡ : ∀ n → {A B : Type ℓ} (hA : isOfHLevel n A) (hB : isOfHLevel n B) →
  isOfHLevel n (A ≡ B)
hLevel≡ n hA hB = hLevelRespectEquiv n (invEquiv univalence) (hLevel≃ n hA hB)

hLevelHLevel1 : isProp (HLevel {ℓ = ℓ} 0)
hLevelHLevel1 x y = ΣProp≡ (λ _ → isPropIsContr) ((hLevel≡ 0 (x .snd) (y .snd) .fst))

hLevelHLevelSuc : ∀ n → isOfHLevel (suc (suc n)) (HLevel {ℓ = ℓ} (suc n))
hLevelHLevelSuc n x y = subst (λ e → isOfHLevel (suc n) e) HLevel≡ (hLevel≡ (suc n) (snd x) (snd y))

hProp≡HLevel1 : hProp {ℓ} ≡ HLevel {ℓ} 1
hProp≡HLevel1 {ℓ} = isoToPath (iso intro elim intro-elim elim-intro)
  where
    intro : hProp {ℓ} → HLevel {ℓ} 1
    intro h = fst h , snd h

    elim : HLevel 1 → hProp
    elim h = (fst h) , (snd h)

    intro-elim : ∀ h → intro (elim h) ≡ h
    intro-elim h = ΣProp≡ (λ _ → isPropIsOfHLevel 1 _) refl

    elim-intro : ∀ h → elim (intro h) ≡ h
    elim-intro h = ΣProp≡ (λ _ → isPropIsProp) refl

isSetHProp : isSet (hProp {ℓ = ℓ})
isSetHProp = subst (λ X → isOfHLevel 2 X) (sym hProp≡HLevel1) (hLevelHLevelSuc 0)

isContrPartial→isContr : ∀ {ℓ} {A : Type ℓ}
                       → (extend : ∀ φ → Partial φ A → A)
                       → (∀ u → u ≡ (extend i1 λ { _ → u}))
                       → isContr A
isContrPartial→isContr {A = A} extend law
  = ex , λ y → law ex ∙ (λ i → Aux.v y i) ∙ sym (law y)
    where ex = extend i0 empty
          module Aux (y : A) (i : I) where
            φ = ~ i ∨ i
            u : Partial φ A
            u = λ { (i = i0) → ex ; (i = i1) → y }
            v = extend φ u

isOfHLevelLift : ∀ {ℓ ℓ'} (n : ℕ) {A : Type ℓ} → isOfHLevel n A → isOfHLevel n (Lift {j = ℓ'} A)
isOfHLevelLift n = retractIsOfHLevel n lower lift λ _ → refl

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
module Type.Core where

open import Context

open import Function

infix  3 _⊢ᵗ_
infixr 6 _⇒ᵏ_ _⇒_
infixl 7 _∙_

-- | A `Kind` is either a star or an arrow.
data Kind : Set where
  ⋆    : Kind
  _⇒ᵏ_ : Kind -> Kind -> Kind

-- | Kind contexts.
Conᵏ : Set
Conᵏ = Con Kind

mutual
  -- | Types of kind `⋆`.
  Star : Conᵏ -> Set
  Star Θ = Θ ⊢ᵗ ⋆

  -- | A type is defined in a context and has a kind.
  data _⊢ᵗ_ Θ : Kind -> Set where
    Var  : ∀ {σ} -> (v : σ ∈ Θ) -> Θ ⊢ᵗ σ
    Lam_ : ∀ {σ τ} -> (β : Θ ▻ σ ⊢ᵗ τ) -> Θ ⊢ᵗ σ ⇒ᵏ τ
    _∙_  : ∀ {σ τ} -> (φ : Θ ⊢ᵗ σ ⇒ᵏ τ) -> (α : Θ ⊢ᵗ σ) -> Θ ⊢ᵗ τ
    _⇒_  : (α : Star Θ) -> (β : Star Θ) -> Star Θ
    π    : ∀ σ -> (β : Star (Θ ▻ σ)) -> Star Θ
    μ    : ∀ {κ} -> (ψ : Θ ⊢ᵗ (κ ⇒ᵏ ⋆) ⇒ᵏ κ ⇒ᵏ ⋆) -> (α : Θ ⊢ᵗ κ) -> Star Θ

-- | Closed types.
Type⁽⁾ : Kind -> Set
Type⁽⁾ σ = ε ⊢ᵗ σ

-- | Closed types that can be used in any context.
Type⁺ : Kind -> Set
Type⁺ σ = ∀ {Γ} -> Γ ⊢ᵗ σ

Star⁺ : Set
Star⁺ = Type⁺ ⋆

bindᵗ : ∀ {Θ σ τ} -> Θ ⊢ᵗ σ -> Θ ▻ σ ⊢ᵗ τ -> Θ ⊢ᵗ τ
bindᵗ α β = (Lam β) ∙ α

-- | Expand the context that a type is defined in, but do not change anything in the type
-- (including variables).
wkᵗ : ∀ {Θ Ξ σ} -> Ξ ⊢ᵗ σ -> Θ ▻▻ Ξ ⊢ᵗ σ
wkᵗ (Var v) = Var (wkᵛ v)
wkᵗ (Lam β) = Lam (wkᵗ β)
wkᵗ (φ ∙ α) = wkᵗ φ ∙ wkᵗ α
wkᵗ (α ⇒ β) = wkᵗ α ⇒ wkᵗ β
wkᵗ (π σ β) = π σ (wkᵗ β)
wkᵗ (μ ψ α) = μ (wkᵗ ψ) (wkᵗ α)

-- | Lift a closed type to any context.
wk⁺ : ∀ {σ} -> Type⁽⁾ σ -> Type⁺ σ
wk⁺ α = wkᵗ α

-- | Rename a type.
renᵗ : ∀ {Θ Ξ σ} -> Θ ⊆ Ξ -> Θ ⊢ᵗ σ -> Ξ ⊢ᵗ σ
renᵗ ι (Var v) = Var (renᵛ ι v)
renᵗ ι (Lam β) = Lam (renᵗ (keep ι) β)
renᵗ ι (φ ∙ α) = renᵗ ι φ ∙ renᵗ ι α
renᵗ ι (α ⇒ β) = renᵗ ι α ⇒ renᵗ ι β
renᵗ ι (π σ α) = π σ (renᵗ (keep ι) α)
renᵗ ι (μ ψ α) = μ (renᵗ ι ψ) (renᵗ ι α)

-- | Extend the context of a type by another context and increase all variables as appropriate.
shiftᵗⁿ : ∀ {Θ σ} Ξ -> Θ ⊢ᵗ σ -> Θ ▻▻ Ξ ⊢ᵗ σ
shiftᵗⁿ Ξ = renᵗ (extʳ Ξ)

-- | Increase all variables in a type by one.
shiftᵗ : ∀ {Θ σ τ} -> Θ ⊢ᵗ σ -> Θ ▻ τ ⊢ᵗ σ
shiftᵗ = shiftᵗⁿ (ε ▻ _)

unshiftᵗ : ∀ {Θ σ τ} -> Θ ▻ σ ▻ σ ⊢ᵗ τ -> Θ ▻ σ ⊢ᵗ τ
unshiftᵗ = renᵗ dupl

shiftᶜⁿ : ∀ {Θ σ} Ξ -> Con (Θ ⊢ᵗ σ) -> Con (Θ ▻▻ Ξ ⊢ᵗ σ)
shiftᶜⁿ Ξ = mapᶜ (shiftᵗⁿ Ξ)

shiftᶜ : ∀ {Θ σ τ} -> Con (Θ ⊢ᵗ σ) -> Con (Θ ▻ τ ⊢ᵗ σ)
shiftᶜ = mapᶜ shiftᵗ

environmentᵗ : Environment _⊢ᵗ_
environmentᵗ = record
  { varᵈ = Var
  ; renᵈ = renᵗ
  }

module TypeEnv = Environment environmentᵗ

_⊢ᵗᵉ_ = TypeEnv._⊢ᵉ_

module _ where
  open TypeEnv

  subᵗ : ∀ {Θ Ξ σ} -> Ξ ⊢ᵗᵉ Θ -> Θ ⊢ᵗ σ -> Ξ ⊢ᵗ σ
  subᵗ ρ (Var v) = lookupᵉ v ρ
  subᵗ ρ (Lam β) = Lam (subᵗ (keepᵉ ρ) β)
  subᵗ ρ (φ ∙ α) = subᵗ ρ φ ∙ subᵗ ρ α
  subᵗ ρ (α ⇒ β) = subᵗ ρ α ⇒ subᵗ ρ β
  subᵗ ρ (π σ β) = π σ (subᵗ (keepᵉ ρ) β)
  subᵗ ρ (μ ψ α) = μ (subᵗ ρ ψ) (subᵗ ρ α)

  _<_>ᵗ : ∀ {Θ σ τ} -> Θ ▻ σ ⊢ᵗ τ -> Θ ⊢ᵗ σ -> Θ ⊢ᵗ τ
  β < α >ᵗ = subᵗ (topᵉ α) β

-- | Right-fold a context with `_⇒ᵏ_ ∘ f`.
--
-- > conToKindBy f (ε ▻ σ₁ ▻ … ▻ σₙ) τ = f σ₁ ⇒ᵏ … ⇒ᵏ f σₙ ⇒ᵏ τ
conToKindBy : ∀ {α} {A : Set α} -> (A -> Kind) -> Con A -> Kind -> Kind
conToKindBy f Θ τ = foldrᶜ (_⇒ᵏ_ ∘ f) τ Θ

-- | Right-fold a context with `_⇒ᵏ_`.
--
-- > conToKind (ε ▻ σ₁ ▻ … ▻ σₙ) τ = σ₁ ⇒ᵏ … ⇒ᵏ σₙ ⇒ᵏ τ
conToKind : Conᵏ -> Kind -> Kind
conToKind = conToKindBy id

-- | Construct an environment with n variables going in reverse order.
--
-- > subVars' = ∅ ▷ (n - 1) ▷ … ▷ 0
--
-- (each variable is denoted by its De Bruijn index).
subVars' : ∀ {Θ Ξ} -> Seq (λ σ -> Ξ ▻▻ Θ ⊢ᵗ σ) Θ
subVars' {ε}     = ø
subVars' {Θ ▻ σ} = mapˢ shiftᵗ subVars' ▶ Var vz

-- | Construct an environment with n variables going in reverse order.
--
-- > subVars' = ∅ ▷ (n - 1) ▷ … ▷ 0
--
-- (each variable is denoted by its De Bruijn index).
subVars : ∀ {α} {A : Set α} {Ξ Θ} {f : A -> Kind} -> Seq (λ σ -> Ξ ▻▻ mapᶜ f Θ ⊢ᵗ f σ) Θ
subVars {Θ = ε}     = ø
subVars {Θ = Θ ▻ σ} = mapˢ shiftᵗ subVars ▶ Var vz

-- | Apply π` to a type `n` times.
--
-- > πⁿ' (ε ▻ σ₁ ▻ … ▻ σₙ) β = πₙ ∘ … ∘ π₁ $ β
πⁿ' : ∀ {Ξ} Θ -> Star (Ξ ▻▻ Θ) -> Star Ξ
πⁿ'  ε      β = β
πⁿ' (Θ ▻ σ) β = πⁿ' Θ (π σ β)

-- | Apply `Lam` to a type `n` times.
--
-- > Lamⁿ' (ε ▻ σ₁ ▻ … ▻ σₙ) β = Lamₙ ∘ … ∘ Lam₁ $ β
Lamⁿ' : ∀ {Ξ τ} Θ -> Ξ ▻▻ Θ ⊢ᵗ τ -> Ξ ⊢ᵗ conToKind Θ τ
Lamⁿ'  ε      β = β
Lamⁿ' (Θ ▻ σ) β = Lamⁿ' Θ (Lam β)

-- | Apply `Lam` to a type `n` times.
--
-- > Lamⁿ' (ε ▻ σ₁ ▻ … ▻ σₙ) β = Lamₙ ∘ … ∘ Lam₁ $ β
Lamⁿ : ∀ {α} {A : Set α} {Ξ τ f} (Θ : Con A) -> Ξ ▻▻ mapᶜ f Θ ⊢ᵗ τ -> Ξ ⊢ᵗ conToKindBy f Θ τ
Lamⁿ  ε      β = β
Lamⁿ (Θ ▻ σ) β = Lamⁿ Θ (Lam β)

-- | Apply a type function to an environment.
--
-- > applyᵗⁿ _ ψ (∅ ▷ α₁ ▷ … ▷ αₙ) = ψ α₁ … αₙ
applyᵗⁿ
  : ∀ {α} {A : Set α} {Ξ f τ}
  -> (Θ : Con A)
  -> Ξ ⊢ᵗ foldrᶜ (_⇒ᵏ_ ∘ f) τ Θ
  -> Seq (λ σ -> Ξ ⊢ᵗ f σ) Θ
  -> Ξ ⊢ᵗ τ
applyᵗⁿ _ ψ  ø      = ψ
applyᵗⁿ _ ψ (ρ ▶ α) = applyᵗⁿ _ ψ ρ ∙ α

instᵗⁿ
  : ∀ {α} {A : Set α} {Θ Ξ σ} {f : Con A -> Kind}
  -> Seq (λ τ -> Θ ⊢ᵗ f τ) Ξ -> Θ ▻▻ mapᶜ f Ξ ⊢ᵗ σ -> Θ ⊢ᵗ σ
instᵗⁿ              ø      β = β
instᵗⁿ {Ξ = Ξ ▻ _} (ρ ▶ α) β = instᵗⁿ ρ (bindᵗ (shiftᵗⁿ (mapᶜ _ Ξ) α) β)

instᵗⁿ' : ∀ {Θ Ξ σ} -> Seq (Θ ⊢ᵗ_) Ξ -> Θ ▻▻ Ξ ⊢ᵗ σ -> Θ ⊢ᵗ σ
instᵗⁿ'              ø      β = β
instᵗⁿ' {Ξ = Ξ ▻ _} (ρ ▶ α) β = instᵗⁿ' ρ (bindᵗ (shiftᵗⁿ Ξ α) β)

conToTypeBy : ∀ {Θ Ξ} -> (Star Θ -> Star Ξ) -> Con (Star Θ) -> Star Ξ -> Star Ξ
conToTypeBy f Δ β = foldrᶜ (_⇒_ ∘ f) β Δ

max_stars_repo_name: AriFordsham/plutus

max_issues_repo_name: AriFordsham/plutus

max_forks_repo_name: AriFordsham/plutus


text:
module Adjunctions where

open import Library
open import Categories
open import Functors

open Cat
open Fun

record Adj {a b c d}(C : Cat {a}{b})(D : Cat {c}{d}) : Set (a ⊔ b ⊔ c ⊔ d)
  where
  constructor adjunction
  field L        : Fun C D
        R        : Fun D C
        left     : {X : Obj C}{Y : Obj D} →
                   Hom D (OMap L X) Y → Hom C X (OMap R Y)
        right    : {X : Obj C}{Y : Obj D} →
                   Hom C X (OMap R Y) → Hom D (OMap L X) Y
        lawa     : {X : Obj C}{Y : Obj D}(f : Hom D (OMap L X) Y) →
                   right (left f) ≅ f
        lawb     : {X : Obj C}{Y : Obj D}(f : Hom C X (OMap R Y)) →
                   left (right f) ≅ f
        natleft  : {X X' : Obj C}{Y Y' : Obj D}
                   (f : Hom C X' X)(g : Hom D Y Y')
                   (h : Hom D (OMap L X) Y) →
                   comp C (HMap R g) (comp C (left h) f)
                   ≅
                   left (comp D g (comp D h (HMap L f)))
        natright : {X X' : Obj C}{Y Y' : Obj D}
                   (f : Hom C X' X)(g : Hom D Y Y')
                   (h : Hom C X (OMap R Y)) →
                   right (comp C (HMap R g) (comp C h f))
                   ≅
                   comp D g (comp D (right h) (HMap L f))

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
------------------------------------------------------------------------
-- A combined definition of strong and weak bisimilarity and
-- expansion, along with various properties
------------------------------------------------------------------------

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

module Delay-monad.Sized.Bisimilarity where

open import Equality.Propositional as E using (_≡_)
open import Logical-equivalence using (_⇔_)
open import Prelude
open import Prelude.Size

open import Function-universe E.equality-with-J hiding (_∘_; Kind)

open import Delay-monad.Sized
open import Delay-monad.Bisimilarity.Kind

------------------------------------------------------------------------
-- The code below is defined for a fixed type family A

module _ {a} {A : Size → Type a} where

  ----------------------------------------------------------------------
  -- The relations

  mutual

    -- A combined definition of all three relations. The definition
    -- uses mixed induction and coinduction.
    --
    -- Note that this type is not defined in the same way as Delay.
    -- One might argue that the now constructor should have the
    -- following type, using a /sized/ identity type Id:
    --
    --   now : ∀ {x y} →
    --         Id (A ∞) i x y →
    --         [ i ] now x ∼ now y

    infix 4 [_]_⟨_⟩_ [_]_⟨_⟩′_

    data [_]_⟨_⟩_ (i : Size) :
           Delay A ∞ → Kind → Delay A ∞ → Type a where
      now    : ∀ {k x} → [ i ] now x ⟨ k ⟩ now x
      later  : ∀ {k x₁ x₂} →
               [ i ] force x₁ ⟨ k ⟩′ force x₂ →
               [ i ] later x₁ ⟨ k ⟩ later x₂
      laterˡ : ∀ {k x₁ x₂} →
               [ i ] force x₁ ⟨ other k ⟩ x₂ →
               [ i ] later x₁ ⟨ other k ⟩ x₂
      laterʳ : ∀ {x₁ x₂} →
               [ i ] x₁ ⟨ other weak ⟩ force x₂ →
               [ i ] x₁ ⟨ other weak ⟩ later x₂

    record [_]_⟨_⟩′_ (i : Size)
             (x₁ : Delay A ∞) (k : Kind) (x₂ : Delay A ∞) :
             Type a where
      coinductive
      field
        force : {j : Size< i} → [ j ] x₁ ⟨ k ⟩ x₂

  open [_]_⟨_⟩′_ public

  -- Strong bisimilarity.

  infix 4 [_]_∼_ [_]_∼′_ _∼_ _∼′_

  [_]_∼_ : Size → Delay A ∞ → Delay A ∞ → Type a
  [_]_∼_ = [_]_⟨ strong ⟩_

  [_]_∼′_ : Size → Delay A ∞ → Delay A ∞ → Type a
  [_]_∼′_ = [_]_⟨ strong ⟩′_

  _∼_ : Delay A ∞ → Delay A ∞ → Type a
  _∼_ = [ ∞ ]_∼_

  _∼′_ : Delay A ∞ → Delay A ∞ → Type a
  _∼′_ = [ ∞ ]_∼′_

  -- Expansion.

  infix 4 [_]_≳_ [_]_≳′_ _≳_ _≳′_

  [_]_≳_ : Size → Delay A ∞ → Delay A ∞ → Type a
  [_]_≳_ = [_]_⟨ other expansion ⟩_

  [_]_≳′_ : Size → Delay A ∞ → Delay A ∞ → Type a
  [_]_≳′_ = [_]_⟨ other expansion ⟩′_

  _≳_ : Delay A ∞ → Delay A ∞ → Type a
  _≳_ = [ ∞ ]_≳_

  _≳′_ : Delay A ∞ → Delay A ∞ → Type a
  _≳′_ = [ ∞ ]_≳′_

  -- The converse of expansion.

  infix 4 [_]_≲_ [_]_≲′_ _≲_ _≲′_

  [_]_≲_ : Size → Delay A ∞ → Delay A ∞ → Type a
  [_]_≲_ i = flip [ i ]_⟨ other expansion ⟩_

  [_]_≲′_ : Size → Delay A ∞ → Delay A ∞ → Type a
  [_]_≲′_ i = flip [ i ]_⟨ other expansion ⟩′_

  _≲_ : Delay A ∞ → Delay A ∞ → Type a
  _≲_ = [ ∞ ]_≲_

  _≲′_ : Delay A ∞ → Delay A ∞ → Type a
  _≲′_ = [ ∞ ]_≲′_

  -- Weak bisimilarity.

  infix 4 [_]_≈_ [_]_≈′_ _≈_ _≈′_

  [_]_≈_ : Size → Delay A ∞ → Delay A ∞ → Type a
  [_]_≈_ = [_]_⟨ other weak ⟩_

  [_]_≈′_ : Size → Delay A ∞ → Delay A ∞ → Type a
  [_]_≈′_ = [_]_⟨ other weak ⟩′_

  _≈_ : Delay A ∞ → Delay A ∞ → Type a
  _≈_ = [ ∞ ]_≈_

  _≈′_ : Delay A ∞ → Delay A ∞ → Type a
  _≈′_ = [ ∞ ]_≈′_

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

  -- Strong bisimilarity is contained in the other relations (and
  -- itself).

  ∼→ : ∀ {k i x y} → [ i ] x ∼ y → [ i ] x ⟨ k ⟩ y
  ∼→ now       = now
  ∼→ (later p) = later λ { .force → ∼→ (force p) }

  -- Expansion is contained in weak bisimilarity (and expansion).

  ≳→ : ∀ {k i x y} → [ i ] x ≳ y → [ i ] x ⟨ other k ⟩ y
  ≳→ now        = now
  ≳→ (later p)  = later λ { .force → ≳→ (force p) }
  ≳→ (laterˡ p) = laterˡ (≳→ p)

  -- In some cases weak bisimilarity is contained in expansion (and
  -- itself).

  ≈→-now : ∀ {k i x y} → [ i ] x ≈ now y → [ i ] x ⟨ other k ⟩ now y
  ≈→-now now        = now
  ≈→-now (laterˡ p) = laterˡ (≈→-now p)

  -- In some cases all three relations are contained in strong
  -- bisimilarity.

  →∼-neverˡ : ∀ {k i x} → [ i ] never ⟨ k ⟩ x → [ i ] never ∼ x
  →∼-neverˡ (later  p) = later λ { .force → →∼-neverˡ (force p) }
  →∼-neverˡ (laterˡ p) = →∼-neverˡ p
  →∼-neverˡ (laterʳ p) = later λ { .force → →∼-neverˡ p }

  →∼-neverʳ : ∀ {k i x} → [ i ] x ⟨ k ⟩ never → [ i ] x ∼ never
  →∼-neverʳ (later  p) = later λ { .force → →∼-neverʳ (force p) }
  →∼-neverʳ (laterˡ p) = later λ { .force → →∼-neverʳ p }
  →∼-neverʳ (laterʳ p) = →∼-neverʳ p

  ----------------------------------------------------------------------
  -- Removing later constructors

  -- Later constructors can sometimes be removed.

  drop-laterʳ :
    ∀ {k i} {j : Size< i} {x y} →
    [ i ] x ⟨ other k ⟩ y →
    [ j ] x ⟨ other k ⟩ drop-later y
  drop-laterʳ now        = now
  drop-laterʳ (later  p) = laterˡ (force p)
  drop-laterʳ (laterʳ p) = p
  drop-laterʳ (laterˡ p) = laterˡ (drop-laterʳ p)

  drop-laterˡ :
    ∀ {i} {j : Size< i} {x y} →
    [ i ] x ≈ y →
    [ j ] drop-later x ≈ y
  drop-laterˡ now        = now
  drop-laterˡ (later  p) = laterʳ (force p)
  drop-laterˡ (laterʳ p) = laterʳ (drop-laterˡ p)
  drop-laterˡ (laterˡ p) = p

  drop-laterˡʳ :
    ∀ {k i} {j : Size< i} {x y} →
    [ i ] x ⟨ k ⟩ y →
    [ j ] drop-later x ⟨ k ⟩ drop-later y
  drop-laterˡʳ now        = now
  drop-laterˡʳ (later  p) = force p
  drop-laterˡʳ (laterʳ p) = drop-laterˡ p
  drop-laterˡʳ (laterˡ p) = drop-laterʳ p

  -- Special cases of the functions above.

  laterʳ⁻¹ : ∀ {k i} {j : Size< i} {x y} →
             [ i ] x ⟨ other k ⟩ later y →
             [ j ] x ⟨ other k ⟩ force y
  laterʳ⁻¹ = drop-laterʳ

  laterˡ⁻¹ : ∀ {i} {j : Size< i} {x y} →
             [ i ] later x ≈ y →
             [ j ] force x ≈ y
  laterˡ⁻¹ = drop-laterˡ

  later⁻¹ : ∀ {k i} {j : Size< i} {x y} →
            [ i ] later x ⟨ k ⟩ later y →
            [ j ] force x ⟨ k ⟩ force y
  later⁻¹ = drop-laterˡʳ

  -- The following size-preserving variant of laterʳ⁻¹ and laterˡ⁻¹
  -- can be defined.
  --
  -- Several other variants cannot be defined if ∀ i → A i is
  -- inhabited, see Delay-monad.Bisimilarity.Sized.Negative.

  laterˡʳ⁻¹ :
    ∀ {k i x y} →
    [ i ] later x ⟨ other k ⟩ force y →
    [ i ] force x ⟨ other k ⟩ later y →
    [ i ] force x ⟨ other k ⟩ force y
  laterˡʳ⁻¹ {k} {i} p q = laterˡʳ⁻¹′ p q E.refl E.refl
    where
    laterˡʳ⁻¹″ :
      ∀ {x′ y′ x y} →
      ({j : Size< i} → [ j ] x′ ⟨ other k ⟩ force y) →
      ({j : Size< i} → [ j ] force x ⟨ other k ⟩ y′) →
      x′ ≡ later x → y′ ≡ later y →
      [ i ] later x ⟨ other k ⟩ later y
    laterˡʳ⁻¹″ p q E.refl E.refl = later λ { .force → laterˡʳ⁻¹ p q }

    laterˡʳ⁻¹′ :
      ∀ {x′ y′ x y} →
      [ i ] later x ⟨ other k ⟩ y′ →
      [ i ] x′ ⟨ other k ⟩ later y →
      force x ≡ x′ → force y ≡ y′ →
      [ i ] x′ ⟨ other k ⟩ y′
    laterˡʳ⁻¹′ (later  p) (later  q) ≡x′    ≡y′    = laterˡʳ⁻¹″ (force p)                (force q)                ≡x′ ≡y′
    laterˡʳ⁻¹′ (laterʳ p) (later  q) ≡x′    ≡y′    = laterˡʳ⁻¹″ (λ { {_} → laterˡ⁻¹ p }) (force q)                ≡x′ ≡y′
    laterˡʳ⁻¹′ (later  p) (laterˡ q) ≡x′    ≡y′    = laterˡʳ⁻¹″ (force p)                (λ { {_} → laterʳ⁻¹ q }) ≡x′ ≡y′
    laterˡʳ⁻¹′ (laterʳ p) (laterˡ q) ≡x′    ≡y′    = laterˡʳ⁻¹″ (λ { {_} → laterˡ⁻¹ p }) (λ { {_} → laterʳ⁻¹ q }) ≡x′ ≡y′
    laterˡʳ⁻¹′ (laterˡ p) _          E.refl E.refl = p
    laterˡʳ⁻¹′ _          (laterʳ q) E.refl ≡y′    = E.subst ([ i ] _ ⟨ _ ⟩_) ≡y′ q

  ----------------------------------------------------------------------
  -- Reflexivity, symmetry/antisymmetry, transitivity

  -- All three relations are reflexive.

  reflexive : ∀ {k i} x → [ i ] x ⟨ k ⟩ x
  reflexive (now _)   = now
  reflexive (later x) = later λ { .force → reflexive (force x) }

  -- Strong and weak bisimilarity are symmetric.

  symmetric :
    ∀ {k i x y} {¬≳ : if k ≟-Kind other expansion then ⊥ else ⊤} →
    [ i ] x ⟨ k ⟩ y → [ i ] y ⟨ k ⟩ x
  symmetric now                   = now
  symmetric (laterˡ {k = weak} p) = laterʳ (symmetric p)
  symmetric (laterʳ p)            = laterˡ (symmetric p)
  symmetric {¬≳ = ¬≳} (later p)   =
    later λ { .force → symmetric {¬≳ = ¬≳} (force p) }

  symmetric {¬≳ = ()} (laterˡ {k = expansion} _)

  -- Some special cases of symmetry hold for expansion.

  symmetric-neverˡ : ∀ {i x} → [ i ] never ≳ x → [ i ] x ≳ never
  symmetric-neverˡ = ∼→ ∘ symmetric ∘ →∼-neverˡ

  symmetric-neverʳ : ∀ {i x} → [ i ] x ≳ never → [ i ] never ≳ x
  symmetric-neverʳ = ∼→ ∘ symmetric ∘ →∼-neverʳ

  -- The expansion relation is antisymmetric (up to weak
  -- bisimilarity).

  antisymmetric-≳ : ∀ {i x y} → [ i ] x ≳ y → [ i ] y ≳ x → [ i ] x ≈ y
  antisymmetric-≳ p _ = ≳→ p

  -- Several more or less size-preserving variants of transitivity.
  --
  -- Many size-preserving variants cannot be defined if ∀ i → A i is
  -- inhabited, see Delay-monad.Sized.Bisimilarity.Negative.

  transitive-∼ʳ :
    ∀ {k i x y z}
      {¬≈ : if k ≟-Kind other weak then ⊥ else ⊤} →
    [ i ] x ⟨ k ⟩ y → [ i ] y ∼ z → [ i ] x ⟨ k ⟩ z
  transitive-∼ʳ           now        now       = now
  transitive-∼ʳ {¬≈ = ¬≈} (laterˡ p) q         = laterˡ
                                                   (transitive-∼ʳ {¬≈ = ¬≈} p q)
  transitive-∼ʳ {¬≈ = ()} (laterʳ _) _
  transitive-∼ʳ {¬≈ = ¬≈} (later  p) (later q) =
    later λ { .force → transitive-∼ʳ {¬≈ = ¬≈} (force p) (force q) }

  transitive-∼ˡ :
    ∀ {k i x y z} →
    x ∼ y → [ i ] y ⟨ k ⟩ z → [ i ] x ⟨ k ⟩ z
  transitive-∼ˡ now       now        = now
  transitive-∼ˡ (later p) (later q)  = later λ { .force →
                                         transitive-∼ˡ (force p) (force q) }
  transitive-∼ˡ (later p) (laterˡ q) = laterˡ (transitive-∼ˡ (force p) q)
  transitive-∼ˡ p         (laterʳ q) = laterʳ (transitive-∼ˡ p q)

  transitive-∞∼ʳ :
    ∀ {k i x y z} →
    [ i ] x ⟨ k ⟩ y → y ∼ z → [ i ] x ⟨ k ⟩ z
  transitive-∞∼ʳ now        now       = now
  transitive-∞∼ʳ (later p)  (later q) = later λ { .force →
                                          transitive-∞∼ʳ (force p) (force q) }
  transitive-∞∼ʳ (laterˡ p) q         = laterˡ (transitive-∞∼ʳ p q)
  transitive-∞∼ʳ (laterʳ p) (later q) = laterʳ (transitive-∞∼ʳ p (force q))

  transitive-≳ˡ :
    ∀ {k i x y z} →
    x ≳ y → [ i ] y ⟨ other k ⟩ z → [ i ] x ⟨ other k ⟩ z
  transitive-≳ˡ now        now        = now
  transitive-≳ˡ (later p)  (later q)  = later λ { .force →
                                          transitive-≳ˡ (force p) (force q) }
  transitive-≳ˡ (later p)  (laterˡ q) = laterˡ (transitive-≳ˡ (force p) q)
  transitive-≳ˡ (laterˡ p) q          = laterˡ (transitive-≳ˡ p q)
  transitive-≳ˡ p          (laterʳ q) = laterʳ (transitive-≳ˡ p q)

  transitive-≈≲ :
    ∀ {i x y z} →
    [ i ] x ≈ y → y ≲ z → [ i ] x ≈ z
  transitive-≈≲ p q = symmetric (transitive-≳ˡ q (symmetric p))

  transitive-≈-now :
    ∀ {i x′ y z} →
    let x = now x′ in
    [ i ] x ≈ y → y ≈ z → [ i ] x ≈ z
  transitive-≈-now now        now        = now
  transitive-≈-now (laterʳ p) q          = transitive-≈-now p (laterˡ⁻¹ q)
  transitive-≈-now p          (laterʳ q) = laterʳ (transitive-≈-now p q)

  mutual

    transitive-≈-later :
      ∀ {i x′ y z} →
      let x = later x′ in
      x ≈ y → y ≈ z → [ i ] x ≈ z
    transitive-≈-later p          (later q)  = later λ { .force →
                                                 transitive-≈ (later⁻¹ p) (force q) }
    transitive-≈-later p          (laterʳ q) = laterʳ (transitive-≈-later p q)
    transitive-≈-later p          (laterˡ q) = transitive-≈ (laterʳ⁻¹ p) q
    transitive-≈-later (laterˡ p) q          = laterˡ (transitive-≈ p q)

    transitive-≈ : ∀ {i x y z} → x ≈ y → y ≈ z → [ i ] x ≈ z
    transitive-≈ {x = now   x} p q = transitive-≈-now   p q
    transitive-≈ {x = later x} p q = transitive-≈-later p q

  -- Equational reasoning combinators.

  infix  -1 _∎ finally finally-≳ finally-≈
  infixr -2 step-∼ˡ step-∼∼ step-≳∼ step-≈∼ step-?∼ step-≳ˡ step-≈
            _≳⟨⟩_ step-≡ˡ _∼⟨⟩_

  _∎ : ∀ {k i} x → [ i ] x ⟨ k ⟩ x
  _∎ = reflexive

  finally : ∀ {k i} x y →
            [ i ] x ⟨ k ⟩ y → [ i ] x ⟨ k ⟩ y
  finally _ _ x?y = x?y

  syntax finally x y x≈y = x ?⟨ x≈y ⟩∎ y ∎

  finally-≳ : ∀ {i} x y →
              [ i ] x ≳ y → [ i ] x ≳ y
  finally-≳ _ _ x≳y = x≳y

  syntax finally-≳ x y x≳y = x ≳⟨ x≳y ⟩∎ y ∎

  finally-≈ : ∀ {i} x y →
              [ i ] x ≈ y → [ i ] x ≈ y
  finally-≈ _ _ x≈y = x≈y

  syntax finally-≈ x y x≈y = x ≈⟨ x≈y ⟩∎ y ∎

  step-∼ˡ : ∀ {k i} x {y z} →
            [ i ] y ⟨ k ⟩ z → x ∼ y → [ i ] x ⟨ k ⟩ z
  step-∼ˡ _ y⟨⟩z x∼y = transitive-∼ˡ x∼y y⟨⟩z

  syntax step-∼ˡ x y⟨⟩z x∼y = x ∼⟨ x∼y ⟩ y⟨⟩z

  step-∼∼ : ∀ {i} x {y z} →
            [ i ] y ∼ z → [ i ] x ∼ y → [ i ] x ∼ z
  step-∼∼ _ y∼z x∼y = transitive-∼ʳ x∼y y∼z

  syntax step-∼∼ x y∼z x∼y = x ∼⟨ x∼y ⟩∼ y∼z

  step-≳∼ : ∀ {i} x {y z} →
            [ i ] y ∼ z → [ i ] x ≳ y → [ i ] x ≳ z
  step-≳∼ _ y∼z x≳y = transitive-∼ʳ x≳y y∼z

  syntax step-≳∼ x y∼z x≳y = x ≳⟨ x≳y ⟩∼ y∼z

  step-≈∼ : ∀ {k i} x {y z} →
            y ∼ z → [ i ] x ⟨ k ⟩ y → [ i ] x ⟨ k ⟩ z
  step-≈∼ _ y∼z x≈y = transitive-∞∼ʳ x≈y y∼z

  syntax step-≈∼ x y∼z x≈y = x ≈⟨ x≈y ⟩∼ y∼z

  step-?∼ : ∀ {k i} x {y z} →
            y ∼ z → [ i ] x ⟨ k ⟩ y → [ i ] x ⟨ k ⟩ z
  step-?∼ _ y∼z x?y = transitive-∞∼ʳ x?y y∼z

  syntax step-?∼ x y∼z x?y = x ?⟨ x?y ⟩∼ y∼z

  step-≳ˡ : ∀ {k i} x {y z} →
            [ i ] y ⟨ other k ⟩ z → x ≳ y →
            [ i ] x ⟨ other k ⟩ z
  step-≳ˡ _ y≳≈z x≳y = transitive-≳ˡ x≳y y≳≈z

  syntax step-≳ˡ x y≳≈z x≳y = x ≳⟨ x≳y ⟩ y≳≈z

  step-≈ : ∀ {i} x {y z} →
           y ≈ z → x ≈ y → [ i ] x ≈ z
  step-≈ _ y≈z x≈y = transitive-≈ x≈y y≈z

  syntax step-≈ x y≈z x≈y = x ≈⟨ x≈y ⟩ y≈z

  _≳⟨⟩_ : ∀ {k i} x {y} →
          [ i ] drop-later x ⟨ other k ⟩ y → [ i ] x ⟨ other k ⟩ y
  now _   ≳⟨⟩ p = p
  later _ ≳⟨⟩ p = laterˡ p

  step-≡ˡ : ∀ {k i} x {y z} →
            [ i ] y ⟨ k ⟩ z → x ≡ y → [ i ] x ⟨ k ⟩ z
  step-≡ˡ _ y⟨⟩z E.refl = y⟨⟩z

  syntax step-≡ˡ x y⟨⟩z x≡y = x ≡⟨ x≡y ⟩ y⟨⟩z

  _∼⟨⟩_ : ∀ {k i} x {y} →
           [ i ] x ⟨ k ⟩ y → [ i ] x ⟨ k ⟩ y
  _ ∼⟨⟩ x≈y = x≈y

  ----------------------------------------------------------------------
  -- Some results related to negation

  -- The computation never is not related to now x.

  never≉now : ∀ {k i x} → ¬ [ i ] never ⟨ k ⟩ now x
  never≉now (laterˡ p) = never≉now p

  -- The computation now x is not related to never.

  now≉never : ∀ {k i x} → ¬ [ i ] now x ⟨ k ⟩ never
  now≉never (laterʳ p) = now≉never p

  -- If A ∞ is uninhabited, then the three relations defined above are
  -- trivial.

  uninhabited→trivial : ∀ {k i} → ¬ A ∞ → ∀ x y → [ i ] x ⟨ k ⟩ y
  uninhabited→trivial ¬A (now   x) _         = ⊥-elim (¬A x)
  uninhabited→trivial ¬A (later x) (now   y) = ⊥-elim (¬A y)
  uninhabited→trivial ¬A (later x) (later y) =
    later λ { .force → uninhabited→trivial ¬A (force x) (force y) }

  -- Expansion and weak bisimilarity are not pointwise propositional.

  ¬-≳≈-propositional :
    ∀ {k} → ¬ (∀ {x y} → E.Is-proposition ([ ∞ ] x ⟨ other k ⟩ y))
  ¬-≳≈-propositional {k} =
    (∀ {x y} → E.Is-proposition ([ ∞ ] x ⟨ other k ⟩ y))  ↝⟨ (λ prop → prop {x = never} {y = never}) ⟩
    E.Is-proposition ([ ∞ ] never ⟨ other k ⟩ never)      ↝⟨ (λ irr → irr _ _) ⟩
    proof₁ ≡ proof₂                                       ↝⟨ (λ ()) ⟩□
    ⊥₀                                                    □
    where
    proof₁ : ∀ {i} → [ i ] never ⟨ other k ⟩ never
    proof₁ = later λ { .force → proof₁ }

    proof₂ : ∀ {i} → [ i ] never ⟨ other k ⟩ never
    proof₂ = laterˡ proof₁

------------------------------------------------------------------------
-- A statement of extensionality for strong bisimilarity

-- A statement of extensionality: strongly bisimilar computations are
-- equal.

Extensionality : (ℓ : Level) → Type (lsuc ℓ)
Extensionality a =
  {A : Size → Type a} {x y : Delay A ∞} → x ∼ y → x ≡ y

max_stars_repo_name: nad/delay-monad

max_issues_repo_name: nad/delay-monad

max_forks_repo_name: nad/delay-monad


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

module Categories.Diagram.Cocone.Properties where

open import Level

open import Categories.Category
open import Categories.Functor
open import Categories.Functor.Properties
open import Categories.NaturalTransformation
open import Categories.Diagram.Cone.Properties
open import Categories.Diagram.Duality

import Categories.Diagram.Cocone as Coc
import Categories.Morphism.Reasoning as MR

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

module _ {F : Functor J C} (G : Functor C D) where
  private
    module C = Category C
    module D = Category D
    module F = Functor F
    module G = Functor G
    module CF = Coc F
    GF = G ∘F F
    module CGF = Coc GF

  F-map-Coconeˡ : CF.Cocone → CGF.Cocone
  F-map-Coconeˡ K = record
    { coapex = record
      { ψ       = λ X → G.F₁ (ψ X)
      ; commute = λ f → [ G ]-resp-∘ (commute f)
      }
    }
    where open CF.Cocone K

  F-map-Cocone⇒ˡ : ∀ {K K′} (f : CF.Cocone⇒ K K′) → CGF.Cocone⇒ (F-map-Coconeˡ K) (F-map-Coconeˡ K′)
  F-map-Cocone⇒ˡ f = record
    { arr     = G.F₁ arr
    ; commute = [ G ]-resp-∘ commute
    }
    where open CF.Cocone⇒ f

module _ {F : Functor J C} (G : Functor J′ J) where
  private
    module C   = Category C
    module J′  = Category J′
    module F   = Functor F
    module G   = Functor G
    module CF  = Coc F
    FG = F ∘F G
    module CFG = Coc FG

  F-map-Coconeʳ : CF.Cocone → CFG.Cocone
  F-map-Coconeʳ K = coCone⇒Cocone C (F-map-Coneʳ G.op (Cocone⇒coCone C K))

  F-map-Cocone⇒ʳ : ∀ {K K′} (f : CF.Cocone⇒ K K′) → CFG.Cocone⇒ (F-map-Coconeʳ K) (F-map-Coconeʳ K′)
  F-map-Cocone⇒ʳ f = coCone⇒⇒Cocone⇒ C (F-map-Cone⇒ʳ G.op (Cocone⇒⇒coCone⇒ C f))

module _ {F G : Functor J C} (α : NaturalTransformation F G) where
  private
    module α  = NaturalTransformation α
    module CF = Coc F
    module CG = Coc G

  nat-map-Cocone : CG.Cocone → CF.Cocone
  nat-map-Cocone K = coCone⇒Cocone C (nat-map-Cone α.op (Cocone⇒coCone C K))

  nat-map-Cocone⇒ : ∀ {K K′} (f : CG.Cocone⇒ K K′) → CF.Cocone⇒ (nat-map-Cocone K) (nat-map-Cocone K′)
  nat-map-Cocone⇒ f = coCone⇒⇒Cocone⇒ C (nat-map-Cone⇒ α.op (Cocone⇒⇒coCone⇒ C f))

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:
-- Andreas, 2014-10-23
-- We want to split on hidden variables.

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

f : {n : ℕ}  → Set₁
f = Set
  where
  g : {n : ℕ} → Set → Set
  g _ = {!.n!}


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Coinductive "natural" numbers
------------------------------------------------------------------------

module Data.Conat where

open import Coinduction
open import Data.Nat using (ℕ; zero; suc)
open import Relation.Binary

------------------------------------------------------------------------
-- The type

data Coℕ : Set where
  zero : Coℕ
  suc  : (n : ∞ Coℕ) → Coℕ

------------------------------------------------------------------------
-- Some operations

fromℕ : ℕ → Coℕ
fromℕ zero    = zero
fromℕ (suc n) = suc (♯ fromℕ n)

∞ℕ : Coℕ
∞ℕ = suc (♯ ∞ℕ)

infixl 6 _+_

_+_ : Coℕ → Coℕ → Coℕ
zero  + n = n
suc m + n = suc (♯ (♭ m + n))

------------------------------------------------------------------------
-- Equality

data _≈_ : Coℕ → Coℕ → Set where
  zero :                                 zero  ≈ zero
  suc  : ∀ {m n} (m≈n : ∞ (♭ m ≈ ♭ n)) → suc m ≈ suc n

setoid : Setoid _ _
setoid = record
  { Carrier       = Coℕ
  ; _≈_           = _≈_
  ; isEquivalence = record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }
  }
  where
  refl : Reflexive _≈_
  refl {zero}  = zero
  refl {suc n} = suc (♯ refl)

  sym : Symmetric _≈_
  sym zero      = zero
  sym (suc m≈n) = suc (♯ sym (♭ m≈n))

  trans : Transitive _≈_
  trans zero      zero      = zero
  trans (suc m≈n) (suc n≈k) = suc (♯ trans (♭ m≈n) (♭ n≈k))


text:
-- A DSL example in the language Agda: "polynomial types"
module TypeDSL where
open import Data.Nat using (ℕ;_+_;_*_)

data E : Set where
  Zero  : E
  One   : E
  Add   : (x : E) -> (y : E) -> E
  Mul   : (x : E) -> (y : E) -> E

two : E
two = Add One One

four : E
four = Mul two two

-- First semantics: compute the natural number "value" of the expression
card : E -> ℕ
card Zero = 0
card One = 1
card (Add x y) = card x + card y
card (Mul x y) = card x * card y

data Empty : Set where
data Unit : Set where unit : Unit
data Either (a : Set) (b : Set) : Set where
  Left  : a -> Either a b
  Right : b -> Either a b
data Both (a : Set) (b : Set) : Set where
  _,_ : a -> b -> Both a b

-- Second semantics: compute the corresponding finite type
typ : E -> Set
typ Zero = Empty
typ One = Unit
typ (Add x y) = Either (typ x) (typ y)   -- disjoint union type    = sum type
typ (Mul x y) = Both   (typ x) (typ y)   -- cartesian product type = pair type

Bool : Set
Bool = typ two

false : Bool
false = Left unit
true : Bool
true = Right unit

BothBoolBool : Set
BothBoolBool = typ four

ex1 : BothBoolBool
ex1 = ( false , true )

open import Data.Vec as V

variable
  a b : Set
  m n : ℕ

enumAdd : Vec a m -> Vec b n -> Vec (Either a b) (m + n)
enumAdd as bs = V.map Left as ++ V.map Right bs

enumMul : Vec a m -> Vec b n -> Vec (Both   a b) (m * n)
enumMul as bs = concat (V.map (\ a -> V.map (\ b -> (a , b)) bs) as)

-- Third semantics: enumerate all the values in a vector
enumerate : (t : E) -> Vec (typ t) (card t)
enumerate Zero = []
enumerate One = [ unit ]
enumerate (Add x y) = enumAdd (enumerate x) (enumerate y)
enumerate (Mul x y) = enumMul (enumerate x) (enumerate y)

test2 : Vec (typ two) (card two) -- Vec Bool 2
test2 = enumerate two
  -- false ∷ true ∷ []

test4 : Vec (typ four) (card four) -- Vec BothBoolBool 4
test4 = enumerate four
{-
(false , false) ∷
(false , true) ∷
(true , false) ∷
(true , true) ∷ []
-}

-- Exercise: add a constructor for function types

max_stars_repo_name: nicolabotta/DSLsofMath

max_issues_repo_name: nicolabotta/DSLsofMath

max_forks_repo_name: nicolabotta/DSLsofMath


text:
module IsLiteralFormula where

open import OscarPrelude
open import PredicateName
open import Term
open import Formula
open import HasNegation

data IsLiteralFormula : Formula → Set
 where
  atomic : (𝑃 : PredicateName) → (τs : Terms) → IsLiteralFormula $ 𝑃[ 𝑃 ♭ τs ]
  logical : (𝑃 : PredicateName) → (τs : Terms) → IsLiteralFormula ∘ ~ $ 𝑃[ 𝑃 ♭ τs ]

eqIsLiteralFormula : ∀ {φ} → (lf₁ lf₂ : IsLiteralFormula φ) → lf₁ ≡ lf₂
eqIsLiteralFormula (atomic _ _) (atomic _ _) = refl
eqIsLiteralFormula (logical _ _) (logical _ _) = refl

instance EqIsLiteralFormula : ∀ {φ} → Eq (IsLiteralFormula φ)
Eq._==_ EqIsLiteralFormula lf₁ lf₂ = yes $ eqIsLiteralFormula lf₁ lf₂


text:
open import Agda.Primitive

postulate
  X : Set
  Id : Set → Set

module Generic1HIT (S : Set) where
  module RecType k (C : Set k) (Necc : Set) where
    postulate P : Set

module Flattening k (F : Set → Set) (C : Set k) (Necc : Set) where
  -- order f before C matters!
  module W = Generic1HIT (F X)  -- use of F matters, application of F matters
  module M = W.RecType k C X    -- k matters

module S¹RecType i (A : Set i) where
  module FlatteningS¹ = Flattening i Id A X    -- i matters here

module HopfJunior = S¹RecType _ Set  -- meta variable matters

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
data Nat : Set where
  zero : Nat -- Comment which gets eaten
  suc  : Nat -> Nat

{-# BUILTIN NATURAL
Nat #-}

f : Nat -> Nat
f a = 3

g : Nat -> Nat
g a = 4

--TODO found first bug

function : Nat -> (Nat -> Nat) -> Nat
function a f = f a

apply : Nat
apply = function 2 g


text:
open import Web.Semantic.DL.ABox using ( ABox )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using ( TBox )

module Web.Semantic.DL.KB where

infixr 4 _,_

data KB (Σ : Signature) (X : Set) : Set where
  _,_ : (T : TBox Σ) → (A : ABox Σ X) → KB Σ X

tbox : ∀ {Σ X} → KB Σ X → TBox Σ
tbox (T , A) = T

abox : ∀ {Σ X} → KB Σ X → ABox Σ X
abox (T , A) = A

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: agda/agda-web-semantic

max_forks_repo_name: agda/agda-web-semantic


text:
-- Andreas, 2022-03-28, issue #5856, reported by Szumi Xie.
-- Patterns in path-lambdas were simply ignored, but should be illegal.

{-# OPTIONS --cubical #-}

open import Agda.Builtin.Cubical.Path

postulate
  A E : Set
  a : A

data C : Set where
  c : E → C

p : a ≡ a
p = λ (c e) → e

-- WAS: panic about unbound identifier e.

-- Expected error:
-- Patterns are not allowed in Path-lambdas
-- when checking that the expression λ .patternInTele0 @ (c e) → e has type a ≡ a


text:
module Issue1245AmbiguousParse where

postulate
  A : Set
  *_* : A → A
  _*_ : A → A → A

module M (_ : A) where

module N (a : A) = M * a * a * a *

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- Safe modules that use --erased-cubical
------------------------------------------------------------------------

{-# OPTIONS --safe --erased-cubical #-}

module README.Safe.Cubical.Erased where

-- Paths, extensionality and univalence.

import Equality.Path

-- Isomorphisms and equalities relating an arbitrary "equality with J"
-- to path equality, along with proofs of extensionality and
-- univalence for the "equality with J".

import Equality.Path.Isomorphisms

-- The cubical identity type.

import Equality.Id

-- Propositional equality, with some extra bells and whistles
-- definable in Cubical Agda.

import Equality.Propositional.Cubical

-- Some tactics aimed at making equational reasoning proofs more
-- readable for path equality.

import Tactic.By.Path

-- Some tactics aimed at making equational reasoning proofs more
-- readable for the cubical identity type.

import Tactic.By.Id

-- Some theory of Erased, developed using Cubical Agda.

import Erased.Cubical

-- Some theory of equivalences with erased "proofs", defined in terms
-- of partly erased contractible fibres, developed using Cubical Agda.

import Equivalence.Erased.Contractible-preimages.Cubical

-- Some theory of equivalences with erased "proofs", developed using
-- Cubical Agda.

import Equivalence.Erased.Cubical

-- A sequential colimit for which everything except for the "base
-- case" is erased.

import Colimit.Sequential.Very-erased

-- The sequential colimit HIT with an erased higher constructor.

import Colimit.Sequential.Erased

-- Sequential colimits.

import Colimit.Sequential

-- The one-step truncation HIT with an erased higher constructor.

import H-level.Truncation.Propositional.One-step.Erased

-- The one-step truncation.

import H-level.Truncation.Propositional.One-step

-- A non-recursive variant of H-level.Truncation.Propositional.Erased.

import H-level.Truncation.Propositional.Non-recursive.Erased

-- A variant of the propositional truncation operator with an erased
-- truncation constructor.

import H-level.Truncation.Propositional.Erased

-- Propositional truncation.

import H-level.Truncation.Propositional

-- A definition of the propositional truncation operator that does not
-- use recursive higher inductive types.

import H-level.Truncation.Propositional.Non-recursive

-- Some properties that hold for Erased do not hold for every
-- accessible modality.

import Erased.Counterexamples.Cubical

-- The "interval".

import Interval

-- Suspensions.

import Suspension

-- Spheres.

import Sphere

-- Pushouts, defined using a HIT.

import Pushout

-- Localisation.

import Localisation

-- Truncation, defined as a HIT.

import H-level.Truncation

-- Homotopy groups of pointed types.

import Pointed-type.Homotopy-group

-- Connectedness for pointed types.

import Pointed-type.Connected

-- A variant of set quotients with erased higher constructors.

import Quotient.Erased.Basics

-- Quotients (set-quotients), defined using a higher inductive type.

import Quotient

-- Two variants of the set quotients from Quotient.

import Quotient.Set-truncated-if-propositional
import Quotient.Higher-constructors-if-propositional

-- A variant of set quotients with erased higher constructors.

import Quotient.Erased

-- Cyclic groups.

import Group.Cyclic

-- Integers, defined using a quotient type.

import Integer.Quotient

-- The Eilenberg-MacLane space K(G, 1).

import Eilenberg-MacLane-space

-- Coherently constant functions.

import Coherently-constant

-- The "circle".

import Circle

-- The circle with an erased higher constructor.

import Circle.Erased

-- The torus, defined as a HIT.

import Torus

-- The figure of eight.

import Figure-of-eight

-- A variant of Nat.Wrapper.Cubical, defined using --erased-cubical.

import Nat.Wrapper.Cubical.Erased

-- A variant of the development in "Internalizing Representation
-- Independence with Univalence" (by Angiuli, Cavallo, Mörtberg and
-- Zeuner) with support for erasure.

import Structure-identity-principle.Erased

-- Truncated queues: any two queues representing the same sequence are
-- equal, and things are set up so that at compile-time (but not at
-- run-time) some queue operations compute in roughly the same way as
-- the corresponding list operations.

import Queue.Truncated

-- Queue instances for the queues in Queue.Truncated.

import Queue.Truncated.Instances

-- Quotiented queues: any two queues representing the same sequence
-- are equal.

import Queue.Quotiented

-- Queue instances for the queues in Queue.Quotiented.

import Queue.Quotiented.Instances

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
------------------------------------------------------------------------------
-- Translation of projection-like functions
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

-- 2012-04-03: More information about what is a projection-like in the
-- patch:
--
--   Mon Apr  2 02:41:41 COT 2012  Andreas Abel <andreas.abel@ifi.lmu.de>
--   * Type signatures and comments explaining what is considered projection-like.

-- 2012-02-23: The function P is not considered a projection-like
-- function after the patch:
--
--   Tue Feb 21 11:41:08 COT 2012  Nils Anders Danielsson <nils.anders.danielsson@gmail.com>
--   * The positivity checker (and more) is now only run once per mutual block.

-- 2011-09-23: From the Agda mailing list
-- Subject: Compiler internals for projection functions
-- There is some additional information about this issue.

-- 2011-09-19: Maybe the information in the issue 465 (Missing
-- patterns in funClauses) is useful.

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

module ProjectionLikeFunction where

open import Common.FOL

postulate
  N : D → Set

-- See Issue #81.
P : D → Set
P i = i ≡ i
{-# ATP definition P #-}

foo : ∀ {n} → N n → n ≡ n
foo {n} Nn = bar
  where
  postulate bar : P n
  {-# ATP prove bar #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
module _ where

open import Common.Prelude
open import Lib.Vec

_∘_ : ∀ {a b c} {A : Set a} {B : A → Set b} {C : ∀ x → B x → Set c}
         (f : ∀ {x} (y : B x) → C x y) (g : ∀ x → B x) → ∀ x → C x (g x)
(f ∘ g) x = f (g x)

sum : ∀ {n} → Vec Nat n → Nat
sum (x ∷ xs) = x + sum xs
sum [] = 0

foldl : ∀ {A}{B : Nat → Set} → (∀ {n} → B n → A → B (suc n)) → B 0 → ∀ {n} → Vec A n → B n
foldl {B = B} f z (x ∷ xs) = foldl {B = λ n → B (suc n)} f (f z x) xs
foldl f z [] = z

reverse : ∀ {A n} → Vec A n → Vec A n
reverse = foldl {B = Vec _} (λ xs x → x ∷ xs) []

downFrom : ∀ n → Vec Nat n
downFrom zero = []
downFrom (suc n) = n ∷ downFrom n

main : IO Unit
main = printNat (sum (reverse (downFrom 6000)))


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.NatSolver.Examples where

open import Cubical.Foundations.Prelude

open import Cubical.Data.FinData
open import Cubical.Data.Nat
open import Cubical.Data.Vec.Base

open import Cubical.Algebra.NatSolver.NatExpression
open import Cubical.Algebra.NatSolver.HornerForms
open import Cubical.Algebra.NatSolver.Solver
open import Cubical.Algebra.NatSolver.Reflection

private
  variable
    ℓ : Level

module ReflectionSolving where
  _ : (x y : ℕ) → (x + y) · (x + y) ≡ x · x + 2 · x · y + y · y
  _ = solve

  {-
    If you want to use the solver in some more complex situation,
    you have to declare a helper variable (`useSolver` below) that
    is a term of a dependent function type as above:
  -}
  module _ (SomeType : Type ℓ-zero) where
    complexSolverApplication :
      (someStuff : SomeType) → (x y : ℕ) → (moreStuff : SomeType)
      → x + y ≡ y + x
    complexSolverApplication someStuff x y moreStuff = useSolver x y
                              where useSolver : (x y : ℕ) → x + y ≡ y + x
                                    useSolver = solve

module SolvingExplained where
  open EqualityToNormalform renaming (solve to natSolve)
  open IteratedHornerOperations hiding (X)

  ℕ[X₀,X₁] = IteratedHornerForms 2
  X₀ : ℕ[X₀,X₁]
  X₀ = Variable 2 (Fin.zero)

  X₁ : ℕ[X₀,X₁]
  X₁ = Variable 2 (suc Fin.zero)

  Two : ℕ[X₀,X₁]
  Two = Constant 2 2

  _ : eval X₀ (1 ∷ 0 ∷ []) ≡ 1
  _ = refl

  _ : eval X₁ (0 ∷ 1 ∷ []) ≡ 1
  _ = refl

  X : Expr 3
  X = ∣ Fin.zero

  Y : Expr 3
  Y = ∣ (suc Fin.zero)

  Z : Expr 3
  Z = ∣ (suc (suc Fin.zero))

  {-
     'normalize' maps an expression to its Horner Normalform.
     Two expressions evaluating to the same ring element
     have the same Horner Normal form.
     This means equality of the represented ring elements
     can be checked by agda's unification (so refl is a proof)

   -}
  _ : normalize ((K 2) ·' X) ≡
      normalize (X +' X)
  _ = refl

  _ : normalize ((K 2) ·' X) ≡ normalize (X +' X)
  _ = refl

  _ : normalize (((K 2) ·' X) ·' Y) ≡ normalize (Y ·' (X +' X))
  _ = refl

  _ : normalize (Z ·' (((K 2) ·' X) ·' Y)) ≡ normalize (Z ·' (Y ·' (X +' X)))
  _ = refl

  {-
    The solver needs to produce an equality between
    actual ring elements. So we need a proof that
    those actual ring elements are equal to a normal form:
  -}
  _ : (x y z : ℕ) →
      eval (normalize ((K 2) ·' X ·' Y)) (x ∷ y ∷ z ∷ [])
      ≡ 2 · x · y
  _ = λ x y z → isEqualToNormalform ((K 2) ·' X ·' Y) (x ∷ y ∷ z ∷ [])

  {-
    Now two of these proofs can be plugged together
    to solve an equation:
  -}
  open Eval
  _ : (x y z : ℕ) → 3 + x + y · y ≡ y · y + x + 1 + 2
  _ = let
        lhs = (K 3) +' X +' (Y ·' Y)
        rhs = Y ·' Y +' X +' (K 1) +' (K 2)
      in (λ x y z →
          ⟦ lhs ⟧ (x ∷ y ∷ z ∷ [])
        ≡⟨ sym (isEqualToNormalform lhs (x ∷ y ∷ z ∷ [])) ⟩
          eval (normalize lhs) (x ∷ y ∷ z ∷ [])
        ≡⟨ refl ⟩
          eval (normalize rhs) (x ∷ y ∷ z ∷ [])
        ≡⟨ isEqualToNormalform rhs (x ∷ y ∷ z ∷ []) ⟩
          ⟦ rhs ⟧ (x ∷ y ∷ z ∷ []) ∎)

  {-
    Parts of that can be automated easily:
  -}
  _ : (x y z : ℕ) → (x + y) · (x + y) ≡ x · x + 2 · x · y + y · y
  _ = λ x y z → let
              lhs = (X +' Y) ·' (X +' Y)
              rhs = X ·' X +' (K 2) ·' X ·' Y +' Y ·' Y
             in natSolve lhs rhs (x ∷ y ∷ z ∷ []) refl

  {-
    A bigger example
  -}
  _ : (x y z : ℕ) → (x + y) · (x + y) · (x + y) · (x + y)
                ≡ x · x · x · x + 4 · x · x · x · y + 6 · x · x · y · y
                  +  4 · x · y · y · y + y · y · y · y
  _ = λ x y z → let
              lhs = (X +' Y) ·' (X +' Y) ·' (X +' Y) ·' (X +' Y)
              rhs = X ·' X ·' X ·' X
                  +' (K 4) ·' X ·' X ·' X ·' Y
                  +' (K 6) ·' X ·' X ·' Y ·' Y
                  +' (K 4) ·' X ·' Y ·' Y ·' Y
                  +' Y ·' Y ·' Y ·' Y
             in natSolve lhs rhs (x ∷ y ∷ z ∷ []) refl
  {-
    this one cannot work so far:

  _ : (x y z : ℕ) → (x + y) · (x - y) ≡ (x · x - (y · y))
  _ = λ x y z → let
                lhs = (X +' Y) ·' (X +' (-' Y))
                rhs = (X ·' X) +' (-' (Y ·' Y))
              in natSolve lhs rhs (x ∷ y ∷ z ∷ []) {!!}
  -}

max_stars_repo_name: FernandoLarrain/cubical


text:
module Tuples where

open import Haskell.Prelude

swap : a × b → b × a
swap (a , b) = b , a

{-# COMPILE AGDA2HS swap #-}

unit2unit : ⊤ → Tuple []
unit2unit tt = []

{-# COMPILE AGDA2HS unit2unit #-}


text:
-- Andreas, 2016-12-29, issue #2366
-- With clauses need to be printed in fresh environment,
-- as they DON'T shadow the pattern variables of the parent clause.
-- (These are not even in scope)

-- {-# OPTIONS -v error.checkclause:60 #-}

open import Agda.Builtin.List

test : {A : Set} → List A → List A
test (x ∷ y ∷ ys) with []
test (x ∷ xs) | q = []
test _ = []

-- ERROR WAS:
-- With clause pattern xs is not an instance of its parent pattern y ∷ ys
-- when checking that the clause
-- test (x ∷ y ∷ ys) with []
-- test (x₁ ∷ xs) | q = []
-- has type {A : Set} → List A → List A
-- NOTE THE x₁!

-- Expected error:
-- With clause pattern xs is not an instance of its parent pattern y ∷ ys
-- when checking that the clause
-- test (x ∷ y ∷ ys) with []
-- test (x ∷ xs) | q = []
-- has type {A : Set} → List A → List A

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


text:
open import Agda.Builtin.Equality
open import Agda.Builtin.Nat

foo : Nat → (Nat → Nat) → Nat
foo zero    f = f zero
foo (suc n) f = foo n λ n → f (suc n)

fsuc : (Nat → Nat) → Nat → Nat
fsuc f n = f (suc n)

foo' : Nat → (Nat → Nat) → Nat
foo' zero    f = f zero
foo' (suc n) f = foo' n (fsuc f)

foo'' : Nat → (Nat → Nat) → Nat
foo'' zero    f = f zero
foo'' (suc n) f = foo'' n λ { n → f (suc n) }

test : foo 50000 (λ n → n) ≡ 50000
test = refl

test' : foo' 50000 (λ n → n) ≡ 50000
test' = refl

test'' : foo'' 50000 (λ n → n) ≡ 50000
test'' = refl


text:
-- Andreas, 2013-02-27 issue reported by Nisse
-- {-# OPTIONS -v tc.polarity:100 -v tc.pos:100 #-}
module Issue802 where

data I : Set where
  i : I

mutual

  data P : I → Set where
    p : (x : I) → Q x x → P x

  Q : I → I → Set
  Q i = P
  -- Polarity of Q should be mixed for both arguments.

f : (x y : I) → Q x y → P y
f i _ q = q

data R (x : I) : P x → Set where
  r : (q : Q x x) → R _ (f x _ q) → R x (p x q)

-- Agda should solve the two meta variables in the type of r.


text:
module BHeap.Heap {A : Set}(_≤_ : A → A → Set) where

open import BHeap _≤_
open import Bound.Lower A
open import Bound.Lower.Order _≤_
open import BTree.Heap _≤_

lemma-bheap-heap : {b : Bound}(h : BHeap b) → Heap (forget h)
lemma-bheap-heap lf = leaf
lemma-bheap-heap (nd {x = x} _ lf lf) = single x
lemma-bheap-heap (nd _ (nd (lexy x≤y) l r) lf) = left x≤y (lemma-bheap-heap (nd (lexy x≤y) l r))
lemma-bheap-heap (nd _ lf (nd (lexy x≤y) l r)) = right x≤y (lemma-bheap-heap (nd (lexy x≤y) l r))
lemma-bheap-heap (nd _ (nd (lexy x≤y) l r) (nd (lexy x≤y') l' r')) = both x≤y x≤y' (lemma-bheap-heap (nd (lexy x≤y) l r)) (lemma-bheap-heap (nd (lexy x≤y') l' r'))

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
-- Andreas, 2013-09-17 catches a bug in constraint solving
-- with meta-variables applied to underapplied record constructors
-- {-# OPTIONS --show-implicit -v tc.meta.assign:50 -v tc.conv.elim:30 #-}
module Issue889 where

record Monad (M : Set → Set) : Set₁ where
  field
    return : ∀ {A} → A → M A
    _>>=_  : ∀ {A} {B : M A → Set} (m : M A) →
             ((x : A) → M (B (return x))) → M (B m)

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

_×_ : (A B : Set) → Set
A × B = Σ A λ _ → B

State : Set → Set → Set
State S X = S → X × S

-- Here is the underapplied record constructor
-- (made underapplied by eta-contraction, resp.).
state-return : ∀ {S X} → X → State S X
state-return x = _,_ x -- λ s → x , s

-- When giving the @_>>=_@ function to the record goal we get:
--
-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/TypeChecking/Conversion.hs:524
state-monad : ∀ {S} → Monad (State S)
state-monad {S} = record { return = state-return; _>>=_ = {!_>>=_!} }
  where
  postulate
    _>>=_ : ∀ {A} {B : State S A → Set} (m : State S A) →
          ((x : A) → State S (B (state-return x))) → State S (B m)
-- Bug arises when checking
--   _B (state-return x) = B (state-return x)
--   _B (_,_ x)          = B (_,_ x)
-- then Agda does something special for record constructors
-- [Miller unification in the presence of records]
-- (now only done for FULLY APPLIED record constructors!)
-- and produces some garbage solution for _B.

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

-- Note that if we define the product type using data instead of
-- record then it works:

data _×′_ (A B : Set) : Set where
  _,_ : A → B → A ×′ B

State′ : Set → Set → Set
State′ S X = S → X ×′ S

state-return′ : ∀ {S X} → X → State′ S X
state-return′ x = λ s → x , s

state-monad′ : ∀ {S} → Monad (State′ S)
state-monad′ {S} = record { return = state-return′; _>>=_ = _>>=_ }
  where
  postulate
    _>>=_ : ∀ {A} {B : State′ S A → Set} (m : State′ S A) →
          ((x : A) → State′ S (B (state-return′ x))) → State′ S (B m)


text:
open import AEff
open import EffectAnnotations
open import Renamings
open import Types hiding (``)

open import Relation.Binary.PropositionalEquality hiding ([_])

module Substitutions where

-- SET OF SUBSTITUTIONS BETWEEN CONTEXTS

Sub : Ctx → Ctx → Set
Sub Γ Γ' = {X : VType} → X ∈ Γ → Γ' ⊢V⦂ X

-- IDENTITY AND EXTENSION SUBSTITUTIONS

id-subst : {Γ : Ctx} → Sub Γ Γ
id-subst x = ` x

_[_]s : {Γ Γ' : Ctx} {X : VType} → Sub Γ Γ' → Γ' ⊢V⦂ X → Sub (Γ ∷ X) Γ'
(s [ V ]s) Hd = V
(s [ V ]s) (Tl x) = s x

-- LIFTING SUBSTITUTIONS

lift : {Γ Γ' : Ctx} {X : VType} → Sub Γ Γ' → Sub (Γ ∷ X) (Γ' ∷ X)
lift s Hd = ` Hd
lift s (Tl x) = V-rename Tl (s x)

-- ACTION OF SUBSTITUTION ON WELL-TYPED VALUES AND COMPUTATIONS

mutual

  infix 40 _[_]v
  infix 40 _[_]m

  _[_]v : {Γ Γ' : Ctx} → {X : VType} → Γ ⊢V⦂ X → Sub Γ Γ' → Γ' ⊢V⦂ X
  (` x) [ s ]v =
    s x
  (`` c) [ s ]v =
    `` c
  (ƛ M) [ s ]v =
    ƛ (M [ lift s ]m)
  ⟨ V ⟩ [ s ]v =
    ⟨ V [ s ]v ⟩

  _[_]m : {Γ Γ' : Ctx} → {C : CType} → Γ ⊢M⦂ C → Sub Γ Γ'  → Γ' ⊢M⦂ C
  (return V) [ s ]m =
    return (V [ s ]v)
  (let= M `in N) [ s ]m =
    let= (M [ s ]m) `in (N [ lift s ]m)
  (letrec M `in N) [ s ]m =
    letrec M [ lift (lift s) ]m `in (N [ lift s ]m)
  (V · W) [ s ]m =
    (V [ s ]v) · (W [ s ]v)
  (↑ op p V M) [ s ]m =
    ↑ op p (V [ s ]v) (M [ s ]m)
  (↓ op V M) [ s ]m =
    ↓ op (V [ s ]v) (M [ s ]m)
  (promise op ∣ p ↦ M `in N) [ s ]m =
    promise op ∣ p ↦ (M [ lift s ]m) `in (N [ lift s ]m)
  (await V until M) [ s ]m =
    await (V [ s ]v) until (M [ lift s ]m)
  (coerce p q M) [ s ]m =
    coerce p q (M [ s ]m)

-- ACTION OF SUBSTITUTION ON WELL-TYPED TERMS

infix 40 _[_]p

_[_]p : {Γ Γ' : Ctx} {o : O} {PP : PType o} → Γ ⊢P⦂ PP → Sub Γ Γ' → Γ' ⊢P⦂ PP
(run M) [ s ]p =
  run (M [ s ]m)
(P ∥ Q) [ s ]p =
  (P [ s ]p) ∥ (Q [ s ]p)
(↑ op p V P) [ s ]p =
  ↑ op p (V [ s ]v) (P [ s ]p)
(↓ op V P) [ s ]p =
  ↓ op (V [ s ]v) (P [ s ]p)

max_stars_repo_name: danelahman/aeff-agda

max_issues_repo_name: danelahman/aeff-agda

max_forks_repo_name: danelahman/aeff-agda


text:
------------------------------------------------------------------------------
-- Problem with a simplified version of the combinators for preorder
-- reasoning
------------------------------------------------------------------------------

{-# OPTIONS --allow-unsolved-metas     #-}
{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOT.Common.FOL.Relation.Binary.PreorderReasoning.ImplicitArgumentsProblem
  where

-- Nils suggested a possible problem with the relation

-- R : {A : Set} → A → A → Set
-- R _ _ = ⊤

-- and a version of the combinators for preorder reasoning without use
-- the wrapper data type. This example shows that Nils was right.

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

record ⊤ : Set where
  constructor tt

R : {A : Set} → A → A → Set
R _ _ = ⊤

R-refl : {A : Set}{x : A} → R x x
R-refl = tt

R-trans : {A : Set}{x y z : A} → R x y → R y z → R x z
R-trans _ _ = tt

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

module Thesis where
  -- From Ulf's thesis (p. 112).

  infix  7 _≃_
  infix  6 chain>_
  infixl 5 _===_by_
  infix  4 _qed

  data _≃_ {A : Set}(x y : A) : Set where
    prf : R x y → x ≃ y

  chain>_ : {A : Set}(x : A) → x ≃ x
  chain> x = prf (R-refl {x = x})

  _===_by_ : {A : Set}{x y : A} → x ≃ y → (z : A) → R y z → x ≃ z
  _===_by_ {x = x} {y} (prf p) z q = prf (R-trans {x = x} {y} {z} p q)

  _qed : {A : Set}{x y : A} → x ≃ y → R x y
  prf p qed = p

  -- Example (no problem with implicit arguments).
  test : (x y : ℕ) → R x y
  test x y =
    chain> x
      === y by tt
    qed

module SL where
  -- Adapted from the Agda standard library 0.8.1 (see
  -- Relation/Binary/PreorderReasoning.agda).

  infix  7 _≃_
  infix  4 begin_
  infixr 5 _≡⟨_⟩_
  infix  6 _∎

  data _≃_ {A : Set}(x y : A) : Set where
    prf : R x y → x ≃ y

  begin_ : {A : Set}{x y : A} → x ≃ y → R x y
  begin_ {x = x} (prf Rxy) = R-refl {x = x}

  _≡⟨_⟩_ : {A : Set}(x : A){y z : A} → R x y → y ≃ z → x ≃ z
  _≡⟨_⟩_ x {y} {z} Rxy (prf Ryz) = prf (R-trans {x = x} {y} {z} Rxy Ryz)

  _∎ : {A : Set}(x : A) → x ≃ x
  _∎ x = prf (R-refl {x = x})

  -- Example (no problem with implicit arguments).
  test : (x y : ℕ) → R x y
  test x y =
    begin
      x ≡⟨ tt ⟩
      y
    ∎

module NonWrapper where
  -- A set of combinators without request a wrapper data type (Mu,
  -- S.-C., Ko, H.-S. and Jansson, P. (2009)).

  infixr 5 _≡⟨_⟩_
  infix  6 _∎

  _≡⟨_⟩_ : {A : Set}(x : A){y z : A} → R x y → R y z → R x z
  _≡⟨_⟩_ x {y} {z} x≡y y≡z = R-trans {x = x} {y} {z} x≡y y≡z

  _∎ : {A : Set}(x : A) → R x x
  _∎ x = R-refl {x = x}

  -- Example.
  test : (x y : ℕ) → R x y
  test x y = x ≡⟨ tt ⟩
             y ∎

------------------------------------------------------------------------------
-- References
--
-- Mu, S.-C., Ko, H.-S. and Jansson, P. (2009). Algebra of programming
-- in Agda: Dependent types for relational program derivation. Journal
-- of Functional Programming 19.5, pp. 545–579.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{- wip, coming to realise that the instance of IsSetoid defined in Data.Equality.properties is over-eager (defining _≡_ for all (A : Set (a : Level)), _≡̇_ for ∀ (x : A : Set (a : Level)) → (B : A → Set (b : Level)) x -}
-- add samples of stuff from unification (AList, etc.)
module Oscar.Data5 where

record ⊤ : Set where
  constructor tt

Const_ : ∀ {a} {A : Set a} {b} {B : Set b} → B → A → B
Const_ x _ = x

infixr 20 _∷_

-- List
data ⟦_⟧ {a} (A : Set a) : Set a where
  ∅ : ⟦ A ⟧
  _∷_ : A → ⟦ A ⟧ → ⟦ A ⟧

-- Nat
⟦⟧ = ⟦ ⊤ ⟧

infix 21 ¡_
pattern ¡_ ⟦A⟧ = tt ∷ ⟦A⟧
--¡ : ⟦⟧ → ⟦⟧
--¡ ⟦A⟧ = tt ∷ ⟦A⟧

-- Fin (with a payload)
data ⟦_⟧[_] {a} (A : ⟦⟧ → Set a) : ⟦⟧ → Set a where
  ∅ : ∀ {n} → ⟦ A ⟧[ ¡ n ]
  _∷_ : ∀ {n} → A n → ⟦ A ⟧[ n ] → ⟦ A ⟧[ ¡ n ]

⟦⟧[_] = ⟦ Const ⊤ ⟧[_]

-- Vec (with an (optional) index)
data ⟦_⟧[_₀] {a} (A : ⟦⟧ → Set a) : ⟦⟧ → Set a where
  ∅ : ⟦ A ⟧[ ∅ ₀]
  _∷_ : ∀ {n} → A n → ⟦ A ⟧[ n ₀] → ⟦ A ⟧[ ¡ n ₀]

⟦⟧[_₀] = ⟦ Const ⊤ ⟧[_₀]

-- m ≤ n, counting down from n-1 to m
data ⟦_⟧[_≤_↓] {a} (A : ⟦⟧ → Set a) (m : ⟦⟧) : ⟦⟧ → Set a where
  ∅ : ⟦ A ⟧[ m ≤ m ↓]
  _∷_ : ∀ {n} → A n → ⟦ A ⟧[ m ≤ n ↓] → ⟦ A ⟧[ m ≤ ¡ n ↓]

⟦⟧[_≤_↓] = ⟦ Const ⊤ ⟧[_≤_↓]

-- m ≤ n, counting up from m to n-1
data ⟦_⟧[↑_≤_] {a} (A : ⟦⟧ → Set a) (m : ⟦⟧) : ⟦⟧ → Set a where
  ∅ : ⟦ A ⟧[↑ m ≤ m ]
  _∷_ : ∀ {n} → A m → ⟦ A ⟧[↑ ¡ m ≤ n ] → ⟦ A ⟧[↑ m ≤ n ]

⟦⟧[↑_≤_] = ⟦ Const ⊤ ⟧[↑_≤_]

-- Inj (almost)
data ⟦_⟧[↓_≤_↓] {a} (A : ⟦⟧ → ⟦⟧ → Set a) : ⟦⟧ → ⟦⟧ → Set a where
  ∅ : ∀ {n} → ⟦ A ⟧[↓ ∅ ≤ n ↓]
  _∷_ : ∀ {m n} → A m n → ⟦ A ⟧[↓ m ≤ n ↓] → ⟦ A ⟧[↓ ¡ m ≤ ¡ n ↓]

⟦⟧[↓_≤_↓] = ⟦ Const Const ⊤ ⟧[↓_≤_↓]

⟦_⟧[_⇒_]∞ : ∀ {a} (A : ⟦⟧ → Set a) → ⟦⟧ → ⟦⟧ → Set a
⟦ A ⟧[ m ⇒ n ]∞ = A m → A n

open import Oscar.Category.Semigroupoid
open import Oscar.Category.Category
open import Oscar.Category.Morphism
open import Oscar.Category.Setoid
--open import Oscar.Data.Equality
--open import Oscar.Data.Equality.properties
open import Oscar.Function

module _ {𝔬 𝔪 𝔮} (G : Semigroupoid 𝔬 𝔪 𝔮) where
  open Semigroupoid G

{-
  _≋̇_ : ∀ {a} {A : ⋆ → Set a} {m n : ⋆} → (A m → A n) → (A m → A n) → Set 𝔮
  _≋̇_ {A = A} {m = m} m→n₁ m→n₂ = {!∀ (am : A m) → m→n₁ am ≋ m→n₂ am!}

  cat2 : ∀ {a} (A : ⋆ → Set a) → Category {!!} {!!} {!!}
  Semigroupoid.⋆ (Category.semigroupoid (cat2 A)) = ⋆
  Setoid.⋆ ((Semigroupoid.𝔐 (Category.semigroupoid (cat2 A)) Morphism.⇒ m) n) = A m → A n
  IsSetoid._≋_ (Setoid.isSetoid ((Semigroupoid.𝔐 (Category.semigroupoid (cat2 A)) Morphism.⇒ m) n)) = _≡̇_
  IsSetoid.isEquivalence (Setoid.isSetoid ((Semigroupoid.𝔐 (Category.semigroupoid (cat2 A)) Morphism.⇒ m) n)) = it
  Semigroupoid._∙_ (Category.semigroupoid (cat2 A)) g f = g ∘ f
  Semigroupoid.isSemigroupoid (Category.semigroupoid (cat2 A)) = it
  Category.ε (cat2 A) = id
  Category.isCategory (cat2 A) = it
-}

  cat2G : ∀ {a} (A : ⋆ → Set a) → ∀ ℓ ⦃ _ : ∀ {n : ⋆} → IsSetoid (A n) ℓ ⦄ → Category {!!} {!!} {!!}
  Semigroupoid.⋆ (Category.semigroupoid (cat2G A ℓ)) = ⋆
  Setoid.⋆ ((Semigroupoid.𝔐 (Category.semigroupoid (cat2G A ℓ)) Morphism.⇒ m) n) = A m → A n
  IsSetoid._≋_ (Setoid.isSetoid ((Semigroupoid.𝔐 (Category.semigroupoid (cat2G A ℓ)) Morphism.⇒ m) n)) m↦n₁ m↦n₂ = ∀ (am : A m) → m↦n₁ am ≋ m↦n₂ am
  -- ∀ (am : A m) → m↦n₁ am ≋ m↦n₂ am
  {-
  _≋̇_ : ∀ {a} {A : ⋆ → Set a} {m n : ⋆} → (A m → A n) → (A m → A n) → Set 𝔮
  _≋̇_ {A = A} {m = m} m→n₁ m→n₂ = {!∀ (am : A m) → m→n₁ am ≋ m→n₂ am!}
  -}
  IsSetoid.isEquivalence (Setoid.isSetoid ((Semigroupoid.𝔐 (Category.semigroupoid (cat2G A ℓ)) Morphism.⇒ m) n)) = {!it!}
  Semigroupoid._∙_ (Category.semigroupoid (cat2G A ℓ)) g f = g ∘ f
  Semigroupoid.isSemigroupoid (Category.semigroupoid (cat2G A ℓ)) = {!it!}
  Category.ε (cat2G A ℓ) = id
  Category.isCategory (cat2G A ℓ) = {!it!}

infix 21 ‼_
pattern ‼_ ⟦A⟧ = tt ∷ ⟦A⟧ -- tricky, works for all above _∷_ constructors only because it is defined afterwards, won't work for any later-defined constructors

open import Agda.Primitive
open import Oscar.Data.Product
open import Oscar.Function

postulate
  ℓ : Level
  Term : ⟦⟧ → Set ℓ
  Step : ⟦⟧ → Set ℓ

Fin = ⟦⟧[_]

Inj = ⟦ Const Fin ⟧[↓_≤_↓]

Terms = λ N n → ⟦ Const (Term n) ⟧[ N ₀]

AList = ⟦ (λ n → Term n × Fin (¡ n)) ⟧[_≤_↓]

Fx : ∀ {a} {A : Set a} → A → A → ∀ {b₁} (B₁ : A → Set b₁) → ∀ {b₂} (B₂ : A → Set b₂) → Set (b₁ ⊔ b₂)
Fx m n B₁ B₂ = B₁ m → B₂ n

Fx₁ : ∀ {a} {A : Set a} → A → ∀ {b₁} (B₁ : A → Set b₁) → ∀ {b₂} (B₂ : A → Set b₂) → Set (b₁ ⊔ b₂)
Fx₁ n B₁ B₂ = Fx n n B₁ B₂

ListStep = λ n → ⟦ Step n ⟧

Rel : ∀ {a} {A : Set a} {b₁} (B₁ : A → Set b₁) {b₂} (B₂ : A → Set b₂) {c₁} (C₁ : A → Set c₁) {c₂} (C₂ : A → Set c₂) → Set (a ⊔ b₁ ⊔ b₂ ⊔ c₁ ⊔ c₂)
Rel B₁ B₂ C₁ C₂ = ∀ {m n} → Fx m n B₁ B₂ → Fx m n C₁ C₂

Morph : ∀ {a} {A : Set a} {b₁} {b₂} (B : (A → Set b₁) × (A → Set b₂)) {c₁} {c₂} (C₂ : (A → Set c₁) × (A → Set c₂)) → Set (a ⊔ b₁ ⊔ b₂ ⊔ c₁ ⊔ c₂)
Morph (B₁ , B₂) (C₁ , C₂) = ∀ {m n} → Fx m n B₁ B₂ → Fx m n C₁ C₂

-- functor mappings
postulate
  _◃_ : Morph (Fin , Term) (Term , Term)
  _◃s_ : ∀ N → Morph (Fin , Term) (Terms N , Terms N)
  sub : ∀ {m n} → AList m n → Fx m n Fin Term
  fmapS : Morph (Term , Term) (Step , Step)
  _◃S_ : Morph (Fin , Term) (ListStep , ListStep)

-- ?
postulate
  _⊹_ : ∀ {n} → ⟦ Step n ⟧ → Fx₁ n Term Term

testNat : ⟦⟧
testNat = ¡ ∅

testListNat : ⟦ ⟦⟧ ⟧
testListNat = ¡ ∅ ∷ ‼ ∅ ∷ ‼ ‼ ∅ ∷ ∅ ∷ ¡ ¡ ¡ ∅ ∷ ∅

testFin : ⟦⟧[ ¡ ¡ ∅ ]
testFin = ‼ ∅

test≤↓ : ⟦⟧[ ‼ ‼ ‼ ∅ ≤ ‼ ‼ ‼ ‼ ‼ ∅ ↓]
test≤↓ = ‼ ‼ ∅

⓪ ⑴ ⑵ ⑶ : ⟦⟧
⓪ = ∅
⑴ = ‼ ∅
⑵ = ‼ ⑴
⑶ = ‼ ⑵

testInj : Inj ⑵ ⑶
testInj = ‼ ∅ ∷ ∅ ∷ ∅


text:
module ProjectionLikeAndMatching where

data Unit : Set where
  * : Unit

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

-- Unbox should not be considered projection-like since it's matching on more than
-- the eliminatee.
unbox : ∀ {A} → Box A → Unit → A
unbox [ x ] * = x

postulate
  Thm : {A : Set} → A → Set
  prf : {A : Set}(x : A) → Thm x

-- If unbox was projection-like we would end up with
--   [_] (apply x) (elim unbox) (apply u) : A
-- and we wouldn't be able to reconstruct the parameter
-- argument to [_].
lem : ∀ {A} (x : A) u → Thm (unbox [ x ] u)
lem x u = prf (unbox [ x ] u)

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Induced preorders
------------------------------------------------------------------------

open import Relation.Binary

module Relation.Binary.InducedPreorders
         {s₁ s₂}
         (S : Setoid s₁ s₂)  -- The underlying equality.
         where

open import Function
open import Data.Product

open Setoid S

-- Every respectful unary relation induces a preorder. (No claim is
-- made that this preorder is unique.)

InducedPreorder₁ : ∀ {p} (P : Carrier → Set p) →
                   P Respects _≈_ → Preorder _ _ _
InducedPreorder₁ P resp = record
  { _≈_        = _≈_
  ; _∼_        = λ c₁ c₂ → P c₁ → P c₂
  ; isPreorder = record
    { isEquivalence = isEquivalence
    ; reflexive     = resp
    ; trans         = flip _∘′_
    }
  }

-- Every respectful binary relation induces a preorder. (No claim is
-- made that this preorder is unique.)

InducedPreorder₂ : ∀ {a r} {A : Set a} →
                   (_R_ : A → Carrier → Set r) →
                   (∀ {x} → _R_ x Respects _≈_) → Preorder _ _ _
InducedPreorder₂ _R_ resp = record
  { _≈_        = _≈_
  ; _∼_        = λ c₁ c₂ → ∀ {a} → a R c₁ → a R c₂
  ; isPreorder = record
    { isEquivalence = isEquivalence
    ; reflexive     = λ c₁≈c₂ → resp c₁≈c₂
    ; trans         = λ c₁∼c₂ c₂∼c₃ → c₂∼c₃ ∘ c₁∼c₂
    }
  }


text:
{-# OPTIONS --without-K --safe #-}
module Cats.Category.Setoids.Facts.Terminal where

open import Level
open import Relation.Binary using (Setoid)

open import Cats.Category
open import Cats.Category.Setoids using (Setoids)

import Data.Unit as Unit

⊤ : ∀ {l l′} → Setoid l l′
⊤ = record
  { Carrier = Lift _ Unit.⊤
  ; _≈_ = λ _ _ → Lift _ Unit.⊤
  }

instance
  hasTerminal : ∀ {l l≈} → HasTerminal (Setoids l l≈)
  hasTerminal = record { ⊤ = ⊤ }

max_stars_repo_name: JLimperg/cats

max_issues_repo_name: JLimperg/cats

max_forks_repo_name: JLimperg/cats


text:
module Data.QuadTree.Implementation.SafeFunctions where

open import Haskell.Prelude renaming (zero to Z; suc to S)
open import Data.Lens.Lens
open import Data.Logic
open import Data.QuadTree.Implementation.PropDepthRelation
open import Data.QuadTree.Implementation.Definition
open import Data.QuadTree.Implementation.ValidTypes
open import Data.QuadTree.Implementation.QuadrantLenses
open import Data.QuadTree.Implementation.DataLenses

{-# FOREIGN AGDA2HS
{-# LANGUAGE Safe #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE Rank2Types #-}
import Data.Nat
import Data.Lens.Lens
import Data.Logic

import Data.QuadTree.Implementation.Definition
import Data.QuadTree.Implementation.ValidTypes
import Data.QuadTree.Implementation.QuadrantLenses
import Data.QuadTree.Implementation.DataLenses
#-}

---- Safe functions

makeTreeSafe : {t : Set} {{eqT : Eq t}} -> (size : Nat × Nat) -> (v : t) -> VQuadTree t {maxDepth $ Wrapper size (Leaf v)}
makeTreeSafe (w , h) v = CVQuadTree (Wrapper (w , h) (Leaf v)) {andCombine (zeroLteAny (log2up $ max w h)) IsTrue.itsTrue} {eqReflexivity (maxDepth $ Wrapper (w , h) (Leaf v))}
{-# COMPILE AGDA2HS makeTreeSafe #-}

getLocationSafe : {t : Set} {{eqT : Eq t}}
  -> (loc : Nat × Nat) -> (dep : Nat)
  -> (qt : VQuadTree t {dep})
  -> {.(IsTrue (isInsideQuadTree loc (qtFromSafe qt)))}
  -> t
getLocationSafe index dep vqt {inside} = view (atLocation index dep {insideQTtoInsidePow index vqt inside}) vqt
{-# COMPILE AGDA2HS getLocationSafe #-}

setLocationSafe : {t : Set} {{eqT : Eq t}}
  -> (loc : Nat × Nat) -> (dep : Nat)
  -> t -> (qt : VQuadTree t {dep})
  -> {.(IsTrue (isInsideQuadTree loc (qtFromSafe qt)))}
  -> VQuadTree t {dep}
setLocationSafe index dep v vqt {inside} = set (atLocation index dep {insideQTtoInsidePow index vqt inside}) v vqt
{-# COMPILE AGDA2HS setLocationSafe #-}

mapLocationSafe : {t : Set} {{eqT : Eq t}}
  -> (loc : Nat × Nat) -> (dep : Nat)
  -> (t -> t) -> (qt : VQuadTree t {dep})
  -> {.(IsTrue (isInsideQuadTree loc (qtFromSafe qt)))}
  -> VQuadTree t {dep}
mapLocationSafe index dep f vqt {inside} = over (atLocation index dep {insideQTtoInsidePow index vqt inside}) f vqt
{-# COMPILE AGDA2HS mapLocationSafe #-}

max_stars_repo_name: JonathanBrouwer/research-project

max_issues_repo_name: JonathanBrouwer/research-project

max_forks_repo_name: JonathanBrouwer/research-project