text:
------------------------------------------------------------------------
-- Coinductive higher lenses
------------------------------------------------------------------------

-- Paolo Capriotti came up with these lenses, and provided an informal
-- proof showing that this lens type is pointwise equivalent to his
-- higher lenses. I turned this proof into the proof presented below,
-- with help from Andrea Vezzosi (see
-- Lens.Non-dependent.Higher.Coherently.Coinductive).

{-# OPTIONS --cubical --guardedness #-}

import Equality.Path as P

module Lens.Non-dependent.Higher.Coinductive
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq

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

open import Bijection equality-with-J using (_↔_)
import Coherently-constant eq as CC
open import Colimit.Sequential eq as C using (∣_∣)
open import Equality.Decidable-UIP equality-with-J using (Constant)
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq using (_≃_)
import Equivalence.Half-adjoint equality-with-J as HA
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional eq as T using (∥_∥; ∣_∣)
import H-level.Truncation.Propositional.Non-recursive eq as N
open import H-level.Truncation.Propositional.One-step eq as O
  using (∥_∥¹; ∥_∥¹-out-^; ∥_∥¹-in-^; ∣_∣; ∣_,_∣-in-^)
open import Preimage equality-with-J using (_⁻¹_)
open import Univalence-axiom equality-with-J

open import Lens.Non-dependent eq
import Lens.Non-dependent.Higher eq as H
import Lens.Non-dependent.Higher.Capriotti eq as Higher
open import Lens.Non-dependent.Higher.Coherently.Coinductive eq

private
  variable
    a b p : Level
    A B   : Type a
    P     : A → Type p
    f     : (x : A) → P x

------------------------------------------------------------------------
-- Weakly constant functions

-- A variant of Constant.

Constant′ :
  {A : Type a} {B : Type b} →
  (A → B) → Type (a ⊔ b)
Constant′ {A = A} {B = B} f =
  ∃ λ (g : ∥ A ∥¹ → B) → ∀ x → g ∣ x ∣ ≡ f x

-- Constant and Constant′ are pointwise equivalent.

Constant≃Constant′ : (f : A → B) → Constant f ≃ Constant′ f
Constant≃Constant′ f = Eq.↔→≃
  (λ c → O.rec′ f c
       , λ x → O.rec′ f c ∣ x ∣  ≡⟨⟩
               f x               ∎)
  (λ (g , h) x y →
     f x      ≡⟨ sym (h x) ⟩
     g ∣ x ∣  ≡⟨ cong g (O.∣∣-constant x y) ⟩
     g ∣ y ∣  ≡⟨ h y ⟩∎
     f y      ∎)
  (λ (g , h) →
     let lem = O.elim λ where
           .O.Elim.∣∣ʳ x →
             f x      ≡⟨ sym (h x) ⟩∎
             g ∣ x ∣  ∎
           .O.Elim.∣∣-constantʳ x y →
             let g′ = O.rec′ f λ x y →
                        trans (sym (h x))
                          (trans (cong g (O.∣∣-constant x y))
                             (h y))
             in
             subst (λ z → g′ z ≡ g z) (O.∣∣-constant x y) (sym (h x))  ≡⟨ subst-in-terms-of-trans-and-cong ⟩

             trans (sym (cong g′ (O.∣∣-constant x y)))
               (trans (sym (h x)) (cong g (O.∣∣-constant x y)))        ≡⟨ cong (flip trans _) $ cong sym
                                                                          O.rec-∣∣-constant ⟩
             trans (sym (trans (sym (h x))
                           (trans (cong g (O.∣∣-constant x y))
                              (h y))))
               (trans (sym (h x)) (cong g (O.∣∣-constant x y)))        ≡⟨ trans (cong (flip trans _) $
                                                                                trans (cong sym $ sym $ trans-assoc _ _ _) $
                                                                                sym-trans _ _) $
                                                                          trans-[trans-sym]- _ _ ⟩∎
             sym (h y)                                                 ∎
     in
     Σ-≡,≡→≡
       (⟨ext⟩ lem)
       (⟨ext⟩ λ x →

        subst (λ g → ∀ x → g ∣ x ∣ ≡ f x)
          (⟨ext⟩ lem) (λ x → refl (f x)) x                         ≡⟨ sym $ push-subst-application _ _ ⟩

        subst (λ g → g ∣ x ∣ ≡ f x) (⟨ext⟩ lem) (refl (f x))       ≡⟨ subst-∘ _ _ _ ⟩

        subst (_≡ f x) (cong (_$ ∣ x ∣) (⟨ext⟩ lem)) (refl (f x))  ≡⟨ subst-trans-sym ⟩

        trans (sym (cong (_$ ∣ x ∣) (⟨ext⟩ lem))) (refl (f x))     ≡⟨ trans-reflʳ _ ⟩

        sym (cong (_$ ∣ x ∣) (⟨ext⟩ lem))                          ≡⟨ cong sym $ cong-ext _ ⟩

        sym (lem ∣ x ∣)                                            ≡⟨⟩

        sym (sym (h x))                                            ≡⟨ sym-sym _ ⟩∎

        h x                                                        ∎))
  (λ c → ⟨ext⟩ λ x → ⟨ext⟩ λ y →
     trans (sym (refl _))
       (trans (cong (O.rec′ f c) (O.∣∣-constant x y)) (refl _))  ≡⟨ trans (cong₂ trans sym-refl (trans-reflʳ _)) $
                                                                    trans-reflˡ _ ⟩

     cong (O.rec′ f c) (O.∣∣-constant x y)                       ≡⟨ O.rec-∣∣-constant ⟩∎

     c x y                                                       ∎)

------------------------------------------------------------------------
-- Coherently constant functions

-- Coherently constant functions.

Coherently-constant :
  {A : Type a} {B : Type b} (f : A → B) → Type (a ⊔ b)
Coherently-constant = Coherently Constant O.rec′

-- Coherently constant functions are weakly constant.

constant : Coherently-constant f → Constant f
constant c = c .property

-- An alternative to Coherently-constant.

Coherently-constant′ :
  {A : Type a} {B : Type b} (f : A → B) → Type (a ⊔ b)
Coherently-constant′ = Coherently Constant′ (λ _ → proj₁)

-- Coherently-constant and Coherently-constant′ are pointwise
-- equivalent (assuming univalence).

Coherently-constant≃Coherently-constant′ :
  Block "Coherently-constant≃Coherently-constant′" →
  {A : Type a} {B : Type b} {f : A → B} →
  Univalence (a ⊔ b) →
  Coherently-constant f ≃ Coherently-constant′ f
Coherently-constant≃Coherently-constant′ ⊠ univ =
  Coherently-cong univ
    Constant≃Constant′
    (λ f c →
       O.rec′ f (_≃_.from (Constant≃Constant′ f) c)   ≡⟨⟩

       proj₁ (_≃_.to (Constant≃Constant′ f)
                (_≃_.from (Constant≃Constant′ f) c))  ≡⟨ cong proj₁ $
                                                         _≃_.right-inverse-of (Constant≃Constant′ f) _ ⟩∎
       proj₁ c                                        ∎)

private

  -- Some definitions used in the implementation of
  -- ∃Coherently-constant′≃.

  module ∃Coherently-constant′≃ where

    to₁ :
      (f : A → B) → Coherently-constant′ f →
      ∀ n → ∥ A ∥¹-in-^ n → B
    to₁ f c zero    = f
    to₁ f c (suc n) = to₁ (proj₁ (c .property)) (c .coherent) n

    to₂ :
      ∀ (f : A → B) (c : Coherently-constant′ f) n x →
      to₁ f c (suc n) ∣ n , x ∣-in-^ ≡ to₁ f c n x
    to₂ f c zero    = proj₂ (c .property)
    to₂ f c (suc n) = to₂ (proj₁ (c .property)) (c .coherent) n

    from :
      (f : ∀ n → ∥ A ∥¹-in-^ n → B) →
      (∀ n x → f (suc n) ∣ n , x ∣-in-^ ≡ f n x) →
      Coherently-constant′ (f 0)
    from f c .property = f 1 , c 0
    from f c .coherent = from (f ∘ suc) (c ∘ suc)

    from-to :
      (f : A → B) (c : Coherently-constant′ f) →
      from (to₁ f c) (to₂ f c) P.≡ c
    from-to f c i .property = (c .property  P.∎) i
    from-to f c i .coherent =
      from-to (proj₁ (c .property)) (c .coherent) i

    to₁-from :
      (f : ∀ n → ∥ A ∥¹-in-^ n → B)
      (c : ∀ n x → f (suc n) ∣ n , x ∣-in-^ ≡ f n x) →
      ∀ n x → to₁ (f 0) (from f c) n x ≡ f n x
    to₁-from f c zero    = refl ∘ f 0
    to₁-from f c (suc n) = to₁-from (f ∘ suc) (c ∘ suc) n

    to₂-from :
      (f : ∀ n → ∥ A ∥¹-in-^ n → B)
      (c : ∀ n x → f (suc n) ∣ n , x ∣-in-^ ≡ f n x) →
      ∀ n x →
      trans (sym (to₁-from f c (suc n) ∣ n , x ∣-in-^))
        (trans (to₂ (f 0) (from f c) n x)
           (to₁-from f c n x)) ≡
      c n x
    to₂-from f c (suc n) = to₂-from (f ∘ suc) (c ∘ suc) n
    to₂-from f c zero    = λ x →
      trans (sym (refl _)) (trans (c 0 x) (refl _))  ≡⟨ trans (cong (flip trans _) sym-refl) $
                                                        trans-reflˡ _ ⟩
      trans (c 0 x) (refl _)                         ≡⟨ trans-reflʳ _ ⟩∎
      c 0 x                                          ∎

-- "Functions from A to B that are coherently constant" can be
-- expressed in a different way.

∃Coherently-constant′≃ :
  (∃ λ (f : A → B) → Coherently-constant′ f)
    ≃
  (∃ λ (f : ∀ n → ∥ A ∥¹-in-^ n → B) →
     ∀ n x → f (suc n) ∣ n , x ∣-in-^ ≡ f n x)
∃Coherently-constant′≃ = Eq.↔→≃
  (λ (f , c) → to₁ f c , to₂ f c)
  (λ (f , c) → f 0 , from f c)
  (λ (f , c) → Σ-≡,≡→≡
     (⟨ext⟩ λ n → ⟨ext⟩ λ x → to₁-from f c n x)
     (⟨ext⟩ λ n → ⟨ext⟩ λ x →
        subst (λ f → ∀ n x → f (suc n) ∣ n , x ∣-in-^ ≡ f n x)
          (⟨ext⟩ λ n → ⟨ext⟩ λ x → to₁-from f c n x)
          (to₂ (f 0) (from f c))
          n x                                                       ≡⟨ trans (cong (_$ x) $ sym $
                                                                              push-subst-application _ _) $
                                                                       sym $ push-subst-application _ _ ⟩
        subst (λ f → f (suc n) ∣ n , x ∣-in-^ ≡ f n x)
          (⟨ext⟩ λ n → ⟨ext⟩ λ x → to₁-from f c n x)
          (to₂ (f 0) (from f c) n x)                                ≡⟨ subst-in-terms-of-trans-and-cong ⟩

        trans (sym (cong (λ f → f (suc n) ∣ n , x ∣-in-^)
                      (⟨ext⟩ λ n → ⟨ext⟩ λ x → to₁-from f c n x)))
          (trans (to₂ (f 0) (from f c) n x)
             (cong (λ f → f n x)
                (⟨ext⟩ λ n → ⟨ext⟩ λ x → to₁-from f c n x)))        ≡⟨ cong₂ (λ p q → trans (sym p) (trans (to₂ (f 0) (from f c) n x) q))
                                                                         (trans (sym $ cong-∘ _ _ _) $
                                                                          trans (cong (cong _) $ cong-ext _) $
                                                                          cong-ext _)
                                                                         (trans (sym $ cong-∘ _ _ _) $
                                                                          trans (cong (cong _) $ cong-ext _) $
                                                                          cong-ext _) ⟩
        trans (sym (to₁-from f c (suc n) ∣ n , x ∣-in-^))
          (trans (to₂ (f 0) (from f c) n x)
             (to₁-from f c n x))                                    ≡⟨ to₂-from f c n x ⟩∎

        c n x                                                       ∎))
  (λ (f , c) → cong (f ,_) $ _↔_.from ≡↔≡ $ from-to f c)
  where
  open ∃Coherently-constant′≃

private

  -- A lemma that is used in the implementation of
  -- Coherently-constant′≃.

  Coherently-constant′≃-lemma :
    (∃ λ (f : A → B) → Coherently-constant′ f) ≃
    (∃ λ (f : A → B) →
     ∃ λ (g : ∀ n → ∥ A ∥¹-in-^ (suc n) → B) →
       (∀ x → g 0 ∣ x ∣ ≡ f x) ×
       (∀ n x → g (suc n) ∣ n , x ∣-in-^ ≡ g n x))
  Coherently-constant′≃-lemma {A = A} {B = B} =
    (∃ λ (f : A → B) → Coherently-constant′ f)          ↝⟨ ∃Coherently-constant′≃ ⟩

    (∃ λ (f : ∀ n → ∥ A ∥¹-in-^ n → B) →
       ∀ n x → f (suc n) ∣ n , x ∣-in-^ ≡ f n x)        ↝⟨ Eq.↔→≃
                                                             (λ (f , eq) →
                                                                f 0 , f ∘ suc , ℕ-case (eq 0) (eq ∘ suc))
                                                             (λ (f , g , eq) → ℕ-case f g , eq)
                                                             (λ (f , g , eq) →
                                                                cong (λ eq → f , g , eq) $ ⟨ext⟩ $
                                                                ℕ-case (refl _) (λ _ → refl _))
                                                             lemma ⟩
    (∃ λ (f : A → B) →
     ∃ λ (g : ∀ n → ∥ A ∥¹-in-^ (suc n) → B) →
       ∀ n x →
         g n ∣ n , x ∣-in-^ ≡
         ℕ-case {P = λ n → ∥ A ∥¹-in-^ n → B} f g n x)  ↝⟨ (∃-cong λ _ → ∃-cong λ _ →
                                                            Πℕ≃ ext) ⟩□
    (∃ λ (f : A → B) →
     ∃ λ (g : ∀ n → ∥ A ∥¹-in-^ (suc n) → B) →
       (∀ x → g 0 ∣ x ∣ ≡ f x) ×
       (∀ n x → g (suc n) ∣ n , x ∣-in-^ ≡ g n x))      □
    where

    -- An alternative (unused) proof of the second step above. If this
    -- proof is used instead of the other one, then the proof of
    -- from-Coherently-constant′≃ below fails (at least at the time of
    -- writing).

    second-step :
      (∃ λ (f : ∀ n → ∥ A ∥¹-in-^ n → B) →
         ∀ n x → f (suc n) ∣ n , x ∣-in-^ ≡ f n x) ≃
      (∃ λ (f : A → B) →
       ∃ λ (g : ∀ n → ∥ A ∥¹-in-^ (suc n) → B) →
         ∀ n x →
           g n ∣ n , x ∣-in-^ ≡
           ℕ-case {P = λ n → ∥ A ∥¹-in-^ n → B} f g n x)
    second-step = from-bijection $ inverse $
      (Σ-cong (inverse $ Πℕ≃ {k = equivalence} ext) λ _ → F.id) F.∘
      Σ-assoc

    abstract

      lemma :
        (p@(f , eq) : ∃ λ (f : ∀ n → ∥ A ∥¹-in-^ n → B) →
                        ∀ n x → f (suc n) ∣ n , x ∣-in-^ ≡ f n x) →
        (ℕ-case (f 0) (f ∘ suc) , ℕ-case (eq 0) (eq ∘ suc)) ≡ p
      lemma (f , eq) =
        Σ-≡,≡→≡
          (⟨ext⟩ $ ℕ-case (refl _) (λ _ → refl _))
          (⟨ext⟩ λ n → ⟨ext⟩ λ x →
           let eq′ = ℕ-case (eq 0) (eq ∘ suc)
               r   = ℕ-case (refl _) (λ _ → refl _)
           in
           subst {y = f}
             (λ f → ∀ n x → f (suc n) ∣ n , x ∣-in-^ ≡ f n x)
             (⟨ext⟩ r) eq′ n x                                            ≡⟨ sym $
                                                                             trans (push-subst-application _ _) $
                                                                             cong (_$ x) $ push-subst-application _ _ ⟩
           subst
             (λ f → f (suc n) ∣ n , x ∣-in-^ ≡ f n x)
             (⟨ext⟩ r) (eq′ n x)                                          ≡⟨ subst-in-terms-of-trans-and-cong ⟩

           trans (sym (cong (λ f → f (suc n) ∣ n , x ∣-in-^) (⟨ext⟩ r)))
             (trans (eq′ n x) (cong (λ f → f n x) (⟨ext⟩ r)))             ≡⟨ trans (cong (flip trans _) $
                                                                                trans (cong sym $
                                                                                trans (sym $ cong-∘ _ _ _) $
                                                                                trans (cong (cong (_$ ∣ n , x ∣-in-^)) $
                                                                                cong-ext _)
                                                                                (cong-refl _))
                                                                                sym-refl) $
                                                                             trans-reflˡ _ ⟩

           trans (eq′ n x) (cong (λ f → f n x) (⟨ext⟩ r))                 ≡⟨ cong (trans _) $
                                                                             trans (sym $ cong-∘ _ _ _) $
                                                                             cong (cong (_$ x)) $
                                                                             cong-ext _ ⟩

           trans (eq′ n x) (cong (_$ x) $ r n)                            ≡⟨ ℕ-case
                                                                               {P = λ n → ∀ x → trans (eq′ n x) (cong (_$ x) $ r n) ≡ eq n x}
                                                                               (λ _ → trans (cong (trans _) $ cong-refl _) $
                                                                                trans-reflʳ _)
                                                                               (λ _ _ → trans (cong (trans _) $ cong-refl _) $
                                                                                trans-reflʳ _)
                                                                               n x ⟩∎
           eq n x                                                         ∎)

-- Coherently-constant′ can be expressed in a different way.

Coherently-constant′≃ :
  Block "Coherently-constant′≃" →
  {f : A → B} →
  Coherently-constant′ f
    ≃
  (∃ λ (g : ∀ n → ∥ A ∥¹-in-^ (suc n) → B) →
     (∀ x → g 0 ∣ x ∣ ≡ f x) ×
     (∀ n x → g (suc n) ∣ n , x ∣-in-^ ≡ g n x))
Coherently-constant′≃ ⊠ {f = f} =
  Eq.⟨ _
     , Eq.drop-Σ-map-id _
         (_≃_.is-equivalence Coherently-constant′≃-lemma)
         f
     ⟩

-- A "computation" rule for Coherently-constant′≃.

from-Coherently-constant′≃-property :
  (bl : Block "Coherently-constant′≃") →
  (f : A → B)
  {c@(g , g₀ , _) :
   ∃ λ (g : ∀ n → ∥ A ∥¹-in-^ (suc n) → B) →
     (∀ x → g 0 ∣ x ∣ ≡ f x) ×
     (∀ n x → g (suc n) ∣ n , x ∣-in-^ ≡ g n x)} →
  _≃_.from (Coherently-constant′≃ bl) c .property ≡ (g 0 , g₀)
from-Coherently-constant′≃-property
  {A = A} {B = B} ⊠ f {c = c@(g , g₀ , g₊)} =

  _≃_.from (Coherently-constant′≃ ⊠) c .property                      ≡⟨⟩

  HA.inverse
    (Eq.drop-Σ-map-id _
       (_≃_.is-equivalence Coherently-constant′≃-lemma)
       f)
    c .property                                                       ≡⟨ cong (λ c → c .property) $
                                                                         Eq.inverse-drop-Σ-map-id
                                                                           {x = f} {eq = _≃_.is-equivalence Coherently-constant′≃-lemma} ⟩
  subst Coherently-constant′
    (cong proj₁ $
     _≃_.right-inverse-of Coherently-constant′≃-lemma (f , c))
    (proj₂ (_≃_.from Coherently-constant′≃-lemma (f , c)))
    .property                                                         ≡⟨ subst-Coherently-property ⟩

  subst Constant′
    (cong proj₁ $
     _≃_.right-inverse-of Coherently-constant′≃-lemma (f , c))
    (proj₂ (_≃_.from Coherently-constant′≃-lemma (f , c)) .property)  ≡⟨⟩

  subst Constant′
    (cong proj₁ $
     trans
       (cong {B = ∃ λ (f : A → B) →
                  ∃ λ (g : ∀ n → ∥ A ∥¹-in-^ (suc n) → B) →
                    (∀ x → g 0 ∣ x ∣ ≡ f x) ×
                    (∀ n x → g (suc n) ∣ n , x ∣-in-^ ≡ g n x)}
             (λ (f , eq) → f 0 , f ∘ suc , eq 0 , eq ∘ suc) $
        _≃_.right-inverse-of ∃Coherently-constant′≃
          (ℕ-case f g , ℕ-case g₀ g₊)) $
     trans
       (cong (λ (f , g , eq) → f , g , eq 0 , eq ∘ suc) $
        cong {B = ∃ λ (f : A → B) →
                  ∃ λ (g : ∀ n → ∥ A ∥¹-in-^ (suc n) → B) →
                    ∀ n x →
                      g n ∣ n , x ∣-in-^ ≡
                      ℕ-case {P = λ n → ∥ A ∥¹-in-^ n → B} f g n x}
             {x = ℕ-case g₀ g₊}
             {y = ℕ-case g₀ g₊}
             (λ eq → f , g , eq) $
        ⟨ext⟩ (ℕ-case (refl _) (λ _ → refl _))) $
     cong (f ,_) (cong (g ,_) (refl _)))
    (g 0 , g₀)                                                        ≡⟨ cong (flip (subst Constant′) _) lemma ⟩

  subst Constant′ (refl _) (g 0 , g₀)                                 ≡⟨ subst-refl _ _ ⟩∎

  g 0 , g₀                                                            ∎
  where
  lemma =
    (cong proj₁ $
     trans
       (cong {B = ∃ λ (f : A → B) →
                  ∃ λ (g : ∀ n → ∥ A ∥¹-in-^ (suc n) → B) →
                    (∀ x → g 0 ∣ x ∣ ≡ f x) ×
                    (∀ n x → g (suc n) ∣ n , x ∣-in-^ ≡ g n x)}
             (λ (f , eq) → f 0 , f ∘ suc , eq 0 , eq ∘ suc) $
        _≃_.right-inverse-of ∃Coherently-constant′≃
          (ℕ-case f g , ℕ-case g₀ g₊)) $
     trans
       (cong (λ (f , g , eq) → f , g , eq 0 , eq ∘ suc) $
        cong {B = ∃ λ (f : A → B) →
                  ∃ λ (g : ∀ n → ∥ A ∥¹-in-^ (suc n) → B) →
                    ∀ n x →
                      g n ∣ n , x ∣-in-^ ≡
                      ℕ-case {P = λ n → ∥ A ∥¹-in-^ n → B} f g n x}
             {x = ℕ-case g₀ g₊}
             {y = ℕ-case g₀ g₊}
             (λ eq → f , g , eq) $
        ⟨ext⟩ (ℕ-case (refl _) (λ _ → refl _))) $
     cong (f ,_) (cong (g ,_) (refl _)))                               ≡⟨ trans (cong-trans _ _ _) $
                                                                          cong₂ trans
                                                                            (trans (cong-∘ _ _ _) $
                                                                             sym $ cong-∘ _ _ _)
                                                                            (trans (cong-trans _ _ _) $
                                                                             cong₂ trans
                                                                               (trans (cong-∘ _ _ _) $
                                                                                cong-∘ _ _ _)
                                                                               (cong-∘ _ _ _)) ⟩
    (trans
       (cong (_$ 0) $ cong proj₁ $
        _≃_.right-inverse-of ∃Coherently-constant′≃
          (ℕ-case f g , ℕ-case g₀ g₊)) $
     trans
       (cong (const f) $
        ⟨ext⟩ (ℕ-case (refl _) (λ _ → refl _))) $
     cong (const f) (cong (g ,_) (refl _)))                            ≡⟨ trans (cong (trans _) $
                                                                                trans (cong₂ trans
                                                                                (cong-const _)
                                                                                (cong-const _)) $
                                                                                trans-refl-refl) $
                                                                          trans-reflʳ _ ⟩
    (cong (_$ 0) $ cong proj₁ $
     _≃_.right-inverse-of ∃Coherently-constant′≃
       (ℕ-case f g , ℕ-case g₀ g₊))                                    ≡⟨ cong (cong (_$ 0)) $
                                                                          proj₁-Σ-≡,≡→≡ _ _ ⟩
    (cong (_$ 0) $ ⟨ext⟩ λ n → ⟨ext⟩ λ x →
     ∃Coherently-constant′≃.to₁-from (ℕ-case f g) (ℕ-case g₀ g₊) n x)  ≡⟨ cong-ext _ ⟩

    (⟨ext⟩ λ x →
     ∃Coherently-constant′≃.to₁-from (ℕ-case f g) (ℕ-case g₀ g₊) 0 x)  ≡⟨⟩

    (⟨ext⟩ λ _ → refl _)                                               ≡⟨ ext-refl ⟩∎

    refl _                                                             ∎

-- Functions from ∥ A ∥ can be expressed as coherently constant
-- functions from A (assuming univalence).

∥∥→≃ :
  ∀ {A : Type a} {B : Type b} →
  Univalence (a ⊔ b) →
  (∥ A ∥ → B)
    ≃
  (∃ λ (f : A → B) → Coherently-constant f)
∥∥→≃ {A = A} {B = B} univ =
  (∥ A ∥ → B)                                   ↝⟨ N.∥∥→≃ ⟩

  (∃ λ (f : ∀ n → ∥ A ∥¹-out-^ n → B) →
     ∀ n x → f (suc n) ∣ x ∣ ≡ f n x)           ↝⟨ (Σ-cong {k₁ = equivalence} (∀-cong ext λ n → →-cong₁ ext (O.∥∥¹-out-^≃∥∥¹-in-^ n)) λ f →
                                                    ∀-cong ext λ n →
                                                    Π-cong-contra ext (inverse $ O.∥∥¹-out-^≃∥∥¹-in-^ n) λ x →
                                                    ≡⇒↝ _ $ cong (λ y → f (suc n) y ≡ f n (_≃_.from (O.∥∥¹-out-^≃∥∥¹-in-^ n) x)) (
    ∣ _≃_.from (O.∥∥¹-out-^≃∥∥¹-in-^ n) x ∣           ≡⟨ sym $ O.∣,∣-in-^≡∣∣ n ⟩∎

    _≃_.from (O.∥∥¹-out-^≃∥∥¹-in-^ (suc n))
      ∣ n , x ∣-in-^                                  ∎)) ⟩

  (∃ λ (f : ∀ n → ∥ A ∥¹-in-^ n → B) →
     ∀ n x → f (suc n) ∣ n , x ∣-in-^ ≡ f n x)  ↝⟨ inverse ∃Coherently-constant′≃ ⟩

  (∃ λ (f : A → B) → Coherently-constant′ f)    ↝⟨ (∃-cong λ _ → inverse $ Coherently-constant≃Coherently-constant′ ⊠ univ) ⟩□

  (∃ λ (f : A → B) → Coherently-constant f)     □

-- A function used in the statement of proj₂-to-∥∥→≃-property≡.

proj₁-to-∥∥→≃-constant :
  {A : Type a} {B : Type b}
  (univ : Univalence (a ⊔ b)) →
  (f : ∥ A ∥ → B) →
  Constant (proj₁ (_≃_.to (∥∥→≃ univ) f))
proj₁-to-∥∥→≃-constant _ f x y =
  f ∣ x ∣  ≡⟨ cong f (T.truncation-is-proposition ∣ x ∣ ∣ y ∣) ⟩∎
  f ∣ y ∣  ∎

-- A "computation rule" for ∥∥→≃.

proj₂-to-∥∥→≃-property≡ :
  {A : Type a} {B : Type b}
  (univ : Univalence (a ⊔ b)) →
  {f : ∥ A ∥ → B} →
  proj₂ (_≃_.to (∥∥→≃ univ) f) .property ≡
  proj₁-to-∥∥→≃-constant univ f
proj₂-to-∥∥→≃-property≡ univ {f = f} = ⟨ext⟩ λ x → ⟨ext⟩ λ y →

  let g , c = _≃_.to C.universal-property (f ∘ _≃_.to N.∥∥≃∥∥) in

  proj₂ (_≃_.to (∥∥→≃ univ) f) .property x y                             ≡⟨⟩

  _≃_.from (Coherently-constant≃Coherently-constant′ ⊠ univ)
    (proj₂
       (_≃_.from ∃Coherently-constant′≃
          (Σ-map (λ g n → g n ∘ _≃_.from (oi n))
                 (λ {g} c n x →
                    ≡⇒→ (cong (λ y → g (suc n) y ≡
                                     g n (_≃_.from (oi n) x))
                           (sym $ O.∣,∣-in-^≡∣∣ n))
                      (c n (_≃_.from (oi n) x)))
             (_≃_.to C.universal-property (f ∘ _≃_.to N.∥∥≃∥∥)))))
    .property x y                                                        ≡⟨⟩

  _≃_.from (Constant≃Constant′ _)
    (proj₂
       (_≃_.from ∃Coherently-constant′≃
          (Σ-map (λ g n → g n ∘ _≃_.from (oi n))
                 (λ {g} c n x →
                    ≡⇒→ (cong (λ y → g (suc n) y ≡
                                     g n (_≃_.from (oi n) x))
                           (sym $ O.∣,∣-in-^≡∣∣ n))
                      (c n (_≃_.from (oi n) x)))
             (_≃_.to C.universal-property (f ∘ _≃_.to N.∥∥≃∥∥))))
       .property)
     x y                                                                 ≡⟨⟩

  _≃_.from (Constant≃Constant′ _)
    ( g 1
    , λ x → ≡⇒→ (cong (λ z → g 1 z ≡ g 0 x) (sym $ refl ∣ _ ∣)) (c 0 x)
    ) x y                                                                ≡⟨⟩

  trans (sym (≡⇒→ (cong (λ z → g 1 z ≡ g 0 x) (sym $ refl ∣ _ ∣))
                (c 0 x)))
    (trans (cong (g 1) (O.∣∣-constant x y))
       (≡⇒→ (cong (λ z → g 1 z ≡ g 0 y) (sym $ refl ∣ _ ∣)) (c 0 y)))    ≡⟨ cong₂ (λ p q → trans (sym p) (trans (cong (g 1) (O.∣∣-constant x y)) q))
                                                                              (trans (cong (λ eq → ≡⇒→ (cong (λ z → g 1 z ≡ g 0 x) eq) (c 0 x))
                                                                                sym-refl) $
                                                                               trans (cong (λ eq → ≡⇒→ eq (c 0 x)) $
                                                                                cong-refl _) $
                                                                               cong (_$ c 0 x) ≡⇒→-refl)
                                                                              (trans (cong (λ eq → ≡⇒→ (cong (λ z → g 1 z ≡ g 0 y) eq) (c 0 y))
                                                                                sym-refl) $
                                                                               trans (cong (λ eq → ≡⇒→ eq (c 0 y)) $
                                                                                cong-refl _) $
                                                                               cong (_$ c 0 y) ≡⇒→-refl) ⟩
  trans (sym (c 0 x)) (trans (cong (g 1) (O.∣∣-constant x y)) (c 0 y))   ≡⟨⟩

  trans (sym (cong (f ∘ _≃_.to N.∥∥≃∥∥) (C.∣∣≡∣∣ x)))
    (trans (cong (f ∘ _≃_.to N.∥∥≃∥∥ ∘ ∣_∣) (O.∣∣-constant x y))
       (cong (f ∘ _≃_.to N.∥∥≃∥∥) (C.∣∣≡∣∣ y)))                          ≡⟨ cong₂ (λ p q → trans (sym p) q)
                                                                              (sym $ cong-∘ _ _ _)
                                                                              (cong₂ trans
                                                                                (sym $ cong-∘ _ _ _)
                                                                                (sym $ cong-∘ _ _ _)) ⟩
  trans (sym (cong f (cong (_≃_.to N.∥∥≃∥∥) (C.∣∣≡∣∣ x))))
    (trans (cong f (cong (_≃_.to N.∥∥≃∥∥ ∘ ∣_∣) (O.∣∣-constant x y)))
       (cong f (cong (_≃_.to N.∥∥≃∥∥) (C.∣∣≡∣∣ y))))                     ≡⟨ trans (cong₂ trans
                                                                                (sym $ cong-sym _ _)
                                                                                (sym $ cong-trans _ _ _)) $
                                                                            sym $ cong-trans _ _ _ ⟩
  cong f
    (trans (sym (cong (_≃_.to N.∥∥≃∥∥) (C.∣∣≡∣∣ x)))
      (trans (cong (_≃_.to N.∥∥≃∥∥ ∘ ∣_∣) (O.∣∣-constant x y))
         (cong (_≃_.to N.∥∥≃∥∥) (C.∣∣≡∣∣ y))))                           ≡⟨ cong (cong f) $
                                                                            mono₁ 1 T.truncation-is-proposition _ _ ⟩∎
  cong f (T.truncation-is-proposition ∣ x ∣ ∣ y ∣)                       ∎
  where
  oi = O.∥∥¹-out-^≃∥∥¹-in-^

-- Two variants of Coherently-constant are pointwise equivalent
-- (assuming univalence).

Coherently-constant≃Coherently-constant :
  {A : Type a} {B : Type b} {f : A → B} →
  Univalence (a ⊔ b) →
  CC.Coherently-constant f ≃ Coherently-constant f
Coherently-constant≃Coherently-constant {A = A} {B = B} {f = f} univ =
  CC.Coherently-constant f                                           ↔⟨⟩

  (∃ λ (g : ∥ A ∥ → B) → f ≡ g ∘ ∣_∣)                                ↝⟨ (Σ-cong (∥∥→≃ univ) λ _ → F.id) ⟩

  (∃ λ ((g , _) : ∃ λ (g : A → B) → Coherently-constant g) → f ≡ g)  ↔⟨ inverse Σ-assoc ⟩

  (∃ λ (g : A → B) → Coherently-constant g × f ≡ g)                  ↝⟨ (∃-cong λ _ → ×-cong₁ λ eq → ≡⇒↝ _ $
                                                                         cong Coherently-constant $ sym eq) ⟩

  (∃ λ (g : A → B) → Coherently-constant f × f ≡ g)                  ↔⟨ ∃-comm ⟩

  Coherently-constant f × (∃ λ (g : A → B) → f ≡ g)                  ↔⟨ (drop-⊤-right λ _ →
                                                                         _⇔_.to contractible⇔↔⊤ (other-singleton-contractible _)) ⟩□
  Coherently-constant f                                              □

-- A "computation rule" for Coherently-constant≃Coherently-constant.

to-Coherently-constant≃Coherently-constant-property :
  ∀ {A : Type a} {B : Type b} {f : A → B}
    {c : CC.Coherently-constant f} {x y}
  (univ : Univalence (a ⊔ b)) →
  _≃_.to (Coherently-constant≃Coherently-constant univ)
    c .property x y ≡
  trans (cong (_$ x) (proj₂ c))
     (trans (proj₁-to-∥∥→≃-constant univ (proj₁ c) _ _)
        (cong (_$ y) (sym (proj₂ c))))
to-Coherently-constant≃Coherently-constant-property
  {f = f} {c = c} {x = x} {y = y} univ =
  _≃_.to (Coherently-constant≃Coherently-constant univ)
    c .property x y                                       ≡⟨⟩

  ≡⇒→ (cong Coherently-constant $ sym (proj₂ c))
    (proj₂ (_≃_.to (∥∥→≃ univ) (proj₁ c))) .property x y  ≡⟨ cong (λ (c : Coherently-constant _) → c .property x y) $ sym $
                                                             subst-in-terms-of-≡⇒↝ equivalence _ _ _ ⟩
  subst Coherently-constant (sym (proj₂ c))
    (proj₂ (_≃_.to (∥∥→≃ univ) (proj₁ c))) .property x y  ≡⟨ cong (λ (f : Constant _) → f x y)
                                                             subst-Coherently-property ⟩
  subst Constant (sym (proj₂ c))
    (proj₂ (_≃_.to (∥∥→≃ univ) (proj₁ c)) .property) x y  ≡⟨ trans (cong (_$ y) $ sym $ push-subst-application _ _) $
                                                             sym $ push-subst-application _ _ ⟩
  subst (λ f → f x ≡ f y) (sym (proj₂ c))
    (proj₂ (_≃_.to (∥∥→≃ univ) (proj₁ c)) .property x y)  ≡⟨ cong (λ (f : Constant _) → subst (λ f → f x ≡ f y) (sym (proj₂ c)) (f x y)) $
                                                             proj₂-to-∥∥→≃-property≡ univ ⟩
  subst (λ f → f x ≡ f y) (sym (proj₂ c))
    (proj₁-to-∥∥→≃-constant univ (proj₁ c) x y)           ≡⟨ subst-in-terms-of-trans-and-cong ⟩

  trans (sym (cong (_$ x) (sym (proj₂ c))))
     (trans (proj₁-to-∥∥→≃-constant univ (proj₁ c) _ _)
        (cong (_$ y) (sym (proj₂ c))))                    ≡⟨ cong (flip trans _) $
                                                             trans (sym $ cong-sym _ _) $
                                                             cong (cong (_$ x)) $ sym-sym _ ⟩∎
  trans (cong (_$ x) (proj₂ c))
     (trans (proj₁-to-∥∥→≃-constant univ (proj₁ c) _ _)
        (cong (_$ y) (sym (proj₂ c))))                    ∎

------------------------------------------------------------------------
-- Lenses, defined as getters with coherently constant fibres

-- The lens type family.

Lens : Type a → Type b → Type (lsuc (a ⊔ b))
Lens A B = ∃ λ (get : A → B) → Coherently-constant (get ⁻¹_)

-- Some derived definitions.

module Lens {A : Type a} {B : Type b} (l : Lens A B) where

  -- A getter.

  get : A → B
  get = proj₁ l

  -- The family of fibres of the getter is coherently constant.

  get⁻¹-coherently-constant : Coherently-constant (get ⁻¹_)
  get⁻¹-coherently-constant = proj₂ l

  -- All the getter's fibres are equivalent.

  get⁻¹-constant : (b₁ b₂ : B) → get ⁻¹ b₁ ≃ get ⁻¹ b₂
  get⁻¹-constant b₁ b₂ =
    ≡⇒≃ (get⁻¹-coherently-constant .property b₁ b₂)

  -- A setter.

  set : A → B → A
  set a b =                    $⟨ _≃_.to (get⁻¹-constant (get a) b) ⟩
    (get ⁻¹ get a → get ⁻¹ b)  ↝⟨ _$ (a , refl _) ⟩
    get ⁻¹ b                   ↝⟨ proj₁ ⟩□
    A                          □

instance

  -- The lenses defined above have getters and setters.

  has-getter-and-setter :
    Has-getter-and-setter (Lens {a = a} {b = b})
  has-getter-and-setter = record
    { get = Lens.get
    ; set = Lens.set
    }

-- Lens is pointwise equivalent to Higher.Lens (assuming univalence).

Higher-lens≃Lens :
  {A : Type a} {B : Type b} →
  Block "Higher-lens≃Lens" →
  Univalence (lsuc (a ⊔ b)) →
  Higher.Lens A B ≃ Lens A B
Higher-lens≃Lens {A = A} {B = B} ⊠ univ =
  Higher.Lens A B                                         ↔⟨⟩
  (∃ λ (get : A → B) → CC.Coherently-constant (get ⁻¹_))  ↝⟨ (∃-cong λ _ → Coherently-constant≃Coherently-constant univ) ⟩□
  (∃ λ (get : A → B) → Coherently-constant (get ⁻¹_))     □

-- The equivalence preserves getters and setters.

Higher-lens≃Lens-preserves-getters-and-setters :
  {A : Type a} {B : Type b}
  (bl : Block "Higher-lens≃Lens")
  (univ : Univalence (lsuc (a ⊔ b))) →
  Preserves-getters-and-setters-⇔ A B
    (_≃_.logical-equivalence (Higher-lens≃Lens bl univ))
Higher-lens≃Lens-preserves-getters-and-setters {A = A} {B = B} bl univ =
  Preserves-getters-and-setters-→-↠-⇔
    (_≃_.surjection (Higher-lens≃Lens bl univ))
    (λ l → get-lemma bl l , set-lemma bl l)
  where
  get-lemma :
    ∀ bl (l : Higher.Lens A B) →
    Lens.get (_≃_.to (Higher-lens≃Lens bl univ) l) ≡ Higher.Lens.get l
  get-lemma ⊠ _ = refl _

  set-lemma :
    ∀ bl (l : Higher.Lens A B) →
    Lens.set (_≃_.to (Higher-lens≃Lens bl univ) l) ≡ Higher.Lens.set l
  set-lemma bl@⊠ l = ⟨ext⟩ λ a → ⟨ext⟩ λ b →
    Lens.set (_≃_.to (Higher-lens≃Lens bl univ) l) a b               ≡⟨⟩

    proj₁ (≡⇒→ (≡⇒→ (cong Coherently-constant (sym get⁻¹-≡))
                    (proj₂ (_≃_.to (∥∥→≃ univ) H))
                    .property (get a) b)
               (a , refl (get a)))                                   ≡⟨ cong (λ (c : Coherently-constant (get ⁻¹_)) →
                                                                                proj₁ (≡⇒→ (c .property (get a) b) (a , refl _))) $ sym $
                                                                        subst-in-terms-of-≡⇒↝ equivalence _ _ _ ⟩
    proj₁ (≡⇒→ (subst Coherently-constant (sym get⁻¹-≡)
                  (proj₂ (_≃_.to (∥∥→≃ univ) H))
                  .property (get a) b)
               (a , refl (get a)))                                   ≡⟨ cong (λ (c : Constant (get ⁻¹_)) →
                                                                                proj₁ (≡⇒→ (c (get a) b) (a , refl _)))
                                                                        subst-Coherently-property ⟩
    proj₁ (≡⇒→ (subst Constant (sym get⁻¹-≡)
                  (proj₂ (_≃_.to (∥∥→≃ univ) H) .property)
                  (get a) b)
               (a , refl (get a)))                                   ≡⟨ cong (λ c → proj₁ (≡⇒→ (subst Constant (sym get⁻¹-≡) c (get a) b)
                                                                                (a , refl _))) $
                                                                        proj₂-to-∥∥→≃-property≡ univ ⟩
    proj₁ (≡⇒→ (subst Constant (sym get⁻¹-≡)
                  (proj₁-to-∥∥→≃-constant univ H)
                  (get a) b)
               (a , refl (get a)))                                   ≡⟨ cong (λ eq → proj₁ (≡⇒→ eq (a , refl _))) $
                                                                        trans (cong (_$ b) $ sym $
                                                                               push-subst-application _ _) $
                                                                        sym $ push-subst-application _ _ ⟩
    proj₁ (≡⇒→ (subst (λ f → f (get a) ≡ f b) (sym get⁻¹-≡)
                  (proj₁-to-∥∥→≃-constant univ H (get a) b))
               (a , refl (get a)))                                   ≡⟨ cong (λ eq → proj₁ (≡⇒→ eq (a , refl _))) $
                                                                        subst-in-terms-of-trans-and-cong ⟩
    proj₁ (≡⇒→ (trans (sym (cong (_$ get a) (sym get⁻¹-≡)))
                  (trans (proj₁-to-∥∥→≃-constant univ H (get a) b)
                     (cong (_$ b) (sym get⁻¹-≡))))
               (a , refl (get a)))                                   ≡⟨⟩

    proj₁ (≡⇒→ (trans (sym (cong (_$ get a) (sym get⁻¹-≡)))
                  (trans (cong H (T.truncation-is-proposition _ _))
                     (cong (_$ b) (sym get⁻¹-≡))))
               (a , refl (get a)))                                   ≡⟨ cong (λ f → proj₁ (f (a , refl _))) $
                                                                        ≡⇒↝-trans equivalence ⟩
    proj₁ (≡⇒→ (trans (cong H (T.truncation-is-proposition _ _))
                  (cong (_$ b) (sym get⁻¹-≡)))
             (≡⇒→ (sym (cong (_$ get a) (sym get⁻¹-≡)))
                (a , refl (get a))))                                 ≡⟨ cong (λ f → proj₁ (f (≡⇒→ (sym (cong (_$ get a) (sym get⁻¹-≡)))
                                                                                (a , refl _)))) $
                                                                        ≡⇒↝-trans equivalence ⟩
    proj₁ (≡⇒→ (cong (_$ b) (sym get⁻¹-≡))
             (≡⇒→ (cong H (T.truncation-is-proposition _ _))
                (≡⇒→ (sym (cong (_$ get a) (sym get⁻¹-≡)))
                   (a , refl (get a)))))                             ≡⟨ cong₂ (λ p q → proj₁ (≡⇒→ p
                                                                                (≡⇒→ (cong H (T.truncation-is-proposition _ _))
                                                                                (≡⇒→ q (a , refl _)))))
                                                                          (cong-sym _ _)
                                                                          (trans (cong sym $ cong-sym _ _) $
                                                                           sym-sym _) ⟩
    proj₁ (≡⇒→ (sym $ cong (_$ b) get⁻¹-≡)
             (≡⇒→ (cong H (T.truncation-is-proposition _ _))
                (≡⇒→ (cong (_$ get a) get⁻¹-≡)
                   (a , refl (get a)))))                             ≡⟨ cong (λ f → proj₁ (f (≡⇒→ (cong H (T.truncation-is-proposition _ _))
                                                                                (≡⇒→ (cong (_$ get a) get⁻¹-≡)
                                                                                (a , refl _))))) $
                                                                        ≡⇒↝-sym equivalence ⟩
    proj₁ (_≃_.from (≡⇒≃ (cong (_$ b) get⁻¹-≡))
             (≡⇒→ (cong H (T.truncation-is-proposition _ _))
                (≡⇒→ (cong (_$ get a) get⁻¹-≡)
                   (a , refl (get a)))))                             ≡⟨⟩

    set a b                                                          ∎
    where
    open Higher.Lens l

max_stars_repo_name: nad/dependent-lenses

max_issues_repo_name: nad/dependent-lenses

max_forks_repo_name: nad/dependent-lenses


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

open import Categories.Category
open import Categories.Functor
open import Data.Product using (_×_; ∃; _,_; proj₁; proj₂; zip; map)
open import Level
open import Relation.Binary using (Rel)
open import Categories.Support.EqReasoning

Comma :
    {o₁ ℓ₁ e₁ o₂ ℓ₂ e₂ o₃ ℓ₃ e₃ : Level}
    {A : Category o₁ ℓ₁ e₁}
    {B : Category o₂ ℓ₂ e₂}
    {C : Category o₃ ℓ₃ e₃}
    → Functor A C → Functor B C
    → Category (o₁ ⊔ o₂ ⊔ ℓ₃) (ℓ₁ ⊔ ℓ₂ ⊔ e₃) (e₁ ⊔ e₂)
Comma {o₁}{ℓ₁}{e₁}
      {o₂}{ℓ₂}{e₂}
      {o₃}{ℓ₃}{e₃}
      {A}{B}{C} T S
  = record
  { Obj         = Obj
  ; _⇒_         = Hom
  ; _≡_         = _≡′_
  ; _∘_         = _∘′_
  ; id          = id′
  ; assoc       = A.assoc , B.assoc
  ; identityˡ   = A.identityˡ , B.identityˡ
  ; identityʳ   = A.identityʳ , B.identityʳ
  ; equiv = record
    { refl  = A.Equiv.refl , B.Equiv.refl
    ; sym   = map A.Equiv.sym B.Equiv.sym
    ; trans = zip A.Equiv.trans B.Equiv.trans
    }
  ; ∘-resp-≡    = zip A.∘-resp-≡ B.∘-resp-≡
  } module Comma where
    module A = Category A
    module B = Category B
    module C = Category C
    module T = Functor T
    module S = Functor S

    open T using () renaming (F₀ to T₀; F₁ to T₁)
    open S using () renaming (F₀ to S₀; F₁ to S₁)

    infixr 9 _∘′_
    infix  4 _≡′_
    infix 10 _,_,_ _,_[_]

    record Obj : Set (o₁ ⊔ o₂ ⊔ ℓ₃) where
        eta-equality
        constructor _,_,_
        field
            α : A.Obj
            β : B.Obj
            f : C [ T₀ α , S₀ β ]

    record Hom (X₁ X₂ : Obj) : Set (ℓ₁ ⊔ ℓ₂ ⊔ e₃) where
        eta-equality
        constructor _,_[_]
        open Obj X₁ renaming (α to α₁; β to β₁; f to f₁)
        open Obj X₂ renaming (α to α₂; β to β₂; f to f₂)

        field
            g         : A [ α₁ , α₂ ]
            h         : B [ β₁ , β₂ ]
            .commutes : C.CommutativeSquare f₁ (T₁ g) (S₁ h) f₂

    _≡′_ : ∀ {X₁ X₂} → Rel (Hom X₁ X₂) _
    (g₁ , h₁ [ _ ]) ≡′ (g₂ , h₂ [ _ ])
        = A [ g₁ ≡ g₂ ]
        × B [ h₁ ≡ h₂ ]

    id′ : {A : Obj} → Hom A A
    id′ { A } = A.id , B.id
        [ begin
              C [ S₁ B.id ∘ f ]
          ↓⟨ S.identity ⟩∘⟨ refl ⟩
              C [ C.id ∘ f ]
          ↓⟨ C.identityˡ ⟩
              f
          ↑⟨ C.identityʳ ⟩
              C [ f ∘ C.id ]
          ↑⟨ refl ⟩∘⟨ T.identity ⟩
              C [ f ∘ T₁ A.id ]
          ∎ ]
          where
            open Obj A
            open C.HomReasoning
            open C.Equiv

    _∘′_ : ∀ {X₁ X₂ X₃} → Hom X₂ X₃ → Hom X₁ X₂ → Hom X₁ X₃
    _∘′_ {X₁}{X₂}{X₃} (g₁ , h₁ [ commutes₁ ]) (g₂ , h₂ [ commutes₂ ])
        = A [ g₁ ∘ g₂ ] , B [ h₁ ∘ h₂ ]
        [ begin
            -- commutes₁ : C [ C [ S₁ h₁ ∘ f₂ ]  ≡ C [ f₃ ∘ T₁ g₁ ] ]
            -- commutes₂ : C [ C [ S₁ h₂ ∘ f₁ ]  ≡ C [ f₂ ∘ T₁ g₂ ] ]
                C [ S₁ (B [ h₁ ∘ h₂ ]) ∘ f₁ ]
            ↓⟨ S.homomorphism ⟩∘⟨ refl ⟩
                C [ C [ S₁ h₁ ∘ S₁ h₂ ] ∘ f₁ ]
            ↓⟨ C.assoc ⟩
                C [ S₁ h₁ ∘  C [ S₁ h₂ ∘ f₁ ] ]
            ↓⟨ refl ⟩∘⟨ commutes₂ ⟩
                C [ S₁ h₁ ∘  C [ f₂ ∘ T₁ g₂ ] ]
            ↑⟨ C.assoc ⟩
                C [ C [ S₁ h₁ ∘  f₂ ] ∘ T₁ g₂ ]
            ↓⟨ commutes₁ ⟩∘⟨ refl ⟩
                C [ C [ f₃ ∘ T₁ g₁ ] ∘ T₁ g₂ ]
            ↓⟨ C.assoc ⟩
                C [ f₃ ∘ C [ T₁ g₁ ∘ T₁ g₂ ] ]
            ↑⟨ refl ⟩∘⟨ T.homomorphism ⟩
                C [ f₃ ∘ T₁ (A [ g₁ ∘ g₂ ]) ]
         ∎ ]
        where
            open C.HomReasoning
            open C.Equiv
            open Obj X₁ renaming (α to α₁; β to β₁; f to f₁)
            open Obj X₂ renaming (α to α₂; β to β₂; f to f₂)
            open Obj X₃ renaming (α to α₃; β to β₃; f to f₃)

_↓_ : ∀ {o₁ ℓ₁ e₁ o₂ ℓ₂ e₂ o₃ ℓ₃ e₃}
      → {A : Category o₁ ℓ₁ e₁}
      → {B : Category o₂ ℓ₂ e₂}
      → {C : Category o₃ ℓ₃ e₃}
      → (S : Functor B C) (T : Functor A C)
      → Category _ _ _
T ↓ S = Comma T S

Dom : {o₁ ℓ₁ e₁ o₂ ℓ₂ e₂ o₃ ℓ₃ e₃ : Level}
    {A : Category o₁ ℓ₁ e₁}
    {B : Category o₂ ℓ₂ e₂}
    {C : Category o₃ ℓ₃ e₃}
    → (T : Functor A C) → (S : Functor B C)
    → Functor (Comma T S) A
Dom {A = A} {B} {C} T S = record
  { F₀ = Obj.α
  ; F₁ = Hom.g
  ; identity = refl
  ; homomorphism = refl
  ; F-resp-≡ = proj₁
  }
 where
  open Comma T S
  open A.Equiv

Cod : {o₁ ℓ₁ e₁ o₂ ℓ₂ e₂ o₃ ℓ₃ e₃ : Level}
    {A : Category o₁ ℓ₁ e₁}
    {B : Category o₂ ℓ₂ e₂}
    {C : Category o₃ ℓ₃ e₃}
    → (T : Functor A C) → (S : Functor B C)
    → Functor (Comma T S) B
Cod {A = A} {B} {C} T S = record
  { F₀ = Obj.β
  ; F₁ = Hom.h
  ; identity = refl
  ; homomorphism = refl
  ; F-resp-≡ = proj₂
  }
 where
  open Comma T S
  open B.Equiv

open import Categories.Functor.Diagonal
open import Categories.FunctorCategory
open import Categories.Categories
open import Categories.NaturalTransformation

CommaF : ∀ {o ℓ e o₁ ℓ₁ e₁ o₂ ℓ₂ e₂ o₃ ℓ₃ e₃}
      → {O : Category o  ℓ  e }
      → {A : Category o₁ ℓ₁ e₁}
      → {B : Category o₂ ℓ₂ e₂}
      → {C : Category o₃ ℓ₃ e₃}
      → (T : Functor A C) (S : Functor O (Functors B C)) -> Functor O (Categories _ _ _)
CommaF {O = O} {A} {B} {C} T S = record
 { F₀ = λ o → Comma T (S.F₀ o)
 ; F₁ = λ {o₁} {o₂} f → record
   { F₀ = λ { (a Comma., b , g) → a Comma., b , (S₁.η f b C.∘ g) }
   ; F₁ = λ { {a₁ Comma., b₁ , g₁} {a₂ Comma., b₂ , g₂} (g Comma., h [ comm ]) →
              g Comma., h [ begin S₀.F₁ o₂ h C.∘ S₁.η f b₁ C.∘ g₁
                                    ↓⟨ C.Equiv.sym C.assoc ⟩
                                  (S₀.F₁ o₂ h C.∘ S₁.η f b₁) C.∘ g₁
                                    ↓⟨ C.∘-resp-≡ˡ (C.Equiv.sym (S₁.commute f h)) ⟩
                                  (S₁.η f b₂ C.∘ S₀.F₁ o₁ h) C.∘ g₁
                                    ↓⟨ C.assoc ⟩
                                  S₁.η f b₂ C.∘ S₀.F₁ o₁ h C.∘ g₁
                                    ↓⟨ C.∘-resp-≡ʳ comm ⟩
                                  S₁.η f b₂ C.∘ g₂ C.∘ T.F₁ g
                                    ↓⟨ C.Equiv.sym C.assoc ⟩
                                  (S₁.η f b₂ C.∘ g₂) C.∘ T.F₁ g
                                    ∎
                          ]};
                          identity = TODO;
                          homomorphism = TODO;
                          F-resp-≡ = TODO }
 ; identity = TODO
 ; homomorphism = TODO
 ; F-resp-≡ = TODO
 }
  where
   module C = Category C
   module T = Functor T
   module S = Functor S
   module S₀ o = Functor (S.F₀ o)
   module S₁ {a b} f = NaturalTransformation (S.F₁ {a} {b} f)
   postulate TODO : ∀ {l} {A : Set l} -> A
   open C.HomReasoning

ext: agda

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


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

module Algebra.Construct.Free.Semilattice.Union where

open import Prelude
open import Path.Reasoning
open import Algebra

open import Algebra.Construct.Free.Semilattice.Definition
open import Algebra.Construct.Free.Semilattice.Eliminators

infixr 5 _∪_
_∪_ : 𝒦 A → 𝒦 A → 𝒦 A
_∪_ = λ xs ys → [ union′ ys ]↓ xs
  where
  union′ : 𝒦 A → A ↘ 𝒦 A
  [ union′ ys ]-set = trunc
  [ union′ ys ] x ∷ xs = x ∷ xs
  [ union′ ys ][] = ys
  [ union′ ys ]-dup = dup
  [ union′ ys ]-com = com

∪-assoc : (xs ys zs : 𝒦 A) → (xs ∪ ys) ∪ zs ≡ xs ∪ (ys ∪ zs)
∪-assoc = λ xs ys zs → ∥ ∪-assoc′ ys zs ∥⇓ xs
  where
  ∪-assoc′ : (ys zs : 𝒦 A) → xs ∈𝒦 A ⇒∥ (xs ∪ ys) ∪ zs ≡ xs ∪ (ys ∪ zs) ∥
  ∥ ∪-assoc′ ys zs ∥-prop = trunc _ _
  ∥ ∪-assoc′ ys zs ∥[] = refl
  ∥ ∪-assoc′ ys zs ∥ x ∷ xs ⟨ Pxs ⟩ = cong (x ∷_) Pxs

∪-identityʳ : (xs : 𝒦 A) → xs ∪ [] ≡ xs
∪-identityʳ = ∥ ∪-identityʳ′ ∥⇓
  where
  ∪-identityʳ′ : xs ∈𝒦 A ⇒∥ xs ∪ [] ≡ xs ∥
  ∥ ∪-identityʳ′ ∥-prop = trunc _ _
  ∥ ∪-identityʳ′ ∥[] = refl
  ∥ ∪-identityʳ′ ∥ x ∷ xs ⟨ Pxs ⟩ = cong (x ∷_) Pxs

cons-distrib-∪ : (x : A) (xs ys : 𝒦 A) → x ∷ xs ∪ ys ≡ xs ∪ (x ∷ ys)
cons-distrib-∪ = λ x xs ys → ∥ cons-distrib-∪′ x ys ∥⇓ xs
  where
  cons-distrib-∪′ : (x : A) (ys : 𝒦 A) → xs ∈𝒦 A ⇒∥ x ∷ xs ∪ ys ≡ xs ∪ (x ∷ ys) ∥
  ∥ cons-distrib-∪′ x ys ∥-prop = trunc _ _
  ∥ cons-distrib-∪′ x ys ∥[] = refl
  ∥ cons-distrib-∪′ x ys ∥ z ∷ xs ⟨ Pxs ⟩ =
    x ∷ ((z ∷ xs) ∪ ys) ≡⟨⟩
    x ∷ z ∷ (xs ∪ ys) ≡⟨ com x z (xs ∪ ys) ⟩
    z ∷ x ∷ (xs ∪ ys) ≡⟨ cong (z ∷_) Pxs ⟩
    ((z ∷ xs) ∪ (x ∷ ys)) ∎

∪-comm : (xs ys : 𝒦 A) → xs ∪ ys ≡ ys ∪ xs
∪-comm = λ xs ys → ∥ ∪-comm′ ys ∥⇓ xs
  where
  ∪-comm′ : (ys : 𝒦 A) → xs ∈𝒦 A ⇒∥ xs ∪ ys ≡ ys ∪ xs ∥
  ∥ ∪-comm′ ys ∥-prop = trunc _ _
  ∥ ∪-comm′ ys ∥[] = sym (∪-identityʳ ys)
  ∥ ∪-comm′ ys ∥ x ∷ xs ⟨ Pxs ⟩ =
    (x ∷ xs) ∪ ys ≡⟨⟩
    x ∷ (xs ∪ ys) ≡⟨ cong (x ∷_) Pxs ⟩
    x ∷ (ys ∪ xs) ≡⟨⟩
    (x ∷ ys) ∪ xs ≡⟨ cons-distrib-∪ x ys xs ⟩
    ys ∪ (x ∷ xs) ∎

∪-idem : (xs : 𝒦 A) → xs ∪ xs ≡ xs
∪-idem = ∥ ∪-idem′ ∥⇓
  where
  ∪-idem′ : xs ∈𝒦 A ⇒∥ xs ∪ xs ≡ xs ∥
  ∥ ∪-idem′ ∥-prop = trunc _ _
  ∥ ∪-idem′ ∥[] = refl
  ∥ ∪-idem′ ∥ x ∷ xs ⟨ Pxs ⟩ =
    ((x ∷ xs) ∪ (x ∷ xs)) ≡˘⟨ cons-distrib-∪ x (x ∷ xs) xs ⟩
    x ∷ x ∷ (xs ∪ xs) ≡⟨ dup x (xs ∪ xs) ⟩
    x ∷ (xs ∪ xs) ≡⟨ cong (x ∷_) Pxs ⟩
    x ∷ xs ∎

module _ {a} {A : Type a} where
  open Semilattice
  open CommutativeMonoid
  open Monoid
  𝒦-semilattice : Semilattice a
  𝒦-semilattice .commutativeMonoid .monoid .𝑆 = 𝒦 A
  𝒦-semilattice .commutativeMonoid .monoid ._∙_ = _∪_
  𝒦-semilattice .commutativeMonoid .monoid .ε = []
  𝒦-semilattice .commutativeMonoid .monoid .assoc = ∪-assoc
  𝒦-semilattice .commutativeMonoid .monoid .ε∙ _ = refl
  𝒦-semilattice .commutativeMonoid .monoid .∙ε = ∪-identityʳ
  𝒦-semilattice .commutativeMonoid .comm = ∪-comm
  𝒦-semilattice .idem = ∪-idem

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
module Properties.Contradiction where

data ⊥ : Set where

¬ : Set → Set
¬ A = A → ⊥

CONTRADICTION : ∀ {A : Set} → ⊥ → A
CONTRADICTION ()

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


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

module container.core where

open import level
open import sum
open import equality
open import function

module _ {li}{I : Set li} where
  -- homsets in the slice category
  _→ⁱ_ : ∀ {lx ly} → (I → Set lx) → (I → Set ly) → Set _
  X →ⁱ Y = (i : I) → X i → Y i

  -- identity of the slice category
  idⁱ : ∀ {lx}{X : I → Set lx} → X →ⁱ X
  idⁱ i x = x

  -- composition in the slice category
  _∘ⁱ_ : ∀ {lx ly lz} {X : I → Set lx}{Y : I → Set ly}{Z : I → Set lz}
       → (Y →ⁱ Z) → (X →ⁱ Y) → (X →ⁱ Z)
  (f ∘ⁱ g) i = f i ∘ g i
  infixl 9 _∘ⁱ_

  -- extensionality
  funext-isoⁱ : ∀ {lx ly} {X : I → Set lx}{Y : (i : I) → X i → Set ly}
              → {f g : (i : I)(x : X i) → Y i x}
              → (∀ i x → f i x ≡ g i x)
              ≅ (f ≡ g)
  funext-isoⁱ {f = f}{g = g}
    = (Π-ap-iso refl≅ λ i → strong-funext-iso)
    ·≅ strong-funext-iso

  funext-invⁱ : ∀ {lx ly} {X : I → Set lx}{Y : (i : I) → X i → Set ly}
              → {f g : (i : I)(x : X i) → Y i x}
              → f ≡ g → ∀ i x → f i x ≡ g i x
  funext-invⁱ = invert funext-isoⁱ

  funextⁱ : ∀ {lx ly} {X : I → Set lx}{Y : (i : I) → X i → Set ly}
          → {f g : (i : I)(x : X i) → Y i x}
          → (∀ i x → f i x ≡ g i x) → f ≡ g
  funextⁱ = apply funext-isoⁱ

-- Definition 1 in Ahrens, Capriotti and Spadotti (arXiv:1504.02949v1 [cs.LO])
record Container (li la lb : Level) : Set (lsuc (li ⊔ la ⊔ lb)) where
  constructor container
  field
    I : Set li
    A : I → Set la
    B : {i : I} → A i → Set lb
    r : {i : I}{a : A i} → B a → I

  -- Definition 2 in Ahrens, Capriotti and Spadotti (arXiv:1504.02949v1 [cs.LO])
  -- functor associated to this indexed container
  F : ∀ {lx} → (I → Set lx) → I → Set _
  F X i = Σ (A i) λ a → (b : B a) → X (r b)

  F-ap-iso : ∀ {lx ly}{X : I → Set lx}{Y : I → Set ly}
           → (∀ i → X i ≅ Y i)
           → ∀ i → F X i ≅ F Y i
  F-ap-iso isom i = Σ-ap-iso refl≅ λ a
                  → Π-ap-iso refl≅ λ b
                  → isom (r b)

  -- morphism map for the functor F
  imap : ∀ {lx ly}
       → {X : I → Set lx}
       → {Y : I → Set ly}
       → (X →ⁱ Y)
       → (F X →ⁱ F Y)
  imap g i (a , f) = a , λ b → g (r b) (f b)

  -- action of a functor on homotopies
  hmap : ∀ {lx ly}
       → {X : I → Set lx}
       → {Y : I → Set ly}
       → {f g : X →ⁱ Y}
       → (∀ i x → f i x ≡ g i x)
       → (∀ i x → imap f i x ≡ imap g i x)
  hmap p i (a , u) = ap (_,_ a) (funext (λ b → p (r b) (u b)))

  hmap-id : ∀ {lx ly}
          → {X : I → Set lx}
          → {Y : I → Set ly}
          → (f : X →ⁱ Y)
          → ∀ i x
          → hmap (λ i x → refl {x = f i x}) i x ≡ refl
  hmap-id f i (a , u) = ap (ap (_,_ a)) (funext-id _)

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


text:
-- TODO: Move these to stuff related to metric spaces

module Continuity where
  open Limit

  -- Statement that the point x of function f is a continous point
  ContinuousPoint : (ℝ → ℝ) → ℝ → Stmt
  ContinuousPoint f(x) = (⦃ limit : Lim f(x) ⦄ → (lim f(x)⦃ limit ⦄ ≡ f(x)))

  -- Statement that the function f is continous
  Continuous : (ℝ → ℝ) → Stmt
  Continuous f = ∀{x} → ContinuousPoint f(x)

module Proofs where
  -- instance postulate DifferentiablePoint-to-ContinuousPoint : ∀{f}{x}{diff} → ⦃ _ : DifferentiablePoint f(x)⦃ diff ⦄ ⦄ → ContinuousPoint f(x)
  -- instance postulate Differentiable-to-Continuous : ∀{f}{diff} → ⦃ _ : Differentiable(f)⦃ diff ⦄ ⦄ → Continuous(f)

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:
-- Andreas, 2021-08-17, issue #5508, reported by james-smith-69781
-- On a case-insensitive file system, an inconsistency slipped into
-- the ModuleToSource map, leading to a failure in getting the module
-- name from the file name, in turn leading to a crash for certain errors.

module Issue5508 where -- case variant intended!

-- WAS: Crash in termination error

A : Set
A = A

record R : Set2 where
  field f : Set1

record S : Set2 where
  field g : Set1

record T : Set2 where
  field g : Set1

open S
open T
-- Now, g is ambiguous.

-- WAS: crash in "Cannot eliminate ... with projection" error

test : R
test .g = Set

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

------------------------------------------------------------------------------
open import LibraBFT.Base.Types
import      LibraBFT.Impl.Consensus.BlockStorage.BlockStore      as BlockStore
import      LibraBFT.Impl.Consensus.BlockStorage.SyncManager     as SyncManager
import      LibraBFT.Impl.Consensus.ConsensusTypes.ExecutedBlock as ExecutedBlock
import      LibraBFT.Impl.Consensus.ConsensusTypes.SyncInfo      as SyncInfo
import      LibraBFT.Impl.Consensus.ConsensusTypes.Vote          as Vote
import      LibraBFT.Impl.Consensus.Liveness.ProposerElection    as ProposerElection
import      LibraBFT.Impl.Consensus.Liveness.ProposalGenerator   as ProposalGenerator
import      LibraBFT.Impl.Consensus.Liveness.RoundState          as RoundState
import      LibraBFT.Impl.Consensus.PersistentLivenessStorage    as PersistentLivenessStorage
import      LibraBFT.Impl.Consensus.SafetyRules.SafetyRules      as SafetyRules
open import LibraBFT.Impl.OBM.Logging.Logging
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Interface.Output
open import LibraBFT.ImplShared.Util.Crypto
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import LibraBFT.Abstract.Types.EpochConfig UID NodeId
open import Optics.All
open import Util.ByteString
open import Util.Hash
import      Util.KVMap                                           as Map
open import Util.PKCS
open import Util.Prelude
-----------------------------------------------------------------------------
open import Data.String                                          using (String)
------------------------------------------------------------------------------

module LibraBFT.Impl.Consensus.RoundManager where

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

processCertificatesM : Instant → LBFT Unit

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

processCommitM : LedgerInfoWithSignatures → LBFT (List ExecutedBlock)
processCommitM finalityProof = pure []

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

generateProposalM
  : Instant → NewRoundEvent
  → LBFT (Either ErrLog ProposalMsg)

processNewRoundEventM : Instant → NewRoundEvent → LBFT Unit
processNewRoundEventM now nre@(NewRoundEvent∙new r _ _) = do
  logInfo fakeInfo   -- (InfoNewRoundEvent nre)
  use (lRoundManager ∙ pgAuthor) >>= λ where
    nothing       → logErr fakeErr -- (here ["lRoundManager.pgAuthor", "Nothing"])
    (just author) → do
      v ← ProposerElection.isValidProposer <$> use lProposerElection <*> pure author <*> pure r
      whenD v $ do
        rcvrs ← use (lRoundManager ∙ rmObmAllAuthors)
        generateProposalM now nre >>= λ where
          -- (Left (ErrEpochEndedNoProposals t)) -> logInfoL (lEC.|.lPM) (here ("EpochEnded":t))
          (Left e)            → logErr (withErrCtx (here' ("Error generating proposal" ∷ [])) e)
          (Right proposalMsg) → act (BroadcastProposal proposalMsg rcvrs)
 where
  here' : List String → List String
  here' t = "RoundManager" ∷ "processNewRoundEventM" ∷ t

abstract
  processNewRoundEventM-abs = processNewRoundEventM
  processNewRoundEventM-abs-≡ : processNewRoundEventM-abs ≡ processNewRoundEventM
  processNewRoundEventM-abs-≡ = refl

generateProposalM now newRoundEvent =
  ProposalGenerator.generateProposalM now (newRoundEvent ^∙ nreRound) ∙?∙ λ proposal →
  SafetyRules.signProposalM proposal ∙?∙ λ signedProposal →
  Right ∘ ProposalMsg∙new signedProposal <$> BlockStore.syncInfoM

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

ensureRoundAndSyncUpM : Instant → Round    → SyncInfo → Author → Bool → LBFT (Either ErrLog Bool)
processProposalM      : Block                                         → LBFT Unit
executeAndVoteM       : Block                                         → LBFT (Either ErrLog Vote)

-- external entry point
-- TODO-2: The sync info that the peer requests if it discovers that its round
-- state is behind the sender's should be sent as an additional argument, for now.
module processProposalMsgM (now : Instant) (pm : ProposalMsg) where
  step₀ : LBFT Unit
  step₁ : Author → LBFT Unit
  step₂ : Either ErrLog Bool → LBFT Unit

  step₀ =
    caseMD pm ^∙ pmProposer of λ where
      nothing → logInfo fakeInfo -- proposal with no author
      (just pAuthor) → step₁ pAuthor

  step₁ pAuthor =
        ensureRoundAndSyncUpM now (pm ^∙ pmProposal ∙ bRound) (pm ^∙ pmSyncInfo)
                              pAuthor true >>= step₂

  step₂ =
        λ where
          (Left e)      → logErr e
          (Right true)  → processProposalM (pm ^∙ pmProposal)
          (Right false) → do
            currentRound ← use (lRoundState ∙ rsCurrentRound)
            logInfo fakeInfo -- dropping proposal for old round

abstract
  processProposalMsgM = processProposalMsgM.step₀

  processProposalMsgM≡ : processProposalMsgM ≡ processProposalMsgM.step₀
  processProposalMsgM≡ = refl

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

module syncUpM (now : Instant) (syncInfo : SyncInfo) (author : Author) (_helpRemote : Bool) where
  step₀       :                                LBFT (Either ErrLog Unit)
  step₁ step₂ : SyncInfo                     → LBFT (Either ErrLog Unit)
  step₃ step₄ : SyncInfo → ValidatorVerifier → LBFT (Either ErrLog Unit)

  here' : List String → List String

  step₀ = do
    -- logEE (here' []) $ do
    localSyncInfo ← BlockStore.syncInfoM
    -- TODO helpRemote
    step₁ localSyncInfo

  step₁ localSyncInfo = do
    ifD SyncInfo.hasNewerCertificates syncInfo localSyncInfo
      then step₂ localSyncInfo
      else ok unit

  step₂ localSyncInfo = do
        vv ← use (lRoundManager ∙ rmEpochState ∙ esVerifier)
        SyncInfo.verifyM syncInfo vv ∙^∙ withErrCtx (here' []) ∙?∙ λ _ → step₃ localSyncInfo vv

  step₃ localSyncInfo vv =
          SyncManager.addCertsM {- reason -} syncInfo (BlockRetriever∙new now author) ∙^∙ withErrCtx (here' [])
            ∙?∙ λ _ → step₄ localSyncInfo vv

  step₄ localSyncInfo vv = do
            processCertificatesM now
            ok unit

  here' t = "RoundManager" ∷ "syncUpM" ∷ t

syncUpM : Instant → SyncInfo → Author → Bool → LBFT (Either ErrLog Unit)
syncUpM = syncUpM.step₀

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

module ensureRoundAndSyncUpM
  (now : Instant) (messageRound : Round) (syncInfo : SyncInfo) (author : Author) (helpRemote : Bool) where
  step₀ : LBFT (Either ErrLog Bool)
  step₁ : LBFT (Either ErrLog Bool)
  step₂ : LBFT (Either ErrLog Bool)

  step₀ = do
    currentRound ← use (lRoundState ∙ rsCurrentRound)
    ifD messageRound <? currentRound
      then ok false
      else step₁

  step₁ =
        syncUpM now syncInfo author helpRemote ∙?∙ λ _ → step₂

  step₂ = do
          currentRound' ← use (lRoundState ∙ rsCurrentRound)
          ifD messageRound /= currentRound'
            then bail fakeErr -- error: after sync, round does not match local
            else ok true

ensureRoundAndSyncUpM = ensureRoundAndSyncUpM.step₀

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

-- In Haskell, RoundManager.processSyncInfoMsgM is NEVER called.
--
-- When processing other messaging (i.e., Proposal and Vote) the first thing that happens,
-- before handling the specific message, is that ensureRoundAndSyncUpM is called to deal
-- with the SyncInfo message in the ProposalMsg or VoteMsg.
-- If a SyncInfo message ever did arrive by itself, all that would happen is that the
-- SyncInfo would be handled by ensureRoundAndSyncUpM (just like other messages).
-- And nothing else (except ensureRoundAndSyncUpM might do "catching up")
--
-- The only place the Haskell implementation uses SyncInfo only messages it during EpochChange.
-- And, in that case, the SyncInfo message is handled in the EpochManager, not here.

processSyncInfoMsgM : Instant → SyncInfo → Author → LBFT Unit
processSyncInfoMsgM now syncInfo peer =
  -- logEE (lEC.|.lSI) (here []) $
  ensureRoundAndSyncUpM now (syncInfo ^∙ siHighestRound + 1) syncInfo peer false >>= λ where
    (Left  e) → logErr (withErrCtx (here' []) e)
    (Right _) → pure unit
 where
  here' : List String → List String
  here' t = "RoundManager" ∷ "processSyncInfoMsgM" ∷ {- lsA peer ∷ lsSI syncInfo ∷ -} t

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

-- external entry point
processLocalTimeoutM : Instant → Epoch → Round → LBFT Unit
processLocalTimeoutM now obmEpoch round = do
  -- logEE lTO (here []) $
  ifMD (RoundState.processLocalTimeoutM now obmEpoch round) continue1 (pure unit)
 where
  here'     : List String → List String
  continue2 : LBFT Unit
  continue3 : (Bool × Vote) → LBFT Unit
  continue4 : Vote → LBFT Unit

  continue1 =
    ifMD (use (lRoundManager ∙ rmSyncOnly))
      -- In Haskell, rmSyncOnly is ALWAYS false.
      -- It is used for an unimplemented "sync only" mode for nodes.
      -- "sync only" mode is an optimization for nodes catching up.
      (do si    ← BlockStore.syncInfoM
          rcvrs ← use (lRoundManager ∙ rmObmAllAuthors)
          act (BroadcastSyncInfo si rcvrs))
      continue2

  continue2 =
    use (lRoundState ∙ rsVoteSent) >>= λ where
      (just vote) →
        ifD (vote ^∙ vVoteData ∙ vdProposed ∙ biRound == round)
          -- already voted in this round, so resend the vote, but with a timeout signature
          then continue3 (true , vote)
          else local-continue2-continue
      _ → local-continue2-continue
   where
    local-continue2-continue : LBFT Unit
    local-continue2-continue =
          -- have not voted in this round, so create and vote on NIL block with timeout signature
          ProposalGenerator.generateNilBlockM round >>= λ where
            (Left         e) → logErr e
            (Right nilBlock) →
              executeAndVoteM nilBlock >>= λ where
                (Left        e) → logErr e
                (Right nilVote) → continue3 (false , nilVote)

  continue3 (useLastVote , timeoutVote) = do
    proposer ← ProposerElection.getValidProposer <$> use lProposerElection <*> pure round
    logInfo fakeInfo
             -- (here [ if useLastVote then "already executed and voted, will send timeout vote"
             --                        else "generate nil timeout vote"
             --       , "expected proposer", lsA proposer ])
    if not (Vote.isTimeout timeoutVote)
      then
        (SafetyRules.signTimeoutM (Vote.timeout timeoutVote) >>= λ where
          (Left  e) → logErr    (withErrCtx (here' []) e)
          (Right s) → continue4 (Vote.addTimeoutSignature timeoutVote s)) -- makes it a timeout vote
      else
        continue4 timeoutVote

  continue4 timeoutVote = do
    RoundState.recordVoteM timeoutVote
    timeoutVoteMsg ← VoteMsg∙new timeoutVote <$> BlockStore.syncInfoM
    rcvrs          ← use (lRoundManager ∙ rmObmAllAuthors)
    -- IMPL-DIFF this is BroadcastVote in Haskell (an alias)
    act (SendVote timeoutVoteMsg rcvrs)

  here' t = "RoundManager" ∷ "processLocalTimeoutM" ∷ {-lsE obmEpoch:lsR round-} t

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

processCertificatesM now = do
  syncInfo ← BlockStore.syncInfoM
  maybeSMP-RWS (RoundState.processCertificatesM now syncInfo) unit (processNewRoundEventM now)

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

-- This function is broken into smaller pieces to aid in the verification
-- effort. The style of indentation used is to make side-by-side reading of the
-- Haskell prototype and Agda model easier.
module processProposalM (proposal : Block) where
  step₀ : LBFT Unit
  step₁ : BlockStore → (Either ObmNotValidProposerReason Unit) → LBFT Unit
  step₂ : Either ErrLog Vote → LBFT Unit
  step₃ : Vote → SyncInfo → LBFT Unit

  step₀ = do
    bs ← use lBlockStore
    vp ← ProposerElection.isValidProposalM proposal
    step₁ bs vp

  step₁ bs vp =
    ifD‖ isLeft vp ≔
         logErr fakeErr -- proposer for block is not valid for this round
       ‖ is-nothing (BlockStore.getQuorumCertForBlock (proposal ^∙ bParentId) bs) ≔
         logErr fakeErr -- QC of parent is not in BS
       ‖ not (maybeS (BlockStore.getBlock (proposal ^∙ bParentId) bs) false
              λ parentBlock →
                ⌊ parentBlock ^∙ ebRound <?ℕ proposal ^∙ bRound ⌋) ≔
         logErr fakeErr -- parentBlock < proposalRound
       ‖ otherwise≔ do
           executeAndVoteM proposal >>= step₂

  step₂ =  λ where
             (Left e)     → logErr e
             (Right vote) → do
               RoundState.recordVoteM vote
               si ← BlockStore.syncInfoM
               step₃ vote si

  step₃ vote si = do
               recipient ← ProposerElection.getValidProposer
                           <$> use lProposerElection
                           <*> pure (proposal ^∙ bRound + 1)
               act (SendVote (VoteMsg∙new vote si) (recipient ∷ []))
               -- TODO-2:                           mkNodesInOrder1 recipient

processProposalM = processProposalM.step₀

------------------------------------------------------------------------------
module executeAndVoteM (b : Block) where
  step₀ :                 LBFT (Either ErrLog Vote)
  step₁ : ExecutedBlock → LBFT (Either ErrLog Vote)
  step₂ : ExecutedBlock → LBFT (Either ErrLog Vote)
  step₃ : Vote          → LBFT (Either ErrLog Vote)

  step₀ =
    BlockStore.executeAndInsertBlockM b ∙^∙ withErrCtx ("" ∷ []) ∙?∙ step₁

  step₁ eb = do
    cr ← use (lRoundState ∙ rsCurrentRound)
    vs ← use (lRoundState ∙ rsVoteSent)
    so ← use (lRoundManager ∙ rmSyncOnly)
    ifD‖ is-just vs ≔
         bail fakeErr -- error: already voted this round
       ‖ so ≔
         bail fakeErr -- error: sync-only set
       ‖ otherwise≔ step₂ eb

  step₂ eb = do
           let maybeSignedVoteProposal' = ExecutedBlock.maybeSignedVoteProposal eb
           SafetyRules.constructAndSignVoteM maybeSignedVoteProposal' {- ∙^∙ logging -}
             ∙?∙ step₃

  step₃ vote =   PersistentLivenessStorage.saveVoteM vote
             ∙?∙ λ _ → ok vote

executeAndVoteM = executeAndVoteM.step₀

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

processVoteM     : Instant → Vote                → LBFT Unit
addVoteM         : Instant → Vote                → LBFT Unit
newQcAggregatedM : Instant → QuorumCert → Author → LBFT Unit
newTcAggregatedM : Instant → TimeoutCertificate  → LBFT Unit

processVoteMsgM : Instant → VoteMsg → LBFT Unit
processVoteMsgM now voteMsg = do
  -- TODO ensureRoundAndSyncUp
  processVoteM now (voteMsg ^∙ vmVote)

processVoteM now vote =
  ifD not (Vote.isTimeout vote)
  then (do
    let nextRound = vote ^∙ vVoteData ∙ vdProposed ∙ biRound + 1
    use (lRoundManager ∙ pgAuthor) >>= λ where
      nothing       → logErr fakeErr -- "lRoundManager.pgAuthor", "Nothing"
      (just author) → do
        v ← ProposerElection.isValidProposer <$> use lProposerElection
                                             <*> pure author <*> pure nextRound
        if v then continue else logErr fakeErr) -- "received vote, but I am not proposer for round"
  else
    continue
 where
  continue : LBFT Unit
  continue = do
    let blockId = vote ^∙ vVoteData ∙ vdProposed ∙ biId
    bs ← use lBlockStore
    ifD (is-just (BlockStore.getQuorumCertForBlock blockId bs))
      then logInfo fakeInfo -- "block already has QC", "dropping unneeded vote"
      else do
      logInfo fakeInfo -- "before"
      addVoteM now vote
      pvA ← use lPendingVotes
      logInfo fakeInfo -- "after"

addVoteM now vote = do
  bs ← use lBlockStore
  maybeSD (bs ^∙ bsHighestTimeoutCert) continue λ tc →
    ifD vote ^∙ vRound == tc ^∙ tcRound
      then logInfo fakeInfo -- "block already has TC", "dropping unneeded vote"
      else continue
 where
  continue : LBFT Unit
  continue = do
    verifier ← use (rmEpochState ∙ esVerifier)
    r ← RoundState.insertVoteM vote verifier
    case r of λ where
      (NewQuorumCertificate qc) →
        newQcAggregatedM now qc (vote ^∙ vAuthor)
      (NewTimeoutCertificate tc) →
        newTcAggregatedM now tc
      _ →
        pure unit

newQcAggregatedM now qc a =
  SyncManager.insertQuorumCertM qc (BlockRetriever∙new now a) >>= λ where
    (Left e)     → logErr e
    (Right unit) → processCertificatesM now

newTcAggregatedM now tc =
  BlockStore.insertTimeoutCertificateM tc >>= λ where
    (Left e)     → logErr e
    (Right unit) → processCertificatesM now

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

-- TODO-1 PROVE IT TERMINATES
{-# TERMINATING #-}
mkRsp : BlockRetrievalRequest → (Author × Epoch × Round) → BlockStore → List Block → HashValue
      → BlockRetrievalResponse

-- external entry point
processBlockRetrievalRequestM : Instant → BlockRetrievalRequest → LBFT Unit
processBlockRetrievalRequestM _now request = do
  -- logEE lSI (here []) $ do
  use (lRoundManager ∙ rmObmMe) >>= λ where
    nothing → logErr fakeErr -- should not happen
    (just me) → continue me
 where

  continue : Author → LBFT Unit
  continue me = do
    e  ← use (lRoundManager ∙ rmSafetyRules ∙ srPersistentStorage ∙ pssSafetyData ∙ sdEpoch)
    r  ← use (lRoundManager ∙ rmRoundState ∙ rsCurrentRound)
    let meer = (me , e , r)
    bs ← use lBlockStore
    act (SendBRP (request ^∙ brqObmFrom) (mkRsp request meer bs [] (request ^∙ brqBlockId)))

mkRsp request meer bs blocks id =
    if-dec length blocks <? request ^∙ brqNumBlocks
    then
      (case BlockStore.getBlock id bs of λ where
        (just executedBlock) → mkRsp request meer bs (blocks ++ (executedBlock ^∙ ebBlock ∷ []))
                                                     (executedBlock ^∙ ebParentId)
        nothing → BlockRetrievalResponse∙new meer
                    (if null blocks then BRSIdNotFound else BRSNotEnoughBlocks)
                    blocks)
    else BlockRetrievalResponse∙new meer BRSSucceeded blocks

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

module start
  (now : Instant)
  (lastVoteSent : Maybe Vote)
  where

  step₁ step₁-abs : SyncInfo → LBFT Unit
  step₂ step₂-abs : Maybe NewRoundEvent → LBFT Unit
  step₃ step₄ step₃-abs step₄-abs : NewRoundEvent → LBFT Unit

  step₀ : LBFT Unit
  step₀ = do
    syncInfo ← BlockStore.syncInfoM
    step₁-abs syncInfo

  step₁ syncInfo = do
    RoundState.processCertificatesM-abs now syncInfo >>= step₂-abs

  here' : List String → List String
  here' t = "RoundManager" ∷ "start" ∷ t

  step₂ = λ where
      nothing    →
        logErr fakeErr -- (here' ["Cannot jump start a round_state from existing certificates."]))
      (just nre) → step₃-abs nre

  step₃ nre = do
        maybeSMP (pure lastVoteSent) unit RoundState.recordVoteM
        step₄-abs nre

  step₄ nre = processNewRoundEventM-abs now nre -- error!("[RoundManager] Error during start: {:?}", e);

  abstract
    step₁-abs = step₁
    step₁-abs-≡ : step₁-abs ≡ step₁
    step₁-abs-≡ = refl

    step₂-abs = step₂
    step₂-abs-≡ : step₂-abs ≡ step₂
    step₂-abs-≡ = refl

    step₃-abs = step₃
    step₃-abs-≡ : step₃-abs ≡ step₃
    step₃-abs-≡ = refl

    step₄-abs = step₄
    step₄-abs-≡ : step₄-abs ≡ step₄
    step₄-abs-≡ = refl

abstract
  start-abs = start.step₀
  start-abs-≡ : start-abs ≡ start.step₀
  start-abs-≡ = refl


text:
module Introduction.Universes where

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

postulate IsEven : Nat -> Prop

data Even : Set where
  even : (n : Nat) -> IsEven n -> Even

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Nat.Unary where

open import Data.Sum
open import Function
open import Nat.Class
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

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

ind : (P : ℕ₁ → Set) → P zero → (∀ {k} → P k → P (succ k)) → ∀ n → P n
ind P z s zero = z
ind P z s (succ n) = ind (P ∘ succ) (s z) (λ {k} → s {succ k}) n

ind′ : (P : ℕ₁ → Set) → P zero → (∀ {k} → P k → P (succ k)) → ∀ n → P n
ind′ P z s zero = z
ind′ P z s (succ n) = s (ind′ P z s n)

rec : {A : Set} → A → (A → A) → ℕ₁ → A
rec {A} z s n = ind (const A) z (λ {_} → s) n

rec-succ : ∀ {A} z (s : A → A) n → rec (s z) s n ≡ s (rec z s n)
rec-succ z s zero = refl
rec-succ z s (succ n) =
  begin
    rec (s z) s (succ n)
  ≡⟨⟩
    rec (s (s z)) s n
  ≡⟨ rec-succ (s z) s n ⟩
    s (rec (s z) s n)
  ≡⟨⟩
    s (rec z s (succ n))
  ∎

data _<_ : ℕ₁ → ℕ₁ → Set where
  z<s : ∀ {n} → zero < succ n
  s<s : ∀ {m n} → m < n → succ m < succ n

n<sn : ∀ {n} → n < succ n
n<sn {zero} = z<s
n<sn {succ n} = s<s n<sn

tighten : ∀ {m n} → m < succ n → m < n ⊎ m ≡ n
tighten {zero} {zero} z<s = inj₂ refl
tighten {zero} {succ n′} z<s = inj₁ z<s
tighten {succ m′} {succ n′} (s<s m′<sn′) with tighten m′<sn′
tighten {succ m′} {succ n′} (s<s m′<sn′) | inj₁ m′<n′ = inj₁ (s<s m′<n′)
tighten {succ m′} {succ n′} (s<s m′<sn′) | inj₂ m′≡n′ = inj₂ (cong succ m′≡n′)

SIndHyp : (ℕ₁ → Set) → ℕ₁ → Set
SIndHyp P n = ∀ {m} → m < n → P m

sind : (P : ℕ₁ → Set) → (∀ {k} → SIndHyp P k → P k) → ∀ n → P n
sind P h n = prf (succ n) {n} n<sn
  where
    lem : {p : ℕ₁} (hp : SIndHyp P p) → SIndHyp P (succ p)
    lem hp m<sp with tighten m<sp
    lem hp m<sp | inj₁ m<p = hp m<p
    lem hp m<sp | inj₂ refl = h hp

    prf : ∀ n → SIndHyp P n
    prf = ind (SIndHyp P) (λ ()) lem

_+_ : ℕ₁ → ℕ₁ → ℕ₁
m + n = rec n succ m

+-zero : ∀ {n} → zero + n ≡ n
+-zero = refl

+-succ : ∀ {m n} → succ m + n ≡ m + succ n
+-succ = refl

instance
  Nat-ℕ₁ : Nat ℕ₁
  Nat-ℕ₁ = record
    { zero = zero
    ; succ = succ
    ; ind = ind
    ; _+_ = _+_
    ; +-zero = +-zero
    ; +-succ = λ {m n} → +-succ {m} {n}
    }

max_stars_repo_name: iblech/agda-quotients

max_issues_repo_name: iblech/agda-quotients

max_forks_repo_name: iblech/agda-quotients


text:
module Relation.Ternary.Separation.Monad.Delay where

open import Level
open import Function
open import Function using (_∘_; case_of_)
open import Relation.Binary.PropositionalEquality
open import Relation.Unary
open import Relation.Unary.PredicateTransformer hiding (_⊔_)
open import Relation.Ternary.Separation
open import Relation.Ternary.Separation.Monad
open import Relation.Ternary.Separation.Morphisms

open import Codata.Delay as D using (now; later) public
open import Data.Unit
open Monads

module _ {ℓ}
  {C : Set ℓ} {u}
  {{r : RawSep C}}
  {{us : IsUnitalSep r u}}
 where

  Delay : ∀ {ℓ} i → Pt C ℓ
  Delay i P c = D.Delay (P c) i

  instance
    delay-monad : ∀ {i} → Monad ⊤ ℓ (λ _ _ → Delay i)
    Monad.return delay-monad px = D.now px
    app (Monad.bind delay-monad f) ►px σ = D.bind ►px λ px → app f px σ


text:
module Cats.Trans where

open import Level using (_⊔_)

open import Cats.Category.Base
open import Cats.Functor using (Functor)

open Functor

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

  infixr 9 _∘_

  private
    module C = Category C
    module D = Category D
    open D.≈-Reasoning

  record Trans (F G : Functor C D) : Set (lo ⊔ la ⊔ la′ ⊔ l≈′) where
    field
      component : (c : C.Obj) → fobj F c D.⇒ fobj G c
      natural : ∀ {c d} {f : c C.⇒ d}
        → component d D.∘ fmap F f D.≈ fmap G f D.∘ component c

  open Trans public

  id : ∀ {F} → Trans F F
  id {F} = record
      { component = λ _ → D.id
      ; natural = D.≈.trans D.id-l (D.≈.sym D.id-r)
      }

  _∘_ : ∀ {F G H} → Trans G H → Trans F G → Trans F H
  _∘_ {F} {G} {H} θ ι = record
      { component = λ c → component θ c D.∘ component ι c
      ; natural = λ {c} {d} {f} →
          begin
            (component θ d D.∘ component ι d) D.∘ fmap F f
          ≈⟨ D.assoc ⟩
            component θ d D.∘ component ι d D.∘ fmap F f
          ≈⟨ D.∘-resp-r (natural ι) ⟩
            component θ d D.∘ fmap G f D.∘ component ι c
          ≈⟨ D.unassoc ⟩
            (component θ d D.∘ fmap G f) D.∘ component ι c
          ≈⟨ D.∘-resp-l (natural θ)  ⟩
            (fmap H f D.∘ component θ c) D.∘ component ι c
          ≈⟨ D.assoc ⟩
            fmap H f D.∘ component θ c D.∘ component ι 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:
module IID-New-Proof-Setup where

open import LF
open import Identity
open import IID
open import IIDr
open import DefinitionalEquality

OPg : Set -> Set1
OPg I = OP I I

-- Encoding indexed inductive types as non-indexed types.
ε : {I : Set}(γ : OPg I) -> OPr I
ε (ι i)     j = σ (i == j) (\_ -> ι ★)
ε (σ A γ)   j = σ A (\a -> ε (γ a) j)
ε (δ H i γ) j = δ H i (ε γ j)

-- Adds a reflexivity proof.
g→rArgs : {I : Set}(γ : OPg I)(U : I -> Set)
	      (a : Args γ U) ->
	      rArgs (ε γ) U (index γ U a)
g→rArgs (ι e)     U arg	= (refl , ★)
g→rArgs (σ A γ)   U arg = (π₀ arg , g→rArgs (γ (π₀ arg)) U (π₁ arg))
g→rArgs (δ H i γ) U arg = (π₀ arg , g→rArgs γ U (π₁ arg))

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Data.Collection.Equivalence where

open import Data.Collection.Core

open import Function using (id; _∘_)
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence using (_⇔_; equivalence)
open Function.Equivalence.Equivalence
open import Relation.Binary.PropositionalEquality

open import Level using (zero)

open import Relation.Nullary
open import Relation.Unary
open import Relation.Binary

nach : ∀ {f t} {A : Set f} {B : Set t} → (A ⇔ B) → A → B
nach = _⟨$⟩_ ∘ to

von : ∀ {f t} {A : Set f} {B : Set t} → (A ⇔ B) → B → A
von = _⟨$⟩_ ∘ from

infixr 5 _≋_

_≋_ : Rel Membership _
A ≋ B = {x : Element} → x ∈ A ⇔ x ∈ B

≋-Reflexive : Reflexive _≋_
≋-Reflexive = equivalence id id

≋-Symmetric : Symmetric _≋_
≋-Symmetric z = record
    { to   = from z
    ; from = to z
    }

≋-Transitive : Transitive _≋_
≋-Transitive P≋Q Q≋R = equivalence (nach Q≋R ∘ nach P≋Q) (von P≋Q ∘ von Q≋R)

≋-IsEquivalence : IsEquivalence _≋_
≋-IsEquivalence = record
    { refl = equivalence id id
    ; sym = ≋-Symmetric
    ; trans = ≋-Transitive
    }

≋-Setoid : Setoid _ _
≋-Setoid = record
    { Carrier = Pred Element zero
    ; _≈_ = _≋_
    ; isEquivalence = ≋-IsEquivalence
    }

--------------------------------------------------------------------------------
--  Conditional Equivalence
--------------------------------------------------------------------------------

_≋[_]_ : ∀ {a} → Membership → Pred Element a → Membership → Set a
A ≋[ P ] B = {x : Element} → P x → x ∈ A ⇔ x ∈ B

-- prefix version of _≋[_]_, with the predicate being the first argument
[_]≋ : ∀ {a} → Pred Element a → Membership → Membership → Set a
[_]≋ P A B = A ≋[ P ] B

≋[]-Reflexive : ∀ {a} {P : Pred Element a} → Reflexive [ P ]≋
≋[]-Reflexive A = equivalence id id

≋[]-Symmetric : ∀ {a} {P : Pred Element a} → Symmetric [ P ]≋
≋[]-Symmetric z ∈P = record
    { to = from (z ∈P)
    ; from = to (z ∈P)
    }

≋[]-Transitive : ∀ {a} {P : Pred Element a} → Transitive [ P ]≋
≋[]-Transitive P≋Q Q≋R ∈P = equivalence (nach (Q≋R ∈P) ∘ nach (P≋Q ∈P)) (von (P≋Q ∈P) ∘ von (Q≋R ∈P))

≋[]-IsEquivalence : ∀ {a} {P : Pred Element a} → IsEquivalence [ P ]≋
≋[]-IsEquivalence {p} = record
    { refl = λ _ → equivalence id id
    ; sym = ≋[]-Symmetric
    ; trans = ≋[]-Transitive
    }

max_stars_repo_name: banacorn/lambda-calculus

max_issues_repo_name: banacorn/lambda-calculus

max_forks_repo_name: banacorn/lambda-calculus


text:
{-# OPTIONS --universe-polymorphism #-}

-- Free category generated by a directed graph.
-- The graph is given by a type (Obj) of nodes and a (Obj × Obj)-indexed
-- Setoid of (directed) edges.  Every inhabitant of the node type is
-- considered to be a (distinct) node of the graph, and (equivalence
-- classes of) inhabitants of the edge type (for a given pair of
-- nodes) are considered edges of the graph.
module Categories.Free.Core where

open import Categories.Category
open import Categories.Functor
  using (Functor)
open import Categories.Support.Equivalence
open import Graphs.Graph
open import Graphs.GraphMorphism
open import Relation.Binary
  using (module IsEquivalence)
open import Relation.Binary.PropositionalEquality
  using ()
  renaming (_≡_ to _≣_; refl to ≣-refl)
open import Data.Star
open import Categories.Support.StarEquality
open import Data.Star.Properties
  using (gmap-◅◅)
open import Level using (_⊔_)

EdgeSetoid : ∀ {o ℓ e} → (G : Graph o ℓ e) (A B : Graph.Obj G) → Setoid ℓ e
EdgeSetoid G A B = Graph.edge-setoid G {A}{B}

module PathEquality {o ℓ e} (G : Graph o ℓ e) = StarEquality (EdgeSetoid G)

Free₀ : ∀ {o ℓ e} → Graph o ℓ e → Category o (o ⊔ ℓ) (o ⊔ ℓ ⊔ e)
Free₀ {o}{ℓ}{e} G = record
  { Obj       = Obj
  ; _⇒_       = Star _↝_
  ; id        = ε
  ; _∘_       = _▻▻_
  ; _≡_       = _≡_
  ; equiv     = equiv
  ; assoc     = λ{A}{B}{C}{D} {f}{g}{h} → ▻▻-assoc {A}{B}{C}{D} f g h
  ; identityˡ = IsEquivalence.reflexive equiv f◅◅ε≣f
  ; identityʳ = IsEquivalence.reflexive equiv ≣-refl
  ; ∘-resp-≡  = _▻▻-cong_
  }
  where
    open Graph G
      hiding (equiv)

    open PathEquality G
      renaming (_≈_ to _≡_; isEquivalence to equiv)

    f◅◅ε≣f : ∀ {A B}{f : Star _↝_ A B} -> (f ◅◅ ε) ≣ f
    f◅◅ε≣f {f = ε} = ≣-refl
    f◅◅ε≣f {f = x ◅ xs} rewrite f◅◅ε≣f {f = xs}  = ≣-refl

Free₁ : ∀ {o₁ ℓ₁ e₁ o₂ ℓ₂ e₂}
  {A : Graph o₁ ℓ₁ e₁}
  {B : Graph o₂ ℓ₂ e₂}
  → GraphMorphism A B → Functor (Free₀ A) (Free₀ B)
Free₁ {o₁}{ℓ₁}{e₁}{o₂}{ℓ₂}{e₂}{A}{B} G = record
  { F₀            = G₀
  ; F₁            = gmap G₀ G₁
  ; identity      = refl
  ; homomorphism  = λ {X}{Y}{Z}{f}{g} → homomorphism {X}{Y}{Z}{f}{g}
  ; F-resp-≡      = F-resp-≡
  }
  where
    open GraphMorphism G
      renaming (F₀ to G₀; F₁ to G₁; F-resp-≈ to G-resp-≈)
    open Category.Equiv (Free₀ B)

    .homomorphism : ∀ {X Y Z}
      {f : Free₀ A [ X , Y ]}
      {g : Free₀ A [ Y , Z ]}
      → Free₀ B [ gmap G₀ G₁ (f ◅◅ g) ≡ gmap G₀ G₁ f ◅◅ gmap G₀ G₁ g ]
    homomorphism {f = f}{g} = reflexive (gmap-◅◅ G₀ G₁ f g)

    .F-resp-≡ : ∀ {X Y}
        {f g : Free₀ A [ X , Y ]}
        → Free₀ A [ f ≡ g ]
        → Free₀ B [ gmap G₀ G₁ f ≡ gmap G₀ G₁ g ]
    F-resp-≡ {X}{Y}{f}{g} f≡g
      = gmap-cong G₀ G₁ G₁ (λ x y x≈y → G-resp-≈ x≈y) f g f≡g
      where
        open StarCong₂ (EdgeSetoid A) (EdgeSetoid B)


text:
-- 2010-10-06 Andreas

module TerminationRecordPatternListAppend where

data Empty : Set where

record Unit : Set where
  constructor unit

data Bool : Set where
  true false : Bool

T : Bool -> Set
T true = Unit
T false = Empty

-- Thorsten suggests on the Agda list  thread "Coinductive families"
-- to encode lists as records
record List (A : Set) : Set where
  constructor list
  field
    isCons : Bool
    head   : T isCons -> A
    tail   : T isCons -> List A

open List public

-- if the record constructor list was counted as structural increase
-- Thorsten's function would not be rejected
append : {A : Set} -> List A -> List A -> List A
append (list true  h t) l' = list true h (\ _ -> append (t _) l')
append (list false _ _) l' = l'

-- but translating away the record pattern produces something
-- that is in any case rejected by the termination checker
append1 : {A : Set} -> List A -> List A -> List A
append1 l l' = append1' l l' (isCons l)
  where append1' : {A : Set} -> List A -> List A -> Bool -> List A
        append1' l l' true  = list true (head l) (\ _ -> append (tail l) l')
        append1' l l' false = l'
-- NEED inspect!

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda