text:
open import Coinduction using ( ♯_ )
open import Data.Natural using ( Natural ; # ; _+_ )
open import Data.Strict using ( Strict ; ! )
open import System.IO.Transducers.Session using ( I ; Σ ; ⟨_⟩ )
open import System.IO.Transducers.Lazy using ( _⇒_ ; inp ; out ; done )

module System.IO.Transducers.Weight where

-- Weight of a trace

weight' : ∀ {S} → (Strict Natural) → S ⇒ ⟨ Natural ⟩
weight' {I}     (! n) = out n done
weight' {Σ W F} (! n) = inp (♯ λ a → weight' (! (n + W a)))

weight : ∀ {S} → S ⇒ ⟨ Natural ⟩
weight = weight' (! (# 0))

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io


text:
open import Everything

module Test.Thickandthin where

module _ {x a b ℓb c ℓc} ⦃ _ : Thickandthin x a b ℓb c ℓc ⦄ where
  open Thickandthin ⦃ … ⦄

  test-thin : 𝓽hin A B
  test-thin = thin

  test-check/thin=1 : 𝓬heck/thin=1 A B C _≈C_
  test-check/thin=1 = check/thin=1

  test-injectivity : ∀ {m : X} {x : A (⇑₀ m)} → 𝓶ap (_≈B_ on thin x) _≈B_
  test-injectivity {x = x} = injectivity₂,₁ x

ext: agda


text:
--{-# OPTIONS --rewriting  #-}
module Array.Rewrites where

open import Array.Base
open import Data.Nat
open import Data.Fin using (Fin; zero; suc)
open import Data.Vec
open import Data.Vec.Properties
open import Relation.Binary.PropositionalEquality

open import Function

--{-# BUILTIN REWRITE _≡_ #-}

thm : ∀ {a}{X : Set a}{s : Vec X 1} →  head s ∷ [] ≡ s
thm {s = x ∷ []} = refl

expand-s→a∘a→s : ∀ {el}{ar : Ar ℕ 1 (el ∷ [])} → ∀ (iv : Ix 1 (el ∷ []))
               → lookup (a→s ar) (ix-lookup iv zero) ≡ unimap ar iv
expand-s→a∘a→s {ar = imap f} (x ∷ []) rewrite (lookup∘tabulate (f ∘ (_∷ [])) x) = refl

imap∘unimap : ∀ {a}{X : Set a}{d s} → (ar : Ar X d s) → imap (λ iv → unimap ar iv) ≡ ar
imap∘unimap (imap ar) = refl

--{-# REWRITE expand-s→a∘a→s     #-}
--{-# REWRITE imap∘unimap        #-}
--{-# REWRITE tabulate∘lookup    #-}
--{-# REWRITE lookup∘tabulate    #-}

n+0≡n : ∀ n → n + 0 ≡ n
n+0≡n zero = refl
n+0≡n (suc n) = cong suc (n+0≡n n)

--{-# REWRITE n+0≡n     #-}

test = λ x → x + 0

max_stars_repo_name: ashinkarov/agda-array

max_issues_repo_name: ashinkarov/agda-array

max_forks_repo_name: ashinkarov/agda-array


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

open import Algebra
open import Relation.Unary
open import Relation.Binary hiding (Decidable)

module Data.FingerTree.Split.Structures
  {r m}
  (ℳ : Monoid r m)
  {s}
  {ℙ : Pred (Monoid.Carrier ℳ) s}
  (ℙ-resp : ℙ Respects (Monoid._≈_ ℳ))
  (ℙ? : Decidable ℙ)
  where

open import Relation.Nullary using (¬_; yes; no; Dec)
open import Level using (_⊔_)
open import Data.Product
open import Function
open import Data.List as List using (List; _∷_; [])

open import Data.FingerTree.Measures ℳ
open import Data.FingerTree.Structures ℳ
open import Data.FingerTree.Reasoning ℳ
open import Data.FingerTree.View ℳ using (deepₗ; deepᵣ)
open import Data.FingerTree.Cons ℳ using (listToTree)

open import Relation.Nullary using (Dec; yes; no)
open import Relation.Nullary.Decidable using (True; toWitness; False; toWitnessFalse)

open σ ⦃ ... ⦄

open Monoid ℳ renaming (Carrier to 𝓡)

open import Data.FingerTree.Relation.Binary.Reasoning.FasterInference.Setoid setoid

open import Data.FingerTree.Split.Point ℳ ℙ-resp ℙ?
open import Data.FingerTree.Split.StoredPredicate ℳ ℙ-resp ℙ?
open import Data.FingerTree.Split.Intermediate ℳ ℙ-resp ℙ?

open import Data.Empty.Irrelevant using (⊥-elim)

module _ {a} {Σ : Set a} ⦃ _ : σ Σ ⦄ where
  splitList : (i : 𝓡) → (xs : List Σ) → .(i ∣ μ xs) → μ⟨ Split′ i (List Σ) Σ ⟩≈ (i ∙ μ xs)
  splitList i [] s = ⊥-elim (¬∄ℙ s)
  splitList i (x ∷ xs) s with ⟪ℙ?⟫ (i ∙ μ x)
  ... | yes p ≈ℙ i∙x [ i∙x≈ ] = [] ∷⟨ x ⟩∷ xs [ s ▻ p ≈◄⟅ ℳ ↯ ⟆  ] ⇑[ ℳ ↯ ]
  ... | no ¬p ≈ℙ i∙x [ i∙x≈ ] with splitList i∙x xs (s ◄ ¬p ≈◄⟅ sym i∙x≈ ⟆) i≈[ i∙x≈ ]
  ... | ys ∷⟨ y ⟩∷ zs [ s′ ] ⇑[ ys≈ ] = (x ∷ ys) ∷⟨ y ⟩∷ zs [ s′ ≈◄⟅ ℳ ↯ ⟆ ] ⇑[ ℳ ↯ ] ≈[ ys≈ ]′ ≈[ ℳ ↯ ]

  splitNode : ∀ i → (xs : Node Σ) → .(i ∣ μ xs) → μ⟨ Split′ i (List Σ) Σ ⟩≈ (i ∙ μ xs)
  splitNode i xs s = do
    ys ← nodeToList xs [ _ ∙> sz ⟿ sz ]
    splitList i ys (s ≈▻⟅ sym (_ ≈? _) ⟆)

  splitDigit : ∀ i → (xs : Digit Σ) → .(i ∣ μ xs) → μ⟨ Split′ i (List Σ) Σ ⟩≈ (i ∙ μ xs)
  splitDigit i xs s = digitToList xs [ _ ∙> sz ⟿ sz ] >>= λ ys → splitList i ys (s ≈▻⟅ sym (_ ≈? _) ⟆)

  splitTree-l : ∀ i → (ls : Digit Σ) → (m : Tree ⟪ Node Σ ⟫) → (rs : Digit Σ) → .(i ∣ μ ls) → μ⟨ Split′ i (Tree Σ) Σ ⟩≈ (i ∙ (μ ls ∙ (μ m ∙ μ rs)))
  splitTree-l i ls m rs s with splitDigit i ls s
  splitTree-l i ls m rs s | lsₗ ∷⟨ mₗ ⟩∷ rsₗ [ p ] ⇑[ l≈ ] = [ ( ℳ ↯ ⍮′ ≪∙ l≈ ⍮ assoc _ _ _) ]≈ do
    ls′ ← listToTree lsₗ [ i ∙> (sz <∙ _) ⟿ sz ]
    rs′ ← deepₗ rsₗ m rs [ i ∙> (_ ∙> (_ ∙> sz)) ⟿ sz ]
    ls′ ∷⟨ mₗ ⟩∷ rs′ [ p ≈◄⟅ ∙≫ sym (μ ls′ ≈? μ lsₗ)  ⟆ ] ⇑

  splitTree-r : ∀ i → (ls : Digit Σ) → (m : Tree ⟪ Node Σ ⟫) → (rs : Digit Σ) → ∀ i∙ls∙m → .(i∙ls∙m ≈  (i ∙ μ ls ∙ μ m)) → .((i ∙ μ ls ∙ μ m) ∣ μ rs) → μ⟨ Split′ i (Tree Σ) Σ ⟩≈ (i ∙ (μ ls ∙ (μ m ∙ μ rs)))
  splitTree-r i ls m rs i′ i′≈ s with splitDigit i′ rs (s ≈◄⟅ sym i′≈ ⟆)
  splitTree-r i ls m rs i′ i′≈ s | lsᵣ ∷⟨ mᵣ ⟩∷ rsᵣ [ p ] ⇑[ r≈ ] = [ lemma r≈ i′≈ ]≈ do
      ls′ ← deepᵣ ls m lsᵣ [ i ∙> (sz <∙ _) ⟿ sz ]
      rs′ ← listToTree rsᵣ [ i ∙> (_ ∙> (_ ∙> sz)) ⟿ sz ]
      ls′ ∷⟨ mᵣ ⟩∷ rs′ [ p ≈◄⟅ ≪∙ i′≈ ⍮ ℳ ↯ ⍮′ ∙≫ sym (μ ls′ ≈? (μ ls ∙ (μ m ∙ μ lsᵣ))) ⟆ ] ⇑
    where
    lemma = λ r≈ i′≈ → begin
      i ∙ (μ ls ∙ (μ m ∙ μ lsᵣ) ∙ (μ mᵣ ∙ μ rsᵣ))
        ≈⟨ ℳ ↯ ⟩
      i ∙ μ ls ∙ μ m ∙ (μ lsᵣ ∙ (μ mᵣ ∙ μ rsᵣ))
        ≈⟨ ≪∙ sym i′≈ ⟩
      i′ ∙ (μ lsᵣ ∙ (μ mᵣ ∙ μ rsᵣ))
        ≈⟨ r≈ ⟩
      i′ ∙ μ rs
        ≈⟨ ≪∙ i′≈ ⟩
      i ∙ μ ls ∙ μ m ∙ μ rs
        ≈⟨ ℳ ↯ ⟩
      i ∙ (μ ls ∙ (μ m ∙ μ rs)) ∎

splitTree : ∀ {a} {Σ : Set a} ⦃ _ : σ Σ ⦄
          → ∀ i
          → (xs : Tree Σ)
          → .(i ∣ μ xs)
          → μ⟨ Split′ i (Tree Σ) Σ ⟩≈ (i ∙ μ xs)
splitTree i empty s = ⊥-elim (¬∄ℙ s)
splitTree i (single x) s = empty ∷⟨ x ⟩∷ empty [ s ≈◄⟅ ℳ ↯ ⟆ ] ⇑[ ℳ ↯ ]
splitTree i (deep (𝓂 ↤ ls & m & rs ⇑[ 𝓂≈ ])) s with ⟪ℙ?⟫ (i ∙ μ ls)
... | yes p₁ ≈ℙ i∙ls [ i∙ls≈ ] = splitTree-l i ls m rs ¬[ ¬ℙ s ]ℙ[ p₁ ]  ≈[ ∙≫ 𝓂≈ ]
... | no ¬p₁ ≈ℙ i∙ls [ i∙ls≈ ] with ⟪ℙ?⟫ (i∙ls ∙ μ m)
... | no ¬p₂ ≈ℙ i∙ls∙m [ i∙ls∙m≈ ] = splitTree-r i ls m rs i∙ls∙m (i∙ls∙m≈ ⍮ ≪∙ i∙ls≈) (s ≈▻⟅ sym 𝓂≈ ⟆ ◄ ¬p₁ ≈◄⟅ sym i∙ls≈ ⟆ ◄ ¬p₂ ≈◄⟅ ≪∙ i∙ls≈ ⟆) ≈[ ∙≫ 𝓂≈ ]
... | yes p₂ ≈ℙ i∙ls∙m [ i∙ls∙m≈ ] with splitTree i∙ls m (s ≈▻⟅ sym 𝓂≈ ⟆ ◄ ¬p₁ ≈◄⟅ sym i∙ls≈ ⟆ ▻ p₂)
... | lsₘ ∷⟨ μmₘ ↤ mₘ ⇑[ mₘ≈ ] ⟩∷ rsₘ [ sₘ ] ⇑[ m≈ ] with splitNode (i∙ls ∙ μ lsₘ) mₘ (sₘ ≈▻⟅ sym mₘ≈ ⟆)
... | lsₗ ∷⟨ mₗ ⟩∷ rsₗ [ sₗ ] ⇑[ l≈ ] = [ lemma 𝓂≈ m≈ mₘ≈ l≈ ]≈ do
      ll ← deepᵣ ls lsₘ lsₗ [ i ∙> (sz <∙ _) ⟿ sz ]
      rr ← deepₗ rsₗ rsₘ rs [ i ∙> (_ ∙> (μ mₗ ∙> sz)) ⟿ sz ]
      ll ∷⟨ mₗ ⟩∷ rr [ sₗ ≈◄⟅ ≪∙ ≪∙ i∙ls≈ ⍮ ℳ ↯ ⍮′ ∙≫ sym (μ ll ≈? (μ ls ∙ (μ lsₘ ∙ μ lsₗ))) ⟆ ] ⇑
  where
  lemma = λ 𝓂≈ m≈ mₘ≈ l≈ → begin
    i ∙ (μ ls ∙ (μ lsₘ ∙ μ lsₗ) ∙ (μ mₗ ∙ (μ rsₗ ∙ (μ rsₘ ∙ μ rs))))
      ≈⟨ ℳ ↯ ⟩
    i ∙ μ ls ∙ μ lsₘ ∙ (μ lsₗ ∙ (μ mₗ ∙ μ rsₗ)) ∙ (μ rsₘ ∙ μ rs)
      ≈⟨ ≪∙ ≪∙ ≪∙ sym i∙ls≈ ⍮ l≈ <∙ (μ rsₘ ∙ μ rs) ⟩
    i∙ls ∙ μ lsₘ ∙ μ mₘ ∙ (μ rsₘ ∙ μ rs)
      ≈⟨ ≪∙ ∙≫ mₘ≈ ⟩
    i∙ls ∙ μ lsₘ ∙ μmₘ ∙ (μ rsₘ ∙ μ rs)
      ≈⟨ ℳ ↯ ⟩
    i∙ls ∙ (μ lsₘ ∙ (μmₘ ∙ μ rsₘ)) ∙ μ rs
      ≈⟨ m≈ <∙ μ rs ⟩
    i∙ls ∙ μ m ∙ μ rs
      ≈⟨ ≪∙ ≪∙ i∙ls≈ ⟩
    i ∙ μ ls ∙ μ m ∙ μ rs
      ≈⟨ ℳ ↯ ⟩
    i ∙ (μ ls ∙ (μ m ∙ μ rs))
      ≈⟨ ∙≫ 𝓂≈ ⟩
    i ∙ 𝓂 ∎

init-ℙ : ∀ {𝓂} → (¬ℙ⟨ε⟩ : False (ℙ? ε)) → (ℙ⟨xs⟩ : True (ℙ? 𝓂)) → ε ∣ 𝓂
¬ℙ (init-ℙ fl tr) = toWitnessFalse fl
!ℙ (init-ℙ fl tr) = ℙ-resp (sym (identityˡ _)) (toWitness tr)

max_stars_repo_name: oisdk/agda-indexed-fingertree

max_issues_repo_name: oisdk/agda-indexed-fingertree

max_forks_repo_name: oisdk/agda-indexed-fingertree


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

open import LogicalFormulae
open import Orders.Total.Definition
open import Orders.Partial.Definition
open import Setoids.Setoids
open import Functions

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

module Setoids.Orders where

partialOrderToSetoidPartialOrder : {a b : _} {A : Set a} (P : PartialOrder {a} A {b}) → SetoidPartialOrder (reflSetoid A) (PartialOrder._<_ P)
SetoidPartialOrder.<WellDefined (partialOrderToSetoidPartialOrder P) a=b c=d a<c rewrite a=b | c=d = a<c
SetoidPartialOrder.irreflexive (partialOrderToSetoidPartialOrder P) = PartialOrder.irreflexive P
SetoidPartialOrder.<Transitive (partialOrderToSetoidPartialOrder P) = PartialOrder.<Transitive P

totalOrderToSetoidTotalOrder : {a b : _} {A : Set a} (T : TotalOrder {a} A {b}) → SetoidTotalOrder (partialOrderToSetoidPartialOrder (TotalOrder.order T))
SetoidTotalOrder.totality (totalOrderToSetoidTotalOrder T) = TotalOrder.totality T


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

open import Categories.Category.Core using (Category)

module Categories.Category.BicartesianClosed {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level

open import Categories.Category.CartesianClosed 𝒞
open import Categories.Category.Cocartesian 𝒞

record BicartesianClosed : Set (levelOfTerm 𝒞) where
  field
    cartesianClosed : CartesianClosed
    cocartesian     : Cocartesian

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of Any predicate transformer for fresh lists
------------------------------------------------------------------------

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

module Data.List.Fresh.Relation.Unary.Any.Properties where

open import Level using (Level; _⊔_; Lift)
open import Data.Bool.Base using (true; false)
open import Data.Empty
open import Data.Nat.Base using (ℕ; zero; suc)
open import Data.Product using (_,_)
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
open import Function using (_∘′_)
open import Relation.Nullary.Reflects using (invert)
open import Relation.Nullary
open import Relation.Unary  as U using (Pred)
open import Relation.Binary as B using (Rel)
open import Relation.Nary
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)

open import Data.List.Fresh
open import Data.List.Fresh.Relation.Unary.All
open import Data.List.Fresh.Relation.Unary.Any

private
  variable
    a b p q r s : Level
    A : Set a
    B : Set b

------------------------------------------------------------------------
-- NonEmpty

module _ {R : Rel A r} {P : Pred A p} where

  Any⇒NonEmpty : {xs : List# A R} → Any P xs → NonEmpty xs
  Any⇒NonEmpty {xs = cons x xs pr} p  = cons x xs pr

------------------------------------------------------------------------
-- Correspondence between Any and All

module _ {R : Rel A r} {P : Pred A p} {Q : Pred A q} (P⇒¬Q : ∀[ P ⇒ ∁ Q ]) where

  Any⇒¬All : {xs : List# A R} → Any P xs → ¬ (All Q xs)
  Any⇒¬All (here p)   (q ∷ _)  = P⇒¬Q p q
  Any⇒¬All (there ps) (_ ∷ qs) = Any⇒¬All ps qs

  All⇒¬Any : {xs : List# A R} → All P xs → ¬ (Any Q xs)
  All⇒¬Any (p ∷ _)  (here q)   = P⇒¬Q p q
  All⇒¬Any (_ ∷ ps) (there qs) = All⇒¬Any ps qs

module _ {R : Rel A r} {P : Pred A p} {Q : Pred A q} (P? : Decidable P) where

  ¬All⇒Any : {xs : List# A R} → ¬ (All P xs) → Any (∁ P) xs
  ¬All⇒Any {xs = []}      ¬ps = ⊥-elim (¬ps [])
  ¬All⇒Any {xs = x ∷# xs} ¬ps with P? x
  ... |  true because  [p] = there (¬All⇒Any (¬ps ∘′ (invert [p] ∷_)))
  ... | false because [¬p] = here (invert [¬p])

  ¬Any⇒All : {xs : List# A R} → ¬ (Any P xs) → All (∁ P) xs
  ¬Any⇒All {xs = []}      ¬ps = []
  ¬Any⇒All {xs = x ∷# xs} ¬ps with P? x
  ... |  true because  [p] = ⊥-elim (¬ps (here (invert [p])))
  ... | false because [¬p] = invert [¬p] ∷ ¬Any⇒All (¬ps ∘′ there)

------------------------------------------------------------------------
-- remove

module _ {R : Rel A r} {P : Pred A p} where

  length-remove : {xs : List# A R} (k : Any P xs) →
    length xs ≡ suc (length (xs ─ k))
  length-remove (here _)  = refl
  length-remove (there p) = cong suc (length-remove p)

------------------------------------------------------------------------
-- append

module _ {R : Rel A r} {P : Pred A p} where

  append⁺ˡ : {xs ys : List# A R} {ps : All (_# ys) xs} →
             Any P xs → Any P (append xs ys ps)
  append⁺ˡ (here px) = here px
  append⁺ˡ (there p) = there (append⁺ˡ p)

  append⁺ʳ : {xs ys : List# A R} {ps : All (_# ys) xs} →
             Any P ys → Any P (append xs ys ps)
  append⁺ʳ {xs = []}      p = p
  append⁺ʳ {xs = x ∷# xs} p = there (append⁺ʳ p)

  append⁻ : ∀ xs {ys : List# A R} {ps : All (_# ys) xs} →
            Any P (append xs ys ps) → Any P xs ⊎ Any P ys
  append⁻ []        p         = inj₂ p
  append⁻ (x ∷# xs) (here px) = inj₁ (here px)
  append⁻ (x ∷# xs) (there p) = Sum.map₁ there (append⁻ xs p)


text:
module Web.Semantic.DL.Category.Properties where

open import Web.Semantic.DL.Category.Properties.Equivalence public using
  ( ≣-refl ; ≣-sym ; ≣-trans )

open import Web.Semantic.DL.Category.Properties.Composition public using
  ( compose-resp-≣ ; compose-unit₁ ; compose-unit₂ ; compose-assoc )

open import Web.Semantic.DL.Category.Properties.Tensor public using
  ( tensor-resp-≣ ; tensor-resp-id ; tensor-resp-compose
  ; symm-iso ; assoc-iso ; assoc⁻¹-iso
  ; unit₁-iso ; unit₁⁻¹-iso ; unit₂-iso ; unit₂⁻¹-iso
  ; assoc-unit ; assoc-assoc ; assoc-symm
  ; unit₁-natural ; unit₂-natural ; symm-natural ; assoc-natural )

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


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

module Lecture3 where

import Lecture2
open Lecture2 public

data unit : U where
  star : unit

𝟙 = unit

ind-unit : {i : Level} {P : unit → UU i} → P star → ((x : unit) → P x)
ind-unit p star = p

data empty : U where

𝟘 = empty

ind-empty : {i : Level} {P : empty → UU i} → ((x : empty) → P x)
ind-empty ()

¬ : {i : Level} → UU i → UU i
¬ A = A → empty

data bool : U where
  true false : bool

not : bool → bool
not true = false
not false = true

ind-bool : {i : Level} {P : bool → UU i} → P true → P false → (x : bool) → P x
ind-bool Pt Pf true = Pt
ind-bool Pt Pf false = Pf

data coprod {i j : Level} (A : UU i) (B : UU j) : UU (i ⊔ j)  where
  inl : A → coprod A B
  inr : B → coprod A B

data Sigma {i j : Level} (A : UU i) (B : A → UU j) : UU (i ⊔ j) where
  dpair : (x : A) → (B x → Sigma A B)

Σ = Sigma

ind-Σ : {i j k : Level} {A : UU i} {B : A → UU j} {C : Σ A B → UU k} →
  ((x : A) (y : B x) → C (dpair x y)) → ((t : Σ A B) → C t)
ind-Σ f (dpair x y) = f x y

pr1 : {i j : Level} {A : UU i} {B : A → UU j} → Sigma A B → A
pr1 (dpair a b) = a

pr2 : {i j : Level} {A : UU i} {B : A → UU j} → (t : Sigma A B) → B (pr1 t)
pr2 (dpair a b) = b

weaken : {i j : Level} (A : UU i) (B : UU j) → (A → UU j)
weaken A B = λ a → B

prod : {i j : Level} (A : UU i) (B : UU j) → UU (i ⊔ j)
prod A B = Sigma A (λ a → B)

_×_ :  {i j : Level} (A : UU i) (B : UU j) → UU (i ⊔ j)
A × B = prod A B

-- WARNING, can't use pair in pattern matching as it's not recognized as a ctor
pair : {i j : Level} {A : UU i} {B : UU j} → A → (B → prod A B)
pair a b = dpair a b

-- Pointed types
U-pt : Type
U-pt = Sigma U (λ X → X)

-- Graphs
Gph : Type
Gph = Sigma U (λ X → (X → X → U))

-- Reflexive graphs
rGph : Type
rGph = Sigma U (λ X → Sigma (X → X → U) (λ R → (x : X) → R x x))

-- Finite sets
Fin : ℕ → U
Fin Nzero = empty
Fin (Nsucc n) = coprod (Fin n) unit

-- Observational equality on the natural numbers
EqN : ℕ → (ℕ → U)
EqN Nzero Nzero = 𝟙
EqN Nzero (Nsucc n) = 𝟘
EqN (Nsucc m) Nzero = 𝟘
EqN (Nsucc m) (Nsucc n) = EqN m n

-- The integers
ℤ : U
ℤ = coprod ℕ (coprod unit ℕ)
--         ^         ^^^^ ^
--     (-∞, -1]       0   [1, ∞)
--     -(n+1)              n+1

-- Inclusion of the negative integers
in-neg : ℕ → ℤ
in-neg n = inl n

-- Negative one
Zneg-one : ℤ
Zneg-one = in-neg Nzero

-- Zero
Zzero : ℤ
Zzero = inr (inl star)

-- One
Zone : ℤ
Zone = inr (inr Nzero)

-- Inclusion of the positive integers
in-pos : ℕ → ℤ
in-pos n = inr (inr n)

-- Since Agda is already strong with nested induction, I dont think we need this definition.
ind-ℤ : {i : Level} (P : ℤ → UU i) → P Zneg-one → ((n : ℕ) → P (inl n) → P (inl (Nsucc n))) → P Zzero → P Zone → ((n : ℕ) → P (inr (inr (n))) → P (inr (inr (Nsucc n)))) → (k : ℤ) → P k
ind-ℤ P p-1 p-S p0 p1 pS (inl Nzero) = p-1
ind-ℤ P p-1 p-S p0 p1 pS (inl (Nsucc x)) = p-S x (ind-ℤ P p-1 p-S p0 p1 pS (inl x))
ind-ℤ P p-1 p-S p0 p1 pS (inr (inl star)) = p0
ind-ℤ P p-1 p-S p0 p1 pS (inr (inr Nzero)) = p1
ind-ℤ P p-1 p-S p0 p1 pS (inr (inr (Nsucc x))) = pS x (ind-ℤ P p-1 p-S p0 p1 pS (inr (inr (x))))

Zsucc : ℤ → ℤ
Zsucc (inl Nzero) = Zzero
Zsucc (inl (Nsucc x)) = inl x
Zsucc (inr (inl star)) = Zone
Zsucc (inr (inr x)) = inr (inr (Nsucc x))

-- Exercise 3.1
-- In this exercise we were asked to show that (A + ¬A) implies (¬¬A → A).
-- In other words, we get double negation elimination for the types that are decidable
dne-dec : {i : Level} (A : UU i) → (coprod A (¬ A)) → (¬ (¬ A) → A)
dne-dec A (inl x) = λ f → x
dne-dec A (inr x) = λ f → ind-empty (f x)

-- Exercise 3.3
-- In this exercise we were asked to show that the observational equality on ℕ is an equivalence relation.
reflexive-EqN : (n : ℕ) → EqN n n
reflexive-EqN Nzero = star
reflexive-EqN (Nsucc n) = reflexive-EqN n

symmetric-EqN : (m n : ℕ) → EqN m n → EqN n m
symmetric-EqN Nzero Nzero t = t
symmetric-EqN Nzero (Nsucc n) t = t
symmetric-EqN (Nsucc n) Nzero t = t
symmetric-EqN (Nsucc m) (Nsucc n) t = symmetric-EqN m n t

transitive-EqN : (l m n : ℕ) → EqN l m → EqN m n → EqN l n
transitive-EqN Nzero Nzero Nzero s t = star
transitive-EqN (Nsucc n) Nzero Nzero s t = ind-empty s
transitive-EqN Nzero (Nsucc n) Nzero s t = ind-empty s
transitive-EqN Nzero Nzero (Nsucc n) s t = ind-empty t
transitive-EqN (Nsucc l) (Nsucc m) Nzero s t = ind-empty t
transitive-EqN (Nsucc l) Nzero (Nsucc n) s t = ind-empty s
transitive-EqN Nzero (Nsucc m) (Nsucc n) s t = ind-empty s
transitive-EqN (Nsucc l) (Nsucc m) (Nsucc n) s t = transitive-EqN l m n s t

-- Exercise 3.4
-- In this exercise we were asked to show that observational equality on the natural numbers is the least reflexive relation, in the sense that it implies all other reflexive relation. As we will see once we introduce the identity type, it follows that observationally equal natural numbers can be identified.

-- We first make an auxilary construction, where the relation is quantified over inside the scope of the variables n and m. This is to ensure that the inductive hypothesis is strong enough to make the induction go through.
least-reflexive-EqN' : {i : Level} (n m : ℕ)
                     (R : ℕ → ℕ → UU i) (ρ : (n : ℕ) → R n n) → EqN n m → R n m
least-reflexive-EqN' Nzero Nzero R ρ p = ρ Nzero
least-reflexive-EqN' Nzero (Nsucc m) R ρ = ind-empty
least-reflexive-EqN' (Nsucc n) Nzero R ρ = ind-empty
least-reflexive-EqN' (Nsucc n) (Nsucc m) R ρ =
  least-reflexive-EqN' n m (λ x y → R (Nsucc x) (Nsucc y)) (λ x → ρ (Nsucc x))

-- Now we solve the actual exercise by rearranging the order of the variables.
least-reflexive-EqN : {i : Level} {R : ℕ → ℕ → UU i}
  (ρ : (n : ℕ) → R n n) → (n m : ℕ) → EqN n m → R n m
least-reflexive-EqN ρ n m p = least-reflexive-EqN' n m _ ρ p

-- Exercise 3.5
-- In this exercise we were asked to show that any function on the natural numbers preserves observational equality. The quick solution uses the fact that observational equality is the least reflexive relation.
preserve_EqN : (f : ℕ → ℕ) (n m : ℕ) → (EqN n m) → (EqN (f n) (f m))
preserve_EqN f =
    least-reflexive-EqN {_} {λ x y → EqN (f x) (f y)}
      (λ x → reflexive-EqN (f x))

-- Exercise 3.6
-- In this exercise we were asked to construct the relations ≤ and < on the natural numbers, and show basic properties about them.

-- Definition of ≤
leqN : ℕ → ℕ → U
leqN Nzero Nzero = unit
leqN Nzero (Nsucc m) = unit
leqN (Nsucc n) Nzero = empty
leqN (Nsucc n) (Nsucc m) = leqN n m

_≤_ = leqN

-- Definition of <
leN : ℕ → ℕ → U
leN Nzero Nzero = empty
leN Nzero (Nsucc m) = unit
leN (Nsucc n) Nzero = empty
leN (Nsucc n) (Nsucc m) = leN n m

_<_ = leN

reflexive-leqN : (n : ℕ) → n ≤ n
reflexive-leqN Nzero = star
reflexive-leqN (Nsucc n) = reflexive-leqN n

anti-reflexive-leN : (n : ℕ) → ¬ (n < n)
anti-reflexive-leN Nzero = ind-empty
anti-reflexive-leN (Nsucc n) = anti-reflexive-leN n

transitive-leqN : (n m l : ℕ) → (n ≤ m) → (m ≤ l) → (n ≤ l)
transitive-leqN Nzero Nzero Nzero p q = reflexive-leqN Nzero
transitive-leqN Nzero Nzero (Nsucc l) p q = q
transitive-leqN Nzero (Nsucc m) Nzero p q = star
transitive-leqN Nzero (Nsucc m) (Nsucc l) p q = star
transitive-leqN (Nsucc n) Nzero l p q = ind-empty p
transitive-leqN (Nsucc n) (Nsucc m) Nzero p q = ind-empty q
transitive-leqN (Nsucc n) (Nsucc m) (Nsucc l) p q = transitive-leqN n m l p q

transitive-leN : (n m l : ℕ) → (leN n m) → (leN m l) → (leN n l)
transitive-leN Nzero Nzero Nzero p q = p
transitive-leN Nzero Nzero (Nsucc l) p q = q
transitive-leN Nzero (Nsucc m) Nzero p q = ind-empty q
transitive-leN Nzero (Nsucc m) (Nsucc l) p q = star
transitive-leN (Nsucc n) Nzero l p q = ind-empty p
transitive-leN (Nsucc n) (Nsucc m) Nzero p q = ind-empty q
transitive-leN (Nsucc n) (Nsucc m) (Nsucc l) p q = transitive-leN n m l p q

succ-leN : (n : ℕ) → leN n (Nsucc n)
succ-leN Nzero = star
succ-leN (Nsucc n) = succ-leN n

-- Exercise 3.7
-- With the construction of the divisibility relation we open the door to basic number theory.
divides : (d n : ℕ) → U
divides d n = Σ ℕ (λ m → EqN (d ** m) n)

-- Exercise 3.8
-- In this exercise we were asked to construct observational equality on the booleans. This construction is analogous to, but simpler than, the construction of observational equality on the natural numbers.
Eq2 : bool → bool → U
Eq2 true true = unit
Eq2 true false = empty
Eq2 false true = empty
Eq2 false false = unit

reflexive-Eq2 : (x : bool) → Eq2 x x
reflexive-Eq2 true = star
reflexive-Eq2 false = star

least-reflexive-Eq2 : {i : Level}
  (R : bool → bool → UU i) (ρ : (x : bool) → R x x)
  (x y : bool) → Eq2 x y → R x y
least-reflexive-Eq2 R ρ true true p = ρ true
least-reflexive-Eq2 R ρ true false p = ind-empty p
least-reflexive-Eq2 R ρ false true p = ind-empty p
least-reflexive-Eq2 R ρ false false p = ρ false

-- Exercise 3.9
-- In this exercise we were asked to show that 1 + 1 satisfies the induction principle of the booleans. In other words, type theory cannot distinguish the booleans from the type 1 + 1. We will see later that they are indeed equivalent types.
t0 : coprod unit unit
t0 = inl star

t1 : coprod unit unit
t1 = inr star

ind-coprod-unit-unit : {i : Level} {P : coprod unit unit → UU i} →
  P t0 → P t1 → (x : coprod unit unit) → P x
ind-coprod-unit-unit p0 p1 (inl star) = p0
ind-coprod-unit-unit p0 p1 (inr star) = p1

-- Exercise 3.10
-- In this exercise we were asked to define the relations ≤ and < on the integers. As a criterion of correctness, we were then also asked to show that the type of all integers l satisfying k ≤ l satisfy the induction principle of the natural numbers.
-- It turns out that this is a long exercise that requires to develop intermediate properties of the relation ≤, involving long proofs. None of them is really hard, but they are probably unintelligible because induction on the integers splits into so many cases.

leqZ : ℤ → ℤ → U
leqZ (inl Nzero) (inl Nzero) = unit
leqZ (inl Nzero) (inl (Nsucc x)) = empty
leqZ (inl Nzero) (inr l) = unit
leqZ (inl (Nsucc x)) (inl Nzero) = unit
leqZ (inl (Nsucc x)) (inl (Nsucc y)) = leqZ (inl x) (inl y)
leqZ (inl (Nsucc x)) (inr l) = unit
leqZ (inr k) (inl x) = empty
leqZ (inr (inl star)) (inr l) = unit
leqZ (inr (inr x)) (inr (inl star)) = empty
leqZ (inr (inr Nzero)) (inr (inr y)) = unit
leqZ (inr (inr (Nsucc x))) (inr (inr Nzero)) = empty
leqZ (inr (inr (Nsucc x))) (inr (inr (Nsucc y))) =
  leqZ (inr (inr (x))) (inr (inr (y)))

reflexive-leqZ : (k : ℤ) → leqZ k k
reflexive-leqZ (inl Nzero) = star
reflexive-leqZ (inl (Nsucc x)) = reflexive-leqZ (inl x)
reflexive-leqZ (inr (inl star)) = star
reflexive-leqZ (inr (inr Nzero)) = star
reflexive-leqZ (inr (inr (Nsucc x))) = reflexive-leqZ (inr (inr x))

transitive-leqZ : (k l m : ℤ) → leqZ k l → leqZ l m → leqZ k m
transitive-leqZ (inl Nzero) (inl Nzero) m p q = q
transitive-leqZ (inl Nzero) (inl (Nsucc x)) m p q = ind-empty p
transitive-leqZ (inl Nzero) (inr (inl star)) (inl Nzero) star q =
  reflexive-leqZ (inl Nzero)
transitive-leqZ (inl Nzero) (inr (inl star)) (inl (Nsucc x)) star q =
  ind-empty q
transitive-leqZ (inl Nzero) (inr (inl star)) (inr (inl star)) star q = star
transitive-leqZ (inl Nzero) (inr (inl star)) (inr (inr x)) star q = star
transitive-leqZ (inl Nzero) (inr (inr x)) (inl y) star q = ind-empty q
transitive-leqZ (inl Nzero) (inr (inr x)) (inr (inl star)) star q =
  ind-empty q
transitive-leqZ (inl Nzero) (inr (inr x)) (inr (inr y)) star q = star
transitive-leqZ (inl (Nsucc x)) (inl Nzero) (inl Nzero) star q = star
transitive-leqZ (inl (Nsucc x)) (inl Nzero) (inl (Nsucc y)) star q =
  ind-empty q
transitive-leqZ (inl (Nsucc x)) (inl Nzero) (inr m) star q = star
transitive-leqZ (inl (Nsucc x)) (inl (Nsucc y)) (inl Nzero) p q = star
transitive-leqZ (inl (Nsucc x)) (inl (Nsucc y)) (inl (Nsucc z)) p q =
  transitive-leqZ (inl x) (inl y) (inl z) p q
transitive-leqZ (inl (Nsucc x)) (inl (Nsucc y)) (inr m) p q = star
transitive-leqZ (inl (Nsucc x)) (inr y) (inl z) star q = ind-empty q
transitive-leqZ (inl (Nsucc x)) (inr y) (inr z) star q = star
transitive-leqZ (inr k) (inl x) m p q = ind-empty p
transitive-leqZ (inr (inl star)) (inr l) (inl x) star q = ind-empty q
transitive-leqZ (inr (inl star)) (inr l) (inr m) star q = star
transitive-leqZ (inr (inr x)) (inr (inl star)) m p q = ind-empty p
transitive-leqZ (inr (inr Nzero)) (inr (inr Nzero)) m p q = q
transitive-leqZ (inr (inr Nzero)) (inr (inr (Nsucc y))) (inl x) star q =
  ind-empty q
transitive-leqZ (inr (inr Nzero)) (inr (inr (Nsucc y))) (inr (inl star))
                star q =
  ind-empty q
transitive-leqZ (inr (inr Nzero)) (inr (inr (Nsucc y))) (inr (inr z))
                star q = star
transitive-leqZ (inr (inr (Nsucc x))) (inr (inr Nzero)) m p q = ind-empty p
transitive-leqZ (inr (inr (Nsucc x))) (inr (inr (Nsucc y))) (inl z) p q =
  ind-empty q
transitive-leqZ (inr (inr (Nsucc x))) (inr (inr (Nsucc y)))
  (inr (inl star)) p q = ind-empty q
transitive-leqZ (inr (inr (Nsucc x))) (inr (inr (Nsucc y)))
  (inr (inr Nzero)) p q = ind-empty q
transitive-leqZ (inr (inr (Nsucc x))) (inr (inr (Nsucc y)))
  (inr (inr (Nsucc z))) p q =
  transitive-leqZ (inr (inr x)) (inr (inr y)) (inr (inr z)) p q

succ-leqZ : (k : ℤ) → leqZ k (Zsucc k)
succ-leqZ (inl Nzero) = star
succ-leqZ (inl (Nsucc Nzero)) = star
succ-leqZ (inl (Nsucc (Nsucc x))) = succ-leqZ (inl (Nsucc x))
succ-leqZ (inr (inl star)) = star
succ-leqZ (inr (inr Nzero)) = star
succ-leqZ (inr (inr (Nsucc x))) = succ-leqZ (inr (inr x))

leqZ-succ-leqZ : (k l : ℤ) → leqZ k l → leqZ k (Zsucc l)
leqZ-succ-leqZ k l p = transitive-leqZ k l (Zsucc l) p (succ-leqZ l)

leZ : ℤ → ℤ → U
leZ (inl Nzero) (inl x) = empty
leZ (inl Nzero) (inr y) = unit
leZ (inl (Nsucc x)) (inl Nzero) = unit
leZ (inl (Nsucc x)) (inl (Nsucc y)) = leZ (inl x) (inl y)
leZ (inl (Nsucc x)) (inr y) = unit
leZ (inr x) (inl y) = empty
leZ (inr (inl star)) (inr (inl star)) = empty
leZ (inr (inl star)) (inr (inr x)) = unit
leZ (inr (inr x)) (inr (inl star)) = empty
leZ (inr (inr Nzero)) (inr (inr Nzero)) = empty
leZ (inr (inr Nzero)) (inr (inr (Nsucc y))) = unit
leZ (inr (inr (Nsucc x))) (inr (inr Nzero)) = empty
leZ (inr (inr (Nsucc x))) (inr (inr (Nsucc y))) =
  leZ (inr (inr x)) (inr (inr y))

fam-shift-leqZ : (k : ℤ) {i : Level} (P : (l : ℤ) → leqZ k l → UU i) → (l : ℤ) → (leqZ (Zsucc k) l) → UU i
fam-shift-leqZ k P l p = P l (transitive-leqZ k (Zsucc k) l (succ-leqZ k) p)

-- ind-Z-leqZ : (k : ℤ) {i : Level} (P : (l : ℤ) → (leqZ k l) → UU i) →
--   P k (reflexive-leqZ k) →
--   ((l : ℤ) (p : leqZ k l) → P l p → P (Zsucc l) (leqZ-succ-leqZ k l p)) →
--   (l : ℤ) (p : leqZ k l) → P l p
-- ind-Z-leqZ (inl Nzero) P pk pS (inl Nzero) star = pk
-- ind-Z-leqZ (inl Nzero) P pk pS (inl (Nsucc x)) ()
-- ind-Z-leqZ (inl Nzero) P pk pS (inr (inl star)) star = pS (inl Nzero) star pk
-- ind-Z-leqZ (inl Nzero) P pk pS (inr (inr Nzero)) star = pS (inr (inl star)) star (pS (inl Nzero) star pk)
-- ind-Z-leqZ (inl Nzero) P pk pS (inr (inr (Nsucc x))) star = pS (inr (inr x)) star (ind-Z-leqZ (inl Nzero) P pk pS (inr (inr x)) star)
-- ind-Z-leqZ (inl (Nsucc Nzero)) {i} P pk pS (inl Nzero) star = pS {!!} {!!} {!!}
-- ind-Z-leqZ (inl (Nsucc (Nsucc x))) {i} P pk pS (inl Nzero) star = {!!}
-- ind-Z-leqZ (inl (Nsucc x)) P pk pS (inl (Nsucc y)) p = {!!}
-- ind-Z-leqZ (inl (Nsucc x)) P pk pS (inr y) p = {!!}
-- ind-Z-leqZ (inr k) P pk pS l p = {!!}

-- Exercise 3.11
Zpred : ℤ → ℤ
Zpred (inl x) = inl (Nsucc x)
Zpred (inr (inl star)) = inl Nzero
Zpred (inr (inr Nzero)) = inr (inl star)
Zpred (inr (inr (Nsucc x))) = inr (inr x)

-- Exercise 3.12
Zadd : ℤ → ℤ → ℤ
Zadd (inl Nzero) l = Zpred l
Zadd (inl (Nsucc x)) l = Zpred (Zadd (inl x) l)
Zadd (inr (inl star)) l = l
Zadd (inr (inr Nzero)) l = Zsucc l
Zadd (inr (inr (Nsucc x))) l = Zsucc (Zadd (inr (inr x)) l)

Zneg : ℤ → ℤ
Zneg (inl x) = inr (inr x)
Zneg (inr (inl star)) = inr (inl star)
Zneg (inr (inr x)) = inl x


text:
{-# OPTIONS --without-K #-}
module PathStructure.Product {a b} {A : Set a} {B : Set b} where

open import Equivalence
open import PathOperations
open import Types

split-path : {x y : A × B} → x ≡ y → (π₁ x ≡ π₁ y) × (π₂ x ≡ π₂ y)
split-path p = ap π₁ p , ap π₂ p

merge-path : {x₁ x₂ : A} {y₁ y₂ : B} →
  (x₁ ≡ x₂) × (y₁ ≡ y₂) → Id (A × B) (x₁ , y₁) (x₂ , y₂)
merge-path (p , q) = ap₂ _,_ p q

split-merge-eq : {x y : A × B} →
  (x ≡ y) ≃ (π₁ x ≡ π₁ y) × (π₂ x ≡ π₂ y)
split-merge-eq
  = split-path
  , (merge-path , λ pq → J
      (λ _ _ p → ∀ {b₁ b₂} (q : b₁ ≡ b₂) →
        split-path (merge-path (p , q)) ≡ p , q)
      (λ _ q → J
        (λ _ _ q →
          split-path (merge-path (refl , q)) ≡ refl , q)
        (λ _ → refl) _ _ q)
      _ _ (π₁ pq) (π₂ pq))
  , (merge-path , J (λ _ _ p → merge-path (split-path p) ≡ p)
      (λ _ → refl) _ _)

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


text:
module Data.List.Size where

import      Lvl
open import Data.List
open import Logic.Predicate
open import Logic.Propositional
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Function.Domain
open import Type

open import Data.Boolean

private variable ℓ : Lvl.Level
private variable T : Type{ℓ}

-- TODO: For general types, not just Bool.
index : (T → ℕ) → (List(T) → ℕ)
index f ∅       = 1
index f (x ⊰ l) = (2 ^ 𝐒(f(x))) ⋅ index f l -- TODO: 2 is temporary. Use unique primes (does not have to include all or even be in order).

{-
index-injective : ∀{f : T → ℕ} → ⦃ Injective(f) ⦄ → Injective(index f)
index-injective = {!!}
-}

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:
{-# OPTIONS --cubical #-}

module all where

import 00-preamble
import 02-pi
import 03-natural-numbers
import 04-inductive-types
import 05-identity-types
import 06-universes
import 07-finite-sets
import 08-equivalences
import 09-contractible-types
import 10-fundamental-theorem
import 11-truncation-levels
import 12-function-extensionality
import 13-propositional-truncation
import 14-univalence
import 15-groups
import 16-sets
import 17-number-theory
import 18-circle
import 19-fundamental-cover
import 20-pullbacks
import 21-pushouts
import 22-cubical-diagrams
-- import 22-descent
-- import 23-id-pushout
-- import 24-sequences
import abelian-groups
import abelian-subgroups
-- import categories
-- import coinductive-types
import combinatorial-objects
import cubical-circle
-- import dn-sheaves
-- import free-group
-- import group-completion
-- import hott-i
import ideals
import integers
-- import lists
-- import localizations-rings
-- import models
-- import mwe
import polynomial-rings
import quotient-groups
-- import rational-numbers
-- import rings
import rings-with-properties
-- import SAT-solver
import subgroups
-- import subrings
-- import subuniverses

max_stars_repo_name: tmoux/HoTT-Intro

max_issues_repo_name: tmoux/HoTT-Intro

max_forks_repo_name: tmoux/HoTT-Intro


text:
{-
This second-order signature was created from the following second-order syntax description:

syntax PDiff | PD

type
  * : 0-ary

term
  zero  : * | 𝟘
  add   : *  *  ->  * | _⊕_ l20
  one   : * | 𝟙
  mult  : *  *  ->  * | _⊗_ l20
  neg   : *  ->  * | ⊖_ r50
  pd : *.*  *  ->  * | ∂_∣_

theory
  (𝟘U⊕ᴸ) a |> add (zero, a) = a
  (𝟘U⊕ᴿ) a |> add (a, zero) = a
  (⊕A) a b c |> add (add(a, b), c) = add (a, add(b, c))
  (⊕C) a b |> add(a, b) = add(b, a)
  (𝟙U⊗ᴸ) a |> mult (one, a) = a
  (𝟙U⊗ᴿ) a |> mult (a, one) = a
  (⊗A) a b c |> mult (mult(a, b), c) = mult (a, mult(b, c))
  (⊗D⊕ᴸ) a b c |> mult (a, add (b, c)) = add (mult(a, b), mult(a, c))
  (⊗D⊕ᴿ) a b c |> mult (add (a, b), c) = add (mult(a, c), mult(b, c))
  (𝟘X⊗ᴸ) a |> mult (zero, a) = zero
  (𝟘X⊗ᴿ) a |> mult (a, zero) = zero
  (⊖N⊕ᴸ) a |> add (neg (a), a) = zero
  (⊖N⊕ᴿ) a |> add (a, neg (a)) = zero
  (⊗C) a b |> mult(a, b) = mult(b, a)
  (∂⊕) a : * |> x : * |- d0 (add (x, a)) = one
  (∂⊗) a : * |> x : * |- d0 (mult(a, x)) = a
  (∂C) f : (*,*).* |> x : *  y : * |- d1 (d0 (f[x,y])) = d0 (d1 (f[x,y]))
  (∂Ch₂) f : (*,*).*  g h : *.* |> x : * |- d0 (f[g[x], h[x]]) = add (mult(pd(z. f[z, h[x]], g[x]), d0(g[x])), mult(pd(z. f[g[x], z], h[x]), d0(h[x])))
  (∂Ch₁) f g : *.* |> x : * |- d0 (f[g[x]]) = mult (pd (z. f[z], g[x]), d0(g[x]))
-}

module PDiff.Signature where

open import SOAS.Context

open import SOAS.Common

open import SOAS.Syntax.Signature *T public
open import SOAS.Syntax.Build *T public

-- Operator symbols
data PDₒ : Set where
  zeroₒ addₒ oneₒ multₒ negₒ pdₒ : PDₒ

-- Term signature
PD:Sig : Signature PDₒ
PD:Sig = sig λ
  {  zeroₒ   → ⟼₀ *
  ;  addₒ    → (⊢₀ *) , (⊢₀ *) ⟼₂ *
  ;  oneₒ    → ⟼₀ *
  ;  multₒ   → (⊢₀ *) , (⊢₀ *) ⟼₂ *
  ;  negₒ    → (⊢₀ *) ⟼₁ *
  ;  pdₒ  → (* ⊢₁ *) , (⊢₀ *) ⟼₂ *
  }

open Signature PD:Sig public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


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

module Definition.Typed.RedSteps where

open import Definition.Untyped
open import Definition.Typed

-- Concatenation of type reduction closures
_⇨*_ : ∀ {Γ A B C} → Γ ⊢ A ⇒* B → Γ ⊢ B ⇒* C → Γ ⊢ A ⇒* C
id ⊢B ⇨* B⇒C = B⇒C
(A⇒A′ ⇨ A′⇒B) ⇨* B⇒C = A⇒A′ ⇨ (A′⇒B ⇨* B⇒C)

-- Concatenation of term reduction closures
_⇨∷*_ : ∀ {Γ A t u r} → Γ ⊢ t ⇒* u ∷ A → Γ ⊢ u ⇒* r ∷ A → Γ ⊢ t ⇒* r ∷ A
id ⊢u ⇨∷* u⇒r = u⇒r
(t⇒t′ ⇨ t′⇒u) ⇨∷* u⇒r = t⇒t′ ⇨ (t′⇒u ⇨∷* u⇒r)

-- Conversion of reduction closures
conv* : ∀ {Γ A B t u} → Γ ⊢ t ⇒* u ∷ A → Γ ⊢ A ≡ B → Γ ⊢ t ⇒* u ∷ B
conv* (id x) A≡B = id (conv x A≡B)
conv* (x ⇨ d) A≡B = conv x A≡B ⇨ conv* d A≡B

-- Universe of reduction closures
univ* : ∀ {Γ A B} → Γ ⊢ A ⇒* B ∷ U → Γ ⊢ A ⇒* B
univ* (id x) = id (univ x)
univ* (x ⇨ A⇒B) = univ x ⇨ univ* A⇒B

-- Application substitution of reduction closures
app-subst* : ∀ {Γ A B t t′ a} → Γ ⊢ t ⇒* t′ ∷ Π A ▹ B → Γ ⊢ a ∷ A
           → Γ ⊢ t ∘ a ⇒* t′ ∘ a ∷ B [ a ]
app-subst* (id x) a₁ = id (x ∘ⱼ a₁)
app-subst* (x ⇨ t⇒t′) a₁ = app-subst x a₁ ⇨ app-subst* t⇒t′ a₁


text:
open import Agda.Primitive

variable
  A : Set _

levelOf : A → Level
levelOf {a} _ = a

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Structures

open import Data.String using (String; _≈?_)
open import Data.List as L using (List; []; _∷_; [_])
open import Data.List.Categorical
open import Data.Nat as ℕ using (ℕ; zero; suc; _+_)
import Data.Nat.Properties as ℕ
open import Data.Nat.DivMod
open import Agda.Builtin.Nat using (div-helper; mod-helper)
open import Data.Nat.Show using () renaming (show to showNat)
open import Data.Vec as V using (Vec; []; _∷_)
open import Data.Fin as F using (Fin; zero; suc; #_)

open import Category.Monad
open import Category.Monad.State

open import Data.Product as Σ
open import Data.Unit
open import Data.Bool using (Bool; true; false; if_then_else_)
open import Data.Maybe using (Maybe; just; nothing)
open import Data.Fin using (Fin; zero; suc; fromℕ<)

open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; subst)
open import Relation.Nullary

open import Reflection hiding (return; _>>=_; _>>_)
open import Reflection.Term
import      Reflection.Name as RN
open import Function
open import Strict

open RawMonad ⦃ ... ⦄

Id = String

data Op : Set where
  Plus Minus Times Divide Eq Neq And Gt Lt : Op

data Expr : Set where
  Nat : ℕ → Expr
  BinOp : Op → Expr → Expr → Expr
  Var : String → Expr
  Call : Id → List Expr → Expr
  Function : Id → List Id → Expr → Expr
  Extern : Id → List Id → Expr
  Let : Id → Expr → Expr → Expr
  Assert : Expr → Expr
  If : Expr → Expr → Expr → Expr

op-to-string : Op → String
op-to-string Plus = "+"
op-to-string Minus = "-"
op-to-string Times = "*"
op-to-string Divide = "/"
op-to-string Eq = "=="
op-to-string Neq = "!="
op-to-string And = "&&"
op-to-string Gt = ">"
op-to-string Lt = "<"

indent : ℕ → String
indent n = "" ++/ L.replicate n "  "

flatten-lets : List Expr → List (Id × Expr) × List Expr

-- Lift all the assigns from the (potentially) nested let
flatten-let : Expr → List (Id × Expr) × Expr
flatten-let (Let x e e₁) = let a₁ , e = flatten-let e
                               a₂ , e₁ = flatten-let e₁
                           in (a₁ ++ [(x , e)] ++ a₂) , e₁
flatten-let e@(Nat _) = [] , e
flatten-let (BinOp x e e₁) = let a  , e = flatten-let e
                                 a₁ , e₁ = flatten-let e₁
                             in (a ++ a₁) , BinOp x e e₁
flatten-let e@(Var _) = [] , e
flatten-let (Call x es) = let as , es' = flatten-lets es
                          in as , Call x es'
flatten-let (Function x args e) = let a , e = flatten-let e
                                  in [] , (Function x args $ L.foldr (uncurry Let) e a)
flatten-let e@(Extern _ _) = [] , e
flatten-let (Assert e) = let a , e = flatten-let e in a , Assert e

flatten-let (If e e₁ e₂) = let a , e = flatten-let e
                               a₁ , e₁ = flatten-let e₁
                               a₂ , e₂ = flatten-let e₂
                               e₁' = L.foldr (uncurry Let) e₁ a₁
                               e₂' = L.foldr (uncurry Let) e₂ a₂
                           in a , (If e e₁' e₂')

flatten-lets [] = [] , []
flatten-lets (e ∷ es) = let a , e = flatten-let e
                            a₁ , es = flatten-lets es
                        in (a ++ a₁) , (e ∷ es)

{-# TERMINATING #-}
expr-to-string : ℕ → Expr → String
expr-to-string ind (Nat x) = indent ind
                          ++ showNat x
expr-to-string ind (BinOp op e e₁) = indent ind ++ "(" ++ expr-to-string 0 e ++ ") " ++ op-to-string op ++ " (" ++ expr-to-string 0 e₁ ++ ")"
expr-to-string ind (Var x) = indent ind
                          ++ x
expr-to-string ind (Call f args) = indent ind
                                ++ f ++ " (" ++ (", " ++/ L.map (expr-to-string 0) args) ++ ")"
expr-to-string ind (Function n ids e) = indent ind
                                     ++ "def " ++ n ++ "(" ++ (", " ++/ ids) ++ "):\n" ++ expr-to-string (ind + 1) e
expr-to-string ind (Extern n ids) = indent ind
                                 ++ "extern def " ++ n ++ " (" ++ (", " ++/ ids) ++ ")"

expr-to-string ind (Let x e@(If _ _ _) e₁) = indent ind
                               ++ "let " ++ x ++ " =\n"
                               ++ expr-to-string (ind + 1) e ++ "\n"
                               ++ expr-to-string ind e₁
expr-to-string ind (Let x e e₁) = indent ind
                               ++ "let " ++ x ++ " = " ++ expr-to-string 0 e ++ "\n"
                               ++ expr-to-string ind e₁
expr-to-string ind (Assert e) = indent ind
                             ++ "assert (" ++ expr-to-string 0 e ++ ")"
expr-to-string ind (If e e₁ e₂) = indent ind
                               ++ "if " ++ expr-to-string 0 e ++ ":\n"
                               ++ expr-to-string (ind + 1) e₁ ++ "\n"
                               ++ indent ind ++ "else:\n"
                               ++ expr-to-string (ind + 1) e₂ ++ "\n"

-- Glorified sigma type for variable-assertion pairs
record Assrt : Set where
  constructor mk
  field v : Id
        a : Expr

Assrts = List Assrt

-- The state used when traversing a Pi type.
record PS : Set where
  field
    cnt : ℕ           -- The source of unique variable names
    cur : Id      -- Current variable name (used to collect assertions from its type)
    ctx : Telescope -- Names in the telscopes to resolve deBruijn indices
    ret : Id      -- Variable that the function returns as a result.
                      -- We assume that there is always a single variable and its name
                      -- is known upfront.  We need this to generate assertions from the
                      -- return type.
    assrts : Assrts   -- Assertions that we generate per each variable.
    kst : KS          -- Compilation state (in case we have to extract some functions used in types)

defaultPS : PS
defaultPS = record { cnt = 1
                   ; cur = ""
                   ; ctx = []
                   ; ret = "__ret"
                   ; assrts = []
                   ; kst = defaultKS
                   }

record PatSt : Set where
  constructor mk
  field
    vars    : List (String × ℕ) --Strings
    assigns : List (Id × Expr)
    conds   : List Expr
    cnt     : ℕ

defaultPatSt : PatSt
defaultPatSt = mk [] [] [] 1

SPS = State PS

kompile-fun    : Type → Term → Name → SKS $ Err Expr
kompile-pi     : Type → SPS $ Err ⊤
--{-# TERMINATING #-}
kompile-cls    : Clauses → (vars : Strings) → (ret : String) → SKS $ Err Expr
kompile-clpats : Telescope → (pats : List $ Arg Pattern) → (exprs : List Expr) → PatSt → Err PatSt
--{-# TERMINATING #-}
kompile-term   : Term → Telescope → SKS $ Err Expr

kompile-funp   : Type → Term → Name → SKS Prog
kompile-funp ty te n = do
  (ok e) ← kompile-fun ty te n where (error x) → return $ error x
  let a , e = flatten-let e
      e = case a of λ where
            [] → e
            a  → L.foldr (uncurry Let) e a
  return $ ok $ expr-to-string 0 e ++ "\n"

private
  kf : String → Err Expr
  kf x = error $ "kompile-fun: " ++ x

  module R = RawMonadState (StateMonadState KS)

kompile-fun ty (pat-lam [] []) n =
  return $ kf "got zero clauses in a lambda term"
kompile-fun ty (pat-lam cs []) n = do
  kst ← R.get
  let (_ , ps) = kompile-pi ty $ record defaultPS{ kst = kst }
      rv = PS.ret ps
      ns = showName n
      vars = L.map proj₁ $ PS.ctx ps
      args = ok $ ", " ++/ vars
      ret-assrts = list-filter (λ where (mk v _) → v ≈? rv) $ PS.assrts ps
      arg-assrts = list-filter (dec-neg λ where (mk v _) → v ≈? rv) $ PS.assrts ps
  R.put $ PS.kst ps
  (ok b) ← kompile-cls cs vars rv where (error x) → return $ error x
  return $! ok $ Function ns vars
              $ flip (L.foldr (λ where (mk v a) → Let (v ++ "_assrt") $ Assert a)) arg-assrts
              $ Let rv b
              $ flip (L.foldr (λ where (mk v a) → Let (v ++ "_assrt") $ Assert a)) ret-assrts
              $ Var rv

kompile-fun _ _ _ =
  return $ kf "expected pattern-matching lambda"

private
  kp : ∀ {X} → String → SPS (Err X)
  kp x = return $ error $ "kompile-pi: " ++ x

  ke : ∀ {X} → String → SPS (Err X)
  ke x = return $ error x

  module P = RawMonadState (StateMonadState PS)

  infixl 10 _p+=c_ _p+=a_
  _p+=c_ : PS → ℕ → PS
  ps p+=c n = record ps{ cnt = PS.cnt ps + n }

  _p+=a_ : PS → Assrt → PS
  ps p+=a a = record ps{ assrts = a ∷ PS.assrts ps }

  ps-fresh : String → SPS String
  ps-fresh x = do
    ps ← P.get
    P.modify (_p+=c 1)
    return $ x ++ showNat (PS.cnt ps)

  lift-ks : ∀ {X} → SKS X → SPS X
  lift-ks xf sps = let (x , sks) = xf (PS.kst sps) in x , record sps {kst = sks}

  sps-kompile-term : Term → SPS $ Err Expr
  sps-kompile-term t = do
    ps ← P.get
    lift-ks $ kompile-term t (PS.ctx ps)

kompile-ty : Type → (pi-ok : Bool) → SPS (Err ⊤)
kompile-ty (Π[ s ∶ arg i x ] y) false = kp "higher-order functions are not supported"
kompile-ty (Π[ s ∶ ty@(arg i x) ] y) true  = do
    v ← ps-fresh "x_"
    P.modify λ k → record k { cur = v }
    (ok t) ← kompile-ty x false
      where e → return e
    P.modify λ k → record k { cur = PS.ret k  -- In case this is a return type
                            ; ctx = PS.ctx k ++ L.[(v , ty)] }
    kompile-ty y true

kompile-ty (con c args) pi-ok =
  kp $ "don't know how to handle `" ++ showName c ++ "` constructor"
kompile-ty (def (quote ℕ) args) _ = return $ ok tt
kompile-ty (def (quote Bool) args) _ = return $ ok tt
kompile-ty (def (quote Fin) (arg _ x ∷ [])) _ = do
  ok p ← sps-kompile-term x where error x → ke x
  v ← PS.cur <$> P.get
  P.modify $ _p+=a (mk v (BinOp Lt (Var v) p))
  return $ ok tt

kompile-ty (def (quote _≡_) (_ ∷ arg _ ty ∷ arg _ x ∷ arg _ y ∷ [])) _ = do
  ok x ← sps-kompile-term x where error x → ke x
  ok y ← sps-kompile-term y where error x → ke x
  v ← PS.cur <$> P.get
  P.modify $ _p+=a (mk v (BinOp Eq x y))
  return $ ok tt

kompile-ty (def (quote Dec) (_ ∷ arg _ p ∷ [])) _ = do
  --_ ← kompile-ty p false
  return $ ok tt

kompile-ty (def n _) _ = kp $ "cannot handle `" ++ showName n ++ "` type"

kompile-ty t _ =
  kp $ "failed with the term `" ++ showTerm t ++ "`"

kompile-pi x = kompile-ty x true

-- The names in the telescopes very oftern are not unique, which
-- would be pretty disasterous if the code generation relies on them.
-- see https://github.com/agda/agda/issues/5048 for more details.
--
-- This function simply ensures that variable names are unique in
-- in the telescope.
tel-rename : Telescope → (db : List (String × ℕ)) → Telescope
tel-rename [] db = []
tel-rename ((v , ty) ∷ tel) db with list-find-el ((_≈? v) ∘ proj₁) db
... | just (_ , n) = (v ++ "_" ++ showNat n , ty)
                     ∷ tel-rename tel (list-update-fst ((_≈? v) ∘ proj₁) db (Σ.map₂ suc))
... | nothing      = (v , ty)
                     ∷ tel-rename tel ((v , 1) ∷ db)

private
  kc : String → SKS $ Err Expr
  kc x = return $ error $ "kompile-cls: " ++ x

  _>>=e_ : ∀ {a}{X : Set a} → Err X → (X → SKS $ Err Expr) → SKS $ Err Expr
  (error s) >>=e _ = return $ error s
  (ok x)    >>=e f = f x

kompile-tel : Telescope → SPS (Err ⊤)
kompile-tel [] = return $ ok tt
kompile-tel ((v , t@(arg i x)) ∷ tel) = do
  (ok τ) ← kompile-ty x false where (error x) → return $ error x
  P.modify λ k → record k{ ctx = PS.ctx k ++ [( v , t )] }
  kompile-tel tel

fold-expr : (Expr → Expr → Expr) → Expr → List Expr → Expr
fold-expr f e [] = e
fold-expr f _ (x ∷ []) = x
fold-expr f e (x ∷ xs) = f x (fold-expr f e xs)

emap : ∀ {a b}{X : Set a}{Y : Set b} → (X → Y) → Err X → Err Y
emap f (error x) = error x
emap f (ok x) = ok $ f x

emap₂ : ∀ {a b c}{X : Set a}{Y : Set b}{Z : Set c}
      → (X → Y → Z) → Err X → Err Y → Err Z
emap₂ f (error x) _ = error x
emap₂ f _ (error x) = error x
emap₂ f (ok x) (ok y) = ok (f x y)

kompile-cls [] ctx ret = kc "zero clauses found"
kompile-cls (clause tel ps t ∷ []) ctx ret =
  -- Make telscope names unique.
  let tel = (tel-rename $! tel) $! [] in
  kompile-clpats tel ps (L.map Var ctx) defaultPatSt >>=e λ pst → do
  let (mk vars assgns _ _) = pst --in
  ok t ← kompile-term t $! tel where (error x) → kc x
  let as = flip (L.foldr (uncurry Let)) assgns
  return $ ok $ as
              $ t
              --Let ret t
              --$ Var ret

kompile-cls (absurd-clause tel ps ∷ []) ctx ret =
  -- Exactly the same as above
  -- We don't really need to make this call, but we keep it
  -- for sanity checks.  I.e. if we'll get an error in the
  -- patterns, it will bubble up to the caller.
  kompile-clpats ((tel-rename $! tel) $! []) ps (L.map Var ctx) defaultPatSt >>=e λ pst → do
  return $ ok $ Assert (Nat 0)

kompile-cls (absurd-clause tel ps ∷ ts@(_ ∷ _)) ctx ret =
  kompile-clpats ((tel-rename $! tel) $! []) ps (L.map Var ctx) defaultPatSt >>=e λ pst → do
  let (mk vars _ conds _) = pst
      cs = fold-expr (BinOp And) (Nat 1) conds
  ok r ← kompile-cls ts ctx ret where (error x) → kc x
  return $ ok $ If cs (Assert (Nat 0)) r

kompile-cls (clause tel ps t ∷ ts@(_ ∷ _)) ctx ret =
  kompile-clpats ((tel-rename $! tel) $! []) ps (L.map Var ctx) defaultPatSt >>=e λ pst → do
  let (mk vars assgns conds _) = pst
      cs = fold-expr (BinOp And) (Nat 1) conds
      as = flip (L.foldr (uncurry Let)) assgns
  --ok t ← kompile-term t tel where (error x) → kc x
  --ok r ← kompile-cls ts ctx ret where (error x) → kc x
  --return $ ok $ If cs (as t) r
  t ← kompile-term t tel
  r ← kompile-cls ts ctx ret
  return $ emap₂ (If cs) (emap as t) r

tel-lookup-name : Telescope → ℕ → Prog
tel-lookup-name tel n with n ℕ.<? L.length (L.reverse tel)
... | yes n<l = ok $ proj₁ $ L.lookup (L.reverse tel) $ fromℕ< n<l
... | no _ = error "Variable lookup in telescope failed"

private
  kcp : String → Err PatSt
  kcp x = error $ "kompile-clpats: " ++ x

  infixl 10 _+=c_ _+=a_ _+=v_ _+=n_
  _+=c_ : PatSt → Expr → PatSt
  p +=c c = record p { conds = PatSt.conds p ++ [ c ] }

  _+=a_ : PatSt → _ → PatSt
  p +=a a = record p { assigns = PatSt.assigns p ++ [ a ] }

  _+=v_ : PatSt → String × ℕ → PatSt
  p +=v v = record p { vars = PatSt.vars p ++ [ v ] }

  _+=n_ : PatSt → ℕ → PatSt
  p +=n n = record p { cnt = PatSt.cnt p + 1 }

  pst-fresh : PatSt → String → Err $ String × PatSt
  pst-fresh pst x =
    return $ x ++ showNat (PatSt.cnt pst) , pst +=n 1

  sz : List $ Arg Pattern → ℕ
  sz [] = 0
  sz (arg i (con c ps) ∷ l) = 1 + sz ps + sz l
  sz (arg i _ ∷ l) = 1 + sz l

  sz++ : ∀ (a b : List $ Arg Pattern) → sz (a L.++ b) ≡ sz a + sz b
  sz++ [] b = refl
  sz++ (arg i (con c ps) ∷ a) b rewrite ℕ.+-assoc (sz ps) (sz a) (sz b)
    = cong suc (cong (sz ps +_) (sz++ a b))
  sz++ (arg i (dot t) ∷ a) b = cong suc $ sz++ a b
  sz++ (arg i (var x₁) ∷ a) b = cong suc $ sz++ a b
  sz++ (arg i (lit l) ∷ a) b = cong suc $ sz++ a b
  sz++ (arg i (proj f) ∷ a) b = cong suc $ sz++ a b
  sz++ (arg i (absurd x₁) ∷ a) b = cong suc $ sz++ a b

  ++-strict : ∀ {X : Set} (a b : List X) → a ++ b ≡ a L.++ b
  ++-strict a b rewrite force′-≡ a L._++_ | force′-≡ b (L._++_ a) = refl

  ps++l<m : ∀ {m} ps l → suc (sz ps + sz l) ℕ.< suc m → sz (ps ++ l) ℕ.< m
  ps++l<m {m} ps l sz<m rewrite ++-strict ps l = subst (ℕ._< m) (sym $ sz++ ps l) (ℕ.≤-pred sz<m)

  a<b⇒a<1+b : ∀ {a b} → a ℕ.< b → a ℕ.< 1 + b
  a<b⇒a<1+b {a} {b} a<b = ℕ.s≤s (ℕ.<⇒≤ a<b)

  a+b<c⇒b<c : ∀ {a b c} → a + b ℕ.< c → b ℕ.< c
  a+b<c⇒b<c {zero} {b} {c} a+b<c = a+b<c
  a+b<c⇒b<c {suc a} {b} {suc c} a+b<c = a<b⇒a<1+b $ a+b<c⇒b<c (ℕ.≤-pred a+b<c)

  sz[l]<m : ∀ {m} ps l → suc (sz ps + sz l) ℕ.< suc m → sz l ℕ.< m
  sz[l]<m {m} ps l sz<m = a+b<c⇒b<c $ ℕ.≤-pred sz<m

--kompile-cls    : Clauses → (vars : Strings) → (ret : String) → SKS $ Err String

kompile-clpats′ : ∀ {m} → Telescope → (pats : List $ Arg Pattern) → .(sz pats ℕ.< m)
               → (exprs : List Expr) → PatSt → Err PatSt

kompile-clpats′ {suc m} tel (arg i (con (quote true) ps) ∷ l) sz<m (v ∷ ctx) pst =
  kompile-clpats′ tel l (sz[l]<m ps l sz<m) ctx $ pst +=c v {- != 0 -} --is true
kompile-clpats′ {suc m} tel (arg i (con (quote false) ps) ∷ l) sz<m (v ∷ ctx) pst =
  kompile-clpats′ tel l (sz[l]<m ps l sz<m) ctx $ pst +=c BinOp Eq v (Nat 0)

kompile-clpats′ {suc m} tel (arg i (con (quote ℕ.zero) ps) ∷ l) sz<m (v ∷ ctx) pst =
  kompile-clpats′ tel l (sz[l]<m ps l sz<m) ctx $ pst +=c BinOp Eq v (Nat 0) --(v == 0)
kompile-clpats′ {suc m} tel (arg i (con (quote ℕ.suc) ps) ∷ l) sz<m (v ∷ ctx) pst =
  kompile-clpats′ tel (ps ++ l) (ps++l<m ps l sz<m) (BinOp Minus v (Nat 1) ∷ ctx) $ pst +=c BinOp Gt v (Nat 0) --(v > 0)

kompile-clpats′ {suc m} tel (arg i (con (quote F.zero) ps) ∷ l) sz<m (v ∷ ctx) pst =
  kompile-clpats′ tel l (sz[l]<m ps l sz<m) ctx $ pst +=c BinOp Eq v (Nat 0) --(v ++ " == 0")
kompile-clpats′ {suc m} tel (arg i (con (quote F.suc) ps@(_ ∷ _ ∷ [])) ∷ l) sz<m (v ∷ ctx) pst = do
  (ub , pst) ← pst-fresh pst "ub_"
  -- XXX here we are not using `ub` in conds.  For two reasons:
  -- 1) as we have assertions, we should check the upper bound on function entry
  -- 2) typically, the value of this argument would be Pat.dot, which we ignore
  --    right now.  It is possible to capture the value of the dot-patterns, as
  --    they carry the value when reconstructed.
  kompile-clpats′ tel (ps ++ l) (ps++l<m ps l sz<m) (Var ub ∷ (BinOp Minus v (Nat 1)) ∷ ctx) $ pst +=c BinOp Gt v (Nat 0) --(v ++ " > 0")

-- For refl we don't need to generate a predicate, as refl is an element of a singleton type.
kompile-clpats′ {suc m} tel (arg i (con (quote refl) ps) ∷ l) sz<m (v ∷ ctx) pst =
  kompile-clpats′ tel l (sz[l]<m ps l sz<m) ctx pst

kompile-clpats′ {suc m} tel (arg i (con (quote _because_) ps) ∷ l) sz<m (v ∷ ctx) pst = do
  pf , pst ← pst-fresh pst $ "pf_"
  kompile-clpats′ tel (ps ++ l) (ps++l<m ps l sz<m) (v ∷ Var pf ∷ ctx) pst
kompile-clpats′ {suc m} tel (arg i (con (quote Reflects.ofʸ) ps) ∷ l) sz<m (v ∷ ctx) pst =
  kompile-clpats′ tel (ps ++ l) (ps++l<m ps l sz<m) (Nat 1 ∷ ctx) pst
kompile-clpats′ {suc m} tel (arg i (con (quote Reflects.ofⁿ) ps) ∷ l) sz<m (v ∷ ctx) pst =
  kompile-clpats′ tel (ps ++ l) (ps++l<m ps l sz<m) (Nat 0 ∷ ctx) pst

kompile-clpats′ {suc m} tel (arg (arg-info _ r) (var i) ∷ l) sz<m (v ∷ vars) pst = do
  s ← tel-lookup-name tel i
  let pst = pst +=v (s , i)
  let pst = if does (s ≈? "_")
            then pst
            else pst +=a (s , v)
  kompile-clpats′ tel l (ℕ.≤-pred sz<m) vars pst

kompile-clpats′ {suc m} tel (arg i (dot t) ∷ l) sz<m (v ∷ vars) pst =
  -- For now we just skip dot patterns.
  kompile-clpats′ tel l (ℕ.≤-pred sz<m) vars pst

kompile-clpats′ {suc m} tel (arg i (absurd _) ∷ l) sz<m (v ∷ ctx) pst =
  -- If have met the absurd pattern, we'd still have to
  -- accumulate remaining conditions, as patterns are not
  -- linear :(  For example, see test4-f in examples.
  kompile-clpats′ tel l (ℕ.≤-pred sz<m) ctx pst

kompile-clpats′ _ [] _ [] pst = ok pst

kompile-clpats′ tel ps _ ctx patst = kcp $ "failed on pattern: ["
                                     ++ (", " ++/ L.map (λ where (arg _ x) → showPattern x) ps)
                                     ++ "], ctx: [" ++ (", " ++/ (L.map (expr-to-string 0) ctx)) ++ "]"

kompile-clpats tel pats ctx pst = kompile-clpats′ {m = suc (sz pats)} tel pats ℕ.≤-refl ctx pst

private
  kt : ∀ {X} → String → SKS $ Err X
  kt x = return $ error $ "kompile-term: " ++ x

mk-mask : (n : ℕ) → List $ Fin n
mk-mask zero =    []
mk-mask (suc n) = L.reverse $ go n (suc n) ℕ.≤-refl
  where
    sa<b⇒a<b : ∀ a b → suc a ℕ.< b → a ℕ.< b
    sa<b⇒a<b zero    (suc b) _        = ℕ.s≤s ℕ.z≤n
    sa<b⇒a<b (suc a) (suc n) (ℕ.s≤s pf) = ℕ.s≤s $ sa<b⇒a<b a n pf

    go : (m n : ℕ) → m ℕ.< n → List $ Fin n
    go 0       (suc _) _  = zero ∷ []
    go (suc m) n       pf = F.fromℕ< pf ∷ go m n (sa<b⇒a<b m n pf)

le-to-el : ∀ {a}{X : Set a} → List (Err X) → Err (List X)
le-to-el [] = ok []
le-to-el (x ∷ l) = _∷_ <$> x ⊛ le-to-el l

mk-iota-mask : ℕ → List ℕ
mk-iota-mask n = L.reverse $! go n []
  where
    go : ℕ → List ℕ → List ℕ
    go zero l = l
    go (suc n) l = n ∷ go n l

{-
kompile-arglist : (n : ℕ) → List $ Arg Term → List $ Fin n → Telescope → SKS $ Err (List Expr)
kompile-arglist n args mask varctx with L.length args ℕ.≟ n | V.fromList args
... | yes p | vargs rewrite p = do
                 l ← mapM (λ where (arg _ x) → kompile-term x varctx)
                          $ L.map (V.lookup vargs) mask
                 return $ le-to-el l
              where open TraversableM (StateMonad KS)

... | no ¬p | _ = kt "Incorrect argument mask"
-}

kompile-arglist-idx : List $ Arg Term → (idx : ℕ) → Telescope → SKS $ Err Expr
kompile-arglist-idx [] _ tel = return $ error "incorrect arglist index"
kompile-arglist-idx (arg _ x ∷ args) zero tel = kompile-term x tel
kompile-arglist-idx (x ∷ args) (suc n) tel = kompile-arglist-idx args n tel

kompile-arglist : List $ Arg Term → List ℕ → Telescope → SKS $ Err (List Expr)
kompile-arglist args [] tel = return $ ok []
kompile-arglist args (x ∷ idxs) tel = do
  ok t ← kompile-arglist-idx args x tel where (error x) → return $ error x
  ok ts ← kompile-arglist args idxs tel where (error x) → return $ error x
  return $ ok $ t ∷ ts

kompile-term (var x []) vars =
  return $ Var <$> tel-lookup-name vars x

kompile-term (var x args@(_ ∷ _)) vars = do
  let f = tel-lookup-name vars x
      l = L.length args
  --args ← kompile-arglist l args (mk-mask l) vars
  args ← kompile-arglist args (mk-iota-mask l) vars
  return $ Call <$> f ⊛ args

kompile-term (lit l@(nat x)) vars = return $ ok $ Nat x

kompile-term (con (quote ℕ.zero) _) _ =
  return $ ok $ Nat 0
kompile-term (con (quote ℕ.suc) (arg _ a ∷ [])) vars = do
  a ← kompile-term a vars
  return $ BinOp <$> ok Plus ⊛ ok (Nat 1) ⊛ a

kompile-term (con (quote F.zero) _) _ =
  return $ ok $ Nat 0
kompile-term (con (quote F.suc) (_ ∷ arg _ a ∷ [])) vars = do
  a ← kompile-term a vars
  return $ BinOp <$> ok Plus ⊛ ok (Nat 1) ⊛ a

kompile-term (con (quote refl) _) _ =
  return $ ok $ Nat 1

kompile-term (con c _) vars  = kt $ "don't know constructor " ++ (showName c)

-- From Agda.Builtin.Nat: div-helper k m n j = k + (n + m - j) div (1 + m)
kompile-term (def (quote div-helper) (arg _ k ∷ arg _ m ∷ arg _ n ∷ arg _ j ∷ [])) vars = do
  k ← kompile-term k vars
  m ← kompile-term m vars
  n ← kompile-term n vars
  j ← kompile-term j vars
  let n+m = BinOp <$> ok Plus ⊛ n ⊛ m
      n+m-j = BinOp <$> ok Minus ⊛ n+m ⊛ j
      k+[n+m-j] = BinOp <$> ok Plus ⊛ k ⊛ n+m-j
      1+m = BinOp <$> ok Plus ⊛ ok (Nat 1) ⊛ m
  return $ BinOp <$> ok Divide ⊛ k+[n+m-j] ⊛ 1+m

kompile-term (def (quote ℕ._≟_) (arg _ a ∷ arg _ b ∷ [])) vars = do
  a ← kompile-term a vars
  b ← kompile-term b vars
  return $ BinOp <$> ok Eq ⊛ a ⊛ b

kompile-term (def (quote _+_) args@(arg _ a ∷ arg _ b ∷ [])) vars = do
  a ← kompile-term a vars
  b ← kompile-term b vars
  return $ BinOp <$> ok Plus ⊛ a ⊛ b

kompile-term (def (quote ℕ._*_) args@(arg _ a ∷ arg _ b ∷ [])) vars = do
  a ← kompile-term a vars
  b ← kompile-term b vars
  return $ BinOp <$> ok Times ⊛ a ⊛ b

kompile-term (def (quote F.fromℕ<) args) vars = do
  ok (x ∷ []) ← kompile-arglist args (0 ∷ []) vars
                where _ → kt "kopmile-arglist is broken"
  return $ ok x

-- The last pattern in the list of `def` matches
kompile-term (def n []) _ =
  kt $ "attempting to compile `" ++ showName n ++ "` as function with 0 arguments"

kompile-term (def n args@(_ ∷ _)) vars = do
  R.modify λ k → record k { funs = KS.funs k ++ [ n ] }
  let n = {-nnorm $-} showName n
      l = L.length args
  --args ← kompile-arglist l args (mk-mask l) vars
  args ← kompile-arglist args (mk-iota-mask l) vars
  return $ Call <$> ok n ⊛ args

kompile-term t vctx = kt $ "failed to compile term `" ++ showTerm t ++ "`"

max_stars_repo_name: ashinkarov/agda-extractor

max_issues_repo_name: ashinkarov/agda-extractor

max_forks_repo_name: ashinkarov/agda-extractor


text:
F : {_ : Set₁} → Set₁
F {A} = A


text:
module Jumble where

open import Basics

swap : {I J : Set} -> I * J -> J * I
swap (i , j) = j , i

_+L_ : {X : Set} -> List X -> List X -> List X
[] +L ys = ys
(x ,- xs) +L ys = x ,- (xs +L ys)
infixr 4 _+L_

catNatural : {X Y : Set}(f : X -> Y)(xs xs' : List X) ->
  (list f xs +L list f xs') == list f (xs +L xs')
catNatural f [] xs' = refl (list f xs')
catNatural f (x ,- xs) xs' = refl (f x ,-_) =$= catNatural f xs xs'

listlist : {X Y Z : Set}(f : Y -> Z)(g : X -> Y)(h : X -> Z)
  (q : (x : X) -> f (g x) == h x) ->
  (xs : List X) -> list f (list g xs) == list h xs
listlist f g h q [] = refl []
listlist f g h q (x ,- xs) = refl (_,-_) =$= q x =$= listlist f g h q xs

_-:>_ : {I : Set} -> (I -> Set) -> (I -> Set) -> (I -> Set)
(S -:> T) i = S i -> T i
infixr 4 _-:>_

[_] : {I : Set} -> (I -> Set) -> Set
[ P ] = forall i -> P i

All : {X : Set} -> (X -> Set) -> (List X -> Set)
All P [] = One
All P (x ,- xs) = P x * All P xs

allPu : forall {X}{T : X -> Set} -> [ T ] -> [ All T ]
allPu t [] = <>
allPu t (x ,- xs) = t x , allPu t xs

allAp : forall {X}{S T : X -> Set} -> [ All (S -:> T) -:> All S -:> All T ]
allAp [] <> <> = <>
allAp (x ,- xs) (f , fs) (s , ss) = f s , allAp xs fs ss

all : {X : Set}{S T : X -> Set} ->
      [ S -:> T ] -> [ All S -:> All T ]
all f xs = allAp xs (allPu f xs)

allRe : forall {X Y}(f : X -> Y){P : Y -> Set}
        (xs : List X) -> All (\ x -> P (f x)) xs -> All P (list f xs)
allRe f [] <> = <>
allRe f (x ,- xs) (p , ps) = p , allRe f xs ps

collect : {I J : Set}(is : List I) -> All (\ i -> List J) is -> List J
collect [] <> = []
collect (i ,- is) (js , jss) = js +L collect is jss

allRePu : forall {X Y}(f : X -> Y){P : Y -> Set}(xs : List X)(g : [ P ]) ->
  allRe f xs (allPu (\ x -> g (f x)) xs) == allPu g (list f xs)
allRePu f [] g = refl <>
allRePu f (x ,- xs) g = refl (g (f x) ,_) =$= allRePu f xs g

all-Pu : forall {X}{S T : X -> Set}(f : [ S -:> T ])(s : [ S ])(xs : List X) ->
  all f xs (allPu s xs) == allPu (\ x -> f x (s x)) xs
all-Pu f s [] = refl <>
all-Pu f s (x ,- xs) = refl (f x (s x) ,_) =$= all-Pu f s xs

cart : forall {I J} -> List I -> List J -> List (I * J)
cart [] js = []
cart (i ,- is) js = list (i ,_) js +L cart is js

{-
all-grr : forall {X Y}{S : X -> Set}{T : Y -> Set}
  (f : X -> Y)(xs : List X)(g : [ S -:> (\ x -> T (f x)) ])(h : [ S ]) ->
  allAp (list f xs) (allPu g ?) (allRe f xs (allPu h xs)) ==
  ?
all-grr = ?
-}

data _<[_]>_ {X : Set} : List X -> List X -> List X -> Set where
  sz : [] <[ [] ]> []
  sl : forall {l ls ms rs} -> ls <[ ms ]> rs -> (l ,- ls) <[ l ,- ms ]> rs
  sr : forall {r ls ms rs} -> ls <[ ms ]> rs -> ls <[ r ,- ms ]> (r ,- rs)

riffle : {X : Set}{ls ms rs : List X} -> ls <[ ms ]> rs ->
         {P : X -> Set} -> All P ls -> All P rs -> All P ms
riffle sz <> <> = <>
riffle (sl x) (p , lp) rp = p , riffle x lp rp
riffle (sr x) lp (p , rp) = p , riffle x lp rp

srs : forall {X : Set}(xs : List X) -> [] <[ xs ]> xs
srs [] = sz
srs (x ,- xs) = sr (srs xs)

slrs : forall {X : Set}(xs ys : List X) -> xs <[ xs +L ys ]> ys
slrs [] ys = srs ys
slrs (x ,- xs) ys = sl (slrs xs ys)

cat : forall {X}{P : X -> Set}(xs ys : List X) -> All P xs -> All P ys -> All P (xs +L ys)
cat xs ys ps qs = riffle (slrs xs ys) ps qs

data IsRiffle {X : Set}{ls ms rs : List X}(i : ls <[ ms ]> rs){P : X -> Set}
  : All P ms -> Set where
  mkRiffle : (lp : All P ls)(rp : All P rs) -> IsRiffle i (riffle i lp rp)
isRiffle : {X : Set}{ls ms rs : List X}(i : ls <[ ms ]> rs){P : X -> Set}(mp : All P ms) -> IsRiffle i mp
isRiffle sz <> = mkRiffle <> <>
isRiffle (sl i) (p , mp) with isRiffle i mp
isRiffle (sl i) (p , .(riffle i lp rp)) | mkRiffle lp rp = mkRiffle (p , lp) rp
isRiffle (sr i) (p , mp) with isRiffle i mp
isRiffle (sr i) (p , .(riffle i lp rp)) | mkRiffle lp rp = mkRiffle lp (p , rp)

data _~_ {X : Set} : List X -> List X -> Set where
  [] : [] ~ []
  _,-_ : forall {x xs ys zs} -> (x ,- []) <[ ys ]> zs -> xs ~ zs -> (x ,- xs) ~ ys

permute : {X : Set}{xs ys : List X} -> xs ~ ys ->
          {P : X -> Set} -> All P xs -> All P ys
permute []        <> = <>
permute (i ,- is) (p , ps) = riffle i (p , <>) (permute is ps)

data SRS {X : Set}(ms : List X) : (xs : List X) -> [] <[ ms ]> xs -> Set where
  mkSRS : SRS ms ms (srs ms)

isSRS : {X : Set}{ms xs : List X}(i : [] <[ ms ]> xs) -> SRS ms xs i
isSRS sz = mkSRS
isSRS (sr i) with isSRS i
isSRS (sr .(srs _)) | mkSRS = mkSRS

mirror : {X : Set}{ls ms rs : List X} -> ls <[ ms ]> rs -> rs <[ ms ]> ls
mirror sz = sz
mirror (sl x) = sr (mirror x)
mirror (sr x) = sl (mirror x)

rotatel : {X : Set}{ls ms rs lrs rrs : List X} -> ls <[ ms ]> rs -> lrs <[ rs ]> rrs ->
  Sg (List X) \ ns -> (ls <[ ns ]> lrs) * (ns <[ ms ]> rrs)
rotatel sz sz = [] , sz , sz
rotatel (sl x) y with rotatel x y
... | _ , a , b = _ , sl a , sl b
rotatel (sr x) (sl y) with rotatel x y
... | _ , a , b = _ , sr a , sl b
rotatel (sr x) (sr y) with rotatel x y
... | _ , a , b = _ , a , sr b

rotater : {X : Set}{lls rls ls ms rs : List X} -> lls <[ ls ]> rls -> ls <[ ms ]> rs ->
  Sg (List X) \ ns -> (lls <[ ms ]> ns) * (rls <[ ns ]> rs)
rotater x y with rotatel (mirror y) (mirror x)
... | _ , a , b = _ , mirror b , mirror a

llswap : {X : Set}{ls ms lrs rrs : List X} ->
 (Sg (List X) \ rs -> (ls <[ ms ]> rs) * (lrs <[ rs ]> rrs)) ->
  Sg (List X) \ ns -> (lrs <[ ms ]> ns) * (ls <[ ns ]> rrs)
llswap (_ , x , y) with rotatel x y
... | _ , a , b = rotater (mirror a) b

reflP : {X : Set}(xs : List X) -> xs ~ xs
reflP [] = []
reflP (x ,- xs) = sl (srs xs) ,- reflP xs

insP : forall {X : Set}{x : X}{xs xs' ys ys'} -> (x ,- []) <[ xs' ]> xs -> (x ,- []) <[ ys' ]> ys
         -> xs ~ ys -> xs' ~ ys'
insP (sl i) j p with isSRS i
insP (sl .(srs _)) j p | mkSRS = j ,- p
insP (sr i) j (k ,- p) =
  let  _ , k' , j' = llswap (_ , j , k)
  in   k' ,- insP i j' p

l2r : forall {X : Set}{x : X}{xs xs' ys'}(i : (x ,- []) <[ xs' ]> xs)(p' : xs' ~ ys') ->
  Sg (List X) \ ys -> Sg ((x ,- []) <[ ys' ]> ys) \ j -> xs ~ ys
l2r (sl i) (j ,- p) with isSRS i
l2r (sl .(srs _)) (j ,- p) | mkSRS = _ , j , p
l2r (sr i) (k' ,- p') with l2r i p'
... | _ , j' , p with llswap (_ , k' , j')
... | _ , j , k = _ , j , (k ,- p)

transP : {X : Set}{xs ys zs : List X} -> xs ~ ys -> ys ~ zs -> xs ~ zs
transP [] [] = []
transP (i ,- p) q' with l2r i q'
... | _ , j , q = j ,- transP p q

symP : {X : Set}{xs ys : List X} -> xs ~ ys -> ys ~ xs
symP [] = []
symP (i ,- p) = insP i (sl (srs _)) (symP p)

_+L[] : {X : Set}(xs : List X) -> (xs +L []) == xs
[] +L[] = refl []
(x ,- xs) +L[] = refl (x ,-_) =$= (xs +L[])

assoc : {X : Set}(xs ys zs : List X) -> ((xs +L ys) +L zs) == (xs +L ys +L zs)
assoc [] ys zs = refl (ys +L zs)
assoc (x ,- xs) ys zs = refl (x ,-_) =$= assoc xs ys zs

insS : {X : Set}(xs : List X)(y : X)(zs : List X) -> (y ,- []) <[ (xs +L y ,- zs) ]> (xs +L zs)
insS [] y zs = sl (srs zs)
insS (x ,- xs) y zs = sr (insS xs y zs)

swapP : {X : Set}(xs ys : List X) -> (xs +L ys) ~ (ys +L xs)
swapP [] ys rewrite ys +L[] = reflP ys
swapP (x ,- xs) ys = insS ys x xs ,- swapP xs ys

catS : forall {X}{as abs bs cs cds ds : List X} ->
        as <[ abs ]> bs -> cs <[ cds ]> ds ->
        (as +L cs) <[ (abs +L cds) ]> (bs +L ds)
catS sz y = y
catS (sl x) y = sl (catS x y)
catS (sr x) y = sr (catS x y)

catP : forall {X : Set}{as bs cs ds : List X} -> as ~ cs -> bs ~ ds -> (as +L bs) ~ (cs +L ds)
catP [] q = q
catP (x ,- p) q = catS x (srs _) ,- catP p q

splimap : forall {X Y}(f : X -> Y){xs xys ys} -> xs <[ xys ]> ys ->
           list f xs <[ list f xys ]> list f ys
splimap f sz = sz
splimap f (sl s) = sl (splimap f s)
splimap f (sr s) = sr (splimap f s)

permap : forall {X Y}(f : X -> Y){xs xs' : List X} -> xs ~ xs' -> list f xs ~ list f xs'
permap f [] = []
permap f (x ,- p) = splimap f x ,- permap f p

cartNil : forall {I}(is : List I){J} -> cart {J = J} is [] == []
cartNil [] = refl []
cartNil (i ,- is) = cartNil is

cartCons : forall {I J}(is : List I)(j : J)(js : List J) ->
  cart is (j ,- js) ~ (list (_, j) is +L cart is js)
cartCons [] j js = []
cartCons (i ,- is) j js with catP (swapP (list (i ,_) js) (list (_, j) is)) (reflP (cart is js))
... | z rewrite assoc (list (i ,_) js) (list (_, j) is) (cart is js)
              | assoc (list (_, j) is) (list (i ,_) js) (cart is js)
  =
  (sl (srs (list (_, j) is +L cart (i ,- is) js))) ,-
  transP (catP (reflP (list (i ,_) js)) (cartCons is j js))
    z

cartLemma : forall {I J}(is : List I)(js : List J) ->
  cart is js ~ list swap (cart js is)
cartLemma {I}{J} [] js rewrite cartNil js {I} = []
cartLemma {I}{J} (i ,- is) js with catP (reflP (list (i ,_) js)) (cartLemma is js)
... | z rewrite sym (listlist swap (_, i) (i ,_) (\ j ->  refl (i , j)) js)
              | catNatural swap (list (_, i) js) (cart js is)
  = transP
  z
  (symP (permap (\ ji -> snd ji , fst ji) (cartCons js i is)))

record _|>_ (I O : Set) : Set1 where
  field
    Cuts   : O -> Set
    inners : {o : O} -> Cuts o -> List I

NatCut : Nat |> Nat
NatCut = record
  { Cuts = \ mn -> Sg Nat \ m -> Sg Nat \ n -> (m +N n) == mn
  ; inners = \ { (m , n , _) -> m ,- n ,- [] }
  }

module TENSOR where
  open _|>_
  _><_ : forall {I J} -> (I |> I) -> (J |> J) -> (I * J) |> (I * J)
  Cuts (C >< D) (i , j) = Cuts C i + Cuts D j
  inners (C >< D) {i , j} (inl c) = list (_, j) (inners C c)
  inners (C >< D) {i , j} (inr d) = list (i ,_) (inners D d)
open TENSOR

record Cutting {I O}(C : I |> O)(P : I -> Set)(o : O) : Set where
  constructor _8><_
  open _|>_ C
  field
    cut     : Cuts o
    pieces  : All P (inners cut)
infixr 3 _8><_
open Cutting public

module INTERIOR {I}(C : I |> I) where

  open _|>_ C

  data Interior (P : I -> Set)(i : I) : Set where
    tile : P i -> Interior P i
    <_>  : Cutting C (Interior P) i -> Interior P i

  ifold : forall {P Q} ->
          [ P -:> Q ] ->
          [ Cutting C Q -:> Q ] ->
          [ Interior P -:> Q ]
  ifolds : forall {P Q} ->
          [ P -:> Q ] ->
          [ Cutting C Q -:> Q ] ->
          [ All (Interior P) -:> All Q ]
  ifold pq cq i (tile p) = pq i p
  ifold pq cq i < c 8>< ps > = cq i (c 8>< ifolds pq cq _ ps)
  ifolds pq cq [] <> = <>
  ifolds pq cq (i ,- is) (x , xs) = ifold pq cq i x , ifolds pq cq is xs

  extend : forall {P Q} ->
          [ P -:> Interior Q ] ->
          [ Interior P -:> Interior Q ]
  extend k = ifold k (\ i x -> < x >)

  SubCut : (i : I)(c : Cuts i) -> Set
  SubCut i c = All (\ i -> One + Cuts i) (inners c)

  subCollect : (is : List I) -> All (\ i -> One + Cuts i) is -> List I
  subCollect is ds = collect is (all (\ i -> (\ _ -> i ,- []) <+> inners) is ds)

  subPieces : (i : I)(c : Cuts i) -> SubCut i c -> List I
  subPieces i c cs = subCollect (inners c) cs

  Recutter : Set
  Recutter = (i : I)(c c' : Cuts i) ->
             Sg (SubCut i c) \ d -> Sg (SubCut i c') \ d' ->
             subPieces i c d ~ subPieces i c' d'

  CutKit : (I -> Set) -> Set
  CutKit P = (i : I)(c : Cuts i) -> P i -> All P (inners c)

  module CHOP {P}(pc : CutKit P)(rec : Recutter) where

    glue : (is : List I) -> (d : All (\ i -> One + Cuts i) is) ->
              All (Interior P) (subCollect is d) -> All (Interior P) is
    glue [] <> <> = <>
    glue (i ,- is) (inl <> , ds) (p , ps) = p , glue is ds ps
    glue (i ,- is) (inr c , ds) ps with isRiffle (slrs (inners c) (subCollect is ds)) ps
    glue (i ,- is) (inr c , ds) .(riffle (slrs (inners c) (subCollect is ds)) lp rp)
      | mkRiffle lp rp = < c 8>< lp > , glue is ds rp

    chop : (i : I)(c c' : Cuts i)(ps : All (Interior P) (inners c)) -> All (Interior P) (inners c')
    chops : (is : List I) -> All (Interior P) is -> (d : All (\ i -> One + Cuts i) is) ->
              All (Interior P) (subCollect is d)
    chop i c c' ps with rec i c c'
    ... | d , d' , m with chops (inners c) ps d
    ... | qs = glue (inners c') d' (permute m qs)
    chops [] <> <> = <>
    chops (i ,- is) (p , ps) (inl <> , ds) = p , chops is ps ds
    chops (i ,- is) (tile p , ps) (inr c' , ds) =
      cat (inners c') (subCollect is ds) (all (\ _ -> tile) _ (pc i c' p)) (chops is ps ds)
    chops (i ,- is) (< c 8>< ps' > , ps) (inr c' , ds) = cat (inners c') (subCollect is ds)
                 (chop i c c' ps')
                 (chops is ps ds)

    mash : forall {Q} -> [ Interior (Interior P -:> Interior Q) -:> Interior P -:> Interior Q ]
    mash {Q} = ifold (\ i f -> f) help where
      help :  [ Cutting C (Interior P -:> Interior Q) -:> Interior P -:> Interior Q ]
      help i (c 8>< fs) (tile p) with pc i c p
      ... | ps = < c 8>< allAp (inners c) fs (all (\ _ -> tile) _ ps) >
      help i (c 8>< fs) < c' 8>< ps > = < c 8>< allAp (inners c) fs (chop i c' c ps) >

    mask : forall {O Q} -> [ O -:> Interior P -:> Interior Q ]
                        -> [ Interior O -:> Interior P -:> Interior Q ]
    mask {O}{Q} f = ifold f help where
      help :  [ Cutting C (Interior P -:> Interior Q) -:> Interior P -:> Interior Q ]
      help i (c 8>< fs) (tile p) with pc i c p
      ... | ps = < c 8>< allAp (inners c) fs (all (\ _ -> tile) _ ps) >
      help i (c 8>< fs) < c' 8>< ps > = < c 8>< allAp (inners c) fs (chop i c' c ps) >

  open CHOP public

  data Holey {I : Set}(P : I -> Set)(i : I) : Set where
    hole : Holey P i
    fill : P i -> Holey P i

  cutHole : forall {P : I -> Set} -> CutKit P -> CutKit (Holey P)
  cutHole f i c hole      = allPu (\ i -> hole) (inners c)
  cutHole f i c (fill p)  = all (\ _ -> fill) (inners c) (f i c p)

  superimpose : forall {P} -> CutKit P -> Recutter ->
                [ Interior (Holey P) -:> Interior (Holey P) -:> Interior (Holey P) ]
  superimpose pc rec = mask (cutHole pc) rec \
    { i hole     y -> y
    ; i (fill x) y -> tile (fill x)
    }

open INTERIOR

module SUBCOLLECTLEMMA where

  open _|>_

  subCollectLemma : forall {I J}(C : I |> I)(D : J |> J)
                    (f : I -> J)(g : (i : I) -> Cuts C i -> Cuts D (f i)) ->
                    (q : (i : I)(c : Cuts C i) -> inners D (g i c) == list f (inners C c)) ->
                    (is : List I)(ps : All (\ i -> One + Cuts C i) is) ->
                    subCollect D (list f is) (allRe f is (all (\ i -> id +map g i) is ps)) ==
                    list f (subCollect C is ps)
  subCollectLemma C D f g q [] <> = refl []
  subCollectLemma C D f g q (i ,- is) (inl <> , ps) =
    refl (f i ,-_) =$= subCollectLemma C D f g q is ps
  subCollectLemma C D f g q (i ,- is) (inr c , ps) =
    (inners D (g i c) +L
     subCollect D (list f is) (allRe f is (allAp is (allPu (\ i -> id +map g i) is) ps)))
      =[ refl _+L_ =$= q i c =$= subCollectLemma C D f g q is ps >=
    (list f (inners C c) +L list f (subCollect C is ps))
      =[ catNatural f (inners C c) (subCollect C is ps) >=
    list f (inners C c +L subCollect C is ps)
      [QED]

open SUBCOLLECTLEMMA

data CutCompare (x x' y y' n : Nat) : Set where
  cutLt : (d : Nat) -> (x +N suc d) == y -> (suc d +N y') == x' ->
    CutCompare x x' y y' n
  cutEq : x == y -> x' == y' ->
    CutCompare x x' y y' n
  cutGt : (d : Nat) -> (y +N suc d) == x -> (suc d +N x') == y' ->
    CutCompare x x' y y' n

sucInj : {x y : Nat} -> suc x == suc y -> x == y
sucInj (refl (suc _)) = refl _

cutCompare : (x x' y y' n : Nat) -> (x +N x') == n -> (y +N y') == n ->
             CutCompare x x' y y' n
cutCompare zero .n zero .n n (refl _) (refl _)
  = cutEq (refl _) (refl _)
cutCompare zero .(suc (y +N y')) (suc y) y' .(suc (y +N y')) (refl _) (refl _)
  = cutLt y (refl _) (refl _)
cutCompare (suc x) x' zero .(suc (x +N x')) .(suc (x +N x')) (refl _) (refl _)
  = cutGt x (refl _) (refl _)
cutCompare (suc x) x' (suc y) y' zero () ()
cutCompare (suc x) x' (suc y) y' (suc n) xq yq
  with cutCompare x x' y y' n (sucInj xq) (sucInj yq)
cutCompare (suc x) x' (suc .(x +N suc d)) y' (suc n) xq yq | cutLt d (refl _) bq
  = cutLt d (refl _) bq
cutCompare (suc x) x' (suc .x) y' (suc n) xq yq | cutEq (refl _) bq = cutEq (refl _) bq
cutCompare (suc .(y +N suc d)) x' (suc y) y' (suc n) xq yq | cutGt d (refl _) bq = cutGt d (refl _) bq

NatRecut : Recutter NatCut
NatRecut n (a , b , qab) (c , d , qcd) with cutCompare a b c d n qab qcd
NatRecut n (a , b , qab) (c , d , qcd) | cutLt e q0 q1 =
  (inl <> , inr (suc e , d , q1) , <>) , (inr (a , suc e , q0) , inl <> , <>) , reflP _
NatRecut n (a , b , qab) (.a , .b , qcd) | cutEq (refl .a) (refl .b) =
  (inl <> , inl <> , <>) , (inl <> , inl <> , <>) , reflP _
NatRecut n (a , b , qab) (c , d , qcd) | cutGt e q0 q1 =
  (inr (c , suc e , q0) , inl <> , <>) , (inl <> , inr (suc e , b , q1) , <>) , reflP _

module TENSORRECUT  {I J}(C : I |> I)(D : J |> J)(rec : Recutter C)(red : Recutter D) where
  open _|>_

  cartLeftLemma : (is : List I)(j : J)(d : Cuts D j) -> subCollect (C >< D) (list (_, j) is)
                (allRe (_, j) is
                   (allPu (\ _ -> inr (inr d)) is)) == cart is (inners D d)
  cartLeftLemma [] j d = refl []
  cartLeftLemma (i ,- is) j d = refl (list (i ,_) (inners D d) +L_) =$= cartLeftLemma is j d

  cartRightLemma : (i : I)(c : Cuts C i)(js : List J) ->
     subCollect (C >< D) (list (i ,_) js)
                 (allRe (i ,_) js (allPu (\ _ -> inr (inl c)) js)) ==
                 list swap (cart js (inners C c))
  cartRightLemma i c [] = refl []
  cartRightLemma i c (j ,- js)
    rewrite sym (catNatural swap (list (j ,_) (inners C c)) (cart js (inners C c)))
                | listlist swap (j ,_) (_, j) (\ i -> refl (i , j)) (inners C c)
                = refl (list (_, j) (inners C c) +L_) =$= cartRightLemma i c js

  TensorRecut : Recutter (C >< D)
  TensorRecut (i , j) (inl c) (inl c') with rec i c c'
  ... | x , y , m
      = allRe (_, j) (inners C c) (all (\ _ -> id +map inl) _ x)
      , allRe (_, j) (inners C c') (all (\ _ -> id +map inl) _ y)
      , lemma where
        lemma : subCollect (C >< D) (list (_, j) (inners C c))
                 (allRe (_, j) (inners C c) (all (\ _ -> id +map inl) (inners C c) x))
                ~
                subCollect (C >< D) (list (_, j) (inners C c'))
                 (allRe (_, j) (inners C c') (all (\ _ -> id +map inl) (inners C c') y))
        lemma rewrite subCollectLemma C (C >< D) (_, j) (\ _ -> inl) (\ i c -> refl _)
                        (inners C c) x
                    | subCollectLemma C (C >< D) (_, j) (\ _ -> inl) (\ i c -> refl _)
                        (inners C c') y
          = permap (_, j) m

  fst (TensorRecut (i , j) (inl c) (inr d)) =
    allRe (_, j) (inners C c) (allPu (\ i -> inr (inr d)) (inners C c))
  fst (snd (TensorRecut (i , j) (inl c) (inr d))) =
    allRe (i ,_) (inners D d) (allPu (\ i -> inr (inl c)) (inners D d))
  snd (snd (TensorRecut (i , j) (inl c) (inr d)))
    rewrite cartLeftLemma (inners C c) j d
          | cartRightLemma i c (inners D d)
          = cartLemma (inners C c) (inners D d)
  fst (TensorRecut (i , j) (inr d) (inl c)) =
    allRe (i ,_) (inners D d) (allPu (\ i -> inr (inl c)) (inners D d))
  fst (snd (TensorRecut (i , j) (inr d) (inl c))) =
    allRe (_, j) (inners C c) (allPu (\ i -> inr (inr d)) (inners C c))
  snd (snd (TensorRecut (i , j) (inr d) (inl c)))
    rewrite cartLeftLemma (inners C c) j d
          | cartRightLemma i c (inners D d)
          = symP (cartLemma (inners C c) (inners D d))
  TensorRecut (i , j) (inr d) (inr d') with red j d d'
  ... | x , y , m
    = allRe (i ,_) (inners D d) (all (\ _ -> id +map inr) _ x)
    , allRe (i ,_) (inners D d') (all (\ _ -> id +map inr) _ y)
    , lemma where
        lemma : subCollect (C >< D) (list (i ,_) (inners D d))
                 (allRe (i ,_) (inners D d) (all (\ _ -> id +map inr) (inners D d) x))
                ~
                subCollect (C >< D) (list (i ,_) (inners D d'))
                 (allRe (i ,_) (inners D d') (all (\ _ -> id +map inr) (inners D d') y))
        lemma rewrite subCollectLemma D (C >< D) (i ,_) (\ _ -> inr) (\ i d -> refl _)
                        (inners D d) x
                    | subCollectLemma D (C >< D) (i ,_) (\ _ -> inr) (\ i d -> refl _)
                        (inners D d') y
                    = permap (i ,_) m

open TENSORRECUT public

RectangleRecut : Recutter (NatCut >< NatCut)
RectangleRecut = TensorRecut NatCut NatCut NatRecut NatRecut

max_stars_repo_name: pigworker/InteriorDesign

max_issues_repo_name: pigworker/InteriorDesign

max_forks_repo_name: pigworker/InteriorDesign


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

module Cubical.Data.Strict2Group.Explicit.Path where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Group.Base
open import Cubical.Data.Strict2Group.Explicit.Base
open import Cubical.Data.Strict2Group.Explicit.Notation

S2G : (ℓ : Level) → Type (ℓ-suc ℓ)
S2G ℓ = Strict2GroupExp ℓ

S2GΣBase : (ℓ : Level) → Type (ℓ-suc ℓ)
S2GΣBase ℓ =
  Σ[ C₀ ∈ Group ℓ ]
  Σ[ C₁ ∈ Group ℓ ]
  Σ[ s ∈ morph C₁ C₀ ]
  Σ[ t ∈ morph C₁ C₀ ]
  Σ[ i ∈ morph C₀ C₁ ]
     ((g f : Group.type C₁) → s .fst g ≡ t .fst f → Group.type C₁) -- ∘

S2GΣRest : {ℓ : Level} → (S2GΣBase ℓ) → Type ℓ
S2GΣRest (C₀ , C₁ , s , t , i , ∘)
  = Σ[ si ∈ ((x : TC₀) → src (id x) ≡ x) ]
    Σ[ ti ∈ ((x : TC₀) → tar (id x) ≡ x) ]
    Σ[ s∘ ∈ ((g f : TC₁) → (coh : CohCond g f) → src (∘ g f coh) ≡ src f) ]
    Σ[ t∘ ∈ ((g f : TC₁) → (coh : CohCond g f) → tar (∘ g f coh) ≡ tar g) ]
    Σ[ isMorph∘ ∈ ({g f g' f' : TC₁} (c : CohCond g f) (c' : CohCond g' f') → ∘ (g ∙₁ g') (f ∙₁ f') (∙c c c') ≡ (∘ g f c) ∙₁ (∘ g' f' c')) ]
    Σ[ assoc∘ ∈ ({h g f : TC₁} → (c1 : CohCond g f) → (c2 : CohCond h g) → ∘ (∘ h g c2) f  ((s∘ h g c2) ∙ c1) ≡ ∘ h (∘ g f c1) (c2 ∙ (sym (t∘ g f c1)))) ]
    Σ[ lUnit∘ ∈ ((f : TC₁) → ∘ (id (tar f)) f (si (tar f)) ≡ f) ]
    ((f : TC₁) → ∘ f (id (src f)) (sym (ti (src f))) ≡ f) -- rUnit∘
    where open S2GBaseNotation C₀ C₁ s t i ∘

S2GΣ : (ℓ : Level) → Type (ℓ-suc ℓ)
S2GΣ ℓ = Σ[ X ∈ S2GΣBase ℓ ] (S2GΣRest X)

S2GΣ→S2G : {ℓ : Level} → S2GΣ ℓ → S2G ℓ
S2GΣ→S2G ((C₀ , C₁ , s , t , i , ∘) , (si , ti , s∘ , t∘ , isMorph∘ , assoc∘ , lUnit∘ , rUnit∘)) = strict2groupexp C₀ C₁ s t i ∘ si ti s∘ t∘ isMorph∘ assoc∘ lUnit∘ rUnit∘

-- Σ-type of data needed to define the type of PathPs between the base data for an S2G
S2GΣBase≡ : {ℓ : Level} → (SB SB' : S2GΣBase ℓ) → Type (ℓ-suc ℓ)
S2GΣBase≡
  (C₀ , C₁ , s , t , i , ∘ )
  (C₀' , C₁' , s' , t' , i' , ∘')
  = Σ[ p-C₀ ∈ (C₀ ≡ C₀') ]
    Σ[ p-C₁ ∈ (C₁ ≡ C₁') ]
    Σ[ p-s ∈ (PathP (λ j → morph (p-C₁ j) (p-C₀ j)) s s') ]
    Σ[ p-t ∈ (PathP (λ j → morph (p-C₁ j) (p-C₀ j)) t t') ]
    Σ[ p-i ∈ (PathP (λ j → morph (p-C₀ j) (p-C₁ j)) i i') ]
      (PathP (λ j → (g f : Group.type (p-C₁ j)) → (fst (p-s j)) g ≡ (fst (p-t j)) f → Group.type (p-C₁ j)) ∘ ∘') -- p∘

S2GΣRest≡ : {ℓ : Level} {SB SB' : S2GΣBase ℓ} (SR : S2GΣRest {ℓ = ℓ} SB) (SR' : S2GΣRest {ℓ = ℓ} SB') (pSB : S2GΣBase≡ {ℓ = ℓ} SB SB') → Type ℓ
S2GΣRest≡ {ℓ}
  {C₀ , C₁ , s , t , i , ∘}
  {C₀' , C₁' , s' , t' , i' , ∘'}
  (si , ti , s∘ , t∘ , isMorph∘ , assoc∘ , lUnit∘ , rUnit∘)
  (si' , ti' , s∘' , t∘' , isMorph∘' , assoc∘' , lUnit∘' , rUnit∘')
  (p-C₀ , p-C₁ , p-s , p-t , p-i , p∘)
  = Σ[ p-si ∈ (PathP (λ j → (x : Group.type (p-C₀ j)) → ((p-s j) .fst) (((p-i j) .fst) x) ≡ x) si si') ]
    Σ[ p-ti ∈ (PathP (λ j → (x : Group.type (p-C₀ j)) → ((p-t j) .fst) (((p-i j) .fst) x) ≡ x) ti ti') ]
    Σ[ p-s∘ ∈ (PathP (λ j → (g f : Group.type (p-C₁ j)) → (coh : (p-s j) .fst g ≡ (p-t j) .fst f) → (p-s j) .fst ((p∘ j) g f coh) ≡ (p-s j) .fst f) s∘ s∘') ]
    Σ[ p-t∘ ∈ (PathP (λ j → (g f : Group.type (p-C₁ j)) → (coh : (p-s j) .fst g ≡ (p-t j) .fst f) → (p-t j) .fst ((p∘ j) g f coh) ≡ (p-t j) .fst g) t∘ t∘') ]
    Σ[ p-isMorph∘ ∈ PathP
       (λ j → {g f g' f' : TC₁j j}
         (coh1 : CohCondj j g f)
         (coh2 : CohCondj j g' f')
           → (p∘ j) (∙₁j j g g') (∙₁j j f f') (∙cj j coh1 coh2) ≡ ∙₁j j (p∘ j g f coh1) (p∘ j g' f' coh2))
        isMorph∘ isMorph∘' ]
    Σ[ p-assococ∘ ∈ (PathP
       (λ j → {h g f : TC₁j j}
         (coh1 : CohCondj j g f)
         (coh2 : CohCondj j h g)
          → (p∘ j (p∘ j h g coh2) f (p-s∘ j h g coh2 ∙ coh1)) ≡ (p∘ j h (p∘ j g f coh1) (coh2 ∙ (sym (p-t∘ j g f coh1)))))
        assoc∘ assoc∘') ]
    Σ[ p-lUnit∘ ∈ (PathP
       (λ j → (f : TC₁j j)
         → p∘ j (idj j (tarj j f)) f (p-si j (tarj j f)) ≡ f)
       lUnit∘ lUnit∘') ]
        (PathP (λ j → (f : TC₁j j)
          → p∘ j f (idj j (srcj j f)) (sym (p-ti j (srcj j f))) ≡ f)
        rUnit∘ rUnit∘') -- p-rUnit∘
    where
      TC₁j = λ (j : I) → Group.type (p-C₁ j)
      TC₀j = λ (j : I) → Group.type (p-C₀ j)

      CohCondj : (j : I) (g f : TC₁j j) → Type ℓ
      CohCondj j g f = (p-s j) .fst g ≡ (p-t j) .fst f

      ∙₁j = λ (j : I) → isGroup.comp (Group.groupStruc (p-C₁ j))
      ∙₀j = λ (j : I) → isGroup.comp (Group.groupStruc (p-C₀ j))

      idj = λ (j : I) → fst (p-i j)
      srcj = λ (j : I) → fst (p-s j)
      tarj = λ (j : I) → fst (p-t j)
      src∙₁j = λ (j : I) → snd (p-s j)
      tar∙₁j = λ (j : I) → snd (p-t j)

      ∙cj : (j : I) → {g f g' f' : TC₁j j} → (c1 : CohCondj j g f) → (c2 : CohCondj j g' f') → (p-s j) .fst (∙₁j j g g') ≡ (p-t j) .fst (∙₁j j f f')
      ∙cj j {g} {f} {g'} {f'} c1 c2 =
        src∙₁j j g g' ∙
        cong (λ z → ∙₀j j z (srcj j g')) c1 ∙
        cong (λ z → ∙₀j j (tarj j f) z) c2 ∙
        sym (tar∙₁j j f f')

S2GR≡ : {ℓ : Level}
  {SB SB' : S2GΣBase ℓ} {SR : S2GΣRest {ℓ = ℓ} SB} {SR' : S2GΣRest {ℓ = ℓ} SB'}
  {pSB : S2GΣBase≡ {ℓ = ℓ} SB SB'} (pSR : S2GΣRest≡ {ℓ = ℓ} {SB = SB} {SB' = SB'} SR SR' pSB)
  → S2GΣ→S2G (SB , SR) ≡ S2GΣ→S2G (SB' , SR')
S2GR≡ {ℓ}
  {C₀ , C₁ , s , t , i , ∘} -- SB
  {C₀' , C₁' , s' , t' , i' , ∘'} --SB'
  {si , ti , s∘ , t∘} -- SR
  {si' , ti' , s∘' , t∘'} -- SR'
  {p-C₀ , p-C₁ , p-s , p-t , p-i , p∘} -- pSB
  (p-si , p-ti , p-s∘ , p-t∘ , p-isMorph∘ , p-assococ∘ , p-lUnit∘ , p-rUnit∘) j
  = strict2groupexp (p-C₀ j) (p-C₁ j) (p-s j) (p-t j) (p-i j) (p∘ j) (p-si j) (p-ti j) (p-s∘ j) (p-t∘ j) (p-isMorph∘ j) (p-assococ∘ j) (p-lUnit∘ j) (p-rUnit∘ j)

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


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

open import Categories.Category.Core

-- Idempotents and Split Idempotents
module Categories.Morphism.Idempotent {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level

open import Categories.Morphism 𝒞
open import Categories.Morphism.Reasoning 𝒞

open Category 𝒞
open HomReasoning

record Idempotent (A : Obj) : Set (ℓ ⊔ e) where
  field
    idem       : A ⇒ A
    idempotent : idem ∘ idem ≈ idem

record IsSplitIdempotent {A : Obj} (i : A ⇒ A) : Set (o ⊔ ℓ ⊔ e) where
  field
    {obj}    : Obj
    retract  : A ⇒ obj
    section  : obj ⇒ A
    retracts : retract ∘ section ≈ id
    splits   : section ∘ retract ≈ i

  retract-absorb : retract ∘ i ≈ retract
  retract-absorb = begin
    retract ∘ i                 ≈˘⟨ refl⟩∘⟨ splits ⟩
    retract ∘ section ∘ retract ≈⟨ cancelˡ retracts ⟩
    retract                     ∎

  section-absorb : i ∘ section ≈ section
  section-absorb = begin
    i ∘ section                   ≈˘⟨ splits ⟩∘⟨refl ⟩
    (section ∘ retract) ∘ section ≈⟨ cancelʳ retracts ⟩
    section                       ∎

  idempotent : i ∘ i ≈ i
  idempotent = begin
    i ∘ i                                     ≈˘⟨ splits ⟩∘⟨ splits ⟩
    (section ∘ retract) ∘ (section ∘ retract) ≈⟨ cancelInner retracts ⟩
    section ∘ retract                         ≈⟨ splits ⟩
    i                                         ∎

record SplitIdempotent (A : Obj) : Set (o ⊔ ℓ ⊔ e) where
  field
    idem : A ⇒ A
    isSplitIdempotent : IsSplitIdempotent idem

  open IsSplitIdempotent isSplitIdempotent public

-- All split idempotents are idempotent
SplitIdempotent⇒Idempotent : ∀ {A} → SplitIdempotent A → Idempotent A
SplitIdempotent⇒Idempotent Split = record { Split }
  where
    module Split = SplitIdempotent Split

module _ {A} {f : A ⇒ A} (S T : IsSplitIdempotent f) where
  private
    module S = IsSplitIdempotent S
    module T = IsSplitIdempotent T

  split-idempotent-unique : S.obj ≅ T.obj
  split-idempotent-unique = record
    { from = T.retract ∘ S.section
    ; to = S.retract ∘ T.section
    ; iso = record
      { isoˡ = begin
        (S.retract ∘ T.section) ∘ (T.retract ∘ S.section) ≈⟨ center T.splits ⟩
        S.retract ∘ f ∘ S.section                         ≈⟨ pullˡ S.retract-absorb ⟩
        S.retract ∘ S.section                             ≈⟨ S.retracts ⟩
        id                                                ∎
      ; isoʳ = begin
        (T.retract ∘ S.section) ∘ (S.retract ∘ T.section) ≈⟨ center S.splits ⟩
        T.retract ∘ f ∘ T.section                         ≈⟨ pullˡ T.retract-absorb ⟩
        T.retract ∘ T.section                             ≈⟨ T.retracts ⟩
        id                                                ∎
      }
    }


text:
-- {-# OPTIONS --verbose tc.proj.like:100 #-}

-- Apparently, there can be projection like functions working on arguments of type Axiom.
module Issue558c where

data ⊤ : Set where
  tt : ⊤

data V : Set where
  aV : ⊤ → V

postulate D : ⊤ → Set
          zero : D tt
          suc : ∀ {t} → D t → V

test : {{v : V}} → ⊤
test {{v}} = tt

module test {t : ⊤} {d : D t} where
  inst : V
  inst = aV tt

  someT : ⊤
  someT = test

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module _ where

module M where

  data D : Set where
    c : D

  pattern c′ = c

open M hiding (c′)

x : D
x = c′

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda