text:
open import MLib.Algebra.PropertyCode
open import MLib.Algebra.PropertyCode.Structures
  using (bimonoidCode; BimonoidK; +; *; 0#; 1#)

module MLib.Algebra.Operations {c ℓ} (struct : Struct bimonoidCode c ℓ) where

open import MLib.Prelude
open import Data.Fin.Permutation as Perm using (Permutation; Permutation′; _⟨$⟩ʳ_; _⟨$⟩ˡ_)
import Data.Fin.Permutation.Components as PC

open Struct struct
open EqReasoning setoid

--------------------------------------------------------------------------------
--  Nicer names for operations
--------------------------------------------------------------------------------

infixl 5 _+′_
infixl 6 _*′_

_+′_ = ⟦ + ⟧
_*′_ = ⟦ * ⟧
0′ = ⟦ 0# ⟧
1′ = ⟦ 1# ⟧

--------------------------------------------------------------------------------
--  Table stuff
--------------------------------------------------------------------------------

module _ {n} where
  open Setoid (Table.setoid setoid n) public
    using ()
    renaming (_≈_ to _≋_)

_≋′_ : ∀ {m n} → Table Carrier m → Table Carrier n → Set ℓ
_≋′_ = Table.Pointwise′ _≈_

open Table using (head; tail; rearrange; fromList; toList; _≗_; select)

--------------------------------------------------------------------------------
--  Operations
--------------------------------------------------------------------------------

sumₜ : ∀ {n} → Table Carrier n → Carrier
sumₜ = Table.foldr _+′_ 0′

sumₗ : List Carrier → Carrier
sumₗ = List.foldr _+′_ 0′

-- An alternative mathematical-style syntax for sumₜ

infixl 10 sumₜ-syntax

sumₜ-syntax : ∀ n → (Fin n → Carrier) → Carrier
sumₜ-syntax _ = sumₜ ∘ Table.tabulate

syntax sumₜ-syntax n (λ i → x) = ∑[ i < n ] x

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

-- When summing over a function from a finite set, we can pull out any value and move it to the front.
sumₜ-punchIn :
  ⦃ props : Has (associative on + ∷ commutative on + ∷ []) ⦄ →
  ∀ {n} t (i : Fin (suc n)) → sumₜ t ≈ lookup t i +′ sumₜ (Table.rearrange (Fin.punchIn i) t)
sumₜ-punchIn f zero = refl
sumₜ-punchIn {zero} t (suc ())
sumₜ-punchIn ⦃ props ⦄ {suc n} t (suc i) =
  let x = head t
      y = lookup t (suc i)
      z = sumₜ (rearrange (Fin.punchIn i) (tail t))
  in begin
    x +′ sumₜ (tail t)  ≈⟨ cong + refl (sumₜ-punchIn (tail t) i) ⟩
    x +′ (y +′ z)       ≈⟨ sym (from props (associative on +) _ _ _) ⟩
    (x +′ y) +′ z       ≈⟨ cong + (from props (commutative on +) _ _) refl ⟩
    (y +′ x) +′ z       ≈⟨ from props (associative on +) _ _ _ ⟩
    y +′ (x +′ z)       ∎

-- '_≈_' is a congruence over 'sumTable n'.
sumₜ-cong : ∀ {n} {t t′ : Table Carrier n} → t ≋ t′ → sumₜ t ≈ sumₜ t′
sumₜ-cong = Table.foldr-cong setoid (cong +)

-- A version of 'sumₜ-cong' with heterogeneous table sizes
sumₜ-cong′ : ∀ {m n} {t : Table Carrier m} {t′ : Table Carrier n} → t ≋′ t′ → sumₜ t ≈ sumₜ t′
sumₜ-cong′ {m} (≡.refl , q) = sumₜ-cong λ i → q i i ≅.refl

-- '_≡_' is a congruence over 'sum n'.
sumₜ-cong≡ : ∀ {n} {t t′ : Table Carrier n} → t ≗ t′ → sumₜ t ≡ sumₜ t′
sumₜ-cong≡ = Table.foldr-cong (≡.setoid Carrier) (≡.cong₂ _+′_)

-- The sum over the constantly zero function is zero.
sumₜ-zero :
  ⦃ props : Has₁ (0# is leftIdentity for +) ⦄ →
  ∀ n → sumₜ (Table.replicate {n} 0′) ≈ 0′
sumₜ-zero zero = refl
sumₜ-zero ⦃ props ⦄ (suc n) =
  begin
    0′ +′ sumₜ (Table.replicate {n} 0′)  ≈⟨ from props (0# is leftIdentity for +) _ ⟩
    sumₜ (Table.replicate {n} 0′)        ≈⟨ sumₜ-zero n ⟩
    0′                                   ∎

-- The '∑' operator distributes over addition.
∑-+′-hom :
  ⦃ props : Has (0# is leftIdentity for + ∷ associative on + ∷ commutative on + ∷ []) ⦄ →
  ∀ n (f g : Fin n → Carrier) → ∑[ i < n ] f i +′ ∑[ i < n ] g i ≈ ∑[ i < n ] (f i +′ g i)
∑-+′-hom ⦃ props ⦄ zero f g = from props (0# is leftIdentity for +) _
∑-+′-hom ⦃ props ⦄ (suc n) f g =
  let fz = f zero
      gz = g zero
      ∑f  = ∑[ i < n ] f (suc i)
      ∑g  = ∑[ i < n ] g (suc i)
      ∑fg = ∑[ i < n ] (f (suc i) +′ g (suc i))
  in begin
    (fz +′ ∑f) +′ (gz +′ ∑g)      ≈⟨ from props (associative on +) _ _ _ ⟩
    fz +′ (∑f +′ (gz +′ ∑g))      ≈⟨ cong + refl (sym (from props (associative on +) _ _ _)) ⟩
    fz +′ ((∑f +′ gz) +′ ∑g)      ≈⟨ cong + refl (cong + (from props (commutative on +) _ _) refl) ⟩
    fz +′ ((gz +′ ∑f) +′ ∑g)      ≈⟨ cong + refl (from props (associative on +) _ _ _) ⟩
    fz +′ (gz +′ (∑f +′ ∑g))      ≈⟨ cong + refl (cong + refl (∑-+′-hom n _ _)) ⟩
    fz +′ (gz +′ ∑fg)             ≈⟨ sym (from props (associative on +) _ _ _) ⟩
    fz +′ gz +′ ∑fg               ∎

-- The '∑' operator commutes with itself.
∑-comm :
  ⦃ props : Has (0# is leftIdentity for + ∷ associative on + ∷ commutative on + ∷ []) ⦄ →
  ∀ n m (f : Fin n → Fin m → Carrier) → ∑[ i < n ] ∑[ j < m ] f i j ≈ ∑[ j < m ] ∑[ i < n ] f i j
∑-comm ⦃ props ⦄ zero m f = sym (sumₜ-zero ⦃ weaken props ⦄ m)
∑-comm (suc n) m f =
  begin
    ∑[ j < m ] f zero j +′ ∑[ i < n ] ∑[ j < m ] f (suc i) j   ≈⟨ cong + refl (∑-comm n m _) ⟩
    ∑[ j < m ] f zero j +′ ∑[ j < m ] ∑[ i < n ] f (suc i) j   ≈⟨ ∑-+′-hom m _ _ ⟩
    ∑[ j < m ] (f zero j +′ ∑[ i < n ] f (suc i) j)            ∎

module _ ⦃ props : Has (associative on + ∷ commutative on + ∷ []) ⦄ where
  open Fin using (punchIn)
  -- Any permutation of a table has the same sum as the original.

  sumₜ-permute : ∀ {n} t (π : Permutation′ n) → sumₜ t ≈ sumₜ (rearrange (π ⟨$⟩ʳ_) t)
  sumₜ-permute {zero} t π = refl
  sumₜ-permute {suc n} t π =
    let f = lookup t
    in
    begin
      sumₜ t                                                                       ≡⟨⟩
      f 0i +′ sumₜ (rearrange (punchIn 0i) t)                                      ≈⟨ cong + refl (sumₜ-permute _ (Perm.remove (π ⟨$⟩ˡ 0i) π)) ⟩
      f 0i +′ sumₜ (rearrange (punchIn 0i ∘ (Perm.remove (π ⟨$⟩ˡ 0i) π ⟨$⟩ʳ_)) t)  ≡⟨ ≡.cong₂ _+′_ ≡.refl (sumₜ-cong≡ (≡.cong f ∘ ≡.sym ∘ Perm.punchIn-permute′ π 0i)) ⟩
      f 0i +′ sumₜ (rearrange ((π ⟨$⟩ʳ_) ∘ punchIn (π ⟨$⟩ˡ 0i)) t)                 ≡⟨ ≡.cong₂ _+′_ (≡.cong f (≡.sym (Perm.inverseʳ π))) ≡.refl ⟩
      f _  +′ sumₜ (rearrange ((π ⟨$⟩ʳ_) ∘ punchIn (π ⟨$⟩ˡ 0i)) t)                 ≈⟨ sym (sumₜ-punchIn (rearrange (π ⟨$⟩ʳ_) t) (π ⟨$⟩ˡ 0i)) ⟩
      sumₜ (rearrange (π ⟨$⟩ʳ_) t)                                                 ∎
    where
      0i = zero
      ππ0 = π ⟨$⟩ʳ (π ⟨$⟩ˡ 0i)

  -- A version of 'sumₜ-permute' allowing heterogeneous sum lengths.

  sumₜ-permute′ : ∀ {m n} t (π : Permutation m n) → sumₜ t ≈ sumₜ (rearrange (π ⟨$⟩ʳ_) t)
  sumₜ-permute′ t π with Perm.↔⇒≡ π
  sumₜ-permute′ t π | ≡.refl = sumₜ-permute t π

  ∑-permute : ∀ {n} (f : Fin n → Carrier) (π : Permutation′ n) → ∑[ i < n ] f i ≈ ∑[ i < n ] f (π ⟨$⟩ʳ i)
  ∑-permute = sumₜ-permute ∘ tabulate

  ∑-permute′ : ∀ {m n} (f : Fin n → Carrier) (π : Permutation m n) → ∑[ i < n ] f i ≈ ∑[ i < m ] f (π ⟨$⟩ʳ i)
  ∑-permute′ = sumₜ-permute′ ∘ tabulate

private
  ⌊i≟i⌋ : ∀ {n} (i : Fin n) → (i Fin.≟ i) ≡ yes ≡.refl
  ⌊i≟i⌋ i with i Fin.≟ i
  ⌊i≟i⌋ i | yes ≡.refl = ≡.refl
  ⌊i≟i⌋ i | no ¬p = ⊥-elim (¬p ≡.refl)

-- If the function takes the same value at 'i' and 'j', then swapping 'i' and
-- 'j' then selecting 'j' is the same as selecting 'i'.

select-transpose : ∀ {n} t (i j : Fin n) → lookup t i ≈ lookup t j → ∀ k → (lookup (select 0′ j t) ∘ PC.transpose i j) k ≈ lookup (select 0′ i t) k
select-transpose _ i j e k with k Fin.≟ i
select-transpose _ i j e k | yes p rewrite ≡.≡-≟-identity Fin._≟_ {j} ≡.refl = sym e
select-transpose _ i j e k | no ¬p with k Fin.≟ j
select-transpose _ i j e k | no ¬p | yes q rewrite proj₂ (≡.≢-≟-identity Fin._≟_ (¬p ∘ ≡.trans q ∘ ≡.sym)) = refl
select-transpose _ i j e k | no ¬p | no ¬q rewrite proj₂ (≡.≢-≟-identity Fin._≟_ ¬q) = refl

-- Summing over a pulse gives you the single value picked out by the pulse.

select-sum :
  ⦃ props : Has (0# is leftIdentity for + ∷ 0# is rightIdentity for + ∷ associative on + ∷ commutative on + ∷ []) ⦄ →
  ∀ {n i} (t : Table Carrier n) → sumₜ (Table.select 0′ i t) ≈ lookup t i
select-sum {zero} {()} t
select-sum ⦃ props ⦄ {suc n} {i} t =
  let f = lookup t
      open Table using (select; rearrange; replicate)
      open PC using (transpose)
  in
  begin
    sumₜ (select 0′ i t)                                                  ≈⟨ sumₜ-permute ⦃ weaken props ⦄ (select 0′ i t) (Perm.transpose zero i) ⟩
    sumₜ (rearrange (transpose zero i) (select 0′ i t))                   ≡⟨ sumₜ-cong≡ (Table.select-const 0′ i t ∘ transpose zero i) ⟩
    sumₜ (rearrange (transpose zero i) (select 0′ i (replicate (f i))))   ≈⟨ sumₜ-cong (select-transpose (replicate (f i)) zero i refl) ⟩
    sumₜ (select 0′ zero (replicate {suc n} (f i)))                       ≡⟨⟩
    f i +′ sumₜ (replicate {n} 0′)                                        ≈⟨ cong + refl (sumₜ-zero ⦃ weaken props ⦄ n) ⟩
    f i +′ 0′                                                             ≈⟨ from props (0# is rightIdentity for +) _ ⟩
    f i                                                                   ∎

sumₜ-fromList : ∀ xs → sumₜ (Table.fromList xs) ≡ sumₗ xs
sumₜ-fromList [] = ≡.refl
sumₜ-fromList (x ∷ xs) = ≡.cong₂ _+′_ ≡.refl (sumₜ-fromList xs)

sumₜ-toList : ∀ {n} (t : Table Carrier n) → sumₜ t ≡ sumₗ (Table.toList t)
sumₜ-toList {zero} _ = ≡.refl
sumₜ-toList {suc n} _ = ≡.cong₂ _+′_ ≡.refl (sumₜ-toList {n} _)

sumDistribˡ :
  ⦃ props : Has (0# is rightZero for * ∷ * ⟨ distributesOverˡ ⟩ₚ + ∷ []) ⦄ →
  ∀ {n} x (t : Table Carrier n) → x *′ sumₜ t ≈ ∑[ i < n ] (x *′ lookup t i)
sumDistribˡ ⦃ props ⦄ {Nat.zero} x f = from props (0# is rightZero for *) x
sumDistribˡ ⦃ props ⦄ {Nat.suc n} x t =
  begin
    x *′ (head t +′ sumₜ (tail t))                                    ≈⟨ from props (* ⟨ distributesOverˡ ⟩ₚ +) _ _ _ ⟩
    (x *′ head t) +′ (x *′ sumₜ (tail t))                             ≈⟨ cong + refl (sumDistribˡ x (tail t)) ⟩
    (x *′ head t) +′ sumₜ (tabulate (λ i → x *′ lookup (tail t) i))   ∎

sumDistribʳ :
  ⦃ props : Has (0# is leftZero for * ∷ * ⟨ distributesOverʳ ⟩ₚ + ∷ []) ⦄ →
  ∀ {n} x (t : Table Carrier n) → sumₜ t *′ x ≈ ∑[ i < n ] (lookup t i *′ x)
sumDistribʳ ⦃ props ⦄ {Nat.zero} x t = from props (0# is leftZero for *) x
sumDistribʳ ⦃ props ⦄ {Nat.suc n} x t =
  begin
    (head t +′ sumₜ (tail t)) *′ x                                    ≈⟨ from props (* ⟨ distributesOverʳ ⟩ₚ +) _ _ _ ⟩
    (head t *′ x) +′ (sumₜ (tail t) *′ x)                             ≈⟨ cong + refl (sumDistribʳ x (tail t)) ⟩
    (head t *′ x) +′ sumₜ (tabulate (λ i → lookup (tail t) i *′ x))   ∎


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed binary relations
------------------------------------------------------------------------

-- The contents of this module should be accessed via
-- `Relation.Binary.Indexed.Heterogeneous`.

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

open import Relation.Binary.Indexed.Heterogeneous.Core

module Relation.Binary.Indexed.Heterogeneous.Structures
  {i a ℓ} {I : Set i} (A : I → Set a) (_≈_ : IRel A ℓ)
  where

open import Function.Base
open import Level using (suc; _⊔_)
open import Relation.Binary using (_⇒_)
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
open import Relation.Binary.Indexed.Heterogeneous.Definitions

------------------------------------------------------------------------
-- Equivalences

record IsIndexedEquivalence : Set (i ⊔ a ⊔ ℓ) where
  field
    refl  : Reflexive  A _≈_
    sym   : Symmetric  A _≈_
    trans : Transitive A _≈_

  reflexive : ∀ {i} → _≡_ ⟨ _⇒_ ⟩ _≈_ {i}
  reflexive P.refl = refl

record IsIndexedPreorder {ℓ₂} (_∼_ : IRel A ℓ₂) : Set (i ⊔ a ⊔ ℓ ⊔ ℓ₂) where
  field
    isEquivalence : IsIndexedEquivalence
    reflexive     : ∀ {i j} → (_≈_ {i} {j}) ⟨ _⇒_ ⟩ _∼_
    trans         : Transitive A _∼_

  module Eq = IsIndexedEquivalence isEquivalence

  refl : Reflexive A _∼_
  refl = reflexive Eq.refl

ext: agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}

-- The Category of Elements

open import Cubical.Categories.Category

module Cubical.Categories.Constructions.Elements {ℓ ℓ'} {C : Precategory ℓ ℓ'} where

open import Cubical.Categories.Instances.Sets
open import Cubical.Categories.Functor
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma

import Cubical.Categories.Morphism as Morphism
import Cubical.Categories.Constructions.Slice as Slice

-- some issues
-- * always need to specify objects during composition because can't infer isSet
open Precategory
open Functor

getIsSet : ∀ {ℓS} {C : Precategory ℓ ℓ'} (F : Functor C (SET ℓS)) → (c : C .ob) → isSet (fst (F ⟅ c ⟆))
getIsSet F c = snd (F ⟅ c ⟆)

infix 50 ∫_
∫_ : ∀ {ℓS} → Functor C (SET ℓS) → Precategory (ℓ-max ℓ ℓS) (ℓ-max ℓ' ℓS)
-- objects are (c , x) pairs where c ∈ C and x ∈ F c
(∫ F) .ob = Σ[ c ∈ C .ob ] fst (F ⟅ c ⟆)
-- morphisms are f : c → c' which take x to x'
(∫ F) .Hom[_,_] (c , x) (c' , x')  = Σ[ f ∈ C [ c , c' ] ] x' ≡ (F ⟪ f ⟫) x
(∫ F) .id (c , x) = C .id c , sym (funExt⁻ (F .F-id) x ∙ refl)
(∫ F) ._⋆_ {c , x} {c₁ , x₁} {c₂ , x₂} (f , p) (g , q)
  = (f ⋆⟨ C ⟩ g) , (x₂
            ≡⟨ q ⟩
              (F ⟪ g ⟫) x₁         -- basically expanding out function composition
            ≡⟨ cong (F ⟪ g ⟫) p ⟩
              (F ⟪ g ⟫) ((F ⟪ f ⟫) x)
            ≡⟨ funExt⁻ (sym (F .F-seq _ _)) _ ⟩
              (F ⟪ f ⋆⟨ C ⟩ g ⟫) x
            ∎)
(∫ F) .⋆IdL o@{c , x} o1@{c' , x'} f'@(f , p) i
  = (cIdL i) , isOfHLevel→isOfHLevelDep 1 (λ a → isS' x' ((F ⟪ a ⟫) x)) p' p cIdL i
    where
      isS = getIsSet F c
      isS' = getIsSet F c'
      cIdL = C .⋆IdL f

      -- proof from composition with id
      p' : x' ≡ (F ⟪ C .id c ⋆⟨ C ⟩ f ⟫) x
      p' = snd ((∫ F) ._⋆_ ((∫ F) .id o) f')
(∫ F) .⋆IdR o@{c , x} o1@{c' , x'} f'@(f , p) i
    = (cIdR i) , isOfHLevel→isOfHLevelDep 1 (λ a → isS' x' ((F ⟪ a ⟫) x)) p' p cIdR i
      where
        cIdR = C .⋆IdR f
        isS' = getIsSet F c'

        p' : x' ≡ (F ⟪ f ⋆⟨ C ⟩ C .id c' ⟫) x
        p' = snd ((∫ F) ._⋆_ f' ((∫ F) .id o1))
(∫ F) .⋆Assoc o@{c , x} o1@{c₁ , x₁} o2@{c₂ , x₂} o3@{c₃ , x₃} f'@(f , p) g'@(g , q) h'@(h , r) i
  = (cAssoc i) , isOfHLevel→isOfHLevelDep 1 (λ a → isS₃ x₃ ((F ⟪ a ⟫) x)) p1 p2 cAssoc i
    where
      cAssoc = C .⋆Assoc f g h
      isS₃ = getIsSet F c₃

      p1 : x₃ ≡ (F ⟪ (f ⋆⟨ C ⟩ g) ⋆⟨ C ⟩ h ⟫) x
      p1 = snd ((∫ F) ._⋆_ ((∫ F) ._⋆_ {o} {o1} {o2} f' g') h')

      p2 : x₃ ≡ (F ⟪ f ⋆⟨ C ⟩ (g ⋆⟨ C ⟩ h) ⟫) x
      p2 = snd ((∫ F) ._⋆_ f' ((∫ F) ._⋆_ {o1} {o2} {o3} g' h'))

-- same thing but for presheaves
∫ᴾ_ : ∀ {ℓS} → Functor (C ^op) (SET ℓS) → Precategory (ℓ-max ℓ ℓS) (ℓ-max ℓ' ℓS)
-- objects are (c , x) pairs where c ∈ C and x ∈ F c
(∫ᴾ F) .ob = Σ[ c ∈ C .ob ] fst (F ⟅ c ⟆)
-- morphisms are f : c → c' which take x to x'
(∫ᴾ F) .Hom[_,_] (c , x) (c' , x')  = Σ[ f ∈ C [ c , c' ] ] x ≡ (F ⟪ f ⟫) x'
(∫ᴾ F) .id (c , x) = C .id c , sym (funExt⁻ (F .F-id) x ∙ refl)
(∫ᴾ F) ._⋆_ {c , x} {c₁ , x₁} {c₂ , x₂} (f , p) (g , q)
  = (f ⋆⟨ C ⟩ g) , (x
            ≡⟨ p ⟩
              (F ⟪ f ⟫) x₁         -- basically expanding out function composition
            ≡⟨ cong (F ⟪ f ⟫) q ⟩
              (F ⟪ f ⟫) ((F ⟪ g ⟫) x₂)
            ≡⟨ funExt⁻ (sym (F .F-seq _ _)) _ ⟩
              (F ⟪ f ⋆⟨ C ⟩ g ⟫) x₂
            ∎)
(∫ᴾ F) .⋆IdL o@{c , x} o1@{c' , x'} f'@(f , p) i
  = (cIdL i) , isOfHLevel→isOfHLevelDep 1 (λ a → isS x ((F ⟪ a ⟫) x')) p' p cIdL i
    where
      isS = getIsSet F c
      isS' = getIsSet F c'
      cIdL = C .⋆IdL f

      -- proof from composition with id
      p' : x ≡ (F ⟪ C .id c ⋆⟨ C ⟩ f ⟫) x'
      p' = snd ((∫ᴾ F) ._⋆_ ((∫ᴾ F) .id o) f')
(∫ᴾ F) .⋆IdR o@{c , x} o1@{c' , x'} f'@(f , p) i
    = (cIdR i) , isOfHLevel→isOfHLevelDep 1 (λ a → isS x ((F ⟪ a ⟫) x')) p' p cIdR i
      where
        cIdR = C .⋆IdR f
        isS = getIsSet F c

        p' : x ≡ (F ⟪ f ⋆⟨ C ⟩ C .id c' ⟫) x'
        p' = snd ((∫ᴾ F) ._⋆_ f' ((∫ᴾ F) .id o1))
(∫ᴾ F) .⋆Assoc o@{c , x} o1@{c₁ , x₁} o2@{c₂ , x₂} o3@{c₃ , x₃} f'@(f , p) g'@(g , q) h'@(h , r) i
  = (cAssoc i) , isOfHLevel→isOfHLevelDep 1 (λ a → isS x ((F ⟪ a ⟫) x₃)) p1 p2 cAssoc i
    where
      cAssoc = C .⋆Assoc f g h
      isS = getIsSet F c

      p1 : x ≡ (F ⟪ (f ⋆⟨ C ⟩ g) ⋆⟨ C ⟩ h ⟫) x₃
      p1 = snd ((∫ᴾ F) ._⋆_ ((∫ᴾ F) ._⋆_ {o} {o1} {o2} f' g') h')

      p2 : x ≡ (F ⟪ f ⋆⟨ C ⟩ (g ⋆⟨ C ⟩ h) ⟫) x₃
      p2 = snd ((∫ᴾ F) ._⋆_ f' ((∫ᴾ F) ._⋆_ {o1} {o2} {o3} g' h'))

-- helpful results

module _ {ℓS} {F : Functor (C ^op) (SET ℓS)} where

  -- morphisms are equal as long as the morphisms in C are equals
  ∫ᴾhomEq : ∀ {o1 o1' o2 o2'} (f : (∫ᴾ F) [ o1 , o2 ]) (g : (∫ᴾ F) [ o1' , o2' ])
          → (p : o1 ≡ o1') (q : o2 ≡ o2')
          → (eqInC : PathP (λ i → C [ fst (p i) , fst (q i) ]) (fst f) (fst g))
          → PathP (λ i → (∫ᴾ F) [ p i , q i ]) f g
  ∫ᴾhomEq (f , eqf) (g , eqg) p q eqInC
    = ΣPathP (eqInC
              , isOfHLevel→isOfHLevelDep 1 {A = Σ[ (o1 , o2) ∈ (∫ᴾ F) .ob × (∫ᴾ F) .ob ] (C [ fst o1 , fst o2 ])}
                                          {B = λ ((o1 , o2) , f) → snd o1 ≡ (F ⟪ f ⟫) (snd o2)}
                                          (λ ((o1 , o2) , f) → snd (F ⟅ (fst o1) ⟆) (snd o1) ((F ⟪ f ⟫) (snd o2)))
                                          eqf
                                          eqg
                                          λ i → ((p i , q i) , eqInC i))

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
module Data.QuadTree.FoldableProofs.FoldableFunctorProof where

open import Haskell.Prelude renaming (zero to Z; suc to S)
open import Data.Logic
open import Data.QuadTree.Implementation.Definition
open import Data.QuadTree.Implementation.ValidTypes
open import Data.QuadTree.Implementation.QuadrantLenses
open import Data.QuadTree.Implementation.SafeFunctions
open import Data.QuadTree.Implementation.PropDepthRelation
open import Data.QuadTree.Implementation.Foldable
open import Data.QuadTree.Implementation.Functors
open import Data.QuadTree.FoldableProofs.FoldableProof
open import Data.QuadTree.FunctorProofs.Valid-QuadrantFunctor

proof-foldfmap-list : {t s : Set} {{monT : Monoid t}} {{monS : Monoid s}} -> (l : List t )
    -> (f : t -> s)
    -> foldMap f l ≡ foldMap id (fmap f l)
proof-foldfmap-list [] f = refl
proof-foldfmap-list (x ∷ xs) f =
    begin
        f x <> foldMap f xs
    =⟨ cong (_<>_ (f x)) (proof-foldfmap-list xs f) ⟩
        f x <> foldMap id (fmap f xs)
    end

fmap-replicate : {A B : Set} -> (f : A -> B) -> (v : A) -> (n : Nat)
    -> fmap f (replicateₙ n v) ≡ replicateₙ n (f v)
fmap-replicate f v Z = refl
fmap-replicate f v (S n) = cong (λ z → f v ∷ z) (fmap-replicate f v n)

fmap-concat : {A B : Set} -> (f : A -> B) -> (l1 l2 : List A)
    -> fmap f (l1 ++ l2) ≡ fmap f l1 ++ fmap f l2
fmap-concat f [] l2 = refl
fmap-concat f (x ∷ l1) l2 = cong (λ z → f x ∷ z) (fmap-concat f l1 l2)

fmap-concat4 : {A B : Set} -> (f : A -> B) -> (l1 l2 l3 l4 : List A)
    -> fmap f (l1 ++ l2 ++ l3 ++ l4) ≡ fmap f l1 ++ fmap f l2 ++ fmap f l3 ++ fmap f l4
fmap-concat4 f l1 l2 l3 l4 =
    begin
        fmap f (l1 ++ l2 ++ l3 ++ l4)
    =⟨ fmap-concat f l1 (l2 ++ l3 ++ l4) ⟩
        fmap f l1 ++ fmap f (l2 ++ l3 ++ l4)
    =⟨ cong (_++_ (map f l1)) (fmap-concat f l2 (l3 ++ l4)) ⟩
        fmap f l1 ++ fmap f l2 ++ fmap f (l3 ++ l4)
    =⟨ cong (λ z → map f l1 ++ map f l2 ++ z) (fmap-concat f l3 l4) ⟩
        fmap f l1 ++ fmap f l2 ++ fmap f l3 ++ fmap f l4
    end

fmap-expand : {A B : Set} {{eqA : Eq A}} {{eqB : Eq B}} -> (f : A -> B) -> (t : Tile A)
    -> fmap f (expand t) ≡ expand (fmap f t)
fmap-expand f t@(TileC v (RegionC (x1 , y1) (x2 , y2))) = fmap-replicate f v (diff x2 x1 * diff y2 y1)

fmap-concat-expand : {A B : Set} {{eqA : Eq A}} {{eqB : Eq B}} -> (f : A -> B) -> (l : List (Tile A))
    -> (fmap f $ concat $ map expand l) ≡ (concat $ map expand $ fmap (fmap f) l)
fmap-concat-expand f [] = refl
fmap-concat-expand f (x ∷ xs) =
    begin
        fmap f (expand x ++ concat (map expand xs))
    =⟨ fmap-concat f (expand x) _ ⟩
        fmap f (expand x) ++ fmap f (concat (map expand xs))
    =⟨ cong (_++_ (fmap f (expand x))) (fmap-concat-expand f xs) ⟩
        fmap f (expand x) ++ concat (map expand $ fmap (fmap f) xs)
    =⟨ cong (λ q -> q ++ concat (map expand $ fmap (fmap f) xs)) (fmap-expand f x) ⟩
        expand (fmap f x) ++ concat (map expand $ fmap (fmap f) xs)
    end

replicate-concat : {t : Set} -> (a b : Nat) -> (v : t)
    -> replicateₙ a v ++ replicateₙ b v ≡ replicateₙ (a + b) v
replicate-concat Z b v = refl
replicate-concat (S a) b v = cong (λ z → v ∷ z) (replicate-concat a b v)

replicate-concat4 : {t : Set} -> (a b c d : Nat) -> (v : t)
    -> replicateₙ a v ++ replicateₙ b v ++ replicateₙ c v ++ replicateₙ d v ≡ replicateₙ (a + b + c + d) v
replicate-concat4 a b c d v =
    begin
        replicateₙ a v ++ replicateₙ b v ++ (replicateₙ c v ++ replicateₙ d v)
    =⟨ cong (λ z → replicateₙ a v ++ replicateₙ b v ++ z) (replicate-concat c d v) ⟩
        replicateₙ a v ++ replicateₙ b v ++ replicateₙ (c + d) v
    =⟨ cong (_++_ (replicateₙ a v)) (replicate-concat b (c + d) v) ⟩
        replicateₙ a v ++ replicateₙ (b + (c + d)) v
    =⟨ replicate-concat a (b + (c + d)) v ⟩
        replicateₙ (a + (b + (c + d))) v
    =⟨ sym (cong (λ z → replicateₙ z v) (add-assoc a b (c + d))) ⟩
        replicateₙ (a + b + (c + d)) v
    =⟨ sym (cong (λ z → replicateₙ z v) (add-assoc (a + b) c d)) ⟩
        replicateₙ (a + b + c + d) v
    end

++-assoc : {t : Set} -> (l1 l2 l3 : List t)
    -> (l1 ++ l2) ++ l3 ≡ l1 ++ (l2 ++ l3)
++-assoc [] l2 l3 = refl
++-assoc (x ∷ xs) l2 l3 = cong (λ z → x ∷ z) (++-assoc xs l2 l3)

concat-cme : {t : Set} -> (l1 l2 : List (Tile t))
    -> concat (map expand (l1 ++ l2)) ≡ (concat $ map expand l1) ++ (concat $ map expand l2)
concat-cme [] l2 = refl
concat-cme l1@(x ∷ xs) l2 =
    begin
        expand x ++ concat (map expand (xs ++ l2))
    =⟨ cong (_++_ (expand x)) (concat-cme xs l2) ⟩
        expand x ++ ((concat $ map expand xs) ++ (concat $ map expand l2))
    =⟨ sym $ ++-assoc (expand x) (concat $ map expand xs) (concat $ map expand l2) ⟩
        (expand x ++ concat (map expand xs)) ++ concat (map expand l2)
    end

concat-cme4 : {t : Set} -> (l1 l2 l3 l4 : List (Tile t))
    -> concat (map expand (l1 ++ l2 ++ l3 ++ l4)) ≡ (concat (map expand l1)) ++ (concat (map expand l2)) ++ (concat (map expand l3)) ++ (concat (map expand l4))
concat-cme4 l1 l2 l3 l4 =
    begin
        concat (map expand (l1 ++ (l2 ++ (l3 ++ l4))))
    =⟨ concat-cme l1 (l2 ++ (l3 ++ l4)) ⟩
        concat (map expand l1) ++ concat (map expand (l2 ++ (l3 ++ l4)))
    =⟨ cong (_++_ (concat (map expand l1))) (concat-cme l2 (l3 ++ l4)) ⟩
        concat (map expand l1) ++ concat (map expand l2) ++ concat (map expand (l3 ++ l4))
    =⟨ cong (λ q -> concat (map expand l1) ++ concat (map expand l2) ++ q) (concat-cme l3 l4) ⟩
        concat (map expand l1) ++ concat (map expand l2) ++ concat (map expand l3) ++ concat (map expand l4)
    end

tilesQd-concat : {A : Set} {{eqA : Eq A}} -> (deps : Nat) -> (a b c d : VQuadrant A {deps}) -> (x1 y1 x2 y2 : Nat)
    -> IsTrue (x1 <= x2) -> IsTrue (y1 <= y2)
    -> ({a b : A} -> IsTrue (a == b) -> a ≡ b)
    -> (concat $ map expand $ (tilesQd deps a (RegionC (x1 , y1) (min x2 (pow 2 deps + x1) , min y2 (pow 2 deps + y1)))
        ++ tilesQd deps b (RegionC (min x2 (pow 2 deps + x1) , y1) (x2 , min y2 (pow 2 deps + y1)))
        ++ tilesQd deps c (RegionC (x1 , min y2 (pow 2 deps + y1)) (min x2 (pow 2 deps + x1) , y2) )
        ++ tilesQd deps d (RegionC (min x2 (pow 2 deps + x1) , min y2 (pow 2 deps + y1)) (x2 , y2) )))
    ≡ (concat $ map expand $ tilesQd (S deps) (combine a b c d) (RegionC (x1 , y1) (x2 , y2)))
tilesQd-concat {A} deps a@(CVQuadrant (Leaf va)) b@(CVQuadrant (Leaf vb)) c@(CVQuadrant (Leaf vc)) d@(CVQuadrant (Leaf vd)) x1 y1 x2 y2 xp yp peq =
    ifc (va == vb && vb == vc && vc == vd)
    then (λ {{pc}} ->
        begin
            (cme $ TileC va rA ∷ TileC vb rB ∷ TileC vc rC ∷ TileC vd rD ∷ [])
        =⟨⟩
            replicateₙ (area rA) va ++ replicateₙ (area rB) vb ++ replicateₙ (area rC) vc ++ replicateₙ (area rD) vd ++ []
        =⟨ cong (λ q -> replicateₙ (area rA) va ++ replicateₙ (area rB) vb ++ replicateₙ (area rC) vc ++ q) (concat-nothing _) ⟩
            replicateₙ (area rA) (va) ++ replicateₙ (area rB) (vb) ++ replicateₙ (area rC) (vc) ++ replicateₙ (area rD) vd
        =⟨ cong (λ v -> replicateₙ (area rA) (va) ++ replicateₙ (area rB) (vb) ++ replicateₙ (area rC) (vc) ++ replicateₙ (area rD) v)
            (sym $ peq $ andSnd {vb == vc} $ andSnd {va == vb} pc) ⟩
            replicateₙ (area rA) (va) ++ replicateₙ (area rB) (vb) ++ replicateₙ (area rC) (vc) ++ replicateₙ (area rD) (vc)
        =⟨ cong (λ v -> replicateₙ (area rA) (va) ++ replicateₙ (area rB) (vb) ++ replicateₙ (area rC) (v) ++ replicateₙ (area rD) (v))
            (sym $ peq $ andFst {vb == vc} $ andSnd {va == vb} pc) ⟩
            replicateₙ (area rA) (va) ++ replicateₙ (area rB) (vb) ++ replicateₙ (area rC) (vb) ++ replicateₙ (area rD) (vb)
        =⟨ cong (λ v -> replicateₙ (area rA) (va) ++ replicateₙ (area rB) (v) ++ replicateₙ (area rC) (v) ++ replicateₙ (area rD) (v))
            (sym $ peq $ andFst {va == vb} pc) ⟩
            replicateₙ (area rA) (va) ++ replicateₙ (area rB) (va) ++ replicateₙ (area rC) (va) ++ replicateₙ (area rD) (va)
        =⟨ replicate-concat4 (area rA) (area rB) (area rC) (area rD) (va) ⟩
            replicateₙ (area rA + area rB + area rC + area rD) (va)
        =⟨ cong (λ q -> replicateₙ q (va)) (square-split x1 y1 (min x2 (mid + x1)) (min y2 (mid + y1)) x2 y2
            (min-rel-1 x1 mid x2 xp) (min-rel-2 x2 (mid + x1)) (min-rel-1 y1 mid y2 yp) (min-rel-2 y2 (mid + y1))) ⟩
            replicateₙ (diff x2 x1 * diff y2 y1) (va)
        =⟨ sym $ concat-nothing (replicateₙ (diff x2 x1 * diff y2 y1) (va)) ⟩
            replicateₙ (diff x2 x1 * diff y2 y1) va ++ []
        =⟨⟩
            (cme $ TileC va (RegionC (x1 , y1) (x2 , y2)) ∷ [])
        =⟨ cong (λ q -> cme $ tilesQd (S deps) q (RegionC (x1 , y1) (x2 , y2))) (sym $ ifcTrue (va == vb && vb == vc && vc == vd) pc) ⟩
            (cme $ tilesQd (S deps) (ifc (va == vb && vb == vc && vc == vd) then CVQuadrant (Leaf va) else CVQuadrant (Node (Leaf va) (Leaf vb) (Leaf vc) (Leaf vd))) (RegionC (x1 , y1) (x2 , y2)))
        end)
    else (λ {{pc}} ->
        begin
            (concat $ map expand $ tilesQd (S deps) (CVQuadrant (Node (Leaf va) (Leaf vb) (Leaf vc) (Leaf vd)) {andCombine (zeroLteAny deps) (falseToNotTrue pc)}) (RegionC (x1 , y1) (x2 , y2)))
        =⟨ cong {x = CVQuadrant (Node (Leaf va) (Leaf vb) (Leaf vc) (Leaf vd)) {andCombine (zeroLteAny deps) (falseToNotTrue pc)}} (λ q -> concat $ map expand $  tilesQd (S deps) q (RegionC (x1 , y1) (x2 , y2))) (sym $ ifcFalse (va == vb && vb == vc && vc == vd) pc) ⟩
            (concat $ map expand $ tilesQd (S deps) (ifc (va == vb && vb == vc && vc == vd) then CVQuadrant (Leaf va) else CVQuadrant (Node (Leaf va) (Leaf vb) (Leaf vc) (Leaf vd))) (RegionC (x1 , y1) (x2 , y2)))
        end) where
        mid = pow 2 deps
        rA = (RegionC (x1 , y1) (min x2 (mid + x1) , min y2 (mid + y1)))
        rB = (RegionC (min x2 (mid + x1) , y1) (x2 , min y2 (mid + y1)))
        rC = (RegionC (x1 , min y2 (mid + y1)) (min x2 (mid + x1) , y2) )
        rD = (RegionC (min x2 (mid + x1) , min y2 (mid + y1)) (x2 , y2) )
        cme : List (Tile A) -> List A
        cme v = concat $ map expand $ v
        area : Region -> Nat
        area (RegionC (x1 , y1) (x2 , y2)) = diff x2 x1 * diff y2 y1
tilesQd-concat deps (CVQuadrant (Leaf x)) (CVQuadrant (Leaf x₁)) (CVQuadrant (Leaf x₂)) (CVQuadrant (Node d d₁ d₂ d₃)) x1 y1 x2 y2 xp yp peq = refl
tilesQd-concat deps (CVQuadrant (Leaf x)) (CVQuadrant (Leaf x₁)) (CVQuadrant (Node c c₁ c₂ c₃)) (CVQuadrant d) x1 y1 x2 y2 xp yp peq = refl
tilesQd-concat deps (CVQuadrant (Leaf x)) (CVQuadrant (Node b b₁ b₂ b₃)) (CVQuadrant c) (CVQuadrant d) x1 y1 x2 y2 xp yp peq = refl
tilesQd-concat deps (CVQuadrant (Node a a₁ a₂ a₃)) (CVQuadrant b) (CVQuadrant c) (CVQuadrant d) x1 y1 x2 y2 xp yp peq = refl

fmap-tilesQd : {A B : Set} {{eqA : Eq A}} {{eqB : Eq B}} -> (f : A -> B) -> (dep : Nat) -> (vqd : VQuadrant A {dep}) -> (x1 y1 x2 y2 : Nat)
    -> IsTrue (x1 <= x2) -> IsTrue (y1 <= y2)
    -> ({a b : A} -> IsTrue (a == b) -> a ≡ b)
    -> ({a b : B} -> IsTrue (a == b) -> a ≡ b)
    -> (concat $ map expand $ fmap (fmap f) $ tilesQd dep vqd (RegionC (x1 , y1) (x2 , y2))) ≡ (concat $ map expand $ tilesQd dep (fmapₑ (quadrantFunctor dep) f vqd) (RegionC (x1 , y1) (x2 , y2)))
fmap-tilesQd f dep (CVQuadrant (Leaf v) {p1}) x1 y1 x2 y2 px py peqA peqB = refl
fmap-tilesQd {A} {B} f dep@(S deps) vqd@(CVQuadrant (Node a@(Leaf va) b@(Leaf vb) c@(Leaf vc) d@(Leaf vd)) {p1}) x1 y1 x2 y2 xp yp peqA peqB =
    ifc ((va == vb) && (vb == vc) && (vc == vd))
    then (λ {{pc}} ->
        (begin
            (cme $ fmap (fmap f) $ tilesQd dep vqd reg)
        =⟨⟩
            (cme $ TileC (f va) rA ∷ TileC (f vb) rB ∷ TileC (f vc) rC ∷ TileC (f vd) rD ∷ [])
        =⟨⟩
            replicateₙ (area rA) (f va) ++ replicateₙ (area rB) (f vb) ++ replicateₙ (area rC) (f vc) ++ replicateₙ (area rD) (f vd) ++ []
        =⟨ cong (λ q -> replicateₙ (area rA) (f va) ++ replicateₙ (area rB) (f vb) ++ replicateₙ (area rC) (f vc) ++ q) (concat-nothing _) ⟩
            replicateₙ (area rA) (f va) ++ replicateₙ (area rB) (f vb) ++ replicateₙ (area rC) (f vc) ++ replicateₙ (area rD) (f vd)
        =⟨ cong (λ v -> replicateₙ (area rA) (f va) ++ replicateₙ (area rB) (f vb) ++ replicateₙ (area rC) (f vc) ++ replicateₙ (area rD) (f v))
            (sym $ peqA $ andSnd {vb == vc} $ andSnd {va == vb} pc) ⟩
            replicateₙ (area rA) (f va) ++ replicateₙ (area rB) (f vb) ++ replicateₙ (area rC) (f vc) ++ replicateₙ (area rD) (f vc)
        =⟨ cong (λ v -> replicateₙ (area rA) (f va) ++ replicateₙ (area rB) (f vb) ++ replicateₙ (area rC) (f v) ++ replicateₙ (area rD) (f v))
            (sym $ peqA $ andFst {vb == vc} $ andSnd {va == vb} pc) ⟩
            replicateₙ (area rA) (f va) ++ replicateₙ (area rB) (f vb) ++ replicateₙ (area rC) (f vb) ++ replicateₙ (area rD) (f vb)
        =⟨ cong (λ v -> replicateₙ (area rA) (f va) ++ replicateₙ (area rB) (f v) ++ replicateₙ (area rC) (f v) ++ replicateₙ (area rD) (f v))
            (sym $ peqA $ andFst {va == vb} pc) ⟩
            replicateₙ (area rA) (f va) ++ replicateₙ (area rB) (f va) ++ replicateₙ (area rC) (f va) ++ replicateₙ (area rD) (f va)
        =⟨ replicate-concat4 (area rA) (area rB) (area rC) (area rD) (f va) ⟩
            replicateₙ (area rA + area rB + area rC + area rD) (f va)
        =⟨ cong (λ q -> replicateₙ q (f va)) (square-split x1 y1 (min x2 (mid + x1)) (min y2 (mid + y1)) x2 y2
            (min-rel-1 x1 mid x2 xp) (min-rel-2 x2 (mid + x1)) (min-rel-1 y1 mid y2 yp) (min-rel-2 y2 (mid + y1))) ⟩
            replicateₙ (diff x2 x1 * diff y2 y1) (f va)
        =⟨ sym $ concat-nothing (replicateₙ (diff x2 x1 * diff y2 y1) (f va)) ⟩
            replicateₙ (diff x2 x1 * diff y2 y1) (f va) ++ []
        =⟨ cong (λ q -> cme $ tilesQd dep q reg)
                (sym $ ifcTrue ((f va == f vb) && (f vb == f vc) && (f vc == f vd))
                    (useEq (cong3 (λ e1 e2 e3 -> e1 && e2 && e3) (eq-subst f va vb) (eq-subst f vb vc) (eq-subst f vc vd)) pc)) ⟩
            (cme $ tilesQd dep (combine
                (fmapₑ (quadrantFunctor deps) f sA)
                (fmapₑ (quadrantFunctor deps) f sB)
                (fmapₑ (quadrantFunctor deps) f sC)
                (fmapₑ (quadrantFunctor deps) f sD)) reg)
        =⟨⟩
            (cme $ tilesQd dep (fmapₑ (quadrantFunctor dep) f vqd) reg)
        end))
    else (λ {{pc}} ->
        (begin
            (cme $ fmap (fmap f) $ tilesQd dep vqd reg)
        =⟨⟩
            (cme $ TileC (f va) rA ∷ TileC (f vb) rB ∷ TileC (f vc) rC ∷ TileC (f vd) rD ∷ [])
        =⟨⟩
            (cme $ tilesQd dep (CVQuadrant (Node (Leaf (f va)) (Leaf (f vb)) (Leaf (f vc)) (Leaf (f vd)))
                {andCombine (zeroLteAny deps) (falseToNotTrue $ useEqFalse (cong3 (λ e1 e2 e3 -> e1 && e2 && e3) (eq-subst f va vb) (eq-subst f vb vc) (eq-subst f vc vd)) pc)}) reg)
        =⟨ cong {x = CVQuadrant (Node (Leaf (f va)) (Leaf (f vb)) (Leaf (f vc)) (Leaf (f vd)))
                {andCombine (zeroLteAny deps) (falseToNotTrue $ useEqFalse (cong3 (λ e1 e2 e3 -> e1 && e2 && e3) (eq-subst f va vb) (eq-subst f vb vc) (eq-subst f vc vd)) pc)}}
             (λ q -> cme $ tilesQd dep q reg) (sym $ ifcFalse ((f va == f vb) && (f vb == f vc) && (f vc == f vd))
             (useEqFalse (cong3 (λ e1 e2 e3 -> e1 && e2 && e3) (eq-subst f va vb) (eq-subst f vb vc) (eq-subst f vc vd)) pc)) ⟩
            (cme $ tilesQd dep (combine
                (fmapₑ (quadrantFunctor deps) f sA)
                (fmapₑ (quadrantFunctor deps) f sB)
                (fmapₑ (quadrantFunctor deps) f sC)
                (fmapₑ (quadrantFunctor deps) f sD)) reg)
        =⟨⟩
            (cme $ tilesQd dep (fmapₑ (quadrantFunctor dep) f vqd) reg)
        end))

    where
        mid = pow 2 deps
        rA = (RegionC (x1 , y1) (min x2 (mid + x1) , min y2 (mid + y1)))
        rB = (RegionC (min x2 (mid + x1) , y1) (x2 , min y2 (mid + y1)))
        rC = (RegionC (x1 , min y2 (mid + y1)) (min x2 (mid + x1) , y2) )
        rD = (RegionC (min x2 (mid + x1) , min y2 (mid + y1)) (x2 , y2) )
        reg = (RegionC (x1 , y1) (x2 , y2))
        sA = CVQuadrant {dep = deps} a {aSub {dep = deps} a b c d p1}
        sB = CVQuadrant {dep = deps} b {bSub {dep = deps} a b c d p1}
        sC = CVQuadrant {dep = deps} c {cSub {dep = deps} a b c d p1}
        sD = CVQuadrant {dep = deps} d {dSub {dep = deps} a b c d p1}
        cme : List (Tile B) -> List B
        cme v = concat $ map expand $ v
        area : Region -> Nat
        area (RegionC (x1 , y1) (x2 , y2)) = diff x2 x1 * diff y2 y1
fmap-tilesQd {A} {B} f dep@(S deps) vqd@(CVQuadrant (Node a@(Leaf _) b@(Leaf _) c@(Leaf _) d@(Node _ _ _ _)) {p1}) x1 y1 x2 y2 xp yp peqA peqB =
    begin
        (cme $ fmap (fmap f) $ tilesQd dep vqd reg)
    =⟨⟩
        (cme $ fmap (fmap f) $ (
            tilesQd deps sA rA ++ tilesQd deps sB rB ++ tilesQd deps sC rC ++ tilesQd deps sD rD
        ))
    =⟨ cong cme $ fmap-concat4 (fmap f) (tilesQd deps sA rA) (tilesQd deps sB rB) (tilesQd deps sC rC) (tilesQd deps sD rD) ⟩
        (cme (
            fmap (fmap f) (tilesQd deps sA rA)
            ++ fmap (fmap f) (tilesQd deps sB rB)
            ++ fmap (fmap f) (tilesQd deps sC rC)
            ++ fmap (fmap f) (tilesQd deps sD rD)
        ))
    =⟨ concat-cme4 (fmap (fmap f) (tilesQd deps sA rA)) (fmap (fmap f) (tilesQd deps sB rB)) (fmap (fmap f) (tilesQd deps sC rC)) (fmap (fmap f) (tilesQd deps sD rD)) ⟩
        (cme $ fmap (fmap f) (tilesQd deps sA rA))
        ++ (cme $ fmap (fmap f) (tilesQd deps sB rB))
        ++ (cme $ fmap (fmap f) (tilesQd deps sC rC))
        ++ (cme $ fmap (fmap f) (tilesQd deps sD rD))
    =⟨ cong4 (λ l1 l2 l3 l4 -> l1 ++ l2 ++ l3 ++ l4)
        (fmap-tilesQd f deps sA x1 y1 (min x2 (mid + x1)) (min y2 (mid + y1)) (min-rel-1 x1 mid x2 xp) (min-rel-1 y1 mid y2 yp) peqA peqB)
        (fmap-tilesQd f deps sB (min x2 (mid + x1)) y1 x2 (min y2 (mid + y1)) (min-rel-2 x2 (mid + x1)) (min-rel-1 y1 mid y2 yp) peqA peqB)
        (fmap-tilesQd f deps sC x1 (min y2 (mid + y1)) (min x2 (mid + x1)) y2 (min-rel-1 x1 mid x2 xp) (min-rel-2 y2 (mid + y1)) peqA peqB)
        (fmap-tilesQd f deps sD (min x2 (mid + x1)) (min y2 (mid + y1)) x2 y2 (min-rel-2 x2 (mid + x1)) (min-rel-2 y2 (mid + y1)) peqA peqB) ⟩

        (cme $ (tilesQd deps (fmapₑ (quadrantFunctor deps) f sA) rA))
        ++ (cme $ (tilesQd deps (fmapₑ (quadrantFunctor deps) f sB) rB))
        ++ (cme $ (tilesQd deps (fmapₑ (quadrantFunctor deps) f sC) rC))
        ++ (cme $ (tilesQd deps (fmapₑ (quadrantFunctor deps) f sD) rD))
    =⟨ sym $ concat-cme4 (tilesQd deps (fmapₑ (quadrantFunctor deps) f sA) rA) (tilesQd deps (fmapₑ (quadrantFunctor deps) f sB) rB) (tilesQd deps (fmapₑ (quadrantFunctor deps) f sC) rC) (tilesQd deps (fmapₑ (quadrantFunctor deps) f sD) rD) ⟩
        (cme (
            tilesQd deps (fmapₑ (quadrantFunctor deps) f sA) rA
            ++ tilesQd deps (fmapₑ (quadrantFunctor deps) f sB) rB
            ++ tilesQd deps (fmapₑ (quadrantFunctor deps) f sC) rC
            ++ tilesQd deps (fmapₑ (quadrantFunctor deps) f sD) rD
        ))
    =⟨ tilesQd-concat deps (fmapₑ (quadrantFunctor deps) f sA) (fmapₑ (quadrantFunctor deps) f sB) (fmapₑ (quadrantFunctor deps) f sC) (fmapₑ (quadrantFunctor deps) f sD) x1 y1 x2 y2 xp yp peqB ⟩
        (cme $ tilesQd dep
            (combine (fmapₑ (quadrantFunctor deps) f sA) (fmapₑ (quadrantFunctor deps) f sB) (fmapₑ (quadrantFunctor deps) f sC) (fmapₑ (quadrantFunctor deps) f sD)) reg)
    =⟨⟩
        (cme $ tilesQd dep (fmapₑ (quadrantFunctor dep) f vqd) reg)
    end where
        cme : List (Tile B) -> List B
        cme v = concat $ map expand $ v
        reg = (RegionC (x1 , y1) (x2 , y2))
        mid = pow 2 deps
        rA = (RegionC (x1 , y1) (min x2 (mid + x1) , min y2 (mid + y1)))
        rB = (RegionC (min x2 (mid + x1) , y1) (x2 , min y2 (mid + y1)))
        rC = (RegionC (x1 , min y2 (mid + y1)) (min x2 (mid + x1) , y2) )
        rD = (RegionC (min x2 (mid + x1) , min y2 (mid + y1)) (x2 , y2) )
        sA = CVQuadrant {dep = deps} a {aSub {dep = deps} a b c d p1}
        sB = CVQuadrant {dep = deps} b {bSub {dep = deps} a b c d p1}
        sC = CVQuadrant {dep = deps} c {cSub {dep = deps} a b c d p1}
        sD = CVQuadrant {dep = deps} d {dSub {dep = deps} a b c d p1}
fmap-tilesQd {A} {B} f dep@(S deps) vqd@(CVQuadrant (Node a@(Leaf _) b@(Leaf _) c@(Node _ _ _ _) d) {p1}) x1 y1 x2 y2 xp yp peqA peqB =
    begin
        (cme $ fmap (fmap f) $ tilesQd dep vqd reg)
    =⟨⟩
        (cme $ fmap (fmap f) $ (
            tilesQd deps sA rA ++ tilesQd deps sB rB ++ tilesQd deps sC rC ++ tilesQd deps sD rD
        ))
    =⟨ cong cme $ fmap-concat4 (fmap f) (tilesQd deps sA rA) (tilesQd deps sB rB) (tilesQd deps sC rC) (tilesQd deps sD rD) ⟩
        (cme (
            fmap (fmap f) (tilesQd deps sA rA)
            ++ fmap (fmap f) (tilesQd deps sB rB)
            ++ fmap (fmap f) (tilesQd deps sC rC)
            ++ fmap (fmap f) (tilesQd deps sD rD)
        ))
    =⟨ concat-cme4 (fmap (fmap f) (tilesQd deps sA rA)) (fmap (fmap f) (tilesQd deps sB rB)) (fmap (fmap f) (tilesQd deps sC rC)) _ ⟩
        (cme $ fmap (fmap f) (tilesQd deps sA rA))
        ++ (cme $ fmap (fmap f) (tilesQd deps sB rB))
        ++ (cme $ fmap (fmap f) (tilesQd deps sC rC))
        ++ (cme $ fmap (fmap f) (tilesQd deps sD rD))
    =⟨ cong4 (λ l1 l2 l3 l4 -> l1 ++ l2 ++ l3 ++ l4)
        (fmap-tilesQd f deps sA x1 y1 (min x2 (mid + x1)) (min y2 (mid + y1)) (min-rel-1 x1 mid x2 xp) (min-rel-1 y1 mid y2 yp) peqA peqB)
        (fmap-tilesQd f deps sB (min x2 (mid + x1)) y1 x2 (min y2 (mid + y1)) (min-rel-2 x2 (mid + x1)) (min-rel-1 y1 mid y2 yp) peqA peqB)
        (fmap-tilesQd f deps sC x1 (min y2 (mid + y1)) (min x2 (mid + x1)) y2 (min-rel-1 x1 mid x2 xp) (min-rel-2 y2 (mid + y1)) peqA peqB)
        (fmap-tilesQd f deps sD (min x2 (mid + x1)) (min y2 (mid + y1)) x2 y2 (min-rel-2 x2 (mid + x1)) (min-rel-2 y2 (mid + y1)) peqA peqB) ⟩

        (cme $ (tilesQd deps (fmapₑ (quadrantFunctor deps) f sA) rA))
        ++ (cme $ (tilesQd deps (fmapₑ (quadrantFunctor deps) f sB) rB))
        ++ (cme $ (tilesQd deps (fmapₑ (quadrantFunctor deps) f sC) rC))
        ++ (cme $ (tilesQd deps (fmapₑ (quadrantFunctor deps) f sD) rD))
    =⟨ sym $ concat-cme4 (tilesQd deps (fmapₑ (quadrantFunctor deps) f sA) rA) (tilesQd deps (fmapₑ (quadrantFunctor deps) f sB) rB) (tilesQd deps (fmapₑ (quadrantFunctor deps) f sC) rC) _ ⟩
        (cme (
            tilesQd deps (fmapₑ (quadrantFunctor deps) f sA) rA
            ++ tilesQd deps (fmapₑ (quadrantFunctor deps) f sB) rB
            ++ tilesQd deps (fmapₑ (quadrantFunctor deps) f sC) rC
            ++ tilesQd deps (fmapₑ (quadrantFunctor deps) f sD) rD
        ))
    =⟨ tilesQd-concat deps (fmapₑ (quadrantFunctor deps) f sA) (fmapₑ (quadrantFunctor deps) f sB) (fmapₑ (quadrantFunctor deps) f sC) (fmapₑ (quadrantFunctor deps) f sD) x1 y1 x2 y2 xp yp peqB ⟩
        (cme $ tilesQd dep
            (combine (fmapₑ (quadrantFunctor deps) f sA) (fmapₑ (quadrantFunctor deps) f sB) (fmapₑ (quadrantFunctor deps) f sC) (fmapₑ (quadrantFunctor deps) f sD)) reg)
    =⟨⟩
        (cme $ tilesQd dep (fmapₑ (quadrantFunctor dep) f vqd) reg)
    end where
        cme : List (Tile B) -> List B
        cme v = concat $ map expand $ v
        reg = (RegionC (x1 , y1) (x2 , y2))
        mid = pow 2 deps
        rA = (RegionC (x1 , y1) (min x2 (mid + x1) , min y2 (mid + y1)))
        rB = (RegionC (min x2 (mid + x1) , y1) (x2 , min y2 (mid + y1)))
        rC = (RegionC (x1 , min y2 (mid + y1)) (min x2 (mid + x1) , y2) )
        rD = (RegionC (min x2 (mid + x1) , min y2 (mid + y1)) (x2 , y2) )
        sA = CVQuadrant {dep = deps} a {aSub {dep = deps} a b c d p1}
        sB = CVQuadrant {dep = deps} b {bSub {dep = deps} a b c d p1}
        sC = CVQuadrant {dep = deps} c {cSub {dep = deps} a b c d p1}
        sD = CVQuadrant {dep = deps} d {dSub {dep = deps} a b c d p1}
fmap-tilesQd {A} {B} f dep@(S deps) vqd@(CVQuadrant (Node a@(Leaf _) b@(Node _ _ _ _) c d) {p1}) x1 y1 x2 y2 xp yp peqA peqB =
    begin
        (cme $ fmap (fmap f) $ tilesQd dep vqd reg)
    =⟨⟩
        (cme $ fmap (fmap f) $ (
            tilesQd deps sA rA ++ tilesQd deps sB rB ++ tilesQd deps sC rC ++ tilesQd deps sD rD
        ))
    =⟨ cong cme $ fmap-concat4 (fmap f) (tilesQd deps sA rA) (tilesQd deps sB rB) (tilesQd deps sC rC) (tilesQd deps sD rD) ⟩
        (cme (
            fmap (fmap f) (tilesQd deps sA rA)
            ++ fmap (fmap f) (tilesQd deps sB rB)
            ++ fmap (fmap f) (tilesQd deps sC rC)
            ++ fmap (fmap f) (tilesQd deps sD rD)
        ))
    =⟨ concat-cme4 (fmap (fmap f) (tilesQd deps sA rA)) (fmap (fmap f) (tilesQd deps sB rB)) (fmap (fmap f) (tilesQd deps sC rC)) _ ⟩
        (cme $ fmap (fmap f) (tilesQd deps sA rA))
        ++ (cme $ fmap (fmap f) (tilesQd deps sB rB))
        ++ (cme $ fmap (fmap f) (tilesQd deps sC rC))
        ++ (cme $ fmap (fmap f) (tilesQd deps sD rD))
    =⟨ cong4 (λ l1 l2 l3 l4 -> l1 ++ l2 ++ l3 ++ l4)
        (fmap-tilesQd f deps sA x1 y1 (min x2 (mid + x1)) (min y2 (mid + y1)) (min-rel-1 x1 mid x2 xp) (min-rel-1 y1 mid y2 yp) peqA peqB)
        (fmap-tilesQd f deps sB (min x2 (mid + x1)) y1 x2 (min y2 (mid + y1)) (min-rel-2 x2 (mid + x1)) (min-rel-1 y1 mid y2 yp) peqA peqB)
        (fmap-tilesQd f deps sC x1 (min y2 (mid + y1)) (min x2 (mid + x1)) y2 (min-rel-1 x1 mid x2 xp) (min-rel-2 y2 (mid + y1)) peqA peqB)
        (fmap-tilesQd f deps sD (min x2 (mid + x1)) (min y2 (mid + y1)) x2 y2 (min-rel-2 x2 (mid + x1)) (min-rel-2 y2 (mid + y1)) peqA peqB) ⟩

        (cme $ (tilesQd deps (fmapₑ (quadrantFunctor deps) f sA) rA))
        ++ (cme $ (tilesQd deps (fmapₑ (quadrantFunctor deps) f sB) rB))
        ++ (cme $ (tilesQd deps (fmapₑ (quadrantFunctor deps) f sC) rC))
        ++ (cme $ (tilesQd deps (fmapₑ (quadrantFunctor deps) f sD) rD))
    =⟨ sym $ concat-cme4 (tilesQd deps (fmapₑ (quadrantFunctor deps) f sA) rA) (tilesQd deps (fmapₑ (quadrantFunctor deps) f sB) rB) (tilesQd deps (fmapₑ (quadrantFunctor deps) f sC) rC) _ ⟩
        (cme (
            tilesQd deps (fmapₑ (quadrantFunctor deps) f sA) rA
            ++ tilesQd deps (fmapₑ (quadrantFunctor deps) f sB) rB
            ++ tilesQd deps (fmapₑ (quadrantFunctor deps) f sC) rC
            ++ tilesQd deps (fmapₑ (quadrantFunctor deps) f sD) rD
        ))
    =⟨ tilesQd-concat deps (fmapₑ (quadrantFunctor deps) f sA) (fmapₑ (quadrantFunctor deps) f sB) (fmapₑ (quadrantFunctor deps) f sC) (fmapₑ (quadrantFunctor deps) f sD) x1 y1 x2 y2 xp yp peqB ⟩
        (cme $ tilesQd dep
            (combine (fmapₑ (quadrantFunctor deps) f sA) (fmapₑ (quadrantFunctor deps) f sB) (fmapₑ (quadrantFunctor deps) f sC) (fmapₑ (quadrantFunctor deps) f sD)) reg)
    =⟨⟩
        (cme $ tilesQd dep (fmapₑ (quadrantFunctor dep) f vqd) reg)
    end where
        cme : List (Tile B) -> List B
        cme v = concat $ map expand $ v
        reg = (RegionC (x1 , y1) (x2 , y2))
        mid = pow 2 deps
        rA = (RegionC (x1 , y1) (min x2 (mid + x1) , min y2 (mid + y1)))
        rB = (RegionC (min x2 (mid + x1) , y1) (x2 , min y2 (mid + y1)))
        rC = (RegionC (x1 , min y2 (mid + y1)) (min x2 (mid + x1) , y2) )
        rD = (RegionC (min x2 (mid + x1) , min y2 (mid + y1)) (x2 , y2) )
        sA = CVQuadrant {dep = deps} a {aSub {dep = deps} a b c d p1}
        sB = CVQuadrant {dep = deps} b {bSub {dep = deps} a b c d p1}
        sC = CVQuadrant {dep = deps} c {cSub {dep = deps} a b c d p1}
        sD = CVQuadrant {dep = deps} d {dSub {dep = deps} a b c d p1}
fmap-tilesQd {A} {B} f dep@(S deps) vqd@(CVQuadrant (Node a@(Node _ _ _ _) b c d) {p1}) x1 y1 x2 y2 xp yp peqA peqB =
    begin
        (cme $ fmap (fmap f) $ tilesQd dep vqd reg)
    =⟨⟩
        (cme $ fmap (fmap f) $ (
            tilesQd deps sA rA ++ tilesQd deps sB rB ++ tilesQd deps sC rC ++ tilesQd deps sD rD
        ))
    =⟨ cong cme $ fmap-concat4 (fmap f) (tilesQd deps sA rA) (tilesQd deps sB rB) (tilesQd deps sC rC) (tilesQd deps sD rD) ⟩
        (cme (
            fmap (fmap f) (tilesQd deps sA rA)
            ++ fmap (fmap f) (tilesQd deps sB rB)
            ++ fmap (fmap f) (tilesQd deps sC rC)
            ++ fmap (fmap f) (tilesQd deps sD rD)
        ))
    =⟨ concat-cme4 (fmap (fmap f) (tilesQd deps sA rA)) (fmap (fmap f) (tilesQd deps sB rB)) (fmap (fmap f) (tilesQd deps sC rC)) _ ⟩
        (cme $ fmap (fmap f) (tilesQd deps sA rA))
        ++ (cme $ fmap (fmap f) (tilesQd deps sB rB))
        ++ (cme $ fmap (fmap f) (tilesQd deps sC rC))
        ++ (cme $ fmap (fmap f) (tilesQd deps sD rD))
    =⟨ cong4 (λ l1 l2 l3 l4 -> l1 ++ l2 ++ l3 ++ l4)
        (fmap-tilesQd f deps sA x1 y1 (min x2 (mid + x1)) (min y2 (mid + y1)) (min-rel-1 x1 mid x2 xp) (min-rel-1 y1 mid y2 yp) peqA peqB)
        (fmap-tilesQd f deps sB (min x2 (mid + x1)) y1 x2 (min y2 (mid + y1)) (min-rel-2 x2 (mid + x1)) (min-rel-1 y1 mid y2 yp) peqA peqB)
        (fmap-tilesQd f deps sC x1 (min y2 (mid + y1)) (min x2 (mid + x1)) y2 (min-rel-1 x1 mid x2 xp) (min-rel-2 y2 (mid + y1)) peqA peqB)
        (fmap-tilesQd f deps sD (min x2 (mid + x1)) (min y2 (mid + y1)) x2 y2 (min-rel-2 x2 (mid + x1)) (min-rel-2 y2 (mid + y1)) peqA peqB) ⟩

        (cme $ (tilesQd deps (fmapₑ (quadrantFunctor deps) f sA) rA))
        ++ (cme $ (tilesQd deps (fmapₑ (quadrantFunctor deps) f sB) rB))
        ++ (cme $ (tilesQd deps (fmapₑ (quadrantFunctor deps) f sC) rC))
        ++ (cme $ (tilesQd deps (fmapₑ (quadrantFunctor deps) f sD) rD))
    =⟨ sym $ concat-cme4 (tilesQd deps (fmapₑ (quadrantFunctor deps) f sA) rA) (tilesQd deps (fmapₑ (quadrantFunctor deps) f sB) rB) (tilesQd deps (fmapₑ (quadrantFunctor deps) f sC) rC) _ ⟩
        (cme (
            tilesQd deps (fmapₑ (quadrantFunctor deps) f sA) rA
            ++ tilesQd deps (fmapₑ (quadrantFunctor deps) f sB) rB
            ++ tilesQd deps (fmapₑ (quadrantFunctor deps) f sC) rC
            ++ tilesQd deps (fmapₑ (quadrantFunctor deps) f sD) rD
        ))
    =⟨ tilesQd-concat deps (fmapₑ (quadrantFunctor deps) f sA) (fmapₑ (quadrantFunctor deps) f sB) (fmapₑ (quadrantFunctor deps) f sC) (fmapₑ (quadrantFunctor deps) f sD) x1 y1 x2 y2 xp yp peqB ⟩
        (cme $ tilesQd dep
            (combine (fmapₑ (quadrantFunctor deps) f sA) (fmapₑ (quadrantFunctor deps) f sB) (fmapₑ (quadrantFunctor deps) f sC) (fmapₑ (quadrantFunctor deps) f sD)) reg)
    =⟨⟩
        (cme $ tilesQd dep (fmapₑ (quadrantFunctor dep) f vqd) reg)
    end where
        cme : List (Tile B) -> List B
        cme v = concat $ map expand $ v
        reg = (RegionC (x1 , y1) (x2 , y2))
        mid = pow 2 deps
        rA = (RegionC (x1 , y1) (min x2 (mid + x1) , min y2 (mid + y1)))
        rB = (RegionC (min x2 (mid + x1) , y1) (x2 , min y2 (mid + y1)))
        rC = (RegionC (x1 , min y2 (mid + y1)) (min x2 (mid + x1) , y2) )
        rD = (RegionC (min x2 (mid + x1) , min y2 (mid + y1)) (x2 , y2) )
        sA = CVQuadrant {dep = deps} a {aSub {dep = deps} a b c d p1}
        sB = CVQuadrant {dep = deps} b {bSub {dep = deps} a b c d p1}
        sC = CVQuadrant {dep = deps} c {cSub {dep = deps} a b c d p1}
        sD = CVQuadrant {dep = deps} d {dSub {dep = deps} a b c d p1}

qdToQt : {A : Set} {{eqA : Eq A}} -> (dep w h : Nat) -> (vqd : VQuadrant A {dep}) -> .(q : IsTrue (dep == log2up (if w < h then h else w)))
    -> tilesQd dep vqd (RegionC (0 , 0) (w , h)) ≡ tilesQt dep (toQt dep w h q vqd)
qdToQt dep w h (CVQuadrant qd {p}) q = refl

fmap-tilesQt : {A B : Set} {{eqA : Eq A}} {{eqB : Eq B}} -> (f : A -> B) -> (dep : Nat) -> (vqt : VQuadTree A {dep})
    -> ({a b : A} -> IsTrue (a == b) -> a ≡ b)
    -> ({a b : B} -> IsTrue (a == b) -> a ≡ b)
    -> (concat $ map expand $ fmap (fmap f) $ tilesQt dep vqt) ≡ (concat $ map expand $ tilesQt dep $ fmapₑ (quadtreeFunctor dep) f vqt)
fmap-tilesQt f dep (CVQuadTree (Wrapper (w , h) (Leaf v))) peqA peqB = refl
fmap-tilesQt {A} {B} f dep@(S deps) vqt@(CVQuadTree (Wrapper (w , h) qd@(Node a b c d)) {p1} {p2}) peqA peqB =
    begin
        (concat $ map expand $ fmap (fmap f) $ tilesQt dep vqt)
    =⟨⟩
        (concat $ map expand $ fmap (fmap f) $ tilesQd dep (CVQuadrant qd {p1}) (RegionC (0 , 0) (w , h)))
    =⟨ fmap-tilesQd f dep (CVQuadrant qd {p1}) 0 0 w h (zeroLteAny w) (zeroLteAny h) peqA peqB ⟩
        (concat $ map expand $ tilesQd dep (fmapₑ (quadrantFunctor dep) f (CVQuadrant qd {p1})) (RegionC (0 , 0) (w , h)))
    =⟨ cong (λ l -> concat $ map expand l) (qdToQt dep w h (combine (fmapₑ (quadrantFunctor deps) f (CVQuadrant a)) _ _ _) p2) ⟩
        (concat $ map expand $ tilesQt dep (fmapₑ (quadtreeFunctor dep) f vqt))
    end

proof-foldfmap-qt : {t s : Set} {{eqT : Eq t}} {{eqS : Eq s}} {{monS : Monoid s}} {{monT : Monoid t}} (dep : Nat) -> (vqt : VQuadTree t {dep})
    -> (f : t -> s)
    -> ({a b : t} -> IsTrue (a == b) -> a ≡ b)
    -> ({a b : s} -> IsTrue (a == b) -> a ≡ b)
    -> foldMapₑ (quadtreeFoldable dep) f vqt ≡ foldMapₑ (quadtreeFoldable dep) id (fmapₑ (quadtreeFunctor dep) f vqt)
proof-foldfmap-qt {t} {s} dep vqt@(CVQuadTree (Wrapper (w , h) (Leaf v)) {p} {q}) f peqA peqB =
    begin
        foldMapₑ (quadtreeFoldable dep) f vqt
    =⟨⟩
        foldMap f (replicateₙ (w * h) v ++ [])
    =⟨ cong (foldMap f) (concat-nothing (replicateₙ (w * h) v)) ⟩
        foldMap f (replicateₙ (w * h) v)
    =⟨ proof-foldfmap-list (replicateₙ (w * h) v) f ⟩
        foldMap id (fmap f (replicateₙ (w * h) v))
    =⟨ cong (foldMap id) (fmap-replicate f v (w * h)) ⟩
        foldMap id (replicateₙ (w * h) (f v))
    =⟨ cong (foldMap id) (sym $ concat-nothing (replicateₙ (w * h) (f v))) ⟩
        foldMap id (replicateₙ (w * h) (f v) ++ [])
    =⟨⟩
        foldMapₑ (quadtreeFoldable dep) id (fmapₑ (quadtreeFunctor dep) f vqt)
    end
proof-foldfmap-qt {t} {s} dep vqt@(CVQuadTree (Wrapper (w , h) (Node qd qd₁ qd₂ qd₃)) {p} {q}) f peqA peqB =
    begin
        foldMapₑ (quadtreeFoldable dep) f vqt
    =⟨⟩
        (foldMap f $ concat $ map expand $ tilesQt dep vqt)
    =⟨ proof-foldfmap-list (concat $ map expand $ tilesQt dep vqt) f ⟩
        (foldMap id $ fmap f $ concat $ map expand $ tilesQt dep vqt)
    =⟨ cong (foldMap id) (fmap-concat-expand f (tilesQt dep vqt)) ⟩
        (foldMap id $ concat $ map expand $ fmap (fmap f) $ tilesQt dep vqt)
    =⟨ cong (foldMap id) (fmap-tilesQt f dep vqt peqA peqB) ⟩
        (foldMap id $ concat $ map expand $ tilesQt dep $ fmapₑ (quadtreeFunctor dep) f vqt)
    =⟨⟩
        foldMapₑ (quadtreeFoldable dep) id (fmapₑ (quadtreeFunctor dep) f vqt)
    end

max_stars_repo_name: JonathanBrouwer/research-project

max_issues_repo_name: JonathanBrouwer/research-project

max_forks_repo_name: JonathanBrouwer/research-project


text:
------------------------------------------------------------------------------
-- Well-founded induction on the relation LTL
------------------------------------------------------------------------------

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

module FOTC.Data.List.WF-Relation.LT-Length.Induction.Acc.WF-I where

open import FOTC.Base
open import FOTC.Data.List
open import FOTC.Data.List.PropertiesI
open import FOTC.Data.List.WF-Relation.LT-Length
open import FOTC.Data.List.WF-Relation.LT-Length.PropertiesI

import FOTC.Data.Nat.Induction.Acc.WF-I
open FOTC.Data.Nat.Induction.Acc.WF-I.<-WF

open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Type
open import FOTC.Induction.WF

-- Parametrized modules
open module InvImg =
  FOTC.Induction.WF.InverseImage {List} {N} {_<_} lengthList-N

------------------------------------------------------------------------------
-- The relation LTL is well-founded (using the inverse image combinator).
LTL-wf : WellFounded LTL
LTL-wf Lxs = wellFounded <-wf Lxs

-- Well-founded induction on the relation LTL.
LTL-wfind : (A : D → Set) →
            (∀ {xs} → List xs → (∀ {ys} → List ys → LTL ys xs → A ys) → A xs) →
            ∀ {xs} → List xs → A xs
LTL-wfind A = WellFoundedInduction LTL-wf

------------------------------------------------------------------------------
-- The relation LTL is well-founded (a different proof).
-- Adapted from FOTC.Data.Nat.Induction.Acc.WellFoundedInduction.WF₁-LT.
module WF₁-LTL where

LTL-wf' : WellFounded LTL
LTL-wf' Lxs = acc (helper Lxs)
  where
  helper : ∀ {xs ys} → List xs → List ys → LTL ys xs → Acc List LTL ys
  helper lnil Lys ys<[] = ⊥-elim (xs<[]→⊥ Lys ys<[])
  helper (lcons x {xs} Lxs) lnil []<x∷xs =
    acc (λ Lys ys<[] → ⊥-elim (xs<[]→⊥ Lys ys<[]))
  helper (lcons x {xs} Lxs) (lcons y {ys} Lys) y∷ys<x∷xs =
    acc (λ {zs} Lzs zs<y∷ys →
           let ys<xs : LTL ys xs
               ys<xs = x∷xs<y∷ys→xs<ys Lys Lxs y∷ys<x∷xs

               zs<xs : LTL zs xs
               zs<xs = case (λ zs<ys → <-trans Lzs Lys Lxs zs<ys ys<xs)
                            (λ h → lg-xs≡lg-ys→ys<zx→xs<zs h ys<xs)
                            (xs<y∷ys→xs<ys∨lg-xs≡lg-ys Lzs Lys zs<y∷ys)

           in  helper Lxs Lzs zs<xs
        )

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module UnknownImplicitInstance where

⟨⟩ : {A : Set} {{a : A}} → A
⟨⟩ {{a}} = a

postulate
  B : Set
  instance b : B
  f : {A : Set₁} {{a : A}} → A

x : Set
x = f

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Numeral.Rational where

open import Data.Tuple
open import Logic
import      Lvl
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Numeral.Integer
open import Numeral.Integer.Oper
open import Relator.Equals
open import Type
open import Type.Quotient

-- Equivalence relation of quotient equality.
-- Essentially (if one would already work in the rationals):
--   (a₁ , a₂) quot-≡_ (b₁ , b₂)
--   ⇔ a₁ ⋅ b₂ ≡ a₂ ⋅ b₁
--   ⇔ a₁ / a₂ ≡ b₁ / b₂
_quot-≡_ : (ℤ ⨯ ℕ₊) → (ℤ ⨯ ℕ₊) → Stmt{Lvl.𝟎}
(a₁ , a₂) quot-≡ (b₁ , b₂) = (a₁ ⋅ b₂ ≡ a₂ ⋅ b₁)

ℤ : Type{Lvl.𝟎}
ℤ = (ℤ ⨯ ℕ₊) / (_quot-≡_)

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:
module Selective.Runtime where
open import Selective.Simulate
open import Selective.SimulationEnvironment
open import Prelude

open import Data.Nat.Show using (show)
open import Codata.Musical.Notation using ( ♯_ ; ♭)
import IO
open ∞Trace

record BlockedCount : Set₂ where
  field
    return-count : ℕ
    receive-count : ℕ
    selective-count : ℕ

count-blocked : (env : Env) → BlockedCount
count-blocked env = loop (Env.blocked-no-progress env)
  where
    open BlockedCount
    loop : ∀ {store inbs bl} → All (IsBlocked store inbs) bl → BlockedCount
    loop [] = record { return-count = 0 ; receive-count = 0 ; selective-count = 0 }
    loop (BlockedReturn _ _ ∷ xs) =
      let rec = loop xs
      in record { return-count = suc (rec .return-count) ; receive-count = rec .receive-count ; selective-count = rec .selective-count }
    loop (BlockedReceive _ _ _ ∷ xs) =
      let rec = loop xs
      in record { return-count = rec .return-count ; receive-count = suc (rec .receive-count) ; selective-count = rec .selective-count }
    loop (BlockedSelective _ _ _ _ _ ∷ xs) =
      let rec = loop xs
      in record { return-count = rec .return-count ; receive-count = rec .receive-count ; selective-count = suc (rec .selective-count) }

show-env : Env → String
show-env env =
  let count = count-blocked env
      open BlockedCount
  in "There are " || show (count .return-count) || " finished actors, " || show (count .receive-count) || " receiving actors, and " || show (count .selective-count) || " selecting actors"

show-final-step : ℕ → String
show-final-step n = "Done after " || (show n) || " steps."

-- run-env continously runs the simulation of an environment
-- and transforms the steps taken into output to the console.
run-env : Env → IO.IO ⊤
run-env env = loop 1 ((simulate env) .force)
  where
    loop : ℕ → Trace ∞ → IO.IO ⊤
    loop n (TraceStop env _) = ♯ IO.putStrLn (show-final-step n) IO.>> ♯ IO.putStrLn (show-env env)
    loop n (x ∷ xs) = ♯ IO.putStrLn ("Step " || show n ) IO.>> ♯ loop (suc n) (xs .force)

run-env-silent : Env → IO.IO ⊤
run-env-silent env = loop 1 ((simulate env) .force)
  where
    loop : ℕ → Trace ∞ → IO.IO ⊤
    loop n (TraceStop env _) = IO.putStrLn (show-final-step n)
    loop n (x ∷ xs) = ♯ IO.return tt IO.>> ♯ loop (suc n) (xs .force)

run-env-end : Env → IO.IO Env
run-env-end env = loop ((simulate env) .force)
  where
    loop : Trace ∞ → IO.IO Env
    loop (TraceStop env _) = IO.return env
    loop (x ∷ xs) = ♯ IO.return x IO.>> ♯ loop (xs .force)

max_stars_repo_name: Zalastax/thesis

max_issues_repo_name: Zalastax/singly-typed-actors

max_forks_repo_name: Zalastax/singly-typed-actors


text:
module TAlgebra where

open import Level
open import Data.Product
open import Relation.Binary
open Setoid

open import Basic
open import Category
import Functor
import Nat
import Adjoint
open import Monad

open Category.Category
open Functor.Functor
open Nat.Nat
open Nat.Export
open Adjoint.Export
open Monad.Monad

record TAlgebra {C₀ C₁ ℓ} {C : Category C₀ C₁ ℓ} (T : Monad C) : Set (C₀ ⊔ C₁ ⊔ ℓ) where
  field
    Tobj : Obj C
    Tmap : Hom C (fobj (MFunctor T) Tobj) Tobj

  field
    join-fmap-alg : C [ C [ Tmap ∘ component (Mjoin T) Tobj ] ≈ C [ Tmap ∘ fmap (MFunctor T) Tmap ] ]
    map-unit : C [ C [ Tmap ∘ component (Munit T) Tobj ] ≈ id C ]

open TAlgebra

record TAlgMap {C₀ C₁ ℓ} {C : Category C₀ C₁ ℓ} {T : Monad C} (a b : TAlgebra T) : Set (C₁ ⊔ ℓ) where
  field
    Thom : Hom C (Tobj a) (Tobj b)

  field
    hom-comm : C [ C [ Tmap b ∘ fmap (MFunctor T) Thom ] ≈ C [ Thom ∘ Tmap a ] ]

open TAlgMap

compose : ∀ {C₀ C₁ ℓ} {C : Category C₀ C₁ ℓ} {T : Monad C} {a b c : TAlgebra T} → TAlgMap b c → TAlgMap a b → TAlgMap a c
compose {C = C} {T} {a} {b} {c} f g = record {
  Thom = C [ Thom f ∘ Thom g ] ;
  hom-comm = begin⟨ C ⟩
    C [ Tmap c ∘ fmap (MFunctor T) (C [ Thom f ∘ Thom g ]) ] ≈⟨ ≈-composite C (refl-hom C) (preserveComp (MFunctor T)) ⟩
    C [ Tmap c ∘ C [ fmap (MFunctor T) (Thom f) ∘ fmap (MFunctor T) (Thom g) ] ] ≈⟨ sym-hom C (assoc C) ⟩
    C [ C [ Tmap c ∘ fmap (MFunctor T) (Thom f) ] ∘ fmap (MFunctor T) (Thom g) ] ≈⟨ ≈-composite C (hom-comm f) (refl-hom C) ⟩
    C [ C [ Thom f ∘ Tmap b ] ∘ fmap (MFunctor T) (Thom g) ] ≈⟨ assoc C ⟩
    C [ Thom f ∘ C [ Tmap b ∘ fmap (MFunctor T) (Thom g) ] ] ≈⟨ ≈-composite C (refl-hom C) (hom-comm g) ⟩
    C [ Thom f ∘ C [ Thom g ∘ Tmap a ] ] ≈⟨ sym-hom C (assoc C) ⟩
    C [ C [ Thom f ∘ Thom g ] ∘ Tmap a ]
  ∎ }

identity : ∀ {C₀ C₁ ℓ} {C : Category C₀ C₁ ℓ} {T : Monad C} {a : TAlgebra T} → TAlgMap a a
identity {C = C} {T} {a} = record {
  Thom = id C ;
  hom-comm = begin⟨ C ⟩
    C [ Tmap a ∘ fmap (MFunctor T) (id C) ] ≈⟨ ≈-composite C (refl-hom C) (preserveId (MFunctor T)) ⟩
    C [ Tmap a ∘ id C ] ≈⟨ rightId C ⟩
    Tmap a ≈⟨ sym-hom C (leftId C) ⟩
    C [ id C ∘ Tmap a ]
  ∎ }

T-Algs : ∀ {C₀ C₁ ℓ} {C : Category C₀ C₁ ℓ} (T : Monad C) → Category _ _ _
T-Algs {C = C} T = record {
  Obj = TAlgebra T;
  Homsetoid = λ a b → record {
    Carrier = TAlgMap a b ;
    _≈_ = λ f g → C [ Thom f ≈ Thom g ] ;
    isEquivalence = record { refl = refl-hom C ; sym = sym-hom C ; trans = trans-hom C } };
  comp = compose;
  id = identity;
  leftId = leftId C;
  rightId = rightId C;
  assoc = assoc C;
  ≈-composite = ≈-composite C }

Free-TAlg : ∀ {C₀ C₁ ℓ} {C : Category C₀ C₁ ℓ} (T : Monad C) → Functor.Functor C (T-Algs T)
Free-TAlg {C = C} T = record {
  fobj = λ x → record {
    Tobj = fobj (MFunctor T) x ;
    Tmap = component (Mjoin T) x ;
    join-fmap-alg = join_join T ;
    map-unit = unit_MFunctor T } ;
  fmapsetoid = λ {a} {b} → record {
    mapping = λ x → record {
      Thom = fmap (MFunctor T) x ;
      hom-comm = naturality (Mjoin T) } ;
    preserveEq = Functor.preserveEq (MFunctor T) } ;
  preserveId = preserveId (MFunctor T) ;
  preserveComp = preserveComp (MFunctor T) }

Forgetful-TAlg : ∀ {C₀ C₁ ℓ} {C : Category C₀ C₁ ℓ} (T : Monad C) → Functor.Functor (T-Algs T) C
Forgetful-TAlg {C = C} T = record {
  fobj = Tobj ;
  fmapsetoid = record { mapping = Thom ; preserveEq = λ x≈y → x≈y } ;
  preserveId = refl-hom C ;
  preserveComp = refl-hom C }

Free⊣Forgetful-TAlg : ∀ {C₀ C₁ ℓ} {C : Category C₀ C₁ ℓ} (T : Monad C) → Free-TAlg T ⊣ Forgetful-TAlg T
Free⊣Forgetful-TAlg {C = C} T = Adjoint.unit-triangular-holds-adjoint {C = C} {D = T-Algs T} {FT} {GT} ηT εT triL (λ {a} → triR {a})
  where
    FT = Free-TAlg T
    GT = Forgetful-TAlg T
    ηT = record {
      component = component (Munit T) ;
      naturality = naturality (Munit T) }
    εT = record {
      component = λ X → record {
        Thom = Tmap X ;
        hom-comm = sym-hom C (join-fmap-alg X) } ;
      naturality = λ {a} {b} {f} → hom-comm f }

    triL : [ C , T-Algs T ] [ Nat.compose (Nat.compose Nat.leftIdNat→ (εT N∘F FT)) (Nat.compose (Nat.assocNat← {F = FT} {GT} {FT}) (Nat.compose (FT F∘N ηT) Nat.rightIdNat←)) ≈ id [ C , T-Algs T ] ]
    triL = λ {a} → begin⟨ C ⟩
      C [ C [ id C ∘ Thom (component εT (fobj FT a)) ] ∘ C [ id C ∘ C [ Thom (fmap FT (component ηT a)) ∘ id C ] ] ] ≈⟨ ≈-composite C (leftId C) (trans-hom C (leftId C) (rightId C)) ⟩
      C [ component (Mjoin T) a ∘ fmap (MFunctor T) (component (Munit T) a) ] ≈⟨ MFunctor_unit T ⟩
      id C
      ∎

    triR : [ T-Algs T , C ] [ Nat.compose (Nat.compose Nat.rightIdNat→ (GT F∘N εT)) (Nat.compose (Nat.assocNat→ {F = GT} {FT} {GT}) (Nat.compose (ηT N∘F GT) Nat.leftIdNat←)) ≈ id [ T-Algs T , C ] ]
    triR = λ {a} → begin⟨ C ⟩
      C [ C [ id C ∘ fmap GT (component εT a) ] ∘ C [ id C ∘ C [ component ηT (fobj GT a) ∘ id C ] ] ] ≈⟨ ≈-composite C (leftId C) (trans-hom C (leftId C) (rightId C)) ⟩
      C [ fmap GT (component εT a) ∘ component ηT (fobj GT a) ] ≈⟨ refl-hom C ⟩
      C [ component (GT F∘N εT) a ∘ component (Munit T) (Tobj a) ] ≈⟨ map-unit a ⟩
      id C
      ∎

max_stars_repo_name: myuon/agda-cate

max_issues_repo_name: myuon/agda-cate

max_forks_repo_name: myuon/agda-cate


text:
open import Nat
open import Prelude
open import dynamics-core
open import contexts
open import lemmas-disjointness
open import exchange

-- this module contains all the proofs of different weakening structural
-- properties that we use for the hypothetical judgements
module weakening where
  mutual
    weaken-subst-Δ : ∀{Δ1 Δ2 Γ σ Γ'} →
                     Δ1 ## Δ2 →
                     Δ1 , Γ ⊢ σ :s: Γ' →
                     (Δ1 ∪ Δ2) , Γ ⊢ σ :s: Γ'
    weaken-subst-Δ disj (STAId x) = STAId x
    weaken-subst-Δ disj (STASubst subst x) = STASubst (weaken-subst-Δ disj subst) (weaken-ta-Δ1 disj x)

    weaken-ta-Δ1 : ∀{Δ1 Δ2 Γ d τ} →
                   Δ1 ## Δ2 →
                   Δ1 , Γ ⊢ d :: τ →
                   (Δ1 ∪ Δ2) , Γ ⊢ d :: τ
    weaken-ta-Δ1 disj TANum = TANum
    weaken-ta-Δ1 disj (TAPlus wt wt₁) = TAPlus (weaken-ta-Δ1 disj wt) (weaken-ta-Δ1 disj wt₁)
    weaken-ta-Δ1 disj (TAVar x₁) = TAVar x₁
    weaken-ta-Δ1 disj (TALam x₁ wt) = TALam x₁ (weaken-ta-Δ1 disj wt)
    weaken-ta-Δ1 disj (TAAp wt wt₁) = TAAp (weaken-ta-Δ1 disj wt) (weaken-ta-Δ1 disj wt₁)
    weaken-ta-Δ1 disj (TAInl wt) = TAInl (weaken-ta-Δ1 disj wt)
    weaken-ta-Δ1 disj (TAInr wt) = TAInr (weaken-ta-Δ1 disj wt)
    weaken-ta-Δ1 disj (TACase wt x wt₁ x₁ wt₂) = TACase (weaken-ta-Δ1 disj wt) x (weaken-ta-Δ1 disj wt₁) x₁ (weaken-ta-Δ1 disj wt₂)
    weaken-ta-Δ1 {Δ1} {Δ2} {Γ} disj (TAEHole {u = u} {Γ' = Γ'} x x₁) = TAEHole (x∈∪l Δ1 Δ2 u _ x ) (weaken-subst-Δ disj x₁)
    weaken-ta-Δ1 {Δ1} {Δ2} {Γ} disj (TANEHole {Γ' = Γ'} {u = u} x wt x₁) = TANEHole (x∈∪l Δ1 Δ2 u _ x) (weaken-ta-Δ1 disj wt) (weaken-subst-Δ disj x₁)
    weaken-ta-Δ1 disj (TACast wt x) = TACast (weaken-ta-Δ1 disj wt) x
    weaken-ta-Δ1 disj (TAFailedCast wt x x₁ x₂) = TAFailedCast (weaken-ta-Δ1 disj wt) x x₁ x₂
    weaken-ta-Δ1 disj (TAPair wt wt₁) = TAPair (weaken-ta-Δ1 disj wt) (weaken-ta-Δ1 disj wt₁)
    weaken-ta-Δ1 disj (TAFst wt) = TAFst (weaken-ta-Δ1 disj wt)
    weaken-ta-Δ1 disj (TASnd wt) = TASnd (weaken-ta-Δ1 disj wt)

  -- this is a little bit of a time saver. since ∪ is commutative on
  -- disjoint contexts, and we need that premise anyway in both positions,
  -- there's no real reason to repeat the inductive argument above
  weaken-ta-Δ2 : ∀{Δ1 Δ2 Γ d τ} →
                 Δ1 ## Δ2 →
                 Δ2 , Γ ⊢ d :: τ →
                 (Δ1 ∪ Δ2) , Γ ⊢ d :: τ
  weaken-ta-Δ2 {Δ1} {Δ2} {Γ} {d} {τ} disj D = tr (λ q → q , Γ ⊢ d :: τ) (∪comm Δ2 Δ1 (##-comm disj)) (weaken-ta-Δ1 (##-comm disj) D)

  -- note that these statements are somewhat stronger than usual. this is
  -- because we don't have implcit α-conversion. this reifies the
  -- often-silent on paper assumption that if you collide with a bound
  -- variable you can just α-convert it away and not worry.
  mutual
    weaken-synth : ∀{x Γ e τ τ'} →
                   freshh x e →
                   Γ ⊢ e => τ →
                   (Γ ,, (x , τ')) ⊢ e => τ
    weaken-synth FRHNum SNum = SNum
    weaken-synth (FRHPlus frsh frsh₁) (SPlus x x₁) = SPlus (weaken-ana frsh x) (weaken-ana frsh₁ x₁)
    weaken-synth (FRHAsc frsh) (SAsc x₁) = SAsc (weaken-ana frsh x₁)
    weaken-synth {Γ = Γ} (FRHVar {x = x} x₁) (SVar {x = y} x₂) = SVar (x∈∪r (■ (x , _)) Γ y _ x₂ (apart-singleton (flip x₁)))
    weaken-synth {Γ = Γ} (FRHLam2 x₁ frsh) (SLam x₂ wt) =
                    SLam (apart-extend1 Γ (flip x₁) x₂)
                         (exchange-synth {Γ = Γ} (flip x₁) ((weaken-synth frsh wt)))
    weaken-synth FRHEHole SEHole = SEHole
    weaken-synth (FRHNEHole frsh) (SNEHole wt) = SNEHole (weaken-synth frsh wt)
    weaken-synth (FRHAp frsh frsh₁) (SAp wt x₂ x₃) = SAp (weaken-synth frsh wt) x₂ (weaken-ana frsh₁ x₃)
    weaken-synth (FRHPair frsh frsh₁) (SPair wt wt₁) = SPair (weaken-synth frsh wt) (weaken-synth frsh₁ wt₁)
    weaken-synth (FRHFst frsh) (SFst wt x) = SFst (weaken-synth frsh wt) x
    weaken-synth (FRHSnd frsh) (SSnd wt x) = SSnd (weaken-synth frsh wt) x

    weaken-ana : ∀{x Γ e τ τ'} →
                 freshh x e →
                 Γ ⊢ e <= τ →
                 (Γ ,, (x , τ')) ⊢ e <= τ
    weaken-ana frsh (ASubsume x₁ x₂) = ASubsume (weaken-synth frsh x₁) x₂
    weaken-ana {Γ = Γ} (FRHLam1 neq frsh) (ALam x₂ x₃ wt) =
                     ALam (apart-extend1 Γ (flip neq) x₂)
                          x₃
                          (exchange-ana {Γ = Γ} (flip neq) (weaken-ana frsh wt))
    weaken-ana (FRHInl frsh) (AInl x x₁) = AInl x (weaken-ana frsh x₁)
    weaken-ana (FRHInr frsh) (AInr x x₁) = AInr x (weaken-ana frsh x₁)
    weaken-ana {Γ = Γ} (FRHCase frshd newx≠y frshd₁ newx≠z frshd₂)
                       (ACase {Γ = .Γ} y#Γ z#Γ msum syn ana₁ ana₂) =
               ACase (apart-extend1 Γ (flip newx≠y) y#Γ)
                     (apart-extend1 Γ (flip newx≠z) z#Γ)
                     msum
                     (weaken-synth {Γ = Γ} frshd syn)
                     (exchange-ana {Γ = Γ} (flip newx≠y) (weaken-ana frshd₁ ana₁))
                     (exchange-ana {Γ = Γ} (flip newx≠z) (weaken-ana frshd₂ ana₂))

  mutual
    weaken-subst-Γ : ∀{x Γ Δ σ Γ' τ} →
                     envfresh x σ →
                     Δ , Γ ⊢ σ :s: Γ' →
                     Δ , (Γ ,, (x , τ)) ⊢ σ :s: Γ'
    weaken-subst-Γ {Γ = Γ} {τ = τ₁} (EFId {x = x₃} x₁) (STAId {Γ' = Γ'} x₂) = STAId (λ x τ x∈Γ' → x∈∪r (■ (x₃ , τ₁)) Γ x τ (x₂ x τ x∈Γ') (apart-singleton λ{refl → somenotnone ((! x∈Γ') · x₁)}))
    weaken-subst-Γ {x = x} {Γ = Γ} (EFSubst x₁ efrsh x₂) (STASubst {y = y} {τ = τ'} subst x₃) =
      STASubst (exchange-subst-Γ {Γ = Γ} (flip x₂) (weaken-subst-Γ {Γ = Γ ,, (y , τ')} efrsh subst))
               (weaken-ta x₁ x₃)

    weaken-ta : ∀{x Γ Δ d τ τ'} →
                fresh x d →
                Δ , Γ ⊢ d :: τ →
                Δ , Γ ,, (x , τ') ⊢ d :: τ
    weaken-ta FNum TANum = TANum
    weaken-ta (FPlus x₁ x₂) (TAPlus x x₃) = TAPlus (weaken-ta x₁ x) (weaken-ta x₂ x₃)
    weaken-ta {x} {Γ} {_} {_} {τ} {τ'} (FVar x₂) (TAVar x₃) = TAVar (x∈∪r (■(x , _)) Γ _ _ x₃ (apart-singleton (flip x₂)))
    weaken-ta {x = x} frsh (TALam {x = y} x₂ wt) with natEQ x y
    weaken-ta (FLam x₁ x₂) (TALam x₃ wt) | Inl refl = abort (x₁ refl)
    weaken-ta {Γ = Γ} {τ' = τ'} (FLam x₁ x₃) (TALam {x = y} x₄ wt) | Inr x₂ = TALam (apart-extend1 Γ (flip x₁) x₄) (exchange-ta-Γ {Γ = Γ} (flip x₁) (weaken-ta x₃ wt))
    weaken-ta (FAp frsh frsh₁) (TAAp wt wt₁) = TAAp (weaken-ta frsh wt) (weaken-ta frsh₁ wt₁)
    weaken-ta (FHole x₁) (TAEHole x₂ x₃) = TAEHole x₂ (weaken-subst-Γ x₁ x₃)
    weaken-ta (FNEHole x₁ frsh) (TANEHole x₂ wt x₃) = TANEHole x₂ (weaken-ta frsh wt) (weaken-subst-Γ x₁ x₃)
    weaken-ta (FCast frsh) (TACast wt x₁) = TACast (weaken-ta frsh wt) x₁
    weaken-ta (FFailedCast frsh) (TAFailedCast wt x₁ x₂ x₃) = TAFailedCast (weaken-ta frsh wt) x₁ x₂ x₃
    weaken-ta (FInl frsh) (TAInl wt) = TAInl (weaken-ta frsh wt)
    weaken-ta (FInr frsh) (TAInr wt) = TAInr (weaken-ta frsh wt)
    weaken-ta {Γ = Γ} (FCase frsh x frsh₁ x₁ frsh₂) (TACase wt x₂ wt₁ x₃ wt₂) =
      TACase (weaken-ta frsh wt)
      (apart-extend1 Γ (flip x) x₂)
      (exchange-ta-Γ {Γ = Γ} (flip x) (weaken-ta frsh₁ wt₁))
      (apart-extend1 Γ (flip x₁) x₃)
      (exchange-ta-Γ {Γ = Γ} (flip x₁) (weaken-ta frsh₂ wt₂))
    weaken-ta (FPair frsh frsh₁) (TAPair wt wt₁) = TAPair (weaken-ta frsh wt) (weaken-ta frsh₁ wt₁)
    weaken-ta (FFst frsh) (TAFst wt) = TAFst (weaken-ta frsh wt)
    weaken-ta (FSnd frsh) (TASnd wt) = TASnd (weaken-ta frsh wt)

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


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

module FiniteFunctions where

open import Data.Vec using (tabulate; _∷_)
open import Data.Fin using (Fin; zero; suc)
open import Data.Nat using (ℕ; suc)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; cong; module ≡-Reasoning)
open import Function using (_∘_)

------------------------------------------------------------------------------
-- Important: Extensionality for finite functions

finext : {n : ℕ} {A : Set} → {f g : Fin n → A} → ((i : Fin n) → f i ≡ g i) →
         (tabulate f ≡ tabulate g)
finext {0} _ = refl
finext {suc n} {_} {f} {g} fi≡gi =
  begin (tabulate {suc n} f
           ≡⟨ refl ⟩
         f zero ∷ tabulate {n} (f ∘ suc)
           ≡⟨ cong (λ x → x ∷ tabulate {n} (f ∘ suc)) (fi≡gi zero) ⟩
         g zero ∷ tabulate {n} (f ∘ suc)
           ≡⟨ cong (_∷_ (g zero))
                (finext {f = f ∘ suc} {g ∘ suc} (fi≡gi ∘ suc)) ⟩
         g zero ∷ tabulate {n} (g ∘ suc)
           ≡⟨ refl ⟩
         tabulate g ∎)
  where open ≡-Reasoning

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use `Data.Universe` instead.
------------------------------------------------------------------------

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

module Universe where

{-# WARNING_ON_IMPORT
"Universe was deprecated in v1.1.
Use Data.Universe instead."
#-}

open import Data.Universe public
open import Data.Universe.Indexed public
  renaming (IndexedUniverse to Indexed-universe)


text:
-- A cut-down example:

module Issue295 where

data ⊥ : Set where

data Arr : Set where
  _⟶_ : ⊥ → ⊥ → Arr

_﹔_ : Arr → Arr → Arr
(a ⟶ b)﹔(c ⟶ d) with b
... | ()

data Fun : Arr → Set where
  ∙ : ∀ a b c d → Fun (a ⟶ b) → Fun (c ⟶ d) → Fun ((a ⟶ b)﹔(c ⟶ d))

f : ∀ a b c d e f → Fun (a ⟶ b) → Fun (c ⟶ d) → Fun (e ⟶ f)
f a b c d e f F G = ∙ a b c d F G

-- The problem does not appear to be restricted to the pretty-printer.
-- With -v10 I get the following output:
--
-- compareTerm (a ⟶ b) ﹔ (b ⟶ c) == a ⟶ c : Arr
-- { compareAtom
-- compareAtom (b ⟶ a) ﹔ (c ⟶ b) | b == a ⟶ c : Arr
-- /tmp/Bug.agda:16,15-28
-- (b ⟶ a) ﹔ (c ⟶ b) | b != a ⟶ c of type Arr
-- when checking that the expression ∙ a b b c F G has type
-- Fun (a ⟶ c)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: dagit/agda

max_forks_repo_name: dagit/agda


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

module lib.modalities.Modalities where

open import lib.modalities.Truncation public

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module Cats.Category.Cat.Facts.Product where

open import Data.Bool using (true ; false)
open import Data.Product using (_,_)
open import Level using (_⊔_)

open import Cats.Category
open import Cats.Category.Cat as Cat using (Cat ; Functor ; _⇒_ ; _∘_ ; id ; _≈_)
open import Cats.Category.Product.Binary using (_×_)
open import Cats.Category.Product.Binary.Facts using (iso-intro)
open import Cats.Trans.Iso using (NatIso)
open import Cats.Util.Logic.Constructive using (_∧_ ; ∧-eliml ; ∧-elimr)

open Functor

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

  private
    module C = Category C
    module D = Category D

  proj₁ : (C × D) ⇒ C
  proj₁ = record
      { fobj = ∧-eliml
      ; fmap = ∧-eliml
      ; fmap-resp = ∧-eliml
      ; fmap-id = C.≈.refl
      ; fmap-∘ = C.≈.refl
      }

  proj₂ : (C × D) ⇒ D
  proj₂ = record
      { fobj = ∧-elimr
      ; fmap = ∧-elimr
      ; fmap-resp = ∧-elimr
      ; fmap-id = D.≈.refl
      ; fmap-∘ = D.≈.refl
      }

  module _ {lo″ la″ l≈″} {X : Category lo″ la″ l≈″} where

    ⟨_,_⟩ : X ⇒ C → X ⇒ D → X ⇒ (C × D)
    ⟨ F , G ⟩ = record
        { fobj = λ x → fobj F x , fobj G x
        ; fmap = λ f → fmap F f , fmap G f
        ; fmap-resp = λ eq → fmap-resp F eq , fmap-resp G eq
        ; fmap-id = fmap-id F , fmap-id G
        ; fmap-∘ = fmap-∘ F , fmap-∘ G
        }

    module _ {F : X ⇒ C} {G : X ⇒ D} where

      ⟨,⟩-proj₁ : proj₁ ∘ ⟨ F , G ⟩ ≈ F
      ⟨,⟩-proj₁ = record
          { iso = C.≅.refl
          ; forth-natural = C.≈.trans C.id-l (C.≈.sym C.id-r)
          }

      ⟨,⟩-proj₂ : proj₂ ∘ ⟨ F , G ⟩ ≈ G
      ⟨,⟩-proj₂ = record
          { iso = D.≅.refl
          ; forth-natural = D.≈.trans D.id-l (D.≈.sym D.id-r)
          }

      ⟨,⟩-unique : ∀ {H} → proj₁ ∘ H ≈ F → proj₂ ∘ H ≈ G → H ≈ ⟨ F , G ⟩
      ⟨,⟩-unique {H} eq₁ eq₂ = record
          { iso = iso-intro (iso eq₁) (iso eq₂)
          ; forth-natural = forth-natural eq₁ , forth-natural eq₂
          }
        where
          open NatIso

instance
  hasBinaryProducts : ∀ lo la l≈ → HasBinaryProducts (Cat lo la l≈)
  hasBinaryProducts lo la l≈ .HasBinaryProducts._×′_ C D
      = mkBinaryProduct proj₁ proj₂ isBinaryProduct
    where
      open module Catt = Category (Cat lo la l≈) using
        (IsBinaryProduct ; mkBinaryProduct ; ∃!-intro)
      module ≈ = Catt.≈

      isBinaryProduct : ∀ {C D : Category lo la l≈}
        → IsBinaryProduct (C × D) proj₁ proj₂
      isBinaryProduct {C} {D} {X} F G = ∃!-intro
          ⟨ F , G ⟩
          (≈.sym (⟨,⟩-proj₁ {G = G}) , ≈.sym (⟨,⟩-proj₂ {F = F}))
          λ { (eq₁ , eq₂) → ≈.sym (⟨,⟩-unique (≈.sym eq₁) (≈.sym eq₂)) }

-- We get the following functors 'for free' from the above definition of
-- products in Cat, but those must have their domain and codomain category at
-- the same levels. The definitions below lift this restriction.

⟨_×_⟩ : ∀ {lo₁ la₁ l≈₁ lo₂ la₂ l≈₂ lo₃ la₃ l≈₃ lo₄ la₄ l≈₄}
  → {C : Category lo₁ la₁ l≈₁} {C′ : Category lo₂ la₂ l≈₂}
  → {D : Category lo₃ la₃ l≈₃} {D′ : Category lo₄ la₄ l≈₄}
  → C ⇒ C′ → D ⇒ D′ → (C × D) ⇒ (C′ × D′)
⟨ F × G ⟩ = ⟨ F ∘ proj₁ , G ∘ proj₂ ⟩

First : ∀ {lo₁ la₁ l≈₁ lo₂ la₂ l≈₂ lo₃ la₃ l≈₃}
  → {C : Category lo₁ la₁ l≈₁} {C′ : Category lo₂ la₂ l≈₂}
  → {D : Category lo₃ la₃ l≈₃}
  → C ⇒ C′ → (C × D) ⇒ (C′ × D)
First F = ⟨ F × id ⟩

Second : ∀ {lo₁ la₁ l≈₁ lo₂ la₂ l≈₂ lo₃ la₃ l≈₃}
  → {C : Category lo₁ la₁ l≈₁} {D : Category lo₂ la₂ l≈₂}
  → {D′ : Category lo₃ la₃ l≈₃}
  → D ⇒ D′ → (C × D) ⇒ (C × D′)
Second F = ⟨ id × F ⟩

Swap : ∀ {lo₁ la₁ l≈₁ lo₂ la₂ l≈₂}
  → {C : Category lo₁ la₁ l≈₁} {D : Category lo₂ la₂ l≈₂}
  → (C × D) ⇒ (D × C)
Swap = ⟨ proj₂ , proj₁ ⟩

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 datatype-functions where
open import lib
open import ctxt
open import syntax-util
open import general-util
open import cedille-types
open import subst
open import rename
open import is-free

data indx : Set where
  Index : var → tk → indx
indices = 𝕃 indx

data datatype : Set where
  Data : var → params → indices → ctrs → datatype

{-# TERMINATING #-}
decompose-arrows : ctxt → type → params × type
decompose-arrows Γ (Abs pi me pi' x atk T) =
  let x' = fresh-var-new Γ x in
  case decompose-arrows (ctxt-var-decl x' Γ) (rename-var Γ x x' T) of λ where
    (ps , T') → Decl posinfo-gen posinfo-gen me x' atk posinfo-gen :: ps , T'
decompose-arrows Γ (TpArrow T me T') =
  let x = fresh-var-new Γ "x" in
  case decompose-arrows (ctxt-var-decl x Γ) T' of λ where
    (ps , T'') → Decl posinfo-gen posinfo-gen me x (Tkt T) posinfo-gen :: ps , T''
decompose-arrows Γ (TpParens pi T pi') = decompose-arrows Γ T
decompose-arrows Γ T = [] , T

decompose-ctr-type : ctxt → type → type × params × 𝕃 tty
decompose-ctr-type Γ T with decompose-arrows Γ T
...| ps , Tᵣ with decompose-tpapps Tᵣ
...| Tₕ , as = Tₕ , ps , as

{-# TERMINATING #-}
kind-to-indices : ctxt → kind → indices
kind-to-indices Γ (KndArrow k k') =
  let x' = fresh-var-new Γ "x" in
  Index x' (Tkk k) :: kind-to-indices (ctxt-var-decl x' Γ) k'
kind-to-indices Γ (KndParens pi k pi') = kind-to-indices Γ k
kind-to-indices Γ (KndPi pi pi' x atk k) =
  let x' = fresh-var-new Γ x in
  Index x' atk :: kind-to-indices (ctxt-var-decl x' Γ) (rename-var Γ x x' k)
kind-to-indices Γ (KndTpArrow T k) =
  let x' = fresh-var-new Γ "x" in
  Index x' (Tkt T) :: kind-to-indices (ctxt-var-decl x' Γ) k
kind-to-indices Γ (KndVar pi x as) with ctxt-lookup-kind-var-def Γ x
...| nothing = []
...| just (ps , k) = kind-to-indices Γ $ fst $ subst-params-args Γ ps as k
kind-to-indices Γ (Star pi) = []

tk-erased : tk → maybeErased → maybeErased
tk-erased (Tkk _) me = Erased
tk-erased (Tkt _) me = me

params-set-erased : maybeErased → params → params
params-set-erased me = map λ where
  (Decl pi pi' me' x atk pi'') → Decl pi pi' me x atk pi''

args-set-erased : maybeErased → args → args
args-set-erased = map ∘ arg-set-erased

indices-to-kind : indices → kind → kind
indices-to-kind = flip $ foldr λ {(Index x atk) → KndPi posinfo-gen posinfo-gen x atk}

params-to-kind : params → kind → kind
params-to-kind = flip $ foldr λ {(Decl pi pi' me x atk pi'') → KndPi pi pi' x atk}

indices-to-tplams : indices → (body : type) → type
indices-to-tplams = flip $ foldr λ where
  (Index x atk) → TpLambda posinfo-gen posinfo-gen x atk

params-to-tplams : params → (body : type) → type
params-to-tplams = flip $ foldr λ where
  (Decl pi pi' me x atk pi'') → TpLambda pi pi' x atk

indices-to-alls : indices → (body : type) → type
indices-to-alls = flip $ foldr λ where
  (Index x atk) → Abs posinfo-gen Erased posinfo-gen x atk

params-to-alls : params → (body : type) → type
params-to-alls = flip $ foldr λ where
  (Decl pi pi' me x atk pi'') → Abs pi (tk-erased atk me) pi' x atk

indices-to-lams : indices → (body : term) → term
indices-to-lams = flip $ foldr λ where
  (Index x atk) → Lam posinfo-gen Erased posinfo-gen x (SomeClass atk)

indices-to-lams' : indices → (body : term) → term
indices-to-lams' = flip $ foldr λ where
  (Index x atk) → Lam posinfo-gen Erased posinfo-gen x NoClass

params-to-lams : params → (body : term) → term
params-to-lams = flip $ foldr λ where
  (Decl pi pi' me x atk pi'') → Lam pi (tk-erased atk me) pi' x (SomeClass atk)

params-to-lams' : params → (body : term) → term
params-to-lams' = flip $ foldr λ where
  (Decl pi pi' me x atk pi'') → Lam pi (tk-erased atk me) pi' x NoClass

indices-to-apps : indices → (body : term) → term
indices-to-apps = flip $ foldl λ where
  (Index x (Tkt T)) t → App t Erased (mvar x)
  (Index x (Tkk k)) t → AppTp t (mtpvar x)

params-to-apps : params → (body : term) → term
params-to-apps = flip $ foldl λ where
  (Decl pi pi' me x (Tkt T) pi'') t → App t me (mvar x)
  (Decl pi pi' me x (Tkk k) pi'') t → AppTp t (mtpvar x)

indices-to-tpapps : indices → (body : type) → type
indices-to-tpapps = flip $ foldl λ where
  (Index x (Tkt T)) T' → TpAppt T' (mvar x)
  (Index x (Tkk k)) T  → TpApp  T  (mtpvar x)

params-to-tpapps : params → (body : type) → type
params-to-tpapps = flip $ foldl λ where
  (Decl pi pi' me x (Tkt T) pi'') T' → TpAppt T' (mvar x)
  (Decl pi pi' me x (Tkk k) pi'') T  → TpApp  T  (mtpvar x)

ctrs-to-lams' : ctrs → (body : term) → term
ctrs-to-lams' = flip $ foldr λ where
  (Ctr _ x T) → Lam posinfo-gen NotErased posinfo-gen x NoClass

ctrs-to-lams : ctxt → var → params → ctrs → (body : term) → term
ctrs-to-lams Γ x ps cs t = foldr
  (λ {(Ctr _ y T) f Γ → Lam posinfo-gen NotErased posinfo-gen y
    (SomeClass $ Tkt $ subst Γ (params-to-tpapps ps $ mtpvar y) y T)
    $ f $ ctxt-var-decl y Γ})
  (λ Γ → t) cs Γ

add-indices-to-ctxt : indices → ctxt → ctxt
add-indices-to-ctxt = flip $ foldr λ {(Index x atk) → ctxt-var-decl x}

add-params-to-ctxt : params → ctxt → ctxt
add-params-to-ctxt = flip $ foldr λ {(Decl _ _ _ x'' _ _) → ctxt-var-decl x''}

add-caseArgs-to-ctxt : caseArgs → ctxt → ctxt
add-caseArgs-to-ctxt = flip $ foldr λ {(CaseTermArg _ _ x) → ctxt-var-decl x; (CaseTypeArg _ x) → ctxt-var-decl x}

add-ctrs-to-ctxt : ctrs → ctxt → ctxt
add-ctrs-to-ctxt = flip $ foldr λ {(Ctr _ x T) → ctxt-var-decl x}

positivity : Set
positivity = 𝔹 × 𝔹 -- occurs positively × occurs negatively

pattern occurs-nil = ff , ff
pattern occurs-pos = tt , ff
pattern occurs-neg = ff , tt
pattern occurs-all = tt , tt

--positivity-inc : positivity → positivity
--positivity-dec : positivity → positivity
positivity-neg : positivity → positivity
positivity-add : positivity → positivity → positivity

--positivity-inc = map-fst λ _ → tt
--positivity-dec = map-snd λ _ → tt
positivity-neg = uncurry $ flip _,_
positivity-add (+ₘ , -ₘ) (+ₙ , -ₙ) = (+ₘ || +ₙ) , (-ₘ || -ₙ)

-- just tt = negative occurrence; just ff = not in the return type; nothing = okay
{-# TERMINATING #-}
ctr-positive : ctxt → var → type → maybe 𝔹
ctr-positive Γ x = arrs+ Γ ∘ hnf' Γ where

  open import conversion

  not-free : ∀ {ed} → ⟦ ed ⟧ → maybe 𝔹
  not-free = maybe-map (λ _ → tt) ∘' maybe-if ∘' is-free-in check-erased x

  if-free : ∀ {ed} → ⟦ ed ⟧ → positivity
  if-free t with is-free-in check-erased x t
  ...| f = f , f

  hnf' : ctxt → type → type
  hnf' Γ T = hnf Γ unfold-all T tt

  mtt = maybe-else tt id
  mff = maybe-else ff id

  posₒ = fst
  negₒ = snd

  occurs : positivity → maybe 𝔹
  occurs p = maybe-if (negₒ p) ≫maybe just tt

  arrs+ : ctxt → type → maybe 𝔹
  type+ : ctxt → type → positivity
  kind+ : ctxt → kind → positivity
  tk+ : ctxt → tk → positivity

  arrs+ Γ (Abs _ _ _ x' atk T) =
    let Γ' = ctxt-var-decl x' Γ in
    occurs (tk+ Γ atk) maybe-or arrs+ Γ' (hnf' Γ' T)
  arrs+ Γ (TpApp T T') = arrs+ Γ T maybe-or not-free T'
  arrs+ Γ (TpAppt T t) = arrs+ Γ T maybe-or not-free t
  arrs+ Γ (TpArrow T _ T') = occurs (type+ Γ (hnf' Γ T)) maybe-or arrs+ Γ (hnf' Γ T')
  arrs+ Γ (TpLambda _ _ x' atk T) =
    let Γ' = ctxt-var-decl x' Γ in
    occurs (tk+ Γ atk) maybe-or arrs+ Γ' (hnf' Γ' T)
  arrs+ Γ (TpVar _ x') = maybe-not (maybe-if (x =string x')) ≫maybe just ff
  arrs+ Γ T = just ff

  type+ Γ (Abs _ _ _ x' atk T) =
    let Γ' = ctxt-var-decl x' Γ; atk+? = tk+ Γ atk in
    positivity-add (positivity-neg $ tk+ Γ atk) (type+ Γ' $ hnf' Γ' T)
  type+ Γ (Iota _ _ x' T T') =
    let Γ' = ctxt-var-decl x' Γ; T? = type+ Γ T in
    positivity-add (type+ Γ T) (type+ Γ' T')
  type+ Γ (Lft _ _ x' t lT) = occurs-all
  type+ Γ (NoSpans T _) = type+ Γ T
  type+ Γ (TpLet _ (DefTerm _ x' T? t) T) = type+ Γ (hnf' Γ (subst Γ t x' T))
  type+ Γ (TpLet _ (DefType _ x' k T) T') = type+ Γ (hnf' Γ (subst Γ T x' T'))
  type+ Γ (TpApp T T') = positivity-add (type+ Γ T) (if-free T')
  type+ Γ (TpAppt T t) = positivity-add (type+ Γ T) (if-free t)
  type+ Γ (TpArrow T _ T') = positivity-add (positivity-neg $ type+ Γ T) (type+ Γ $ hnf' Γ T')
  type+ Γ (TpEq _ tₗ tᵣ _) = occurs-nil
  type+ Γ (TpHole _) = occurs-nil
  type+ Γ (TpLambda _ _ x' atk T)=
    let Γ' = ctxt-var-decl x' Γ in
    positivity-add (positivity-neg $ tk+ Γ atk) (type+ Γ' (hnf' Γ' T))
  type+ Γ (TpParens _ T _) = type+ Γ T
  type+ Γ (TpVar _ x') = x =string x' , ff

  kind+ Γ (KndArrow k k') = positivity-add (positivity-neg $ kind+ Γ k) (kind+ Γ k')
  kind+ Γ (KndParens _ k _) = kind+ Γ k
  kind+ Γ (KndPi _ _ x' atk k) =
    let Γ' = ctxt-var-decl x' Γ in
    positivity-add (positivity-neg $ tk+ Γ atk) (kind+ Γ' k)
  kind+ Γ (KndTpArrow T k) = positivity-add (positivity-neg $ type+ Γ T) (kind+ Γ k)
  kind+ Γ (KndVar _ κ as) =
    maybe-else' (ctxt-lookup-kind-var-def Γ κ) occurs-nil $ uncurry λ ps k → kind+ Γ (fst (subst-params-args Γ ps as k))
  kind+ Γ (Star _) = occurs-nil

  tk+ Γ (Tkt T) = type+ Γ (hnf' Γ T)
  tk+ Γ (Tkk k) = kind+ Γ k

max_stars_repo_name: CarlOlson/cedille

max_issues_repo_name: CarlOlson/cedille

max_forks_repo_name: CarlOlson/cedille


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Functor.Algebra where

-- Algebra for a Functor

open import Level
open import Function using (_$_)

open import Categories.Category using (Category)
open import Categories.Functor using (Functor; Endofunctor)

private
  variable
    o ℓ e : Level

module _ {C : Category o ℓ e} where

  record F-Algebra (F : Endofunctor C) : Set (o ⊔ ℓ) where
    open Category C
    field
      A : Obj
      α : Functor.F₀ F A ⇒ A

  open F-Algebra

  -- Given an F-Algebra F, one can apply F to it to obtain an new 'iterated' F-Algebra
  iterate : {F : Endofunctor C} → F-Algebra F → F-Algebra F
  iterate {F} c = record { A = Functor.F₀ F $ A c ; α = Functor.F₁ F $ α c }

  record F-Algebra-Morphism {F : Endofunctor C} (X Y : F-Algebra F) : Set (ℓ ⊔ e) where
    open Category C
    module X = F-Algebra X
    module Y = F-Algebra Y
    open Functor F
    field
      f : X.A ⇒ Y.A
      commutes : f ∘ X.α ≈ Y.α ∘ F₁ f

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories