text:
------------------------------------------------------------------------
-- Colists
------------------------------------------------------------------------

{-# OPTIONS --without-K --sized-types #-}

open import Equality

module Colist {c⁺} (eq : ∀ {a p} → Equality-with-J a p c⁺) where

private
  open module E = Derived-definitions-and-properties eq using (_≡_)

open import Logical-equivalence using (_⇔_)
open import Prelude
open import Prelude.Size

open import Conat eq as Conat using (Conat; zero; suc; force; infinity)
open import Function-universe eq hiding (id; _∘_)
import Nat eq as Nat

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

-- Colists.

mutual

  infixr 5 _∷_

  data Colist {a} (A : Type a) (i : Size) : Type a where
    []  : Colist A i
    _∷_ : A → Colist′ A i → Colist A i

  record Colist′ {a} (A : Type a) (i : Size) : Type a where
    coinductive
    field
      force : {j : Size< i} → Colist A j

open Colist′ public

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

-- A variant of cons.

infixr 5 _∷′_

_∷′_ : ∀ {i a} {A : Type a} → A → Colist A i → Colist A i
x ∷′ xs = x ∷ λ { .force → xs }

-- The colist's tail, if any.

tail : ∀ {a} {A : Type a} {i} → Colist A i → Colist′ A i
tail xs@[]    = λ { .force → xs }
tail (x ∷ xs) = xs

-- A map function.

map : ∀ {a b i} {A : Type a} {B : Type b} →
      (A → B) → Colist A i → Colist B i
map f []       = []
map f (x ∷ xs) = f x ∷ λ { .force → map f (force xs) }

-- The length of a colist.

length : ∀ {a i} {A : Type a} → Colist A i → Conat i
length []       = zero
length (n ∷ ns) = suc λ { .force → length (force ns) }

-- The colist replicate n x contains exactly n copies of x (and
-- nothing else).

replicate : ∀ {a i} {A : Type a} → Conat i → A → Colist A i
replicate zero    x = []
replicate (suc n) x = x ∷ λ { .force → replicate (force n) x }

-- Repeats the given element indefinitely.

repeat : ∀ {a i} {A : Type a} → A → Colist A i
repeat = replicate infinity

-- Appends one colist to another.

infixr 5 _++_

_++_ : ∀ {a i} {A : Type a} → Colist A i → Colist A i → Colist A i
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ λ { .force → force xs ++ ys }

-- The colist cycle x xs is an endless cycle of repetitions of the
-- colist x ∷ xs.

cycle : ∀ {a i} {A : Type a} → A → Colist′ A i → Colist A i
cycle x xs = x ∷ λ { .force → force xs ++ cycle x xs }

-- "Scan left".

scanl : ∀ {a b i} {A : Type a} {B : Type b} →
        (A → B → A) → A → Colist B i → Colist A i
scanl c n []       = n ∷ λ { .force → [] }
scanl c n (x ∷ xs) = n ∷ λ { .force → scanl c (c n x) (force xs) }

-- The natural numbers in strictly increasing order.

nats : ∀ {i} → Colist ℕ i
nats = 0 ∷ λ { .force → map suc nats }

-- The colist nats-from n is the natural numbers greater than or equal
-- to n, in strictly increasing order.

nats-from : ∀ {i} → ℕ → Colist ℕ i
nats-from n = n ∷ λ { .force → nats-from (suc n) }

-- The list take n xs is the longest possible prefix of xs that
-- contains at most n elements.

take : ∀ {a} {A : Type a} → ℕ → Colist A ∞ → List A
take zero    _        = []
take _       []       = []
take (suc n) (x ∷ xs) = x ∷ take n (force xs)

-- The sum of the successor of every element in the list.

sum-of-successors : ∀ {i} → Colist (Conat ∞) i → Conat i
sum-of-successors []       = zero
sum-of-successors (n ∷ ns) = suc λ { .force →
  n Conat.+ sum-of-successors (ns .force) }

------------------------------------------------------------------------
-- Bisimilarity

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

  -- [ ∞ ] xs ∼ ys means that xs and ys are "equal".

  mutual

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

    data [_]_∼_ (i : Size) : Colist A ∞ → Colist A ∞ → Type a where
      []  : [ i ] [] ∼ []
      _∷_ : ∀ {x y xs ys} →
            x ≡ y → [ i ] force xs ∼′ force ys → [ i ] x ∷ xs ∼ y ∷ ys

    record [_]_∼′_ (i : Size) (xs ys : Colist A ∞) : Type a where
      coinductive
      field
        force : {j : Size< i} → [ j ] xs ∼ ys

  open [_]_∼′_ public

  -- Bisimilarity is an equivalence relation.

  reflexive-∼ : ∀ {i} xs → [ i ] xs ∼ xs
  reflexive-∼ []       = []
  reflexive-∼ (x ∷ xs) =
    E.refl _ ∷ λ { .force → reflexive-∼ (force xs) }

  symmetric-∼ : ∀ {i xs ys} →
                [ i ] xs ∼ ys → [ i ] ys ∼ xs
  symmetric-∼ []        = []
  symmetric-∼ (p₁ ∷ p₂) =
    E.sym p₁ ∷ λ { .force → symmetric-∼ (force p₂) }

  transitive-∼ : ∀ {i xs ys zs} →
                 [ i ] xs ∼ ys → [ i ] ys ∼ zs → [ i ] xs ∼ zs
  transitive-∼ []        []        = []
  transitive-∼ (p₁ ∷ p₂) (q₁ ∷ q₂) =
    E.trans p₁ q₁ ∷ λ { .force → transitive-∼ (force p₂) (force q₂) }

  -- Equational reasoning combinators.

  infix  -1 _∎
  infixr -2 step-∼ step-≡ _∼⟨⟩_

  _∎ : ∀ {i} xs → [ i ] xs ∼ xs
  _∎ = reflexive-∼

  step-∼ : ∀ {i} xs {ys zs} →
           [ i ] ys ∼ zs → [ i ] xs ∼ ys → [ i ] xs ∼ zs
  step-∼ _ ys∼zs xs∼ys = transitive-∼ xs∼ys ys∼zs

  syntax step-∼ xs ys∼zs xs∼ys = xs ∼⟨ xs∼ys ⟩ ys∼zs

  step-≡ : ∀ {i} xs {ys zs} → [ i ] ys ∼ zs → xs ≡ ys → [ i ] xs ∼ zs
  step-≡ {i} _ ys∼zs xs≡ys = E.subst ([ i ]_∼ _) (E.sym xs≡ys) ys∼zs

  syntax step-≡ xs ys∼zs xs≡ys = xs ≡⟨ xs≡ys ⟩ ys∼zs

  _∼⟨⟩_ : ∀ {i} xs {ys} → [ i ] xs ∼ ys → [ i ] xs ∼ ys
  _ ∼⟨⟩ xs∼ys = xs∼ys

  -- A property relating Colist._∷_ and _∷′_.

  ∷∼∷′ : ∀ {i} {x : A} {xs} →
         [ i ] x ∷ xs ∼ x ∷′ force xs
  ∷∼∷′ = E.refl _ ∷ λ { .force → reflexive-∼ _ }

-- Functor laws.

map-id :
  ∀ {a i} {A : Type a} (xs : Colist A ∞) →
  [ i ] map id xs ∼ xs
map-id []       = []
map-id (_ ∷ xs) = E.refl _ ∷ λ { .force → map-id (force xs) }

map-∘ :
  ∀ {a b c i} {A : Type a} {B : Type b} {C : Type c}
    {f : B → C} {g : A → B}
  (xs : Colist A ∞) →
  [ i ] map (f ∘ g) xs ∼ map f (map g xs)
map-∘ []       = []
map-∘ (_ ∷ xs) = E.refl _ ∷ λ { .force → map-∘ (force xs) }

-- If two non-empty colists are bisimilar, then their heads are
-- bisimilar.

head-cong : ∀ {a i} {A : Type a} {x y : A} {xs ys} →
            [ i ] x ∷ xs ∼ y ∷ ys → x ≡ y
head-cong (p ∷ _) = p

-- Some preservation lemmas.

tail-cong :
  ∀ {a i} {A : Type a} {xs ys : Colist A ∞} →
  [ i ] xs ∼ ys → [ i ] force (tail xs) ∼′ force (tail ys)
tail-cong []       = λ { .force → [] }
tail-cong (_ ∷ ps) = ps

map-cong :
  ∀ {a b i} {A : Type a} {B : Type b} {f g : A → B} {xs ys} →
  (∀ x → f x ≡ g x) → [ i ] xs ∼ ys → [ i ] map f xs ∼ map g ys
map-cong             f≡g []                           = []
map-cong {f = f} {g} f≡g (_∷_ {x = x} {y = y} x≡y ps) =
  (f x  E.≡⟨ E.cong f x≡y ⟩
   f y  E.≡⟨ f≡g y ⟩∎
   g y  ∎) ∷ λ { .force →
  map-cong f≡g (force ps) }

length-cong :
  ∀ {a i} {A : Type a} {xs ys : Colist A ∞} →
  [ i ] xs ∼ ys → Conat.[ i ] length xs ∼ length ys
length-cong []       = zero
length-cong (_ ∷ ps) = suc λ { .force → length-cong (force ps) }

replicate-cong :
  ∀ {a i} {A : Type a} {m n} {x : A} →
  Conat.[ i ] m ∼ n → [ i ] replicate m x ∼ replicate n x
replicate-cong zero    = []
replicate-cong (suc p) =
  E.refl _ ∷ λ { .force → replicate-cong (force p) }

infixr 5 _++-cong_

_++-cong_ :
  ∀ {a i} {A : Type a} {xs₁ xs₂ ys₁ ys₂ : Colist A ∞} →
  [ i ] xs₁ ∼ ys₁ → [ i ] xs₂ ∼ ys₂ → [ i ] xs₁ ++ xs₂ ∼ ys₁ ++ ys₂
[]       ++-cong qs = qs
(p ∷ ps) ++-cong qs = p ∷ λ { .force → force ps ++-cong qs }

cycle-cong :
  ∀ {a i} {A : Type a} {x : A} {xs ys} →
  [ i ] force xs ∼′ force ys → [ i ] cycle x xs ∼ cycle x ys
cycle-cong p = E.refl _ ∷ λ { .force → force p ++-cong cycle-cong p }

scanl-cong :
  ∀ {a b i} {A : Type a} {B : Type b} {c : A → B → A} {n : A} {xs ys} →
  [ i ] xs ∼ ys → [ i ] scanl c n xs ∼ scanl c n ys
scanl-cong [] = E.refl _ ∷ λ { .force → [] }

scanl-cong {c = c} {n}
           (_∷_ {x = x} {y = y} {xs = xs} {ys = ys} x≡y ps) =
  E.refl n ∷ λ { .force →
    scanl c (c n x) (force xs)  ≡⟨ E.cong (λ x → scanl _ (c _ x) _) x≡y ⟩
    scanl c (c n y) (force xs)  ∼⟨ scanl-cong (force ps) ⟩
    scanl c (c n y) (force ys)  ∎ }

take-cong :
  ∀ {a} {A : Type a} n {xs ys : Colist A ∞} →
  [ ∞ ] xs ∼ ys → take n xs ≡ take n ys
take-cong n       []       = E.refl _
take-cong zero    (p ∷ ps) = E.refl _
take-cong (suc n) (p ∷ ps) = E.cong₂ _∷_ p (take-cong n (force ps))

sum-of-successors-cong :
  ∀ {i ms ns} →
  [ i ] ms ∼ ns →
  Conat.[ i ] sum-of-successors ms ∼ sum-of-successors ns
sum-of-successors-cong []       = zero
sum-of-successors-cong (p ∷ ps) = suc λ { .force →
  E.subst (Conat.[ _ ] _ ∼_) p (Conat.reflexive-∼ _)
    Conat.+-cong
  sum-of-successors-cong (ps .force) }

-- The length of replicate n x is bisimilar to n.

length-replicate :
  ∀ {a i} {A : Type a} {x : A} n →
  Conat.[ i ] length (replicate n x) ∼ n
length-replicate zero    = zero
length-replicate (suc n) =
  suc λ { .force → length-replicate (force n) }

-- A lemma relating nats and nats-from n.

map-+-nats∼nats-from :
  ∀ {i} n → [ i ] map (n +_) nats ∼ nats-from n
map-+-nats∼nats-from n = Nat.+-right-identity ∷ λ { .force →
  map (n +_) (map suc nats)  ∼⟨ symmetric-∼ (map-∘ _) ⟩
  map ((n +_) ∘ suc) nats    ∼⟨ map-cong (λ _ → E.sym (Nat.suc+≡+suc _)) (_ ∎) ⟩
  map (suc n +_) nats        ∼⟨ map-+-nats∼nats-from (suc n) ⟩
  nats-from (suc n)          ∎ }

-- The colist nats is bisimilar to nats-from 0.

nats∼nats-from-0 : ∀ {i} → [ i ] nats ∼ nats-from 0
nats∼nats-from-0 =
  nats             ∼⟨ symmetric-∼ (map-id _) ⟩
  map id nats      ∼⟨⟩
  map (0 +_) nats  ∼⟨ map-+-nats∼nats-from _ ⟩
  nats-from 0      ∎

------------------------------------------------------------------------
-- The ◇ predicate

-- ◇ ∞ P xs means that P holds for some element in xs.

data ◇ {a p} {A : Type a} (i : Size)
       (P : A → Type p) : Colist A ∞ → Type (a ⊔ p) where
  here  : ∀ {x xs} → P x → ◇ i P (x ∷ xs)
  there : ∀ {x xs} {j : Size< i} → ◇ j P (force xs) → ◇ i P (x ∷ xs)

-- ◇ respects bisimilarity.

◇-∼ :
  ∀ {a p i} {A : Type a} {P : A → Type p} {xs ys} →
  [ ∞ ] xs ∼ ys → ◇ i P xs → ◇ i P ys
◇-∼ (x≡y ∷ _) (here p)  = here (E.subst _ x≡y p)
◇-∼ (_   ∷ b) (there p) = there (◇-∼ (force b) p)

-- A map function for ◇.

◇-map : ∀ {a p q i} {A : Type a} {P : A → Type p} {Q : A → Type q} →
        (∀ {x} → P x → Q x) →
        (∀ {xs} → ◇ i P xs → ◇ i Q xs)
◇-map f (here p)  = here (f p)
◇-map f (there p) = there (◇-map f p)

-- A variant of ◇-map.

◇-map′ : ∀ {a b c p q i} {A : Type a} {B : Type b} {C : Type c}
           {P : B → Type p} {Q : C → Type q}
           {f : A → B} {g : A → C} →
         (∀ {x} → P (f x) → Q (g x)) →
         (∀ {xs} → ◇ i P (map f xs) → ◇ i Q (map g xs))
◇-map′ g {_ ∷ _} (here p)  = here (g p)
◇-map′ g {_ ∷ _} (there p) = there (◇-map′ g p)
◇-map′ g {[]}    ()

-- If a predicate holds for some element in a colist, then it holds
-- for some value.

◇-witness : ∀ {a p i} {A : Type a} {P : A → Type p} {xs} →
            ◇ i P xs → ∃ P
◇-witness (here p)  = _ , p
◇-witness (there p) = ◇-witness p

-- If const P holds for some element, then P holds.

◇-const : ∀ {a p i} {A : Type a} {P : Type p} {xs : Colist A ∞} →
          ◇ i (const P) xs → P
◇-const = proj₂ ∘ ◇-witness

-- Colist membership.

infix 4 [_]_∈_

[_]_∈_ : ∀ {a} {A : Type a} → Size → A → Colist A ∞ → Type a
[ i ] x ∈ xs = ◇ i (x ≡_) xs

-- A generalisation of "◇ ∞ P xs holds iff P holds for some element in
-- xs".

◇⇔∈× : ∀ {a p i} {A : Type a} {P : A → Type p} {xs} →
       ◇ i P xs ⇔ ∃ λ x → [ i ] x ∈ xs × P x
◇⇔∈× {P = P} = record { to = to; from = from }
  where
  to : ∀ {i xs} → ◇ i P xs → ∃ λ x → [ i ] x ∈ xs × P x
  to (here p)  = _ , here (E.refl _) , p
  to (there p) = Σ-map id (Σ-map there id) (to p)

  from : ∀ {i xs} → (∃ λ x → [ i ] x ∈ xs × P x) → ◇ i P xs
  from (x , here eq   , p) = here (E.subst P eq p)
  from (x , there x∈xs , p) = there (from (x , x∈xs , p))

-- If P holds for some element in replicate (suc n) x, then it also
-- holds for x, and vice versa.

◇-replicate-suc⇔ :
  ∀ {a p i} {A : Type a} {P : A → Type p} {x : A} {n} →
  ◇ i P (replicate (suc n) x) ⇔ P x
◇-replicate-suc⇔ {P = P} {x} = record
  { to   = to _
  ; from = here
  }
  where
  to : ∀ {i} n → ◇ i P (replicate n x) → P x
  to zero    ()
  to (suc n) (here p)  = p
  to (suc n) (there p) = to (force n) p

-- If P holds for some element in cycle x xs, then it also holds for
-- some element in x ∷ xs, and vice versa.

◇-cycle⇔ :
  ∀ {a p i} {A : Type a} {P : A → Type p} {x : A} {xs} →
  ◇ i P (cycle x xs) ⇔ ◇ i P (x ∷ xs)
◇-cycle⇔ {i = i} {P = P} {x} {xs} = record
  { to   = ◇ i P (cycle x xs)               ↝⟨ ◇-∼ (transitive-∼ ∷∼∷′ (symmetric-∼ ∷∼∷′)) ⟩
           ◇ i P ((x ∷ xs) ++ cycle x xs)   ↝⟨ to _ ⟩
           ◇ i P (x ∷ xs) ⊎ ◇ i P (x ∷ xs)  ↝⟨ [ id , id ] ⟩□
           ◇ i P (x ∷ xs)                   □
  ; from = ◇ i P (x ∷ xs)                  ↝⟨ from ⟩
           ◇ i P ((x ∷ xs) ++ cycle x xs)  ↝⟨ ◇-∼ (transitive-∼ ∷∼∷′ (symmetric-∼ ∷∼∷′)) ⟩□
           ◇ i P (cycle x xs)              □
  }
  where
  to : ∀ {i} ys → ◇ i P (ys ++ cycle x xs) → ◇ i P ys ⊎ ◇ i P (x ∷ xs)
  to []       (here p)  = inj₂ (here p)
  to []       (there p) = case to (force xs) p of
                            [ inj₂ ∘ there , inj₂ ]
  to (y ∷ ys) (here p)  = inj₁ (here p)
  to (y ∷ ys) (there p) = ⊎-map there id (to (force ys) p)

  from : ∀ {i ys} → ◇ i P ys → ◇ i P (ys ++ cycle x xs)
  from (here p)   = here p
  from (there ps) = there (from ps)

------------------------------------------------------------------------
-- The □ predicate

-- □ ∞ P xs means that P holds for every element in xs.

mutual

  data □ {a p} {A : Type a} (i : Size)
         (P : A → Type p) : Colist A ∞ → Type (a ⊔ p) where
    []  : □ i P []
    _∷_ : ∀ {x xs} → P x → □′ i P (force xs) → □ i P (x ∷ xs)

  record □′ {a p} {A : Type a} (i : Size)
            (P : A → Type p) (xs : Colist A ∞) : Type (a ⊔ p) where
    coinductive
    field
      force : {j : Size< i} → □ j P xs

open □′ public

-- Some projections.

□-head : ∀ {a p i} {A : Type a} {P : A → Type p} {x xs} →
         □ i P (x ∷ xs) → P x
□-head (p ∷ _) = p

□-tail : ∀ {a p i} {j : Size< i} {A : Type a} {P : A → Type p} {x xs} →
         □ i P (x ∷ xs) → □ j P (force xs)
□-tail (_ ∷ ps) = force ps

-- □ respects bisimilarity.

□-∼ :
  ∀ {i a p} {A : Type a} {P : A → Type p} {xs ys} →
  [ i ] xs ∼ ys → □ i P xs → □ i P ys
□-∼ []       _        = []
□-∼ (eq ∷ b) (p ∷ ps) =
  E.subst _ eq p ∷ λ { .force →
  □-∼ (force b) (force ps) }

-- A generalisation of "□ ∞ P xs holds iff P is true for every element
-- in xs".

□⇔∈→ : ∀ {a p i} {A : Type a} {P : A → Type p} {xs} →
       □ i P xs ⇔ (∀ x → [ i ] x ∈ xs → P x)
□⇔∈→ {P = P} = record { to = to; from = from _ }
  where
  to : ∀ {i xs} → □ i P xs → (∀ x → [ i ] x ∈ xs → P x)
  to (p ∷ ps) x (here eq)    = E.subst P (E.sym eq) p
  to (p ∷ ps) x (there x∈xs) = to (force ps) x x∈xs

  from : ∀ {i} xs → (∀ x → [ i ] x ∈ xs → P x) → □ i P xs
  from []       f = []
  from (x ∷ xs) f =
    f x (here (E.refl _)) ∷ λ { .force →
    from (force xs) (λ x → f x ∘ there) }

-- If P is universally true, then □ i P is also universally true.

□-replicate : ∀ {a p i} {A : Type a} {P : A → Type p} →
              (∀ x → P x) →
              (∀ xs → □ i P xs)
□-replicate f _ = _⇔_.from □⇔∈→ (λ x _ → f x)

-- Something resembling applicative functor application for □.

infixl 4 _□-⊛_

_□-⊛_ :
  ∀ {i a p q} {A : Type a} {P : A → Type p} {Q : A → Type q} {xs} →
  □ i (λ x → P x → Q x) xs → □ i P xs → □ i Q xs
[]       □-⊛ _        = []
(f ∷ fs) □-⊛ (p ∷ ps) = f p ∷ λ { .force → force fs □-⊛ force ps }

-- A map function for □.

□-map : ∀ {a p q i} {A : Type a} {P : A → Type p} {Q : A → Type q} →
        (∀ {x} → P x → Q x) →
        (∀ {xs} → □ i P xs → □ i Q xs)
□-map f ps = □-replicate (λ _ → f) _ □-⊛ ps

-- A variant of □-map.

□-map′ : ∀ {a b c p q i} {A : Type a} {B : Type b} {C : Type c}
           {P : B → Type p} {Q : C → Type q}
           {f : A → B} {g : A → C} →
         (∀ {x} → P (f x) → Q (g x)) →
         (∀ {xs} → □ i P (map f xs) → □ i Q (map g xs))
□-map′ g {[]}    []       = []
□-map′ g {_ ∷ _} (p ∷ ps) = g p ∷ λ { .force → □-map′ g (force ps) }

-- Something resembling applicative functor application for □ and ◇.

infixl 4 _□◇-⊛_

_□◇-⊛_ :
  ∀ {a p q i} {A : Type a} {P : A → Type p} {Q : A → Type q} {xs} →
  □ i (λ x → P x → Q x) xs → ◇ i P xs → ◇ i Q xs
(f ∷ _)  □◇-⊛ (here p)  = here (f p)
(_ ∷ fs) □◇-⊛ (there p) = there (force fs □◇-⊛ p)

-- A combination of some of the combinators above.

□◇-witness :
  ∀ {a p q i} {A : Type a} {P : A → Type p} {Q : A → Type q} {xs} →
  □ i P xs → ◇ i Q xs → ∃ λ x → P x × Q x
□◇-witness p q = ◇-witness (□-map _,_ p □◇-⊛ q)

-- If P holds for every element in replicate (suc n) x, then it also holds
-- for x, and vice versa.

□-replicate-suc⇔ :
  ∀ {a p i} {A : Type a} {P : A → Type p} {x : A} {n} →
  □ i P (replicate (suc n) x) ⇔ P x
□-replicate-suc⇔ {P = P} {x} = record
  { to   = □-head
  ; from = from _
  }
  where
  from : ∀ {i} n → P x → □ i P (replicate n x)
  from zero    p = []
  from (suc n) p = p ∷ λ { .force → from (force n) p }

-- If P holds for every element in cycle x xs, then it also holds for
-- every element in x ∷ xs, and vice versa.

□-cycle⇔ :
  ∀ {a p i} {A : Type a} {P : A → Type p} {x : A} {xs} →
  □ i P (cycle x xs) ⇔ □ i P (x ∷ xs)
□-cycle⇔ {i = i} {P = P} {x} {xs} = record
  { to   = □ i P (cycle x xs)              ↝⟨ (λ { (p ∷ ps) → p ∷ ps }) ⟩
           □ i P ((x ∷ xs) ++ cycle x xs)  ↝⟨ to _ ⟩□
           □ i P (x ∷ xs)                  □
  ; from = □ i P (x ∷ xs)                  ↝⟨ (λ hyp → from hyp hyp) ⟩
           □ i P ((x ∷ xs) ++ cycle x xs)  ↝⟨ (λ { (p ∷ ps) → p ∷ ps }) ⟩□
           □ i P (cycle x xs)              □
  }
  where
  to : ∀ {i} ys → □ i P (ys ++ cycle x xs) → □ i P ys
  to []       _        = []
  to (y ∷ ys) (p ∷ ps) = p ∷ λ { .force → to (force ys) (force ps) }

  from : ∀ {i ys} →
         □ i P (x ∷ xs) → □ i P ys → □ i P (ys ++ cycle x xs)
  from ps       (q ∷ qs) = q ∷ λ { .force → from ps (force qs) }
  from (p ∷ ps) []       = p ∷ λ { .force → from (p ∷ ps) (force ps) }

------------------------------------------------------------------------
-- A variant of ◇ with a sized predicate

-- ◇ˢ ∞ P xs means that (some instance of) P holds for some element in
-- xs.

data ◇ˢ {a p} {A : Type a} (i : Size)
        (P : Size → A → Type p) : Colist A ∞ → Type (a ⊔ p) where
  here  : ∀ {x xs} → P i x → ◇ˢ i P (x ∷ xs)
  there : ∀ {x xs} {j : Size< i} → ◇ˢ j P (force xs) → ◇ˢ i P (x ∷ xs)

-- ◇ˢ respects bisimilarity.

◇ˢ-∼ :
  ∀ {a p i} {A : Type a} {P : Size → A → Type p} {xs ys} →
  [ ∞ ] xs ∼ ys → ◇ˢ i P xs → ◇ˢ i P ys
◇ˢ-∼ (eq ∷ _) (here p)  = here (E.subst _ eq p)
◇ˢ-∼ (_  ∷ b) (there p) = there (◇ˢ-∼ (force b) p)

-- If P is upwards closed, then flip ◇ˢ P is upwards closed.

◇ˢ-upwards-closed :
  ∀ {a p} {A : Type a} {P : Size → A → Type p} →
  (∀ {i} {j : Size< i} {x} → P j x → P i x) →
  (∀ {i} {j : Size< i} {xs} → ◇ˢ j P xs → ◇ˢ i P xs)
◇ˢ-upwards-closed P-closed (here p)  = here (P-closed p)
◇ˢ-upwards-closed P-closed (there p) =
  there (◇ˢ-upwards-closed P-closed p)

-- A variant of the previous lemma.

◇ˢ-upwards-closed-∞ :
  ∀ {a p} {A : Type a} {P : Size → A → Type p} →
  (∀ {i x} → P i x → P ∞ x) →
  (∀ {i xs} → ◇ˢ i P xs → ◇ˢ ∞ P xs)
◇ˢ-upwards-closed-∞ P-closed-∞ (here p)  = here (P-closed-∞ p)
◇ˢ-upwards-closed-∞ P-closed-∞ (there p) =
  there (◇ˢ-upwards-closed-∞ P-closed-∞ p)

-- A map function for ◇ˢ.

◇ˢ-map :
  ∀ {a p q i}
    {A : Type a} {P : Size → A → Type p} {Q : Size → A → Type q} →
  (∀ {i x} → P i x → Q i x) →
  (∀ {xs} → ◇ˢ i P xs → ◇ˢ i Q xs)
◇ˢ-map f (here p)  = here (f p)
◇ˢ-map f (there p) = there (◇ˢ-map f p)

-- A variant of ◇ˢ-map.

◇ˢ-map′ : ∀ {a b c p q i} {A : Type a} {B : Type b} {C : Type c}
            {P : Size → B → Type p} {Q : Size → C → Type q}
            {f : A → B} {g : A → C} →
          (∀ {i x} → P i (f x) → Q i (g x)) →
          (∀ {xs} → ◇ˢ i P (map f xs) → ◇ˢ i Q (map g xs))
◇ˢ-map′ g {_ ∷ _} (here p)  = here (g p)
◇ˢ-map′ g {_ ∷ _} (there p) = there (◇ˢ-map′ g p)
◇ˢ-map′ g {[]}    ()

-- If a predicate holds for some element in a colist, then it holds
-- for some value (assuming that P is upwards closed).

◇ˢ-witness : ∀ {a p i} {A : Type a} {P : Size → A → Type p} {xs} →
             (∀ {i} {j : Size< i} {x} → P j x → P i x) →
             ◇ˢ i P xs → ∃ (P i)
◇ˢ-witness closed (here p)  = _ , p
◇ˢ-witness closed (there p) = Σ-map id closed (◇ˢ-witness closed p)

-- If P ∞ holds for some element in xs, then ◇ˢ ∞ P xs holds.

∈×∞→◇ˢ : ∀ {a p} {A : Type a} {P : Size → A → Type p} {x xs} →
         [ ∞ ] x ∈ xs → P ∞ x → ◇ˢ ∞ P xs
∈×∞→◇ˢ (here eq)    p = here (E.subst _ eq p)
∈×∞→◇ˢ (there x∈xs) p = there (∈×∞→◇ˢ x∈xs p)

-- If P i x implies P ∞ x for any i and x, then ◇ˢ ∞ P xs holds iff
-- P ∞ holds for some element in xs.

◇ˢ⇔∈× : ∀ {a p} {A : Type a} {P : Size → A → Type p} {xs} →
        (∀ {i x} → P i x → P ∞ x) →
        ◇ˢ ∞ P xs ⇔ (∃ λ x → [ ∞ ] x ∈ xs × P ∞ x)
◇ˢ⇔∈× {P = P} →∞ = record
  { to   = to
  ; from = λ { (_ , x∈xs , p) → ∈×∞→◇ˢ x∈xs p }
  }
  where
  to : ∀ {i xs} → ◇ˢ i P xs → ∃ λ x → [ ∞ ] x ∈ xs × P ∞ x
  to (here p)  = _ , here (E.refl _) , →∞ p
  to (there p) = Σ-map id (Σ-map there id) (to p)

-- Sized variants of the previous lemma.

◇ˢ→∈× : ∀ {a p} {A : Type a} {P : Size → A → Type p} →
        (∀ {i} {j : Size< i} {x} → P j x → P i x) →
        ∀ {i xs} → ◇ˢ i P xs → ∃ λ x → [ i ] x ∈ xs × P i x
◇ˢ→∈× closed (here p)  = _ , here (E.refl _) , p
◇ˢ→∈× closed (there p) = Σ-map id (Σ-map there closed) (◇ˢ→∈× closed p)

∈×→◇ˢ : ∀ {a p} {A : Type a} {P : Size → A → Type p} →
        (∀ {i} {j : Size< i} {x} → P i x → P j x) →
        ∀ {i x xs} → [ i ] x ∈ xs → P i x → ◇ˢ i P xs
∈×→◇ˢ closed (here eq)    p = here (E.subst _ eq p)
∈×→◇ˢ closed (there x∈xs) p = there (∈×→◇ˢ closed x∈xs (closed p))

-- ◇ ∞ (P ∞) is "contained in" ◇ˢ ∞ P.

◇∞→◇ˢ∞ : ∀ {a p} {A : Type a} {P : Size → A → Type p} {xs} →
         ◇ ∞ (P ∞) xs → ◇ˢ ∞ P xs
◇∞→◇ˢ∞ {P = P} {xs} =
  ◇ ∞ (P ∞) xs                    ↝⟨ _⇔_.to ◇⇔∈× ⟩
  (∃ λ x → [ ∞ ] x ∈ xs × P ∞ x)  ↝⟨ (λ { (_ , x∈xs , p) → ∈×∞→◇ˢ x∈xs p }) ⟩□
  ◇ˢ ∞ P xs                       □

-- If P i x implies P ∞ x for any i and x, then ◇ˢ ∞ P is pointwise
-- logically equivalent to ◇ ∞ (P ∞).

◇ˢ∞⇔◇∞ : ∀ {a p} {A : Type a} {P : Size → A → Type p} {xs} →
         (∀ {i x} → P i x → P ∞ x) →
         ◇ˢ ∞ P xs ⇔ ◇ ∞ (P ∞) xs
◇ˢ∞⇔◇∞ {P = P} {xs} →∞ =
  ◇ˢ ∞ P xs                       ↝⟨ ◇ˢ⇔∈× →∞ ⟩
  (∃ λ x → [ ∞ ] x ∈ xs × P ∞ x)  ↝⟨ inverse ◇⇔∈× ⟩□
  ◇ ∞ (P ∞) xs                    □

-- ◇ˢ i (const P) is pointwise logically equivalent to ◇ i P.

◇ˢ⇔◇ : ∀ {a p i} {A : Type a} {P : A → Type p} {xs} →
       ◇ˢ i (λ _ → P) xs ⇔ ◇ i P xs
◇ˢ⇔◇ {P = P} {xs} = record { to = to; from = from }
  where
  to : ∀ {i xs} → ◇ˢ i (λ _ → P) xs → ◇ i P xs
  to (here p)  = here p
  to (there p) = there (to p)

  from : ∀ {i xs} → ◇ i P xs → ◇ˢ i (λ _ → P) xs
  from (here p)  = here p
  from (there p) = there (from p)

-- If ◇ˢ i P (x ∷ xs) holds, then ◇ˢ i P (cycle x xs) also holds.

◇ˢ-cycle← :
  ∀ {a p i} {A : Type a} {P : Size → A → Type p} {x : A} {xs} →
  ◇ˢ i P (x ∷ xs) → ◇ˢ i P (cycle x xs)
◇ˢ-cycle← {i = i} {P = P} {x} {xs} =
  ◇ˢ i P (x ∷ xs)                  ↝⟨ from ⟩
  ◇ˢ i P ((x ∷ xs) ++ cycle x xs)  ↝⟨ ◇ˢ-∼ (transitive-∼ ∷∼∷′ (symmetric-∼ ∷∼∷′)) ⟩□
  ◇ˢ i P (cycle x xs)              □
  where
  from : ∀ {i ys} → ◇ˢ i P ys → ◇ˢ i P (ys ++ cycle x xs)
  from (here p)   = here p
  from (there ps) = there (from ps)

-- If P i x implies P ∞ x for any i and x, then ◇ˢ ∞ P (cycle x xs) is
-- logically equivalent to ◇ˢ ∞ P (x ∷ xs).

◇ˢ-cycle⇔ :
  ∀ {a p} {A : Type a} {P : Size → A → Type p} {x : A} {xs} →
  (∀ {i x} → P i x → P ∞ x) →
  ◇ˢ ∞ P (cycle x xs) ⇔ ◇ˢ ∞ P (x ∷ xs)
◇ˢ-cycle⇔ {P = P} {x} {xs} →∞ = record
  { to   = ◇ˢ ∞ P (cycle x xs)                ↝⟨ ◇ˢ-∼ (transitive-∼ ∷∼∷′ (symmetric-∼ ∷∼∷′)) ⟩
           ◇ˢ ∞ P ((x ∷ xs) ++ cycle x xs)    ↝⟨ to _ ⟩
           ◇ˢ ∞ P (x ∷ xs) ⊎ ◇ˢ ∞ P (x ∷ xs)  ↝⟨ [ id , id ] ⟩□
           ◇ˢ ∞ P (x ∷ xs)                    □
  ; from = ◇ˢ-cycle←
  }
  where
  to :
    ∀ {i} ys → ◇ˢ i P (ys ++ cycle x xs) → ◇ˢ ∞ P ys ⊎ ◇ˢ ∞ P (x ∷ xs)
  to []       (here p)  = inj₂ (here (→∞ p))
  to []       (there p) = case to (force xs) p of
                            [ inj₂ ∘ there , inj₂ ]
  to (y ∷ ys) (here p)  = inj₁ (here (→∞ p))
  to (y ∷ ys) (there p) = ⊎-map there id (to (force ys) p)

------------------------------------------------------------------------
-- A variant of □ with a sized predicate

-- □ˢ ∞ P xs means that (some instance of) P holds for every element
-- in xs.

mutual

  data □ˢ {a p} {A : Type a} (i : Size)
          (P : Size → A → Type p) : Colist A ∞ → Type (a ⊔ p) where
    []  : □ˢ i P []
    _∷_ : ∀ {x xs} → P i x → □ˢ′ i P (force xs) → □ˢ i P (x ∷ xs)

  record □ˢ′ {a p} {A : Type a} (i : Size)
             (P : Size → A → Type p) (xs : Colist A ∞) :
             Type (a ⊔ p) where
    coinductive
    field
      force : {j : Size< i} → □ˢ j P xs

open □ˢ′ public

-- Some projections.

□ˢ-head : ∀ {a p i} {A : Type a} {P : Size → A → Type p} {x xs} →
          □ˢ i P (x ∷ xs) → P i x
□ˢ-head (p ∷ _) = p

□ˢ-tail : ∀ {a p i} {j : Size< i}
            {A : Type a} {P : Size → A → Type p} {x xs} →
          □ˢ i P (x ∷ xs) → □ˢ j P (force xs)
□ˢ-tail (_ ∷ ps) = force ps

-- □ˢ respects bisimilarity.

□ˢ-∼ :
  ∀ {i a p} {A : Type a} {P : Size → A → Type p} {xs ys} →
  [ i ] xs ∼ ys → □ˢ i P xs → □ˢ i P ys
□ˢ-∼ []       _        = []
□ˢ-∼ (eq ∷ b) (p ∷ ps) =
  E.subst _ eq p ∷ λ { .force →
  □ˢ-∼ (force b) (force ps) }

-- If P is downwards closed, then flip □ˢ P is downwards closed.

□ˢ-downwards-closed :
  ∀ {a p} {A : Type a} {P : Size → A → Type p} →
  (∀ {i} {j : Size< i} {x} → P i x → P j x) →
  (∀ {i} {j : Size< i} {xs} → □ˢ i P xs → □ˢ j P xs)
□ˢ-downwards-closed P-closed []       = []
□ˢ-downwards-closed P-closed (p ∷ ps) =
  P-closed p ∷ λ { .force → □ˢ-downwards-closed P-closed (force ps) }

-- A variant of the previous lemma.

□ˢ-downwards-closed-∞ :
  ∀ {a p} {A : Type a} {P : Size → A → Type p} →
  (∀ {i x} → P ∞ x → P i x) →
  (∀ {i xs} → □ˢ ∞ P xs → □ˢ i P xs)
□ˢ-downwards-closed-∞ P-closed-∞ []       = []
□ˢ-downwards-closed-∞ P-closed-∞ (p ∷ ps) =
  P-closed-∞ p ∷ λ { .force →
  □ˢ-downwards-closed-∞ P-closed-∞ (force ps) }

-- If □ˢ ∞ P xs holds, then P ∞ holds for every element in xs.

□ˢ∞∈→ : ∀ {a p} {A : Type a} {P : Size → A → Type p} {xs x} →
        □ˢ ∞ P xs → [ ∞ ] x ∈ xs → P ∞ x
□ˢ∞∈→ (p ∷ ps) (here eq)    = E.subst _ (E.sym eq) p
□ˢ∞∈→ (p ∷ ps) (there x∈xs) = □ˢ∞∈→ (force ps) x∈xs

-- If P ∞ x implies P i x for any i and x, then □ˢ ∞ P xs holds iff P ∞
-- holds for every element in xs.

□ˢ⇔∈→ : ∀ {a p} {A : Type a} {P : Size → A → Type p} {xs} →
        (∀ {i x} → P ∞ x → P i x) →
        □ˢ ∞ P xs ⇔ (∀ x → [ ∞ ] x ∈ xs → P ∞ x)
□ˢ⇔∈→ {P = P} ∞→ = record { to = λ p _ → □ˢ∞∈→ p; from = from _ }
  where
  from : ∀ {i} xs → (∀ x → [ ∞ ] x ∈ xs → P ∞ x) → □ˢ i P xs
  from []       f = []
  from (x ∷ xs) f =
    ∞→ (f x (here (E.refl _))) ∷ λ { .force →
    from (force xs) (λ x → f x ∘ there) }

-- Sized variants of the previous lemma.

□ˢ∈→ : ∀ {a p} {A : Type a} {P : Size → A → Type p} →
       (∀ {i} {j : Size< i} {x} → P j x → P i x) →
       ∀ {i x xs} → □ˢ i P xs → [ i ] x ∈ xs → P i x
□ˢ∈→ closed (p ∷ ps) (here eq)    = E.subst _ (E.sym eq) p
□ˢ∈→ closed (p ∷ ps) (there x∈xs) = closed (□ˢ∈→ closed (force ps) x∈xs)

∈→→□ˢ : ∀ {a p} {A : Type a} {P : Size → A → Type p} →
        (∀ {i} {j : Size< i} {x} → P i x → P j x) →
        ∀ {i} xs → (∀ x → [ i ] x ∈ xs → P i x) → □ˢ i P xs
∈→→□ˢ closed []       f = []
∈→→□ˢ closed (x ∷ xs) f =
  f x (here (E.refl _)) ∷ λ { .force →
  ∈→→□ˢ closed (force xs) (λ x → closed ∘ f x ∘ there) }

-- □ˢ ∞ P is "contained in" □ ∞ (P ∞).

□ˢ∞→□∞ : ∀ {a p} {A : Type a} {P : Size → A → Type p} {xs} →
         □ˢ ∞ P xs → □ ∞ (P ∞) xs
□ˢ∞→□∞ {P = P} {xs} =
  □ˢ ∞ P xs                     ↝⟨ (λ p _ → □ˢ∞∈→ p) ⟩
  (∀ x → [ ∞ ] x ∈ xs → P ∞ x)  ↝⟨ _⇔_.from □⇔∈→ ⟩□
  □ ∞ (P ∞) xs                  □

-- If P ∞ x implies P i x for any i and x, then □ˢ ∞ P is pointwise
-- logically equivalent to □ ∞ (P ∞).

□ˢ∞⇔□∞ : ∀ {a p} {A : Type a} {P : Size → A → Type p} {xs} →
         (∀ {i x} → P ∞ x → P i x) →
         □ˢ ∞ P xs ⇔ □ ∞ (P ∞) xs
□ˢ∞⇔□∞ {P = P} {xs} ∞→ =
  □ˢ ∞ P xs                     ↝⟨ □ˢ⇔∈→ ∞→ ⟩
  (∀ x → [ ∞ ] x ∈ xs → P ∞ x)  ↝⟨ inverse □⇔∈→ ⟩□
  □ ∞ (P ∞) xs                  □

-- □ˢ i (const P) is pointwise logically equivalent to □ i P.

□ˢ⇔□ : ∀ {a p i} {A : Type a} {P : A → Type p} {xs} →
       □ˢ i (λ _ → P) xs ⇔ □ i P xs
□ˢ⇔□ {P = P} {xs} = record { to = to; from = from }
  where
  to : ∀ {i xs} → □ˢ i (λ _ → P) xs → □ i P xs
  to []       = []
  to (p ∷ ps) = p ∷ λ { .force → to (force ps) }

  from : ∀ {i xs} → □ i P xs → □ˢ i (λ _ → P) xs
  from []       = []
  from (p ∷ ps) = p ∷ λ { .force → from (force ps) }

-- If P is universally true, then □ˢ i P is also universally true.

□ˢ-replicate : ∀ {a p i} {A : Type a} {P : Size → A → Type p} →
               (∀ {i} x → P i x) →
               (∀ xs → □ˢ i P xs)
□ˢ-replicate f []       = []
□ˢ-replicate f (x ∷ xs) = f x ∷ λ { .force → □ˢ-replicate f (force xs) }

-- Something resembling applicative functor application for □ˢ.

infixl 4 _□ˢ-⊛_

_□ˢ-⊛_ : ∀ {i a p q} {A : Type a}
           {P : Size → A → Type p} {Q : Size → A → Type q} {xs} →
         □ˢ i (λ j x → P j x → Q j x) xs → □ˢ i P xs → □ˢ i Q xs
[]       □ˢ-⊛ _        = []
(f ∷ fs) □ˢ-⊛ (p ∷ ps) = f p ∷ λ { .force → force fs □ˢ-⊛ force ps }

-- A map function for □ˢ.

□ˢ-map :
  ∀ {a p q i}
    {A : Type a} {P : Size → A → Type p} {Q : Size → A → Type q} →
  (∀ {i x} → P i x → Q i x) →
  (∀ {xs} → □ˢ i P xs → □ˢ i Q xs)
□ˢ-map f ps = □ˢ-replicate (λ _ → f) _ □ˢ-⊛ ps

-- A variant of □ˢ-map.

□ˢ-map′ : ∀ {a b c p q i} {A : Type a} {B : Type b} {C : Type c}
            {P : Size → B → Type p} {Q : Size → C → Type q}
            {f : A → B} {g : A → C} →
          (∀ {i x} → P i (f x) → Q i (g x)) →
          (∀ {xs} → □ˢ i P (map f xs) → □ˢ i Q (map g xs))
□ˢ-map′ g {[]}    []       = []
□ˢ-map′ g {_ ∷ _} (p ∷ ps) = g p ∷ λ { .force → □ˢ-map′ g (force ps) }

-- Something resembling applicative functor application for □ˢ and ◇ˢ.

infixl 4 _□ˢ◇ˢ-⊛_

_□ˢ◇ˢ-⊛_ : ∀ {a p q i} {A : Type a}
             {P : Size → A → Type p} {Q : Size → A → Type q} {xs} →
           □ˢ i (λ j x → P j x → Q j x) xs → ◇ˢ i P xs → ◇ˢ i Q xs
(f ∷ _)  □ˢ◇ˢ-⊛ (here p)  = here (f p)
(_ ∷ fs) □ˢ◇ˢ-⊛ (there p) = there (force fs □ˢ◇ˢ-⊛ p)

-- A combination of some of the combinators above.

□ˢ◇ˢ-witness :
  ∀ {a p q i}
    {A : Type a} {P : Size → A → Type p} {Q : Size → A → Type q} {xs} →
  (∀ {i} {j : Size< i} {x} → P j x → P i x) →
  (∀ {i} {j : Size< i} {x} → Q j x → Q i x) →
  □ˢ i P xs → ◇ˢ i Q xs → ∃ λ x → P i x × Q i x
□ˢ◇ˢ-witness P-closed Q-closed p q =
  ◇ˢ-witness (λ { {_} {_} → Σ-map P-closed Q-closed })
             (□ˢ-map _,_ p □ˢ◇ˢ-⊛ q)

-- If □ˢ i P (cycle x xs) holds, then □ˢ i P (x ∷ xs) also holds.

□ˢ-cycle→ :
  ∀ {a p i} {A : Type a} {P : Size → A → Type p} {x : A} {xs} →
  □ˢ i P (cycle x xs) → □ˢ i P (x ∷ xs)
□ˢ-cycle→ {i = i} {P = P} {x} {xs} =
  □ˢ i P (cycle x xs)              ↝⟨ (λ { (p ∷ ps) → p ∷ ps }) ⟩
  □ˢ i P ((x ∷ xs) ++ cycle x xs)  ↝⟨ to _ ⟩□
  □ˢ i P (x ∷ xs)                  □
  where
  to : ∀ {i} ys → □ˢ i P (ys ++ cycle x xs) → □ˢ i P ys
  to []       _        = []
  to (y ∷ ys) (p ∷ ps) = p ∷ λ { .force → to (force ys) (force ps) }

-- If P ∞ x implies P i x for any i and x, then □ˢ ∞ P (cycle x xs) is
-- logically equivalent to □ˢ ∞ P (x ∷ xs).

□ˢ-cycle⇔ :
  ∀ {a p} {A : Type a} {P : Size → A → Type p} {x : A} {xs} →
  (∀ {i x} → P ∞ x → P i x) →
  □ˢ ∞ P (cycle x xs) ⇔ □ˢ ∞ P (x ∷ xs)
□ˢ-cycle⇔ {P = P} {x} {xs} ∞→ = record
  { to   = □ˢ-cycle→
  ; from = □ˢ ∞ P (x ∷ xs)                  ↝⟨ (λ hyp → from hyp hyp) ⟩
           □ˢ ∞ P ((x ∷ xs) ++ cycle x xs)  ↝⟨ (λ { (p ∷ ps) → p ∷ ps }) ⟩□
           □ˢ ∞ P (cycle x xs)              □
  }
  where
  from : ∀ {i ys} →
         □ˢ ∞ P (x ∷ xs) → □ˢ i P ys → □ˢ i P (ys ++ cycle x xs)
  from ps       (q ∷ qs) = q ∷ λ { .force → from ps (force qs) }
  from (p ∷ ps) []       = ∞→ p ∷ λ { .force →
                           from (p ∷ ps) (force ps) }

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


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

module Dodo.Binary.Transitive where

-- Stdlib imports
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; _≢_; refl)
open import Level using (Level; _⊔_)
open import Function using (flip; _∘_)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_,_; _×_; proj₁; proj₂; ∃-syntax)
open import Relation.Unary using (Pred; _∈_)
open import Relation.Binary using (Rel; REL)
open import Relation.Binary using (Transitive)
open import Relation.Binary.Construct.Closure.Transitive using (TransClosure; [_]; _∷_; _∷ʳ_; _++_)
-- Local imports
open import Dodo.Unary.Equality
open import Dodo.Binary.Equality
open import Dodo.Binary.Domain

⁺-flip : {a ℓ : Level} {A : Set a} → {R : Rel A ℓ}
  → {x y : A}
  → TransClosure R x y
  → TransClosure (flip R) y x
⁺-flip [ x∼y ]      = [ x∼y ]
⁺-flip (x∼z ∷ z∼⁺y) = ⁺-flip z∼⁺y ∷ʳ x∼z

⁺-map : {a b ℓ₁ ℓ₂ : Level} {A : Set a} {B : Set b}
  → {R : Rel A ℓ₁} {Q : Rel B ℓ₂}
  → (f : A → B)
  → (map : ∀ {x y : A} → R x y → Q (f x) (f y))
  → {x y : A}
  → TransClosure R x y
  → TransClosure Q (f x) (f y)
⁺-map _ map [ Rxy ] = [ map Rxy ]
⁺-map _ map ( Rxz ∷ R⁺zy ) = map Rxz ∷ ⁺-map _ map R⁺zy

⁺-dom : ∀ {a ℓ : Level} {A : Set a} {R : Rel A ℓ}
  → {x y : A}
  → TransClosure R x y
    ------------------
  → x ∈ dom R
⁺-dom {R = R} [ Rxy ] = take-dom R Rxy
⁺-dom {R = R} ( Rxz ∷ R⁺zy ) = take-dom R Rxz

⁺-codom : ∀ {a ℓ : Level} {A : Set a} {R : Rel A ℓ}
  → {x y : A}
  → TransClosure R x y
    ------------------
  → y ∈ codom R
⁺-codom {R = R} [ Rxy ] = take-codom R Rxy
⁺-codom {R = R} ( Rxz ∷ R⁺zy ) = ⁺-codom R⁺zy

⁺-udrˡ : ∀ {a ℓ : Level} {A : Set a} {R : Rel A ℓ}
  → {x y : A}
  → TransClosure R x y
    ------------------
  → x ∈ udr R
⁺-udrˡ = inj₁ ∘ ⁺-dom

⁺-udrʳ : ∀ {a ℓ : Level} {A : Set a} {R : Rel A ℓ}
  → {x y : A}
  → TransClosure R x y
    ------------------
  → y ∈ udr R
⁺-udrʳ = inj₂ ∘ ⁺-codom

⁺-predʳ : {a ℓ₁ ℓ₂ : Level} {A : Set a} {P : Pred A ℓ₁} {R : Rel A ℓ₂}
  → (f : ∀ {x y : A} → P x → R x y → P y)
  → {x y : A}
  → TransClosure R x y
  → P x
  → P y
⁺-predʳ f [ Rxy ]        Px = f Px Rxy
⁺-predʳ f ( Rxz ∷ R⁺zy ) Px = ⁺-predʳ f R⁺zy (f Px Rxz)

⁺-predˡ : {a ℓ₁ ℓ₂ : Level} {A : Set a} {P : Pred A ℓ₁} {R : Rel A ℓ₂}
  → (f : ∀ {x y : A} → P y → R x y → P x)
  → {x y : A}
  → TransClosure R x y
  → P y
  → P x
⁺-predˡ f [ Rxy ]        Px = f Px Rxy
⁺-predˡ f ( Rxz ∷ R⁺zy ) Px = f (⁺-predˡ f R⁺zy Px) Rxz

⁺-lift-predʳ : {a ℓ₁ ℓ₂ : Level} {A : Set a} {P : Pred A ℓ₁} {R : Rel A ℓ₂}
  → (f : ∀ {x y : A} → R x y → P y)
  → {x y : A}
  → TransClosure R x y
  → P y
⁺-lift-predʳ f [ Rxy ] = f Rxy
⁺-lift-predʳ f ( Rxz ∷ R⁺zy ) = ⁺-lift-predʳ f R⁺zy

⁺-lift-predˡ : {a ℓ₁ ℓ₂ : Level} {A : Set a} {P : Pred A ℓ₁} {R : Rel A ℓ₂}
  → (f : ∀ {x y : A} → R x y → P x)
  → {x y : A}
  → TransClosure R x y
  → P x
⁺-lift-predˡ f [ Rxy ] = f Rxy
⁺-lift-predˡ f ( Rxz ∷ R⁺zy ) = f Rxz

module _ {a ℓ : Level} {A : Set a} {R : Rel A ℓ} where

  ⁺-idem : TransClosure R ⇔₂ TransClosure (TransClosure R)
  ⁺-idem = ⇔: ⊆-proof ⊇-proof
    where
    ⊆-proof : TransClosure R ⊆₂' TransClosure (TransClosure R)
    ⊆-proof _ _ R⁺xy = [ R⁺xy ]

    ⊇-proof : TransClosure (TransClosure R) ⊆₂' TransClosure R
    ⊇-proof _ _ [ R⁺xy ] = R⁺xy
    ⊇-proof _ y ( _∷_ {_} {z} R⁺xz R⁺⁺zy ) = R⁺xz ++ ⊇-proof z y R⁺⁺zy

  ⁺-join : ∀ {x y : A} → TransClosure (TransClosure R) x y → TransClosure R x y
  ⁺-join = ⇔₂-apply-⊇₂ ⁺-idem

module _ {a ℓ : Level} {A : Set a} {R : Rel A ℓ} where

  ⁺-preserves-dom : dom R ⇔₁ dom (TransClosure R)
  ⁺-preserves-dom = ⇔: ⊆-proof ⊇-proof
    where
    ⊆-proof : dom R ⊆₁' dom (TransClosure R)
    ⊆-proof x (y , Rxy) = (y , [ Rxy ])

    ⊇-proof : dom (TransClosure R) ⊆₁' dom R
    ⊇-proof x (y , R⁺xy) = ⁺-dom R⁺xy

  ⁺-preserves-codom : codom R ⇔₁ codom (TransClosure R)
  ⁺-preserves-codom = ⇔: ⊆-proof ⊇-proof
    where
    ⊆-proof : codom R ⊆₁' codom (TransClosure R)
    ⊆-proof y (x , Rxy) = (x , [ Rxy ])

    ⊇-proof : codom (TransClosure R) ⊆₁' codom R
    ⊇-proof y (x , R⁺xy) = ⁺-codom R⁺xy

  ⁺-preserves-udr : udr R ⇔₁ udr (TransClosure R)
  ⁺-preserves-udr = ⇔: ⊆-proof ⊇-proof
    where
    ⊆-proof : udr R ⊆₁' udr (TransClosure R)
    ⊆-proof _ (inj₁ x∈dom)   = inj₁ (⇔₁-apply-⊆₁ ⁺-preserves-dom x∈dom)
    ⊆-proof _ (inj₂ x∈codom) = inj₂ (⇔₁-apply-⊆₁ ⁺-preserves-codom x∈codom)

    ⊇-proof : udr (TransClosure R) ⊆₁' udr R
    ⊇-proof _ (inj₁ x∈dom)   = inj₁ (⇔₁-apply-⊇₁ ⁺-preserves-dom x∈dom)
    ⊇-proof _ (inj₂ x∈codom) = inj₂ (⇔₁-apply-⊇₁ ⁺-preserves-codom x∈codom)

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

  ⁺-preserves-⊆₂ : P ⊆₂ Q → TransClosure P ⊆₂ TransClosure Q
  ⁺-preserves-⊆₂ P⊆Q = ⊆: lemma
    where
    lemma : TransClosure P ⊆₂' TransClosure Q
    lemma _ _ [ Pxy ] = [ ⊆₂-apply P⊆Q Pxy ]
    lemma _ y ( _∷_ {_} {z} Pxz P⁺zy ) = ⊆₂-apply P⊆Q Pxz ∷ lemma z y P⁺zy

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

  ⁺-preserves-⇔₂ : P ⇔₂ Q → TransClosure P ⇔₂ TransClosure Q
  ⁺-preserves-⇔₂ = ⇔₂-compose ⁺-preserves-⊆₂ ⁺-preserves-⊆₂

module _ {a ℓ : Level} {A : Set a} {R : Rel A ℓ} where

  ⁺-trans-⇔₂ : Transitive R → R ⇔₂ TransClosure R
  ⁺-trans-⇔₂ transR = ⇔: ⊆-proof ⊇-proof
    where
    ⊆-proof : R ⊆₂' TransClosure R
    ⊆-proof _ _ = [_]

    ⊇-proof : TransClosure R ⊆₂' R
    ⊇-proof _ _ [ Rxy ] = Rxy
    ⊇-proof _ y (_∷_ {_} {w} Rxw R⁺wy) = transR Rxw (⊇-proof w y R⁺wy)

  ⁺-trans-⊆₂ : Transitive R → TransClosure R ⊆₂ R
  ⁺-trans-⊆₂ transR = ⇔₂-to-⊇₂ (⁺-trans-⇔₂ transR)

  ⁺-join-trans : Transitive R → {x y : A} → TransClosure R x y → R x y
  ⁺-join-trans = ⊆₂-apply ∘ ⁺-trans-⊆₂

  ⁺-unconsʳ :
      {x y : A}
    → TransClosure R x y
    → R x y ⊎ ∃[ z ] (TransClosure R x z × R z y)
  ⁺-unconsʳ [ Rxy ] = inj₁ Rxy
  ⁺-unconsʳ ( Rxz ∷ R⁺zy ) with ⁺-unconsʳ R⁺zy
  ... | inj₁ Rzy = inj₂ (_ , [ Rxz ] , Rzy)
  ... | inj₂ (v , R⁺zv , Rvy) = inj₂ (v , Rxz ∷ R⁺zv , Rvy)

ext: agda

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


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

module Data.List.Filter where

open import Prelude
open import Data.List
open import Data.List.Membership
open import Data.Sigma.Properties
open import Data.Bool.Properties
open import Data.Fin

module _ {p} {P : A → Type p} where
  filter : (P? : ∀ x → Dec (P x)) → List A → List (∃ P)
  filter P? = foldr f []
    where
    f : _ → List (∃ P) → List (∃ P)
    f y ys with P? y
    ... | yes t = (y , t) ∷ ys
    ... | no _  = ys

  filter-preserves : (isPropP : ∀ x → isProp (P x)) (P? : ∀ x → Dec (P x)) (xs : List A) →
                     (x : A) →
                     (v : P x) →
                     (x ∈ xs) →
                     ((x , v) ∈ filter P? xs)
  filter-preserves isPropP P? (x ∷ xs) y v (n , y∈xs) with P? x
  filter-preserves isPropP P? (x ∷ xs) y v (f0   , y∈xs) | yes t = f0 , ΣProp≡ isPropP y∈xs
  filter-preserves isPropP P? (x ∷ xs) y v (fs n , y∈xs) | yes t = let m , q = filter-preserves isPropP P? xs y v (n , y∈xs) in fs m , q
  filter-preserves isPropP P? (x ∷ xs) y v (f0   , y∈xs) | no ¬t = ⊥-elim (¬t (subst P (sym y∈xs) v))
  filter-preserves isPropP P? (x ∷ xs) y v (fs n , y∈xs) | no ¬t = filter-preserves isPropP P? xs y v (n , y∈xs)

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
open import FRP.JS.Nat using ( ℕ ; float ) renaming
  ( _+_ to _+n_ ; _∸_ to _∸n_ ; _*_ to _*n_ ; _≟_ to _≟n_ ; _≠_ to _≠n_
  ; _/_ to _/n_ ; _/?_ to _/?n_ ; _≤_ to _≤n_ ; _<_ to _<n_ )
open import FRP.JS.Float using ( ℝ )
open import FRP.JS.Bool using ( Bool )
open import FRP.JS.True using ( True )
open import FRP.JS.Maybe using ( Maybe )

module FRP.JS.Delay where

record Delay : Set where
  constructor _ms
  field toℕ : ℕ

{-# COMPILED_JS Delay function(x,v) { return v["_ms"](x); } #-}
{-# COMPILED_JS _ms function(d) { return d; } #-}

_≟_ : Delay → Delay → Bool
(d ms) ≟ (e ms) = d ≟n e

{-# COMPILED_JS _≟_ function(d) { return function(e) { return d === e; }; } #-}

_≠_ : Delay → Delay → Bool
(d ms) ≠ (e ms) = d ≠n e

{-# COMPILED_JS _≠_ function(d) { return function(e) { return d !== e; }; } #-}

_≤_ : Delay → Delay → Bool
(d ms) ≤ (e ms) = d ≤n e

{-# COMPILED_JS _≤_ function(d) { return function(e) { return d <= e; }; } #-}

_<_ : Delay → Delay → Bool
(d ms) < (e ms) = d <n e

{-# COMPILED_JS _<_ function(d) { return function(e) { return d < e; }; } #-}

_+_ : Delay → Delay → Delay
(d ms) + (e ms) = (d +n e) ms

{-# COMPILED_JS _+_ function(d) { return function(e) { return d + e; }; } #-}

_∸_ : Delay → Delay → Delay
(d ms) ∸ (e ms) = (d ∸n e) ms

{-# COMPILED_JS _∸_ function(d) { return function(e) { return Math.min(0, d - e); }; } #-}

_*_ : ℕ → Delay → Delay
n * (d ms) = (n *n d) ms

{-# COMPILED_JS _*_ function(n) { return function(d) { return n * d; }; } #-}

_/_ : ∀ (d e : Delay) → {e≠0 : True (e ≠ 0 ms)} → ℝ
_/_ (d ms) (e ms) {e≠0} = _/n_ d e {e≠0}

{-# COMPILED_JS _/_ function(d) { return function(e) { return function() { return d / e; }; }; } #-}

_/?_ : Delay → Delay → Maybe ℝ
(d ms) /? (e ms) = d /?n e

{-# COMPILED_JS _/?_ function(d) { return function(e) { if (e === 0) { return null; } else { return d / e; } }; } #-}

_sec : ℕ → Delay
n sec = n * (1000 ms)

{-# COMPILED_JS _sec function(t) { return t * 1000; } #-}

_min : ℕ → Delay
n min = n * (60000 ms)

{-# COMPILED_JS _min function(t) { return t * 60000; } #-}

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
-- This variant of the code is due to Ulf Norell.

open import Agda.Builtin.Size

data ⊥ : Set where

mutual

  data Unit (i : Size) : Set where
    c : Unit′ i → Unit i

  data Unit₁ (i : Size) : Set where
    c₁ : ⊥ → Unit i → Unit₁ i

  record Unit′ (i : Size) : Set where
    coinductive
    field
      force : {j : Size< i} → Unit₁ j

open Unit′ public

tail : Unit ∞ → Unit₁ ∞
tail (c x) = force x

u : (∀ {i} → Unit′ i → Unit i) →
    ∀ {i} → Unit₁ i
u cons = tail (cons λ { .force → u cons })

bad : Unit₁ ∞
bad = u c

refute : Unit₁ ∞ → ⊥
refute (c₁ () _)

loop : ⊥
loop = refute bad

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import Relation.Binary.Core

module Definitions
  {a ℓ} {A : Set a}   -- The underlying set
  (_≈_ : Rel A ℓ)     -- The underlying equality
  where

open import Algebra.Core
open import Data.Product
open import Algebra.Definitions

Alternativeˡ : Op₂ A → Set _
Alternativeˡ _∙_ = ∀ x y  →  ((x ∙ x) ∙ y) ≈ (x ∙ (y ∙ y))

Alternativeʳ : Op₂ A → Set _
Alternativeʳ _∙_ = ∀ x y → (x ∙ (y ∙ y)) ≈ ((x ∙ y) ∙ y)

Alternative : Op₂ A → Set _
Alternative _∙_ = (Alternativeˡ _∙_ ) × ( Alternativeʳ _∙_)

Flexible : Op₂ A → Set _
Flexible _∙_ = ∀ x y → ((x ∙ y) ∙ x) ≈ (x ∙ (y ∙ x))

Medial : Op₂ A → Set _
Medial _∙_ = ∀ x y u z → ((x ∙ y) ∙ (u ∙ z)) ≈ ((x ∙ u) ∙ (y ∙ z))

LeftSemimedial : Op₂ A → Set _
LeftSemimedial _∙_ = ∀ x y z → ((x ∙ x) ∙ (y ∙ z)) ≈ ((x ∙ y) ∙ (x ∙ z))

RightSemimedial : Op₂ A → Set _
RightSemimedial _∙_ = ∀ x y z → ((y ∙ z) ∙ (x ∙ x)) ≈ ((y ∙ x) ∙ (z ∙ x))

Semimedial : Op₂ A → Set _
Semimedial _∙_ = (LeftSemimedial _∙_) × (RightSemimedial _∙_)

LatinSquare₁ : Op₂ A → Set _
LatinSquare₁ _*_ = ∀ a b x  → (a * x) ≈ b

LatinSquare₂ : Op₂ A → Set _
LatinSquare₂ _*_ = ∀ a b y → (y * a) ≈ b

LatinSquare : Op₂ A → Set _
LatinSquare _*_ = (LatinSquare₁ _*_) × (LatinSquare₂ _*_)

LeftBol : Op₂ A → Set _
LeftBol _∙_ = ∀ x y z → (x ∙ (y ∙ (x ∙ z))) ≈ ((x ∙ (y ∙ z)) ∙ z )

RightBol : Op₂ A → Set _
RightBol _∙_ = ∀ x y z → (((z ∙ x) ∙ y) ∙ x) ≈ (z ∙ ((x ∙ y) ∙ x))

MoufangIdentity₁ : Op₂ A → Set _
MoufangIdentity₁  _∙_  = ∀ x y z → (z ∙ (x ∙ (z ∙ y))) ≈ (((z ∙ x) ∙ z) ∙ y)

MoufangIdentity₂ : Op₂ A → Set _
MoufangIdentity₂ _∙_ = ∀ x y z → (x ∙ (z ∙ (y ∙ z))) ≈ (((x ∙ z) ∙ y) ∙ z)

MoufangIdentity₃ : Op₂ A → Set _
MoufangIdentity₃ _∙_ = ∀ x y z → ((z ∙ x) ∙ (y ∙ z)) ≈ ((z ∙ (x ∙ y)) ∙ z)

MoufangIdentity₄ : Op₂ A → Set _
MoufangIdentity₄ _∙_ = ∀ x y z → ((z ∙ x) ∙ (y ∙ z)) ≈ (z ∙ ((x ∙ y) ∙ z))

-- (x²y)x = x²(yx)
JordanIdentity: : Op₂ A → Set _
JordanIdentity: _∙_ = ∀ x y → (((x ∙ x) ∙ y) ∙ x) ≈ (((x ∙ x) ∙ y) ∙ x)

-- x = xyx
PesudoInverse₁ : Op₂ A → Set _
PesudoInverse₁ _∙_ = ∀ x y → ((x ∙ y) ∙ x) ≈ x

-- y = yxy
PseudoInverse₂ : Op₂ A → Set _
PseudoInverse₂ _∙_ = ∀ x y → ((y ∙ x) ∙ y) ≈ y

PseudoInverse : Op₂ A → Set _
PseudoInverse ∙ = (PesudoInverse₁ ∙) × (PseudoInverse₂ ∙)

-- JacobiIdentity is (x ∙ (y ∙ z)) + ((y ∙ (z ∙ x)) + (z ∙ (x ∙ y))) = 0
-- Using the antisymmetry property Jacobi identity may be rewritten as a modification of the associative property

JacobiIdentity : Op₂ A → Op₂ A → Set _
JacobiIdentity _∙_  _-_ = ∀ x y z → (x ∙ (y ∙ z)) ≈ ((y ∙ (z ∙ x)) - (z ∙ (x ∙ y)))


text:
-- Andreas, 2014-06-16

data D A : Set where
  c : {x : A} → A → D A

f : ∀(A : Set) → D A → Set
f A (c a b) = D A

-- Expected error:
-- The constructor c expects 2 arguments (including hidden ones), but
-- has been given 3 (including hidden ones)
-- when checking that the pattern c a b has type D A

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --without-K #-}
open import HoTT.Base using (𝒰 ; Level ; module variables)

module HoTT.Exercises.Chapter1 where

open variables

module Exercise1 where
  open HoTT.Base hiding (_∘_)

  _∘_ : {A B C : 𝒰 i} (g : B → C) (f : A → B) → A → C
  g ∘ f = λ x → g (f x)

  _ : {A B C D : 𝒰 i} {f : A → B} {g : B → C} {h : C → D} →
      h ∘ (g ∘ f) == (h ∘ g) ∘ f
  _ = refl

module Exercise2 where
  open HoTT.Base hiding (×-rec ; Σ-rec)

  ×-rec : (C : 𝒰 i) → (A → B → C) → A × B → C
  ×-rec _ g x = g (pr₁ x) (pr₂ x)

  _ : {C : 𝒰 i} {g : A → B → C} {a : A} {b : B} →
      ×-rec C g (a , b) == g a b
  _ = refl

  Σ-rec : (C : 𝒰 i) → ((x : A) → P x → C) → Σ A P → C
  Σ-rec _ g x = g (pr₁ x) (pr₂ x)

  _ : {C : 𝒰 i} {g : (x : A) → P x → C} {a : A} {b : P a} →
      Σ-rec C g (a , b) == g a b
  _ = refl

module Exercise3 where
  open HoTT.Base hiding (×-ind ; Σ-ind)

  ×-ind : {A B : 𝒰 i} (C : A × B → 𝒰 i) →
            ((a : A) → (b : B) → C (a , b)) → (x : A × B) → C x
  ×-ind C g x = transport C (×-uniq x) (g (pr₁ x) (pr₂ x))

  Σ-ind : {A : 𝒰 i} {B : A → 𝒰 i} (C : Σ A B → 𝒰 i) →
          ((a : A) → (b : B a) → C (a , b)) → (x : Σ A B) → C x
  Σ-ind C g x = transport C (Σ-uniq x) (g (pr₁ x) (pr₂ x))

module Exercise4 where
  open HoTT.Base hiding (ℕ-rec)

  iter : (C : 𝒰 i) → C → (C → C) → ℕ → C
  iter C c₀ cₛ 0 = c₀
  iter C c₀ cₛ (succ n) = cₛ (iter C c₀ cₛ n)

  f : {C : 𝒰 i} {cₛ : ℕ → C → C} → ℕ × C → ℕ × C
  f {cₛ = cₛ} (n , c) = succ n , cₛ n c

  iterℕ : (C : 𝒰 i) → C → (ℕ → C → C) → ℕ → ℕ × C
  iterℕ C c₀ cₛ n = iter (ℕ × C) (0 , c₀) (f {C = C} {cₛ = cₛ}) n

  ℕ-rec : (C : 𝒰 i) → C → (ℕ → C → C) → ℕ → C
  ℕ-rec C c₀ cₛ n = pr₂ (iterℕ C c₀ cₛ n)

  module _ {C : 𝒰 i} {c₀ : C} {cₛ : ℕ → C → C} where
    _ : ℕ-rec C c₀ cₛ 0 == c₀
    _ = refl

    _ : (n : ℕ) → ℕ-rec C c₀ cₛ (succ n) == cₛ n (ℕ-rec C c₀ cₛ n)
    _ = ℕ-ind D d₀ dₛ
      where
      E : ℕ → 𝒰₀
      E n = pr₁ (iterℕ C c₀ cₛ n) == n
      e₀ : E 0
      e₀ = refl
      eₛ : (n : ℕ) → E n → E (succ n)
      eₛ n = ×-ind (λ z → pr₁ z == n → pr₁ (f z) == succ n)
        (λ _ _ p → ap succ p) (iterℕ C c₀ cₛ n)

      D : ℕ → 𝒰 i
      D n = ℕ-rec C c₀ cₛ (succ n) == cₛ n (ℕ-rec C c₀ cₛ n)
      d₀ : D 0
      d₀ = refl
      dₛ : (n : ℕ) → D n → D (succ n)
      dₛ n _ = ×-ind (λ z → pr₁ z == n → pr₂ (f (f z)) == cₛ (succ n) (pr₂ (f z)))
        (λ x y p → ap (λ n → cₛ (succ n) (cₛ x y)) p)
        (iterℕ C c₀ cₛ n) (ℕ-ind E e₀ eₛ n)

module Exercise5 where
  open HoTT.Base hiding (_+_ ; inl ; inr ; +-ind)

  _+_ : 𝒰 i → 𝒰 i → 𝒰 i
  _+_ A B = Σ[ x ∶ 𝟐 ] (𝟐-rec A B x)

  private variable C : A + B → 𝒰 i

  inl : A → A + B
  inl a = 0₂ , a

  inr : B → A + B
  inr b = 1₂ , b

  +-ind : (C : A + B → 𝒰 i) → ((a : A) → C (inl a)) → ((b : B) → C (inr b)) →
          (x : A + B) → C x
  +-ind C g₀ g₁ (0₂ , a) = g₀ a
  +-ind C g₀ g₁ (1₂ , b) = g₁ b

  _ : {g₀ : (a : A) → C (inl a)} {g₁ : (b : B) → C (inr b)} {a : A} →
      +-ind C g₀ g₁ (inl a) == g₀ a
  _ = refl

  _ : {g₀ : (a : A) → C (inl a)} {g₁ : (b : B) → C (inr b)} {b : B} →
      +-ind C g₀ g₁ (inr b) == g₁ b
  _ = refl

module Exercise6 where
  open HoTT.Base hiding (_×_ ; _,_ ; pr₁ ; pr₂ ; ×-uniq ; ×-ind)
  open import HoTT.Identity.Pi

  _×_ : 𝒰 i → 𝒰 i → 𝒰 i
  _×_ A B = (x : 𝟐) → 𝟐-rec A B x

  _,_ : A → B → A × B
  _,_ a b = 𝟐-ind _ a b

  pr₁ : A × B → A
  pr₁ x = x 0₂

  pr₂ : A × B → B
  pr₂ x = x 1₂

  ×-uniq : (x : A × B) → pr₁ x , pr₂ x == x
  ×-uniq x = funext λ b → 𝟐-ind (λ b → (pr₁ x , pr₂ x) b == x b) refl refl b

  ×-ind : (C : A × B → 𝒰 i) → ((a : A) (b : B) → C (a , b)) → (x : A × B) → C x
  ×-ind C g x = transport C (×-uniq x) (g (pr₁ x) (pr₂ x))

  module _ {C : A × B → 𝒰 i} {g : (a : A) (b : B) → C (a , b)} {a : A} {b : B}
    where
    _ : ×-ind C g (a , b) == g a b
    _ = ap (λ p → transport C p (g a b))
          (ap funext (funext (𝟐-ind _ refl refl)) ∙ =Π-η refl)

  -- Alternative solution from https://pcapriotti.github.io/hott-exercises/chapter1.ex6.html
  {-
  ×-uniq-compute : (x : A × B) → pr₁ x , pr₂ x == x
  ×-uniq-compute x = ×-uniq (pr₁ x , pr₂ x) ⁻¹ ∙ ×-uniq x

  ×-ind' : (C : A × B → 𝒰 i) → ((a : A) (b : B) → C (a , b)) → (x : A × B) → C x
  ×-ind' C g x = transport C (×-uniq-compute x) (g (pr₁ x) (pr₂ x))

  module _ {C : A × B → 𝒰 i} {g : (a : A) (b : B) → C (a , b)} {a : A} {b : B}
    where
    _ : ×-ind' C g (a , b) == g a b
    _ = ap (λ p → transport C p (g a b)) (∙-invₗ (×-uniq (a , b)))
  -}

module Exercise7 where
  open HoTT.Base hiding (=-ind')
  open import HoTT.Identity.Sigma
  open import HoTT.Identity

  -- TODO: Using Lemma 3.11.8 might simplify this.
  =-ind' : (a : A) → (C : (x : A) → a == x → 𝒰 j) →
           C a refl → (x : A) → (p : a == x) → C x p
  =-ind' {A = A} a C c x p = transport (λ{(x , p) → C x p}) q c
    where
    D : (x y : A) → x == y → 𝒰 _
    D x y p = transport (x ==_) p refl == p
    d : (x : A) → D x x refl
    d x = refl

    q : (a , refl) == (x , p)
    q = pair⁼ (p , =-ind D d p)

module Exercise8 where
  open HoTT.Base hiding (_+_) renaming (ℕ-rec to rec ; ℕ-ind to ind)
  open import HoTT.Identity

  _+_ : ℕ → ℕ → ℕ
  n + m = rec m (λ _ → succ) n
  infix 17 _+_

  _*_ : ℕ → ℕ → ℕ
  n * m = rec 0 (λ _ x → m + x) n
  infix 18 _*_

  _^_ : ℕ → ℕ → ℕ
  n ^ m = rec 1 (λ _ x → m * x) n
  infix 19 _^_

  +-assoc : (a b c : ℕ) → (a + b) + c == a + (b + c)
  +-assoc a b c = ind D d₀ dₛ a
    where
    D : ℕ → 𝒰₀
    D a = (a + b) + c == a + (b + c)
    d₀ : D 0
    d₀ = refl
    dₛ : (n : ℕ) → D n → D (succ n)
    dₛ n p = ap succ p

  +-unitₗ : (a : ℕ) → 0 + a == a
  +-unitₗ a = refl

  +-unitᵣ : (a : ℕ) → a + 0 == a
  +-unitᵣ a = ind (λ a → a + 0 == a) refl (λ _ → ap succ) a

  +-commute : (a b : ℕ) → a + b == b + a
  +-commute = ind D d₀ dₛ
    where
    D : ℕ → 𝒰₀
    D a = (b : ℕ) → a + b == b + a
    d₀ : D 0
    d₀ b = +-unitₗ b ∙ +-unitᵣ b ⁻¹
    dₛ : (n : ℕ) → D n → D (succ n)
    dₛ n p b = ap succ (p b) ∙ ind E e₀ eₛ b
      where
      E : ℕ → 𝒰₀
      E b = (succ b) + n == b + (succ n)
      e₀ : E 0
      e₀ = refl
      eₛ : (m : ℕ) → E m → E (succ m)
      eₛ m q = ap succ q

  *-unitₗ : (a : ℕ) → 1 * a == a
  *-unitₗ = +-unitᵣ

  *-unitᵣ : (a : ℕ) → a * 1 == a
  *-unitᵣ = ind (λ a → a * 1 == a) refl (λ _ → ap succ)

  *-distₗ : (a b c : ℕ) → a * (b + c) == a * b + a * c
  *-distₗ a b c = ind D d₀ dₛ a
    where
    D : ℕ → 𝒰₀
    D a = a * (b + c) == a * b + a * c
    d₀ : D 0
    d₀ = refl
    dₛ : (a : ℕ) → D a → D (succ a)
    dₛ a p =
      succ a * (b + c)          =⟨⟩
      (b + c) + a * (b + c)     =⟨ ap ((b + c) +_) p ⟩
      (b + c) + (a * b + a * c) =⟨ +-assoc b c (a * b + a * c) ⟩
      b + (c + (a * b + a * c)) =⟨ ap (b +_) (+-assoc c (a * b) (a * c) ⁻¹) ⟩
      b + ((c + a * b) + a * c) =⟨ ap (λ n → b + (n + a * c)) (+-commute c (a * b)) ⟩
      b + ((a * b + c) + a * c) =⟨ ap (b +_) (+-assoc (a * b) c (a * c)) ⟩
      b + (a * b + (c + a * c)) =⟨ +-assoc b (a * b) (c + a * c) ⁻¹ ⟩
      (b + a * b) + (c + a * c) =⟨⟩
      succ a * b + succ a * c   ∎
      where open =-Reasoning

  *-zeroₗ : (a : ℕ) → 0 * a == 0
  *-zeroₗ _ = refl

  *-zeroᵣ : (a : ℕ) → a * 0 == 0
  *-zeroᵣ a = ind (λ n → n * 0 == 0) refl (λ _ p → p) a

  *-comm : (a b : ℕ) → a * b == b * a
  *-comm a b = ind D d₀ dₛ a
    where
    D : ℕ → 𝒰₀
    D n = n * b == b * n
    d₀ : D 0
    d₀ = *-zeroᵣ b ⁻¹
    dₛ : (n : ℕ) → D n → D (succ n)
    dₛ n p = ap (b +_) p ∙ ap (_+ (b * n)) (*-unitᵣ b ⁻¹) ∙ *-distₗ b 1 n ⁻¹

  *-distᵣ : (a b c : ℕ) → (a + b) * c == (a * c) + (b * c)
  *-distᵣ a b c =
    (a + b) * c   =⟨ *-comm (a + b) c ⟩
    c * (a + b)   =⟨ *-distₗ c a b ⟩
    c * a + c * b =⟨ ap (_+ (c * b)) (*-comm c a) ⟩
    a * c + c * b =⟨ ap ((a * c) +_) (*-comm c b) ⟩
    a * c + b * c ∎
    where open =-Reasoning

  *-assoc : (a b c : ℕ) → (a * b) * c == a * (b * c)
  *-assoc a b c = ind D d₀ dₛ a
    where
    D : ℕ → 𝒰₀
    D n = (n * b) * c == n * (b * c)
    d₀ : D 0
    d₀ = refl
    dₛ : (n : ℕ) → D n → D (succ n)
    dₛ n p = *-distᵣ b (n * b) c ∙ ap ((b * c) +_) p

module Exercise9 where
  open HoTT.Base

  Fin : ℕ → 𝒰₀
  Fin n = ℕ-rec 𝟎 (λ _ A → 𝟏 + A) n

  fmax : (n : ℕ) → Fin (succ n)
  fmax = ℕ-ind (Fin ∘ succ) (inl ★) (λ _ → inr)

module Exercise10 where
  open HoTT.Base

  ack : ℕ → ℕ → ℕ
  ack m n = ℕ-rec succ cₛ m n
    where
    cₛ : ℕ → (ℕ → ℕ) → ℕ → ℕ
    cₛ m c n = c (ℕ-rec 1 (λ _ → c) n)

module Exercise11 where
  open HoTT.Base

  _ : ¬ ¬ ¬ A → ¬ A
  _ = λ f a → f (λ g → g a)

module Exercise12 where
  open HoTT.Base

  _ : A → B → A
  _ = λ a _ → a

  _ : A → ¬ ¬ A
  _ = λ a f → f a

  _ : ¬ A + ¬ B → ¬ (A × B)
  _ = λ x y → +-rec (λ f → 𝟎-rec (f (pr₁ y))) (λ f → 𝟎-rec (f (pr₂ y))) x

module Exercise13 where
  open HoTT.Base

  _ : ¬ ¬ (A + ¬ A)
  _ = λ f → f (inr (f ∘ inl))

module Exercise14 where
  -- For induction, we must have a function C : (s : A) → (t : A) → (q : s == t) → 𝒰.
  -- Since q : s == t, the equality type q == refl {s} does not make sense because
  -- we are trying to equate elements of two different types.

module Exercise15 {C : A → 𝒰 i} where
  open HoTT.Base using (_==_ ; refl ; =-ind ; id)

  _ : {x y : A} → (p : x == y) → C x → C y
  _ = =-ind D d
    where
    D : (x y : A) → x == y → 𝒰 _
    D x y p = C x → C y
    d : (x : A) → D x x refl
    d _ = id

module Exercise16 where
  -- This is just a subset of Exercise8. See +-commute above.

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott


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

module decidable where

open import level using (Level)
open import sets.empty using (⊥; ¬_)
open import sets.unit using (⊤; tt)

-- Decidable relations.

data Dec {i} (P : Set i) : Set i where
  yes : ( p :   P) → Dec P
  no  : (¬p : ¬ P) → Dec P

True : ∀ {i}{P : Set i} → Dec P → Set
True (yes _) = ⊤
True (no _) = ⊥

witness : ∀ {i}{P : Set i}{d : Dec P} → True d → P
witness {d = yes x} _ = x
witness {d = no _} ()

decide : ∀ {i} {P : Set i} {d : Dec P} → P → True d
decide {d = yes p} = λ _ → tt
decide {d = no f} = f

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


text:
{-

This file contains a summary of the proofs that π₄(S³) ≡ ℤ/2ℤ

- The first proof "π₄S³≃ℤ/2ℤ" closely follows Brunerie's thesis.

- The second proof "π₄S³≃ℤ/2ℤ-direct" is much more direct and avoids
  all of the more advanced constructions in chapters 4-6 in Brunerie's
  thesis.

- The third proof "π₄S³≃ℤ/2ℤ-computation" uses ideas from the direct
  proof to define an alternative Brunerie number which computes to -2
  in a few seconds and the main result is hence obtained by computation
  as conjectured on page 85 of Brunerie's thesis.

The --experimental-lossy-unification flag is used to speed up type checking.
The file still type checks without it, but it's a lot slower (about 10 times).

-}
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Homotopy.Group.Pi4S3.Summary where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed

open import Cubical.Data.Nat.Base
open import Cubical.Data.Int.Base
open import Cubical.Data.Sigma.Base

open import Cubical.HITs.Sn
open import Cubical.HITs.SetTruncation

open import Cubical.Homotopy.HopfInvariant.Base
open import Cubical.Homotopy.HopfInvariant.Homomorphism
open import Cubical.Homotopy.HopfInvariant.HopfMap
open import Cubical.Homotopy.HopfInvariant.Brunerie
open import Cubical.Homotopy.Whitehead
open import Cubical.Homotopy.Group.Base hiding (π)
open import Cubical.Homotopy.Group.Pi3S2
open import Cubical.Homotopy.Group.Pi4S3.BrunerieNumber
open import Cubical.Homotopy.Group.Pi4S3.DirectProof as DirectProof

open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Instances.Bool
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.GroupPath
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.Instances.Int
open import Cubical.Algebra.Group.Instances.IntMod
open import Cubical.Algebra.Group.ZAction

-- Homotopy groups (shifted version of π'Gr to get nicer numbering)
π : ℕ → Pointed₀ → Group₀
π n X = π'Gr (predℕ n) X

-- Nicer notation for the spheres (as pointed types)
𝕊² 𝕊³ : Pointed₀
𝕊² = S₊∙ 2
𝕊³ = S₊∙ 3

-- The Brunerie number; defined in Cubical.Homotopy.Group.Pi4S3.BrunerieNumber
-- as "abs (HopfInvariant-π' 0 ([ (∣ idfun∙ _ ∣₂ , ∣ idfun∙ _ ∣₂) ]×))"
β : ℕ
β = Brunerie

-- The connection to π₄(S³) is then also proved in the BrunerieNumber
-- file following Corollary 3.4.5 in Guillaume Brunerie's PhD thesis.
βSpec : GroupEquiv (π 4 𝕊³) (ℤGroup/ β)
βSpec = BrunerieIso

-- Ideally one could prove that β is 2 by normalization, but this does
-- not seem to terminate before we run out of memory. To try normalize
-- this use "C-u C-c C-n β≡2" (which normalizes the term, ignoring
-- abstract's). So instead we prove this by hand as in the second half
-- of Guillaume's thesis.
β≡2 : β ≡ 2
β≡2 = Brunerie≡2

-- This involves a lot of theory, for example that π₃(S²) ≃ ℤGroup where
-- the underlying map is induced by the Hopf invariant (which involves
-- the cup product on cohomology).
_ : GroupEquiv (π 3 𝕊²) ℤGroup
_ = hopfInvariantEquiv

-- Which is a consequence of the fact that π₃(S²) is generated by the
-- Hopf map.
_ : gen₁-by (π 3 𝕊²) ∣ HopfMap ∣₂
_ = π₂S³-gen-by-HopfMap

-- etc. For more details see the proof of "Brunerie≡2".

-- Combining all of this gives us the desired equivalence of groups:
π₄S³≃ℤ/2ℤ : GroupEquiv (π 4 𝕊³) (ℤGroup/ 2)
π₄S³≃ℤ/2ℤ = subst (GroupEquiv (π 4 𝕊³)) (cong ℤGroup/_ β≡2) βSpec

-- By the SIP this induces an equality of groups:
π₄S³≡ℤ/2ℤ : π 4 𝕊³ ≡ ℤGroup/ 2
π₄S³≡ℤ/2ℤ = GroupPath _ _ .fst π₄S³≃ℤ/2ℤ

-- As a sanity check we also establish the equality with Bool:
π₄S³≡Bool : π 4 𝕊³ ≡ BoolGroup
π₄S³≡Bool = π₄S³≡ℤ/2ℤ ∙ GroupPath _ _ .fst (GroupIso→GroupEquiv ℤGroup/2≅Bool)

-- We also have a much more direct proof in Cubical.Homotopy.Group.Pi4S3.DirectProof,
-- not relying on any of the more advanced constructions in chapters
-- 4-6 in Brunerie's thesis (but still using chapters 1-3 for the
-- construction). For details see the header of that file.

π₄S³≃ℤ/2ℤ-direct : GroupEquiv (π 4 𝕊³) (ℤGroup/ 2)
π₄S³≃ℤ/2ℤ-direct = DirectProof.BrunerieGroupEquiv

-- This direct proof allows us to define a much simplified version of
-- the Brunerie number:
β' : ℤ
β' = fst DirectProof.computer η₃'

-- This number computes definitionally to -2 in a few seconds!
β'≡-2 : β' ≡ -2
β'≡-2 = refl

-- As a sanity check we have proved (commented as typechecking is quite slow):
-- β'Spec : GroupEquiv (π 4 𝕊³) (ℤGroup/ abs β')
-- β'Spec = DirectProof.BrunerieGroupEquiv'

-- Combining all of this gives us the desired equivalence of groups by
-- computation as conjectured in Brunerie's thesis:
π₄S³≃ℤ/2ℤ-computation : GroupEquiv (π 4 𝕊³) (ℤGroup/ 2)
π₄S³≃ℤ/2ℤ-computation = DirectProof.BrunerieGroupEquiv''

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- 2010-10-02
-- termination checker now recognizes projections

module Issue334 where

data Functor : Set₁ where
  |Id|  : Functor
  _|x|_ : Functor → Functor → Functor

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

[_] : Functor → Set → Set
[ |Id|    ] X = X
[ F |x| G ] X = [ F ] X × [ G ] X

data µ_ (F : Functor) : Set where
  <_> : [ F ] (µ F) → µ F

mapFold : ∀ {X} F G → ([ G ] X → X) → [ F ] (µ G) → [ F ] X
mapFold |Id|         G  φ < x >   = φ (mapFold G G φ x)
mapFold (F1 |x| F2 ) G  φ (x , y) = mapFold F1 G φ x , mapFold F2 G φ y

-- after record pattern translation, this becomes
-- mapFold (F1 |x| F2) G φ r = mapFold F1 G φ (proj₁ r) , mapFold F2 G φ (proj₂ r)
-- foetus now honors  proj₁ p <= p

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-
  Computer Aided Formal Reasoning (G53CFR, G54CFR)
  Thorsten Altenkirch

  Lecture 2: A first taste of Agda

  In this lecture we start to explore the Agda system, a functional
  programming language based on Type Theory. We start with some
  ordinary examples which we could have developed in Haskell as well.
-}

module l02 where

-- module myNat where

  {- Agda has no automatically loaded prelude. Hence we can start from
     scratch and define the natural numbers. Later we will use the
     standard libray. -}

  data ℕ : Set where -- to type ℕ we type \bn
    zero : ℕ
    suc : (m : ℕ) → ℕ -- \-> or \to

  {- To process an Agda file we use C-c C-c from emacs. Once Agda has
     checked the file the type checker also colours the different
     symbols. -}

  {- We define addition. Note Agda's syntax for mixfix operations. The
     arguments are represented by _s -}

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

  {- Try to evaluate: (suc (suc zero)) + (suc (suc zero))
     by typing in C-c C-n -}

{- Better we import the library definition of ℕ
   This way we can type 2 instead of (suc (suc zero))
-}

-- open import Data.Nat

{- We define Lists :  -}

data List (A : Set) : Set where
  [] : List A
  _∷_ : (a : A) → (as : List A) → List A

{- In future we'll use
     open import Data.List -}

{- declare the fixity of ∷ (type \::) -}

infixr 5 _∷_

{- Two example lists -}

{-
l1 : List ℕ
l1 = 1 ∷ 2 ∷ 3 ∷ []

l2 : List ℕ
l2 = 4 ∷ 5 ∷ []
-}

{- implementing append (++) -}

_++_ : {A : Set} → List A → List A → List A
[] ++ bs = bs
(a ∷ as) ++ bs = a ∷ (as ++ bs)

{- Note that Agda checks wether a function is terminating.
   If we type
   (a ∷ as) ++ bs = (a ∷ as) ++ bs
   in the 2nd line Agda will complain by coloring the offending
   function calls in red.
-}

{- What does the following variant of ++ do ? -}

_++'_ : {A : Set} → List A → List A → List A
as ++' [] = as
as ++' (b ∷ bs) = (b ∷ as) ++' bs

{- Indeed it can be used to define reverse.  This way to implement
   reverse is often called fast reverse because it is "tail recursive"
   which leads to a more efficient execution than the naive
   implementation. -}

rev : {A : Set} → List A → List A
rev as = [] ++' as

{- We tried to define a function which accesses the nth element of a list:

_!!_ : {A : Set} → List A → ℕ → A
[] !! n = {!!}
(a ∷ as) !! zero = a
(a ∷ as) !! suc n = as !! n

  but there is no way to complete the first line (consider what happens
  if A is the empty type!
-}

{- To fix this we handle errors explicitely, using Maybe -}

-- open import Data.Maybe

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

{- This version of the function can either return an element of the list
    (just a) or an error (nothing).
-}
_!!_ : {A : Set} → List A → ℕ → Maybe A
[] !! n = nothing
(a ∷ as) !! zero = just a
(a ∷ as) !! suc n = as !! n

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


text:
------------------------------------------------------------------------
-- The syntax of a toy programming language that only supports
-- allocation and deallocation of memory
------------------------------------------------------------------------

module Only-allocation where

open import Equality.Propositional
open import Prelude
open import Prelude.Size

open import Colist equality-with-J

------------------------------------------------------------------------
-- Programs

-- Statements.

data Stmt : Type where
  alloc dealloc : Stmt

-- Programs are potentially infinite sequences of statements.

Program : Size → Type
Program i = Colist Stmt i

------------------------------------------------------------------------
-- Some examples

-- A program that runs in bounded space.

bounded : ∀ {i} → Program i
bounded = alloc ∷′ dealloc ∷ λ { .force → bounded }

-- Another program that runs in bounded space.

bounded₂ : ∀ {i} → Program i
bounded₂ =
  alloc   ∷′ alloc   ∷′
  dealloc ∷′ dealloc ∷ λ { .force → bounded₂ }

-- A program that does not run in bounded space.

unbounded : ∀ {i} → Program i
unbounded = alloc ∷ λ { .force → unbounded }

max_stars_repo_name: nad/definitional-interpreters

max_issues_repo_name: nad/definitional-interpreters

max_forks_repo_name: nad/definitional-interpreters


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

module Categories.Adjoint.Instance.PosetCore where

-- The adjunction between the "forgetful" functor from Posets to
-- Setoids and the core functor for posets.

open import Level using (_⊔_)
import Function
open import Function.Equality using (Π; _⟶_)
open import Relation.Binary using (Setoid; Poset)
open import Relation.Binary.OrderMorphism using (_⇒-Poset_) renaming (_∘_ to _∙_)

open import Categories.Adjoint using (_⊣_)
import Categories.Adjoint.Instance.0-Truncation as Setd
import Categories.Adjoint.Instance.01-Truncation as Pos
open import Categories.Category using (Category)
open import Categories.Category.Construction.Thin
open import Categories.Category.Instance.Posets using (fun-resp-≈; Posets)
open import Categories.Category.Instance.Setoids using (Setoids)
open import Categories.Functor.Instance.Core using () renaming (Core to CatCore)
import Categories.Functor.Instance.Core as Cat
open import Categories.Functor using (Functor; _∘F_; id)
import Categories.Morphism as Morphism
open import Categories.Morphism.IsoEquiv using (⌞_⌟)
open import Categories.NaturalTransformation using (ntHelper)
open import Categories.NaturalTransformation.NaturalIsomorphism
  using (_≃_; niHelper)

open Π
open _⇒-Poset_

-- The "forgetful" functor from Setoids to Posets (forgetting symmetry).

Forgetful : ∀ {c ℓ} → Functor (Setoids c ℓ) (Posets c ℓ ℓ)
Forgetful = record
  { F₀           = Forgetful₀
  ; F₁           = λ f → record { fun = _⟨$⟩_ f ; monotone = cong f }
  ; identity     = λ {S}       → refl S
  ; homomorphism = λ {_ _ S}   → refl S
  ; F-resp-≈     = λ {S _} f≗g → f≗g (refl S)
  }
  where
    Forgetful₀ : ∀ {c ℓ} → Setoid c ℓ → Poset c ℓ ℓ
    Forgetful₀ S = record
      { _≈_               = _≈_
      ; _≤_               = _≈_
      ; isPartialOrder    = record
        { isPreorder      = record
          { isEquivalence = isEquivalence
          ; reflexive     = Function.id
          ; trans         = trans
          }
        ; antisym         = Function.const
        }
      }
      where open Setoid S

    open Setoid

-- The "core" functor from Posets to Setoids.
--
-- This functor simply forgets the _≤_ relation, mapping a Poset to
-- the Setoid over which it is defined.  This Setoid is the "core" of
-- the Poset in the sense that the "equality" _≈_ associated with the
-- Poset is really an equivalence, and antisymmetry ensures that this
-- equivalence is equivalent to the symmetric core of _≤_.

Core : ∀ {c ℓ₁ ℓ₂} → Functor (Posets c ℓ₁ ℓ₂) (Setoids c ℓ₁)
Core = record
  { F₀           = λ A → record { isEquivalence = isEquivalence A }
  ; F₁           = λ f → record { _⟨$⟩_ = fun f ; cong = fun-resp-≈ f }
  ; identity     = Function.id
  ; homomorphism = λ {_ _ _ f g} → fun-resp-≈ (g ∙ f)
  ; F-resp-≈     = λ {_ B} {f _} f≗g x≈y → Eq.trans B (fun-resp-≈ f x≈y) f≗g
  }
  where open Poset

-- Core is right-adjoint to the forgetful functor

CoreAdj : ∀ {o ℓ} → Forgetful ⊣ Core {o} {ℓ} {ℓ}
CoreAdj = record
  { unit   = ntHelper record { η = unit   ; commute = cong                  }
  ; counit = ntHelper record { η = counit ; commute = λ {_ B} _ → Eq.refl B }
  ; zig    = λ {S} → Setoid.refl S
  ; zag    = Function.id
  }
  where
    open Poset
    open Functor Core      using () renaming (F₀ to Core₀; F₁ to Core₁)
    open Functor Forgetful using () renaming (F₀ to U₀   ; F₁ to U₁)

    unit : ∀ S → S ⟶ Core₀ (U₀ S)
    unit S = record { _⟨$⟩_ = Function.id ; cong = Function.id }

    counit : ∀ A → U₀ (Core₀ A) ⇒-Poset A
    counit C = record { fun = Function.id ; monotone = reflexive C }

-- The core functor commutes with inclusion, i.e. the core of a thin
-- category is the 0-Groupoid generated by the associated equivalence.
--
-- Note that the core functor does not commute with truncation,
-- because the latter forgets too much (there are many more isos in
-- the (0,1)-truncated category).

Core-commutes : ∀ {c ℓ} e → Setd.Inclusion e ∘F Core ≃
                Cat.Core ∘F Pos.Inclusion {c} {ℓ ⊔ e} {ℓ} e
Core-commutes e = niHelper record
  { η   = λ A → record { F₀ = Function.id ; F₁ = EqIsIso.≈⇒≅ e A }
  ; η⁻¹ = λ A → record { F₀ = Function.id ; F₁ = EqIsIso.≅⇒≈ e A }
  ; commute = λ {A B} f →
    let open Morphism (Thin e B)
    in niHelper record { η   = λ _ → ≅.refl ; η⁻¹ = λ _ → ≅.refl }
  ; iso = λ A →
    let open Poset A
        open Morphism (Thin e A)
    in record
    { isoˡ = niHelper record { η = λ _ → Eq.refl ; η⁻¹ = λ _ → Eq.refl }
    ; isoʳ = niHelper record { η = λ _ → ≅.refl  ; η⁻¹ = λ _ → ≅.refl  }
    }
  }

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
--#include "prelude.agda"
--#include "PropPrelude.agda"

proof_reverse_nil :: PropPrelude.prop_reverse_nil
  = ref@_ (reverse Unit Nil@_)

proof_append_nil_1 :: PropPrelude.prop_append_nil_1
  = ?

proof_append_nil_2 :: PropPrelude.prop_append_nil_2
  = \ (xs::List Unit) -> ref@_ (append Unit Nil@_ xs)

max_issues_repo_name: siddharthist/CoverTranslator


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Adjunction.CompositionLaws where

open import Level

open import Relation.Binary using (Rel; IsEquivalence)
open import Data.Sum
open import Data.Product
open import Function using (flip)

open import Categories.Category
open import Categories.Functor hiding (equiv; assoc; identityˡ; identityʳ; ∘-resp-≡) renaming (id to idF; _≡_ to _≡F_; _∘_ to _∘F_)
open import Categories.NaturalTransformation hiding (equiv; setoid) renaming (id to idT; _≡_ to _≡T_)
open import Categories.Monad
open import Categories.Support.Equivalence

open import Categories.Adjunction
open import Categories.Adjunction.Composition

.assoc : ∀ {o₀ ℓ₀ e₀ o₁ ℓ₁ e₁ o₂ ℓ₂ e₂ o₃ ℓ₃ e₃}
           {C₀ : Category o₀ ℓ₀ e₀} {C₁ : Category o₁ ℓ₁ e₁} {C₂ : Category o₂ ℓ₂ e₂} {C₃ : Category o₃ ℓ₃ e₃}
           {F : Functor C₀ C₁} {G : Functor C₁ C₂} {H : Functor C₂ C₃}
           {F′ : Functor C₁ C₀} {G′ : Functor C₂ C₁} {H′ : Functor C₃ C₂}
           {T : F ⊣ F′} {U : G ⊣ G′} {V : H ⊣ H′}
       → (V ∘ U) ∘ T ≡ V ∘ (U ∘ T)
assoc {C₀ = C₀} {C₁} {C₂} {C₃} {F} {G} {H} {F′} {G′} {H′} {T} {U} {V} = (λ {x} → pf₀ {x}) , λ {x} → pf₁ {x}
  where
    module C₀ = Category C₀
    module C₁ = Category C₁
    module C₂ = Category C₂
    module C₃ = Category C₃
    module F = Functor F
    module G = Functor G renaming (F₀ to G₀; F₁ to G₁; F-resp-≡ to G-resp-≡)
    module H = Functor H renaming (F₀ to H₀; F₁ to H₁; F-resp-≡ to H-resp-≡)
    module F′ = Functor F′ renaming (F₀ to F′₀; F₁ to F′₁; F-resp-≡ to F′-resp-≡)
    module G′ = Functor G′ renaming (F₀ to G′₀; F₁ to G′₁; F-resp-≡ to G′-resp-≡)
    module H′ = Functor H′ renaming (F₀ to H′₀; F₁ to H′₁; F-resp-≡ to H′-resp-≡)
    module T = Adjunction T renaming (unit to Tη′; counit to Tε′)
    module U = Adjunction U renaming (unit to Uη′; counit to Uε′)
    module V = Adjunction V renaming (unit to Vη′; counit to Vε′)
    module Tη = NaturalTransformation (Adjunction.unit T)
    module Tε = NaturalTransformation (Adjunction.counit T)
    module Uη = NaturalTransformation (Adjunction.unit U)
    module Uε = NaturalTransformation (Adjunction.counit U)
    module Vη = NaturalTransformation (Adjunction.unit V)
    module Vε = NaturalTransformation (Adjunction.counit V)

    pf₀ : {x : C₀.Obj} → F′.F′₁ (G′.G′₁ (Vη.η (G.G₀ (F.F₀ x))) C₁.∘ Uη.η (F.F₀ x)) C₀.∘
                           Tη.η x
                           C₀.≡
                           F′.F′₁ (G′.G′₁ (Vη.η (G.G₀ (F.F₀ x)))) C₀.∘
                           F′.F′₁ (Uη.η (F.F₀ x)) C₀.∘ Tη.η x
    pf₀ {x} = begin
               F′.F′₁ (G′.G′₁ (Vη.η (G.G₀ (F.F₀ x))) C₁.∘ Uη.η (F.F₀ x)) C₀.∘
                 Tη.η x
             ↓⟨ C₀.∘-resp-≡ˡ F′.homomorphism ⟩
               C₀ [ F′.F′₁ (G′.G′₁ (Vη.η (G.G₀ (F.F₀ x)))) ∘
                 F′.F′₁ (Uη.η (F.F₀ x)) ]
                 C₀.∘ Tη.η x
             ↓⟨ C₀.assoc ⟩
               F′.F′₁ (G′.G′₁ (Vη.η (G.G₀ (F.F₀ x)))) C₀.∘
                 F′.F′₁ (Uη.η (F.F₀ x)) C₀.∘ Tη.η x
             ∎
        where open C₀.HomReasoning

    pf₁ : {x : C₃.Obj} → (Vε.η x C₃.∘ H.H₁ (Uε.η (H′.H′₀ x))) C₃.∘
                               H.H₁ (G.G₁ (Tε.η (G′.G′₀ (H′.H′₀ x))))
                         C₃.≡
                         Vε.η x C₃.∘
                           H.H₁ (Uε.η (H′.H′₀ x) C₂.∘ G.G₁ (Tε.η (G′.G′₀ (H′.H′₀ x))))
    pf₁ {x} = begin
               (Vε.η x C₃.∘ H.H₁ (Uε.η (H′.H′₀ x))) C₃.∘
                 H.H₁ (G.G₁ (Tε.η (G′.G′₀ (H′.H′₀ x))))
             ↓⟨ C₃.assoc ⟩
               Vε.η x C₃.∘
                 H.H₁ (Uε.η (H′.H′₀ x)) C₃.∘ H.H₁ (G.G₁ (Tε.η (G′.G′₀ (H′.H′₀ x))))
             ↑⟨ C₃.∘-resp-≡ʳ H.homomorphism ⟩
               Vε.η x C₃.∘
                 H.H₁ (C₂ [ Uε.η (H′.H′₀ x) ∘ G.G₁ (Tε.η (G′.G′₀ (H′.H′₀ x))) ])
             ∎
      where open C₃.HomReasoning

.identityˡ : ∀ {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {F : Functor C D} {G : Functor D C} {T : F ⊣ G}
             → id ∘ T ≡ T
identityˡ {C = C} {D} {F} {G} {T} = ( (λ {x} → pf₀ {x}) , D.identityˡ )
  where
    module C = Category C
    module D = Category D
    module F = Functor F
    module G = Functor G
    module T = Adjunction T renaming (unit to Tη′; counit to Tε′)
    module Tη = NaturalTransformation T.Tη′
    module Tε = NaturalTransformation T.Tε′

    pf₀ : {x : C.Obj} → G.F₁ D.id C.∘ NaturalTransformation.η Tη.op x C.≡
                             NaturalTransformation.η Tη.op x
    pf₀ {x} = begin
               G.F₁ D.id C.∘ NaturalTransformation.η Tη.op x
             ↓⟨ C.∘-resp-≡ˡ G.identity ⟩
               C.id C.∘ NaturalTransformation.η Tη.op x
             ↓⟨ C.identityˡ ⟩
               NaturalTransformation.η Tη.op x
             ∎
      where open C.HomReasoning

.identityʳ : ∀ {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {F : Functor C D} {G : Functor D C} {T : F ⊣ G}
             → T ∘ id ≡ T
identityʳ {C = C} {D} {F} {G} {T} = (λ {x} → C.identityʳ) , (λ {x} → pf₀ {x})
  where
    module C = Category C
    module D = Category D
    module F = Functor F
    module G = Functor G
    module T = Adjunction T renaming (unit to Tη′; counit to Tε′)
    module Tη = NaturalTransformation T.Tη′
    module Tε = NaturalTransformation T.Tε′

    pf₀ : {x : D.Obj} → NaturalTransformation.η Tε.op x D.∘ F.F₁ C.id D.≡
                        NaturalTransformation.η Tε.op x
    pf₀ {x} = begin
               NaturalTransformation.η Tε.op x D.∘ F.F₁ C.id
             ↓⟨ D.∘-resp-≡ʳ F.identity ⟩
               NaturalTransformation.η Tε.op x D.∘ D.id
             ↓⟨ D.identityʳ ⟩
               NaturalTransformation.η Tε.op x
             ∎
      where open D.HomReasoning

.∘-resp-≡  : ∀ {o₀ ℓ₀ e₀ o₁ ℓ₁ e₁ o₂ ℓ₂ e₂}
               {A : Category o₀ ℓ₀ e₀} {B : Category o₁ ℓ₁ e₁} {C : Category o₂ ℓ₂ e₂}
               {F : Functor B C} {G : Functor A B} {F′ : Functor C B} {G′ : Functor B A}
               {T T′ : G ⊣ G′} {U U′ : F ⊣ F′}
           → T ≡ T′ → U ≡ U′ → U ∘ T ≡ U′ ∘ T′
∘-resp-≡ {A = A} {B} {C} {F} {G} {F′} {G′} {T} {T′} {U} {U′} (Tη≡T′η , Tε≡T′ε) (Uη≡U′η , Uε≡U′ε) =
         (λ {x} → A.∘-resp-≡ (G′.F-resp-≡ Uη≡U′η) Tη≡T′η)
         ,
         (λ {x} → C.∘-resp-≡ Uε≡U′ε (F.F-resp-≡ Tε≡T′ε))
  where
    module A = Category A
    module B = Category B
    module C = Category C
    module F = Functor F
    module G = Functor G
    module F′ = Functor F′
    module G′ = Functor G′
    module T = Adjunction T renaming (unit to Tη′; counit to Tε′)
    module U = Adjunction U renaming (unit to Uη′; counit to Uε′)
    module T′ = Adjunction T′ renaming (unit to T′η′; counit to T′ε′)
    module U′ = Adjunction U′ renaming (unit to U′η′; counit to U′ε′)
    module Tη = NaturalTransformation (Adjunction.unit T)
    module Tε = NaturalTransformation (Adjunction.counit T)
    module Uη = NaturalTransformation (Adjunction.unit U)
    module Uε = NaturalTransformation (Adjunction.counit U)
    module T′η = NaturalTransformation (Adjunction.unit T′)
    module T′ε = NaturalTransformation (Adjunction.counit T′)
    module U′η = NaturalTransformation (Adjunction.unit U′)
    module U′ε = NaturalTransformation (Adjunction.counit U′)

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


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

-- Some basic theorms about natural numbers.
module hott.types.nat.theorems where

open import hott.core
open import hott.functions
open import hott.types.nat

-- 0 is the right identity of addition.
x+0≡x : ∀(x : ℕ) → x + 0 ≡ x
x+0≡x  0                = begin 0 + 0 ≡ 0 by definition ∎
x+0≡x (succ n)
  = begin succ n + 0 ≡ succ (n + 0) by definition
                     ≡ succ n       by ap succ (x+0≡x (n))
  ∎

-- Alternate from of 0 being right identity.
x≡x+0 : ∀(x : ℕ) → x ≡ x + 0
x≡x+0 n = x+0≡x n ⁻¹

-- This is really refl but it is better to use these when proving
-- properties about ℕ. One does not have to remember which is
-- definitional equality and which is not.
0+x≡x : ∀ (x : ℕ) → 0 + x ≡ x
0+x≡x n = begin 0 + n ≡ n by definition ∎

-- This is really refl but it is better to use these when proving
-- properties about ℕ. One does not have to remember which is
-- definitional equality and which is not.
x≡0+x : ∀ (x : ℕ) → x ≡ 0 + x
x≡0+x n = begin n ≡ 0 + n by definition ∎

-- Commutativity of addition.
x+y≡y+x : ∀ (x y : ℕ) → x + y ≡ y + x
x+y≡y+x 0 n
        = begin 0 + n ≡ n     by  definition
                      ≡ n + 0 by  x≡x+0 (n)
          ∎
x+y≡y+x n 0
        = begin n + 0 ≡ n      by x+0≡x (n)
                      ≡ 0 + n  by definition
          ∎
x+y≡y+x (succ m) (succ n)
  = begin succ m + succ n
          ≡ succ (m + succ n)   by definition
          ≡ succ (succ n + m)   by applying succ on x+y≡y+x m (succ n)
          ≡ succ (succ (n + m)) by definition
          ≡ succ (succ (m + n)) by applying succ ∘ succ on (x+y≡y+x n m)
          ≡ succ (succ m + n)   by applying succ on definition
          ≡ succ (n + succ m)   by applying succ on x+y≡y+x (succ m) n
          ≡ succ n + succ m     by definition
  ∎
-- Associativity of +
x+[y+z]≡[x+y]+z : ∀ (x y z : ℕ) → x + (y + z) ≡ (x + y) + z
x+[y+z]≡[x+y]+z zero      y z
                = begin 0 + (y + z)
                        ≡ y + z        by definition
                        ≡ (0 + y) + z  by definition
                ∎
x+[y+z]≡[x+y]+z (succ x)  y z
  = begin succ x + (y + z)
          ≡ succ (x + (y  + z)) by definition
          ≡ succ ((x + y) + z) by applying succ on x+[y+z]≡[x+y]+z x y z
          ≡ succ (x + y)  + z  by definition
          ≡ (succ x + y)  + z  by definition
  ∎

max_stars_repo_name: piyush-kurur/hott

max_issues_repo_name: piyush-kurur/hott

max_forks_repo_name: piyush-kurur/hott


text:
{-# OPTIONS --cubical #-}

module Type.Cubical.InductivePath where

open import Functional
import      Lvl
open import Type
import      Type.Cubical as Cubical
open import Type.Cubical.InductiveInterval

private variable ℓ : Lvl.Level
private variable A B P : Type{ℓ}
private variable x y z : A

data Path {P : Type{ℓ}} : P → P → Type{ℓ} where
  intro : (p : Interval → P) → Path(p(𝟎)) (p(𝟏))

point : (x : P) → Path x x
point x = intro(const x)

pointOn : ∀{x y : A} → Path x y → (Interval → A)
pointOn (intro p) = p

reverse : Path x y → Path y x
reverse(intro f) = intro(f ∘ flip)

spaceMap : Path A B → (A → B)
spaceMap (intro p) = transp p

{-
concat : Path x y → Path y z → Path x z
concat xy yz = {!xy yz!}
-}

module _ where
  private variable X : Type{ℓ}
  private variable Y : X → Type{ℓ}

  {- TODO: Define an eliminator for Path and use it to prove this?
  mapping : ∀{f g : (x : X) → Y(x)} → (∀{x} → Path(f(x)) (g(x))) → Path f g
  mapping {X = X}{Y = Y}{f = f}{g = g} ppt = intro(i ↦ x ↦ {!pointOn(ppt{x}) i!}) where
    p : (∀{x} → Path(f(x)) (g(x))) → Interval → (x : X) → Y(x)
    p ppt i x with ppt{x}
    ... | q = {!q!}
  -}

  mappingPoint : ∀{f g : (x : X) → Y(x)} → Path f g → (∀{x} → Path(f(x)) (g(x)))
  mappingPoint (intro pfg) {x} = intro (i ↦ pfg i x)

module _ where
  private variable X X₁ X₂ Y Y₁ Y₂ : Type{ℓ}

  map : (f : X → Y) → ∀{a b} → Path a b → Path (f(a)) (f(b))
  map f (intro ab) = intro(f ∘ ab)

  liftedSpaceMap : (S : X → Type{ℓ}) → ∀{a b} → Path a b → S(a) → S(b)
  liftedSpaceMap S p = spaceMap(map S p)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
------------------------------------------------------------------------
-- Some results related to strong bisimilarity for the delay monad
------------------------------------------------------------------------

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

open import Prelude

module Bisimilarity.Delay-monad {a} {A : Type a} where

open import Delay-monad
open import Delay-monad.Bisimilarity as D using (force)
open import Equality.Propositional
open import Logical-equivalence using (_⇔_)

open import Function-universe equality-with-J hiding (id; _∘_)

open import Labelled-transition-system
open import Labelled-transition-system.Delay-monad A

open import Bisimilarity delay-monad
import Bisimilarity.Equational-reasoning-instances
open import Equational-reasoning

------------------------------------------------------------------------
-- The direct and the indirect definitions of strong bisimilarity are
-- pointwise logically equivalent

-- An emulation of the constructor D.later.

later-cong : ∀ {i x y} →
             [ i ] force x ∼′ force y → [ i ] later x ∼ later y
later-cong x∼′y =
  ⟨ (λ { later → _ , later , x∼′y })
  , (λ { later → _ , later , x∼′y })
  ⟩

-- The direct definition of strong bisimilarity is contained in the
-- one obtained from the transition relation.

direct→indirect : ∀ {i x y} →
                  D.[ i ] x ∼ y → [ i ] x ∼ y
direct→indirect D.now       = reflexive
direct→indirect (D.later p) = later-cong λ { .force →
                                direct→indirect (force p) }

-- The definition of strong bisimilarity obtained from the transition
-- relation is contained in the direct one.

indirect→direct : ∀ {i} x y → [ i ] x ∼ y → D.[ i ] x ∼ y
indirect→direct (now x) (now y) nx∼ny
  with left-to-right nx∼ny now
... | _ , now , _ = D.now

indirect→direct (later x) (later y) lx∼ly
  with left-to-right lx∼ly later
... | _ , later , x∼′y  = D.later λ { .force →
                            indirect→direct _ _ (force x∼′y) }

indirect→direct (now x) (later y) nx∼ly
  with left-to-right nx∼ly now
... | _ , () , _

indirect→direct (later x) (now y) lx∼ny
  with left-to-right lx∼ny later
... | _ , () , _

-- The direct definition of strong bisimilarity is pointwise logically
-- equivalent to the one obtained from the transition relation.
--
-- TODO: Are the two definitions isomorphic?

direct⇔indirect : ∀ {i x y} → D.[ i ] x ∼ y ⇔ [ i ] x ∼ y
direct⇔indirect = record
  { to   = direct→indirect
  ; from = indirect→direct _ _
  }

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
-- Andreas, 2018-04-16, inspired by issue #3032 reported by sattlerc

-- A termination issue without visible recursion.

postulate
  A : Set
  B : Set
  t : B

mutual

  data C : (b : B) → Set where
    c : (x : C t) → C (foo t bar)

  postulate
    bar : C t

  foo : (b : B) → C b → B
  foo y (c x) = y

-- Should not termination check.
-- y is actually "foo t bar" here, a potentially non-terminating recursive call.


text:
------------------------------------------------------------------------------
-- Testing Agda internal term: @Def@
------------------------------------------------------------------------------

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

module Agda.InternalTerms.DefTerm1 where

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

postulate
  D   : Set
  _≡_ : D → D → Set
  P   : D → Set
  a   : D

-- A definition with one argument.
postulate foo : P a
{-# ATP axiom foo #-}

-- We need to have at least one conjecture to generate a TPTP file.
postulate bar : ∀ d → d ≡ d
{-# ATP prove bar #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
{-# OPTIONS --safe #-}
module Cubical.HITs.Wedge where

open import Cubical.HITs.Wedge.Base public

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical