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

module CauchyProofsS where

-- Proofs about permutations defined in module Cauchy (multiplicative2)

open import Level using (Level; _⊔_) renaming (zero to lzero; suc to lsuc)

open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans; subst; subst₂; cong; cong₂; setoid;
        proof-irrelevance; module ≡-Reasoning)
open import Relation.Binary.PropositionalEquality.TrustMe
  using (trustMe)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Data.Nat.Properties
  using (m≤m+n; n≤m+n; n≤1+n; cancel-+-left; cancel-*-right; strictTotalOrder;
         cancel-*-right-≤; ≰⇒>; ¬i+1+j≤i; 1+n≰n; ≤⇒pred≤)
open import Data.Nat.Properties.Simple
  using (+-right-identity; +-suc; +-assoc; +-comm;
        *-assoc; *-comm; *-right-zero; distribʳ-*-+; +-*-suc)
open import Data.Nat.DivMod using (DivMod; result; _divMod_; _div_; _mod_)
open import Relation.Binary
  using (Rel; Decidable; Setoid; StrictTotalOrder; IsStrictTotalOrder;
         tri<; tri≈; tri>)
open import Relation.Binary.Core using (Transitive; _⇒_)

open import Data.String using (String)
  renaming (_++_ to _++S_)
open import Data.Nat.Show using (show)
open import Data.Bool using (Bool; false; true; _∨_)
open import Data.Nat using (ℕ; suc; _+_; _∸_; _*_; _<_; _≮_; _≤_; _≰_;
  _≥_; z≤n; s≤s; _≟_; _≤?_; ≤-pred; module ≤-Reasoning)
open import Data.Fin
  using (Fin; zero; suc; toℕ; fromℕ; fromℕ≤; _ℕ-_; _≺_; reduce≥;
         raise; inject+; inject₁; inject≤; _≻toℕ_; #_)
  renaming (_+_ to _F+_)
open import Data.Fin.Properties
  using (bounded; inject+-lemma; to-from; toℕ-injective; inject≤-lemma;
         toℕ-fromℕ≤; fromℕ≤-toℕ)
open import Data.Vec.Properties
  using (lookup∘tabulate; tabulate∘lookup; lookup-allFin; tabulate-∘;
         tabulate-allFin; allFin-map; lookup-++-inject+; lookup-++-≥;
         module UsingVectorEquality)
open import Data.Product using (Σ; swap)

open import Data.List
  using (List; []; _∷_; _∷ʳ_; foldl; replicate; reverse; downFrom;
         concatMap; gfilter; initLast; InitLast; _∷ʳ'_)
  renaming (_++_ to _++L_; map to mapL; concat to concatL; zip to zipL)
open import Data.List.NonEmpty
  using (List⁺; [_]; _∷⁺_; head; last; _⁺++_)
  renaming (toList to nonEmptyListtoList; _∷ʳ_ to _n∷ʳ_; tail to ntail)
open import Data.List.Any using (Any; here; there; any; module Membership)
open import Data.Maybe using (Maybe; nothing; just; maybe′)
open import Data.Vec
  using (Vec; tabulate; []; _∷_; tail; lookup; zip; zipWith; splitAt;
         _[_]≔_; allFin; toList)
  renaming (_++_ to _++V_; map to mapV; concat to concatV)
open import Function using (id; _∘_; _$_; _∋_)

open import Data.Empty   using (⊥; ⊥-elim)
open import Data.Unit    using (⊤; tt)
open import Data.Sum     using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_; _,_; proj₁; proj₂)

open import DivModUtils using (mod-lemma)
open import Proofs
open import Cauchy
open import Perm
open import CauchyProofs
open import CauchyProofsT

------------------------------------------------------------------------------
-- Main lemma swap⋆idemp

subst-allFin : ∀ {m n} → (eq : m ≡ n) → subst Cauchy eq (allFin m) ≡ allFin n
subst-allFin refl = refl

concat-simplify : {A : Set} → (m n : ℕ) → (f : Fin (suc m) → Vec A (suc n)) →
  concatV (mapV f (allFin (suc m))) ≡
  f zero ++V concatV (mapV (f ∘ suc) (allFin m))
concat-simplify m n f =
  begin (concatV (mapV f (allFin (suc m)))
        ≡⟨ cong
            (λ x → concatV (mapV f x))
            (allFin-map m) ⟩
         concatV (mapV f (zero ∷ mapV suc (allFin m)))
        ≡⟨ refl ⟩
         concatV (f zero ∷ mapV f (mapV suc (allFin m)))
        ≡⟨ cong (λ x → concatV (f zero ∷ x)) (sym (map-∘ f suc (allFin m))) ⟩
          f zero ++V concatV (mapV (λ a → f (suc a)) (allFin m)) ∎)
  where open ≡-Reasoning

concat-simplify-inject : {A : Set} → (m n : ℕ) (i : Fin (suc (suc n))) →
  (f : Fin (suc (suc m)) → Vec A (suc (suc n))) →
  lookup
    (inject+ (suc m * suc (suc n)) i)
    (concatV (mapV f (allFin (suc (suc m))))) ≡
  lookup i (f zero)
concat-simplify-inject m n i f =
  begin (lookup
           (inject+ (suc m * suc (suc n)) i)
           (concatV (mapV f (allFin (suc (suc m)))))
        ≡⟨ cong
             (lookup (inject+ (suc m * suc (suc n)) i))
             (concat-simplify (suc m) (suc n) f) ⟩
         lookup
           (inject+ (suc m * suc (suc n)) i)
           (f zero ++V concatV (mapV (λ a → f (suc a)) (allFin (suc m))))
        ≡⟨ lookup-++-inject+
             (f zero) (concatV (mapV (λ a → f (suc a)) (allFin (suc m)))) i ⟩
          lookup i (f zero) ∎)
  where open ≡-Reasoning

concat-simplify-raise : {A : Set} → (m n : ℕ) (i : Fin (suc m * suc (suc n))) →
  (f : Fin (suc (suc m)) → Vec A (suc (suc n))) →
  lookup
    (raise (suc (suc n)) i)
    (concatV (mapV f (allFin (suc (suc m))))) ≡
  lookup i (concatV (mapV (λ a → f (suc a)) (allFin (suc m))))
concat-simplify-raise m n i f =
  begin (lookup
           (raise (suc (suc n)) i)
           (concatV (mapV f (allFin (suc (suc m)))))
        ≡⟨ cong
            (lookup (raise (suc (suc n)) i))
            (concat-simplify (suc m) (suc n) f) ⟩
         lookup
           (raise (suc (suc n)) i)
           (f zero ++V concatV (mapV (λ a → f (suc a)) (allFin (suc m))))
         ≡⟨ lookup-++-raise
             (f zero) (concatV (mapV (λ a → f (suc a)) (allFin (suc m)))) i ⟩
         lookup i (concatV (mapV (λ a → f (suc a)) (allFin (suc m)))) ∎)
  where open ≡-Reasoning

lookup-subst-1 : ∀ {m m'}
  (i : Fin m') (xs : Vec (Fin m) m) (eq : m ≡ m') (eq' : m' ≡ m)
  (irr : sym eq ≡ eq') →
  lookup i (subst (λ s → Vec (Fin s) s) eq xs) ≡
  subst Fin eq (lookup (subst Fin eq' i) xs)
lookup-subst-1 i xs refl .refl refl = refl

subst-inject-mod : ∀ {n m m'} → (eq : suc (suc m) ≡ suc (suc m')) →
  subst Fin eq (inject≤ (n mod (suc m)) (i≤si (suc m))) ≡
  inject≤ (n mod (suc m')) (i≤si (suc m'))
subst-inject-mod refl = refl

cmp = IsStrictTotalOrder.compare
        (StrictTotalOrder.isStrictTotalOrder strictTotalOrder)

max-b-d : (m n : ℕ) → (b : Fin (suc (suc m))) (d : Fin (suc (suc n))) →
  (p= : suc (toℕ b * suc (suc n) + toℕ d) ≡ suc (suc m) * suc (suc n)) →
  (toℕ b ≡ suc m × toℕ d ≡ suc n)
max-b-d m n b d p= with cmp (toℕ b) (suc m) | cmp (toℕ d) (suc n)
max-b-d m n b d p= | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim (1+n≰n contra)
  where contra = begin (1 + suc (toℕ b * suc (suc n) + toℕ d)
                        ≡⟨ cong suc (sym (+-suc (toℕ b * suc (suc n)) (toℕ d))) ⟩
                        1 + (toℕ b * suc (suc n) + suc (toℕ d))
                        ≡⟨ sym (+-suc (toℕ b * suc (suc n)) (suc (toℕ d))) ⟩
                        toℕ b * suc (suc n) + suc (suc (toℕ d))
                        ≤⟨ cong+l≤ (s≤s a₁) (toℕ b * suc (suc n)) ⟩
                        toℕ b * suc (suc n) + suc (suc n)
                        ≡⟨ +-comm (toℕ b * suc (suc n)) (suc (suc n)) ⟩
                        suc (toℕ b) * suc (suc n)
                        ≤⟨ cong*r≤ (≰⇒> ¬c) (suc (suc n)) ⟩
                        suc (suc m) * suc (suc n)
                        ≡⟨ sym p= ⟩
                        suc (toℕ b * suc (suc n) + toℕ d) ∎)
                 where open ≤-Reasoning
max-b-d m n b d p= | tri< a ¬b= ¬c | tri≈ ¬a d= ¬c₁ =
  ⊥-elim (¬b= (cancel-+-left 1
    (cancel-*-right (suc (toℕ b)) (suc (suc m)) {suc n} contra)))
  where
    contra : suc (toℕ b) * suc (suc n) ≡ suc (suc m) * suc (suc n)
    contra = begin (suc (toℕ b) * suc (suc n)
                   ≡⟨  refl ⟩
                   suc (suc n) + toℕ b * suc (suc n)
                   ≡⟨  +-comm (suc (suc n)) (toℕ b * suc (suc n)) ⟩
                   toℕ b * suc (suc n) + suc (suc n)
                   ≡⟨  +-suc (toℕ b * suc (suc n)) (suc n) ⟩
                   suc (toℕ b * suc (suc n) + suc n)
                   ≡⟨  cong (λ x → suc (toℕ b * suc (suc n) + x)) (sym d=) ⟩
                   suc (toℕ b * suc (suc n) + toℕ d)
                   ≡⟨  p= ⟩
                   suc (suc m) * suc (suc n) ∎)
             where open ≡-Reasoning
max-b-d m n b d p= | tri< a ¬b ¬c | tri> ¬a ¬b₁ c =
  ⊥-elim (1+n≰n (trans≤ (bounded d) c))
max-b-d m n b d p= | tri≈ ¬a b= ¬c | tri< a ¬d= ¬c₁ =
  ⊥-elim (¬d= (cancel-+-left 1
    (cancel-+-left (suc m * suc (suc n)) contra)))
  where
     contra : suc m * suc (suc n) + suc (toℕ d) ≡ suc m * suc (suc n) + suc (suc n)
     contra = begin (suc m * suc (suc n) + suc (toℕ d)
                    ≡⟨ cong (λ x → x * suc (suc n) + suc (toℕ d)) (sym b=) ⟩
                    toℕ b * suc (suc n) + suc (toℕ d)
                    ≡⟨ +-suc (toℕ b * suc (suc n)) (toℕ d) ⟩
                    suc (toℕ b * suc (suc n) + toℕ d)
                    ≡⟨ p= ⟩
                    suc (suc m) * suc (suc n)
                    ≡⟨ +-comm (suc (suc n)) (suc m * suc (suc n)) ⟩
                    suc m * suc (suc n) + suc (suc n) ∎)
              where open ≡-Reasoning
max-b-d m n b d p= | tri≈ ¬a b₁ ¬c | tri≈ ¬a₁ b₂ ¬c₁ = (b₁ , b₂)
max-b-d m n b d p= | tri≈ ¬a b₁ ¬c | tri> ¬a₁ ¬b c =
  ⊥-elim (1+n≰n (trans≤ (bounded d) c))
max-b-d m n b d p= | tri> ¬a ¬b c | tri< a ¬b₁ ¬c =
  ⊥-elim (1+n≰n (trans≤ (bounded b) c))
max-b-d m n b d p= | tri> ¬a ¬b c | tri≈ ¬a₁ b₁ ¬c =
  ⊥-elim (1+n≰n (trans≤ (bounded b) c))
max-b-d m n b d p= | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ =
  ⊥-elim (1+n≰n (trans≤ (bounded d) c₁))

subst-fin : (a b : ℕ) → (eq : suc a ≡ suc b) → subst Fin eq (fromℕ a) ≡ fromℕ b
subst-fin a .a refl = refl

lookup-fromℕ-allFin : {A : Set} → (n : ℕ) → (f : Fin (suc n) → A) →
  lookup (fromℕ n) (tabulate {suc n} f) ≡ f (fromℕ n)
lookup-fromℕ-allFin 0 f = refl
lookup-fromℕ-allFin (suc n) f = lookup-fromℕ-allFin n (f ∘ suc)

fin=1 : (m n : ℕ) →
  fromℕ (suc m + suc n * suc (suc m)) ≡
  fromℕ (suc (m + suc (suc (m + n * suc (suc m)))))
fin=1 m n = toℕ-injective p
  where p = begin (toℕ (fromℕ (suc m + suc n * suc (suc m)))
                 ≡⟨ to-from (suc m + suc n * suc (suc m)) ⟩
                   suc m + suc n * suc (suc m)
                 ≡⟨ refl ⟩
                   suc (m + suc (suc (m + n * suc (suc m))))
                ≡⟨ sym (to-from (suc (m + suc (suc (m + n * suc (suc m)))))) ⟩
                   toℕ (fromℕ (suc (m + suc (suc (m + n * suc (suc m)))))) ∎)
            where open ≡-Reasoning

concat-map-map-tabulate : (m n : ℕ) → (f : Fin m × Fin n → Fin (m * n)) →
  concatV (mapV (λ b → mapV (λ d → f (b , d)) (allFin n)) (allFin m)) ≡
  tabulate (λ k → f (fin-project m n k))
concat-map-map-tabulate m n f =
  begin (concatV (mapV (λ b → mapV (λ d → f (b , d)) (allFin n)) (allFin m))
       ≡⟨ cong concatV (sym (tabulate-∘ (λ b → mapV (λ d → f (b , d)) (allFin n)) id)) ⟩
         concatV (tabulate (λ b → mapV (λ d → f (b , d)) (allFin n)))
       ≡⟨ cong concatV
            (finext (λ b → sym (tabulate-∘ (λ d → f (b , d)) id))) ⟩
         concatV (tabulate (λ b → tabulate (λ d → f (b , d))))
       ≡⟨ tabulate-concat f ⟩
         tabulate (λ k → f (fin-project m n k)) ∎)
  where open ≡-Reasoning

fin-project-2 : (n m : ℕ) →
 fin-project (suc (suc n)) (suc (suc m)) (fromℕ (suc m + suc n * suc (suc m)))
 ≡ (fromℕ (suc n) , fromℕ (suc m))
fin-project-2 n m with toℕ (fromℕ (suc m + suc n * suc (suc m))) divMod (suc (suc m))
fin-project-2 n m | result q r k≡r+q*sn with suc (suc n) ≤? q
fin-project-2 n m | result q r k≡r+q*sn | yes p =
  ⊥-elim (absurd (suc n) (suc m) q r (fromℕ (suc m + suc n * suc (suc m))) k≡r+q*sn p)
fin-project-2 n m | result q r k≡r+q*sn | no ¬p =
  let (b= , d=) = max-b-d n m (fromℕ≤ (s≤s (≤-pred (≰⇒> ¬p)))) r pr
  in cong₂ _,_
       (toℕ-injective (trans b= (sym (to-from (suc n)))))
       (toℕ-injective (trans d= (sym (to-from (suc m)))))
  where
        pr : suc (toℕ (fromℕ≤ (s≤s (≤-pred (≰⇒> ¬p)))) * suc (suc m) + toℕ r) ≡
             suc (suc n) * suc (suc m)
        pr =
          begin (_
-- agda bug?
-- replacing _ by the actual term:
-- suc (toℕ (fromℕ≤ (s≤s (≤-pred (≰⇒> ¬p)))) * suc (suc m) + toℕ r)
-- gives an occurs check error
                 ≡⟨ cong
                      (λ x → suc (x * suc (suc m) + toℕ r))
                      (toℕ-fromℕ≤ (s≤s (≤-pred (≰⇒> ¬p)))) ⟩
                 suc (q * suc (suc m) + toℕ r)
                 ≡⟨ cong suc (+-comm (q * suc (suc m)) (toℕ r)) ⟩
                 suc (toℕ r + q * suc (suc m))
                 ≡⟨ cong suc (sym k≡r+q*sn) ⟩
                 suc (suc (toℕ (fromℕ (m + suc (suc (m + n * suc (suc m)))))))
                 ≡⟨ cong
                     (λ x → suc (suc x))
                     (to-from (m + suc (suc (m + n * suc (suc m))))) ⟩
                 suc (suc n) * suc (suc m) ∎)
          where open ≡-Reasoning

-- index (b,d) in matrix becomes (d,b) in transpose
-- And yes, it is obvious:
-- (b*n+d)*m = b*n*m + d*m            -- expand
--           = b*(n*m -1) + b*1 + d*m -- add 0 = b*1 - b*1
--           = b + d*m                -- modulus

num-lem : (m n : ℕ) → (b : Fin (suc (suc m))) → (d : Fin (suc (suc n))) →
  (((toℕ b * suc (suc n)) + toℕ d) * (suc (suc m))) ≡
  (toℕ d * suc (suc m) + toℕ b) + toℕ b * suc (m + suc n * suc (suc m))
num-lem m n b d =
  begin (((toℕ b * suc (suc n)) + toℕ d) * suc (suc m)
        ≡⟨ distribʳ-*-+ (suc (suc m)) (toℕ b * suc (suc n)) (toℕ d) ⟩
         (toℕ b * suc (suc n)) * suc (suc m) + toℕ d * suc (suc m)
        ≡⟨ cong
            (λ x → x + toℕ d * suc (suc m))
            (trans
              (*-assoc (toℕ b) (suc (suc n)) (suc (suc m)))
              (*-comm (toℕ b) (suc (suc n) * suc (suc m)))) ⟩
         (suc (suc n) * suc (suc m)) * toℕ b + toℕ d * suc (suc m)
        ≡⟨ refl ⟩
         suc (suc m + suc n * suc (suc m)) * toℕ b + toℕ d * suc (suc m)
        ≡⟨ refl ⟩
         (toℕ b + (suc m + suc n * suc (suc m)) * toℕ b) + toℕ d * suc (suc m)
         ≡⟨ cong
              (λ x → x + toℕ d * suc (suc m))
              (+-comm (toℕ b) ((suc m + suc n * suc (suc m)) * toℕ b)) ⟩
         ((suc m + suc n * suc (suc m)) * toℕ b + toℕ b) + toℕ d * suc (suc m)
        ≡⟨ +-assoc
            ((suc m + suc n * suc (suc m)) * toℕ b)
            (toℕ b)
            (toℕ d * suc (suc m)) ⟩
         (suc m + suc n * suc (suc m)) * toℕ b + (toℕ b + toℕ d * suc (suc m))
        ≡⟨ cong₂ _+_
            (*-comm (suc m + suc n * suc (suc m)) (toℕ b))
            (+-comm (toℕ b) (toℕ d * suc (suc m))) ⟩
        toℕ b * (suc m + suc n * suc (suc m)) + (toℕ d * suc (suc m) + toℕ b)
        ≡⟨ +-comm
             (toℕ b * (suc m + suc n * suc (suc m)))
             (toℕ d * suc (suc m) + toℕ b) ⟩
        (toℕ d * suc (suc m) + toℕ b) + toℕ b * (suc m + suc n * suc (suc m)) ∎)
  where open ≡-Reasoning

mod-lem : (m n : ℕ) → (b : Fin (suc (suc m))) → (d : Fin (suc (suc n))) →
      (leq : suc (toℕ d * suc (suc m) + toℕ b) ≤ suc m + suc n * suc (suc m)) →
      ((((toℕ b * suc (suc n)) + toℕ d) * (suc (suc m)))
        mod (suc m + suc n * suc (suc m)))
    ≡ inject≤ (fromℕ (toℕ d * suc (suc m) + toℕ b)) leq
mod-lem m n b d leq =
  begin (((((toℕ b * suc (suc n)) + toℕ d) * (suc (suc m)))
               mod (suc m + suc n * suc (suc m)))
         ≡⟨ cong
             (λ x → x mod (suc m + suc n * suc (suc m)))
             (num-lem m n b d) ⟩
         (((toℕ d * suc (suc m) + toℕ b) + (toℕ b * (suc m + suc n * suc (suc m))))
               mod (suc m + suc n * suc (suc m)))
          ≡⟨ cong
              (λ x → ((x + (toℕ b * (suc m + suc n * suc (suc m))))
                     mod (suc m + suc n * suc (suc m))))
             (trans
                (sym (to-from (toℕ d * suc (suc m) + toℕ b)))
                (sym (inject≤-lemma (fromℕ (toℕ d * suc (suc m) + toℕ b)) leq) )) ⟩
         (((toℕ (inject≤ (fromℕ (toℕ d * suc (suc m) + toℕ b)) leq)) +
           (toℕ b * (suc m + suc n * suc (suc m))))
           mod (suc m + suc n * suc (suc m)))
          ≡⟨ mod-lemma (toℕ b) (m + suc n * suc (suc m))
              (inject≤ (fromℕ (toℕ d * suc (suc m) + toℕ b)) leq) ⟩
         inject≤ (fromℕ (toℕ d * suc (suc m) + toℕ b)) leq ∎)
  where open ≡-Reasoning

not-max-b-d : (m n : ℕ) (b : Fin (suc (suc m))) (d : Fin (suc (suc n)))
  (p≠ : ¬ suc (toℕ b * suc (suc n) + toℕ d) ≡ suc (suc m) * suc (suc n)) →
   suc (toℕ b * suc (suc n) + toℕ d) ≤ suc n + suc m * suc (suc n)
not-max-b-d m n b d p≠ with
      cmp (suc (toℕ b * suc (suc n) + toℕ d)) (suc (suc m) * suc (suc n))
... | tri< a ¬b ¬c = ≤-pred a
... | tri≈ ¬a b≡ ¬c = ⊥-elim (p≠ b≡)
... | tri> ¬a ¬b c = ⊥-elim (1+n≰n contra)
  where contra = begin (suc (suc (suc m) * suc (suc n))
                       ≤⟨ c ⟩
                        suc (toℕ b * suc (suc n) + toℕ d)
                       ≡⟨ sym (+-suc (toℕ b * suc (suc n)) (toℕ d)) ⟩
                        toℕ b * suc (suc n) + suc (toℕ d)
                       ≤⟨ cong+l≤ (bounded d) (toℕ b * suc (suc n)) ⟩
                        toℕ b * suc (suc n) + suc (suc n)
                       ≤⟨ cong+r≤
                           (cong*r≤ (bounded' (suc m) b) (suc (suc n)))
                           (suc (suc n)) ⟩
                        suc m * suc (suc n) + suc (suc n)
                       ≡⟨ +-comm (suc m * suc (suc n)) (suc (suc n)) ⟩
                        suc (suc m) * suc (suc n) ∎)
                 where open ≤-Reasoning

not-max-b-d' : (m n : ℕ) (b : Fin (suc (suc m))) (d : Fin (suc (suc n)))
  (p≠ : ¬ suc (toℕ b * suc (suc n) + toℕ d) ≡ suc (suc m) * suc (suc n)) →
  (¬ suc (toℕ d * suc (suc m) + toℕ b) ≡ suc (suc n) * suc (suc m))
not-max-b-d' m n b d p≠ with
  (suc (toℕ d * suc (suc m) + toℕ b)) ≟ (suc (suc n) * suc (suc m))
... | no ¬w = ¬w
... | yes w =
  let (d≡sn , b≡sm) = max-b-d n m d b w in ⊥-elim (p≠ (contra b≡sm d≡sn))
  where contra : (b≡sm : toℕ b ≡ suc m) (d≡sn : toℕ d ≡ suc n) →
                 suc (toℕ b * suc (suc n) + toℕ d) ≡ suc (suc m) * suc (suc n)
        contra b≡sm d≡sn =
          begin (suc (toℕ b * suc (suc n) + toℕ d)
                ≡⟨ cong₂ (λ x y → suc (x * suc (suc n) + y)) b≡sm d≡sn ⟩
                 suc (suc m * suc (suc n) + suc n)
                ≡⟨ sym (+-suc (suc m * suc (suc n)) (suc n)) ⟩
                 suc m * suc (suc n) + suc (suc n)
                ≡⟨  +-comm (suc m * suc (suc n)) (suc (suc n)) ⟩
                 suc (suc m) * suc (suc n) ∎)
          where open ≡-Reasoning

inject-mod : (m n : ℕ) (b : Fin (suc (suc m))) (d : Fin (suc (suc n)))
     (leq : suc (toℕ b * suc (suc n) + toℕ d) ≤ suc n + suc m * suc (suc n)) →
        inject≤
          (((toℕ d * suc (suc m) + toℕ b) * suc (suc n)) mod
             (suc n + suc m * suc (suc n)))
          (i≤si (suc n + suc m * suc (suc n)))
      ≡ inject≤
           (fromℕ (toℕ b * suc (suc n) + toℕ d))
           (i*n+k≤m*n b d)
inject-mod m n b d leq =
   begin (inject≤
            (((toℕ d * suc (suc m) + toℕ b) * suc (suc n)) mod
             (suc n + suc m * suc (suc n)))
            (i≤si (suc n + suc m * suc (suc n)))
        ≡⟨ cong₂D!
             inject≤
             (sym (mod-lem n m d b leq))
             (≤-proof-irrelevance
               (subst
                 (λ _ →
                   suc n + suc m * suc (suc n) ≤ suc (suc n + suc m * suc (suc n)))
                 (sym (mod-lem n m d b leq))
                 (i≤si (suc n + suc m * suc (suc n))))
               (i≤si (suc n + suc m * suc (suc n)))) ⟩
          inject≤
            (inject≤ (fromℕ (toℕ  b * suc (suc n) + toℕ d)) leq)
            (i≤si (suc n + suc m * suc (suc n)))
        ≡⟨ toℕ-injective
            (trans
              (inject≤-lemma
                (inject≤ (fromℕ (toℕ b * suc (suc n) + toℕ d)) leq)
                (i≤si (suc n + suc m * suc (suc n))))
              (trans
                (inject≤-lemma (fromℕ (toℕ b * suc (suc n) + toℕ d)) leq)
                (sym (inject≤-lemma
                       (fromℕ (toℕ b * suc (suc n) + toℕ d))
                       (i*n+k≤m*n b d))))) ⟩
         inject≤
           (fromℕ (toℕ b * suc (suc n) + toℕ d))
           (i*n+k≤m*n b d) ∎)
   where open ≡-Reasoning

fin-project-3 : (m n : ℕ) (b : Fin (suc (suc m))) (d : Fin (suc (suc n))) →
  (p≠ : ¬ suc (toℕ d * suc (suc m) + toℕ b) ≡ suc (suc n) * suc (suc m)) →
  fin-project (suc (suc n)) (suc (suc m))
    (inject≤
      ((((toℕ b * suc (suc n)) + toℕ d) * (suc (suc m))) mod
       (suc m + suc n * suc (suc m)))
      (i≤si (suc m + suc n * suc (suc m))))
  ≡ (d , b)
fin-project-3 m n b d p≠ with
  (toℕ (inject≤
         ((((toℕ b * suc (suc n)) + toℕ d) * (suc (suc m))) mod
          (suc m + suc n * suc (suc m)))
         (i≤si (suc m + suc n * suc (suc m))))) divMod (suc (suc m))
fin-project-3 m n b d p≠ | result q r k≡r+q*sn with suc (suc n) ≤? q
fin-project-3 m n b d p≠ | result q r k≡r+q*sn | yes p =
  ⊥-elim (absurd (suc n) (suc m) q r
           (inject≤
             ((((toℕ b * suc (suc n)) + toℕ d) * (suc (suc m))) mod
               (suc m + suc n * suc (suc m)))
             (i≤si (suc m + suc n * suc (suc m))))
             k≡r+q*sn
             p)
fin-project-3 m n b d p≠ | result q r k≡r+q*sn | no ¬p =
  let (r≡b , q≡d) = addMul-lemma′ q (toℕ d) (suc m) r b (sym simplified)
  in cong₂ _,_ (toℕ-injective (trans (toℕ-fromℕ≤ (s≤s (≤-pred (≰⇒> ¬p)))) q≡d)) r≡b
  where simplified : toℕ d * suc (suc m) + toℕ b ≡ q * suc (suc m) + toℕ r
        simplified = begin (toℕ d * suc (suc m) + toℕ b
                            ≡⟨ sym (to-from (toℕ d * suc (suc m) + toℕ b)) ⟩
                           toℕ (fromℕ (toℕ d * suc (suc m) + toℕ b))
                           ≡⟨ sym (inject≤-lemma
                                    (fromℕ (toℕ d * suc (suc m) + toℕ b))
                                    (i*n+k≤m*n d b)) ⟩
                           toℕ (inject≤
                             (fromℕ (toℕ d * suc (suc m) + toℕ b))
                             (i*n+k≤m*n d b))
                           ≡⟨ cong toℕ
                                (sym (inject-mod n m d b (not-max-b-d n m d b p≠))) ⟩
                           toℕ (inject≤
                             ((((toℕ b * suc (suc n)) + toℕ d) * (suc (suc m))) mod
                               (suc m + suc n * suc (suc m)))
                             (i≤si (suc m + suc n * suc (suc m))))
                           ≡⟨ k≡r+q*sn ⟩
                           toℕ r + q * suc (suc m)
                           ≡⟨ +-comm (toℕ r) (q * suc (suc m)) ⟩
                           q * suc (suc m) + toℕ r ∎)
                     where open ≡-Reasoning

transpose2 : (m n : ℕ) (i : Fin (m * n)) →
  let fin-result b d dec dec' = fin-divMod m n i
      fin-result bt dt dect dec't =
        fin-divMod n m (subst Fin (*-comm m n) (transposeIndex m n b d)) in
  toℕ (transposeIndex n m bt dt) ≡ toℕ i
transpose2 m n i =
  let fin-result b d dec dec' = fin-divMod m n i
      fin-result bt dt dect dec't =
        fin-divMod n m (subst Fin (*-comm m n) (transposeIndex m n b d))
      (dbt≡ , bdt≡) = fin-addMul-lemma n m d bt b dt pr
  in fpr
  where pr = let fin-result b d dec dec' = fin-divMod m n i
                 fin-result bt dt dect dec't =
                   fin-divMod n m (subst Fin (*-comm m n) (transposeIndex m n b d)) in
             begin (toℕ d * m + toℕ b
                   ≡⟨ sym (to-from _) ⟩
                   toℕ (fromℕ (toℕ d * m + toℕ b))
                   ≡⟨ sym (inject≤-lemma _ _) ⟩
                   toℕ (transposeIndex m n b d)
                   ≡⟨ sym (toℕ-fin (m * n) (n * m) (*-comm m n)
                           (transposeIndex m n b d)) ⟩
                   toℕ (subst Fin (*-comm m n) (transposeIndex m n b d))
                   ≡⟨ dect ⟩
                   toℕ dt + toℕ bt * m
                   ≡⟨ +-comm (toℕ dt) (toℕ bt * m) ⟩
                   toℕ bt * m + toℕ dt ∎)
             where open ≡-Reasoning
        fpr = let fin-result b d dec dec' = fin-divMod m n i
                  fin-result bt dt dect dec't =
                    fin-divMod n m (subst Fin (*-comm m n) (transposeIndex m n b d))
                  (dbt≡ , bdt≡) = fin-addMul-lemma n m d bt b dt pr in
              begin (toℕ (transposeIndex n m bt dt)
                   ≡⟨ inject≤-lemma _ _ ⟩
                     toℕ (fromℕ (toℕ dt * n + toℕ bt))
                   ≡⟨ to-from _ ⟩
                     toℕ dt * n + toℕ bt
                   ≡⟨ cong₂ (λ x y → toℕ x * n + toℕ y)
                        (sym bdt≡) (sym dbt≡) ⟩
                     toℕ b * n + toℕ d
                   ≡⟨ +-comm (toℕ b * n) (toℕ d) ⟩
                     toℕ d + toℕ b * n
                   ≡⟨ sym dec ⟩
                     toℕ i ∎)
              where open ≡-Reasoning

lookup-transpose : (m n : ℕ) (i : Fin (m * n)) →
  lookup
    (lookup i
      (concatV
        (mapV (λ b → mapV (λ d → transposeIndex m n b d) (allFin n))
        (allFin m))))
    (subst Cauchy (*-comm n m)
      (concatV
        (mapV (λ d → mapV (λ b → transposeIndex n m d b) (allFin m))
        (allFin n))))
  ≡ i
lookup-transpose m n i =
  let fin-result b d dec dec' = fin-divMod m n i
      fin-result bt dt dect dect' =
        fin-divMod n m (subst Fin (*-comm m n) (transposeIndex m n b d)) in
  begin (lookup
          (lookup i
            (concatV
              (mapV (λ b → mapV (λ d → transposeIndex m n b d) (allFin n))
              (allFin m))))
            (subst Cauchy (*-comm n m)
              (concatV
                (mapV (λ d → mapV (λ b → transposeIndex n m d b) (allFin m))
                (allFin n))))
       ≡⟨ cong (λ x → lookup x
                 (subst Cauchy (*-comm n m)
                   (concatV
                     (mapV
                        (λ d → mapV (λ b → transposeIndex n m d b) (allFin m))
                        (allFin n)))))
           (trans (lookup-2d m n i (allFin m) (allFin n)
                    (λ {(b , d) → transposeIndex m n b d}))
                  (cong₂ (transposeIndex m n)
                    (lookup-allFin b) (lookup-allFin d))) ⟩
         lookup
            (transposeIndex m n b d)
            (subst Cauchy (*-comm n m)
              (concatV
                (mapV (λ d → mapV (λ b → transposeIndex n m d b) (allFin m))
                (allFin n))))
       ≡⟨ lookup-subst-1
           (transposeIndex m n b d)
           (concatV
             (mapV
               (λ d → mapV (λ b → transposeIndex n m d b) (allFin m))
               (allFin n)))
           (*-comm n m)
           (*-comm m n)
           (proof-irrelevance (sym (*-comm n m)) (*-comm m n)) ⟩
         subst Fin (*-comm n m)
           (lookup
             (subst Fin (*-comm m n) (transposeIndex m n b d))
             (concatV
               (mapV
                 (λ d → mapV (λ b → transposeIndex n m d b) (allFin m))
                 (allFin n))))
       ≡⟨ cong (λ x → subst Fin (*-comm n m) x)
            (trans
              (lookup-2d n m (subst Fin (*-comm m n) (transposeIndex m n b d))
                (allFin n) (allFin m)
                (λ {(d , b) → transposeIndex n m d b}))
              (cong₂ (transposeIndex n m)
                (lookup-allFin bt) (lookup-allFin dt))) ⟩
         subst Fin (*-comm n m) (transposeIndex n m bt dt)
       ≡⟨ toℕ-injective
           (trans
             (toℕ-fin (n * m) (m * n) (*-comm n m) (transposeIndex n m bt dt))
             (transpose2 m n i)) ⟩
         i ∎)
  where open ≡-Reasoning

swap⋆idemp : (m n : ℕ) →
  scompcauchy
    (swap⋆cauchy m n)
    (subst Cauchy (*-comm n m) (swap⋆cauchy n m))
  ≡
  allFin (m * n)
swap⋆idemp m n =
  begin (scompcauchy
           (concatV
             (mapV
               (λ b → mapV (λ d → transposeIndex m n b d) (allFin n))
               (allFin m)))
           (subst Cauchy (*-comm n m)
             (concatV
               (mapV
                 (λ d → mapV (λ b → transposeIndex n m d b) (allFin m))
                 (allFin n))))
         ≡⟨ refl ⟩
         tabulate (λ i →
           lookup
             (lookup i
               (concatV
                 (mapV
                   (λ b → mapV (λ d → transposeIndex m n b d) (allFin n))
                   (allFin m))))
             (subst Cauchy (*-comm n m)
               (concatV
                 (mapV
                   (λ d → mapV (λ b → transposeIndex n m d b) (allFin m))
                   (allFin n)))))
         ≡⟨ finext (lookup-transpose m n) ⟩
         allFin (m * n) ∎)
  where open ≡-Reasoning

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


text:
-- Andreas, 2017-07-28, issue 1077

open import Issue1077

foz = foo
baz = bar

-- WAS: bar not in scope

-- NOW: import fails because module Issue1077 is rejected

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}
module Cubical.Data.Nat.Order where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels

open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Sigma
open import Cubical.Data.Sum as ⊎

open import Cubical.Data.Nat.Base
open import Cubical.Data.Nat.Properties

open import Cubical.Induction.WellFounded

open import Cubical.Relation.Nullary

infix 4 _≤_ _<_

_≤_ : ℕ → ℕ → Type₀
m ≤ n = Σ[ k ∈ ℕ ] k + m ≡ n

_<_ : ℕ → ℕ → Type₀
m < n = suc m ≤ n

data Trichotomy (m n : ℕ) : Type₀ where
  lt : m < n → Trichotomy m n
  eq : m ≡ n → Trichotomy m n
  gt : n < m → Trichotomy m n

private
  variable
    k l m n : ℕ

private
  witness-prop : ∀ j → isProp (j + m ≡ n)
  witness-prop {m} {n} j = isSetℕ (j + m) n

m≤n-isProp : isProp (m ≤ n)
m≤n-isProp {m} {n} (k , p) (l , q)
  = Σ≡Prop witness-prop lemma
  where
  lemma : k ≡ l
  lemma = inj-+m (p ∙ (sym q))

zero-≤ : 0 ≤ n
zero-≤ {n} = n , +-zero n

suc-≤-suc : m ≤ n → suc m ≤ suc n
suc-≤-suc (k , p) = k , (+-suc k _) ∙ (cong suc p)

≤-+k : m ≤ n → m + k ≤ n + k
≤-+k {m} {k = k} (i , p)
  = i , +-assoc i m k ∙ cong (_+ k) p

≤-k+ : m ≤ n → k + m ≤ k + n
≤-k+ {m} {n} {k}
  = subst (_≤ k + n) (+-comm m k)
  ∘ subst (m + k ≤_) (+-comm n k)
  ∘ ≤-+k

pred-≤-pred : suc m ≤ suc n → m ≤ n
pred-≤-pred (k , p) = k , injSuc ((sym (+-suc k _)) ∙ p)

≤-refl : m ≤ m
≤-refl = 0 , refl

≤-suc : m ≤ n → m ≤ suc n
≤-suc (k , p) = suc k , cong suc p

≤-predℕ : predℕ n ≤ n
≤-predℕ {zero} = ≤-refl
≤-predℕ {suc n} = ≤-suc ≤-refl

≤-trans : k ≤ m → m ≤ n → k ≤ n
≤-trans {k} {m} {n} (i , p) (j , q) = i + j , l2 ∙ (l1 ∙ q)
  where
  l1 : j + i + k ≡ j + m
  l1 = (sym (+-assoc j i k)) ∙ (cong (j +_) p)
  l2 : i + j + k ≡ j + i + k
  l2 = cong (_+ k) (+-comm i j)

≤-antisym : m ≤ n → n ≤ m → m ≡ n
≤-antisym {m} (i , p) (j , q) = (cong (_+ m) l3) ∙ p
  where
  l1 : j + i + m ≡ m
  l1 = (sym (+-assoc j i m)) ∙ ((cong (j +_) p) ∙ q)
  l2 : j + i ≡ 0
  l2 = m+n≡n→m≡0 l1
  l3 : 0 ≡ i
  l3 = sym (snd (m+n≡0→m≡0×n≡0 l2))

≤-k+-cancel : k + m ≤ k + n → m ≤ n
≤-k+-cancel {k} {m} (l , p) = l , inj-m+ (sub k m ∙ p)
 where
 sub : ∀ k m → k + (l + m) ≡ l + (k + m)
 sub k m = +-assoc k l m ∙ cong (_+ m) (+-comm k l) ∙ sym (+-assoc l k m)

≤-+k-cancel : m + k ≤ n + k → m ≤ n
≤-+k-cancel {m} {k} {n} (l , p) = l , cancelled
 where
 cancelled : l + m ≡ n
 cancelled = inj-+m (sym (+-assoc l m k) ∙ p)

≤-·k : m ≤ n → m · k ≤ n · k
≤-·k {m} {n} {k} (d , r) = d · k , reason where
  reason : d · k + m · k ≡ n · k
  reason = d · k + m · k ≡⟨ ·-distribʳ d m k ⟩
           (d + m) · k   ≡⟨ cong (_· k) r ⟩
           n · k         ∎

<-k+-cancel : k + m < k + n → m < n
<-k+-cancel {k} {m} {n} = ≤-k+-cancel ∘ subst (_≤ k + n) (sym (+-suc k m))

¬-<-zero : ¬ m < 0
¬-<-zero (k , p) = snotz ((sym (+-suc k _)) ∙ p)

¬m<m : ¬ m < m
¬m<m {m} = ¬-<-zero ∘ ≤-+k-cancel {k = m}

≤0→≡0 : n ≤ 0 → n ≡ 0
≤0→≡0 {zero} ineq = refl
≤0→≡0 {suc n} ineq = ⊥.rec (¬-<-zero ineq)

predℕ-≤-predℕ : m ≤ n → (predℕ m) ≤ (predℕ n)
predℕ-≤-predℕ {zero} {zero}   ineq = ≤-refl
predℕ-≤-predℕ {zero} {suc n}  ineq = zero-≤
predℕ-≤-predℕ {suc m} {zero}  ineq = ⊥.rec (¬-<-zero ineq)
predℕ-≤-predℕ {suc m} {suc n} ineq = pred-≤-pred ineq

¬m+n<m : ¬ m + n < m
¬m+n<m {m} {n} = ¬-<-zero ∘ <-k+-cancel ∘ subst (m + n <_) (sym (+-zero m))

<-weaken : m < n → m ≤ n
<-weaken (k , p) = suc k , sym (+-suc k _) ∙ p

≤<-trans : l ≤ m → m < n → l < n
≤<-trans p = ≤-trans (suc-≤-suc p)

<≤-trans : l < m → m ≤ n → l < n
<≤-trans = ≤-trans

<-trans : l < m → m < n → l < n
<-trans p = ≤<-trans (<-weaken p)

<-asym : m < n → ¬ n ≤ m
<-asym m<n = ¬m<m ∘ <≤-trans m<n

<-+k : m < n → m + k < n + k
<-+k p = ≤-+k p

<-k+ : m < n → k + m < k + n
<-k+ {m} {n} {k} p = subst (λ km → km ≤ k + n) (+-suc k m) (≤-k+ p)

<-·sk : m < n → m · suc k < n · suc k
<-·sk {m} {n} {k} (d , r) = (d · suc k + k) , reason where
  reason : (d · suc k + k) + suc (m · suc k) ≡ n · suc k
  reason = (d · suc k + k) + suc (m · suc k) ≡⟨ sym (+-assoc (d · suc k) k _) ⟩
           d · suc k + (k + suc (m · suc k)) ≡[ i ]⟨ d · suc k + +-suc k (m · suc k) i ⟩
           d · suc k + suc m · suc k         ≡⟨ ·-distribʳ d (suc m) (suc k) ⟩
           (d + suc m) · suc k               ≡⟨ cong (_· suc k) r ⟩
           n · suc k                         ∎

≤-∸-+-cancel : m ≤ n → (n ∸ m) + m ≡ n
≤-∸-+-cancel {zero} {n} _ = +-zero _
≤-∸-+-cancel {suc m} {zero} m≤n = ⊥.rec (¬-<-zero m≤n)
≤-∸-+-cancel {suc m} {suc n} m+1≤n+1 = +-suc _ _ ∙ cong suc (≤-∸-+-cancel (pred-≤-pred m+1≤n+1))

left-≤-max : m ≤ max m n
left-≤-max {zero} {n} = zero-≤
left-≤-max {suc m} {zero} = ≤-refl
left-≤-max {suc m} {suc n} = suc-≤-suc left-≤-max

right-≤-max : n ≤ max m n
right-≤-max {zero} {m} = zero-≤
right-≤-max {suc n} {zero} = ≤-refl
right-≤-max {suc n} {suc m} = suc-≤-suc right-≤-max

min-≤-left : min m n ≤ m
min-≤-left {zero} {n} = ≤-refl
min-≤-left {suc m} {zero} = zero-≤
min-≤-left {suc m} {suc n} = suc-≤-suc min-≤-left

min-≤-right : min m n ≤ n
min-≤-right {zero} {n} = zero-≤
min-≤-right {suc m} {zero} = ≤-refl
min-≤-right {suc m} {suc n} = suc-≤-suc min-≤-right

Trichotomy-suc : Trichotomy m n → Trichotomy (suc m) (suc n)
Trichotomy-suc (lt m<n) = lt (suc-≤-suc m<n)
Trichotomy-suc (eq m=n) = eq (cong suc m=n)
Trichotomy-suc (gt n<m) = gt (suc-≤-suc n<m)

_≟_ : ∀ m n → Trichotomy m n
zero ≟ zero = eq refl
zero ≟ suc n = lt (n , +-comm n 1)
suc m ≟ zero = gt (m , +-comm m 1)
suc m ≟ suc n = Trichotomy-suc (m ≟ n)

<-split : m < suc n → (m < n) ⊎ (m ≡ n)
<-split {n = zero} = inr ∘ snd ∘ m+n≡0→m≡0×n≡0 ∘ snd ∘ pred-≤-pred
<-split {zero} {suc n} = λ _ → inl (suc-≤-suc zero-≤)
<-split {suc m} {suc n} = ⊎.map suc-≤-suc (cong suc) ∘ <-split ∘ pred-≤-pred

private
  acc-suc : Acc _<_ n → Acc _<_ (suc n)
  acc-suc a
    = acc λ y y<sn
    → case <-split y<sn of λ
    { (inl y<n) → access a y y<n
    ; (inr y≡n) → subst _ (sym y≡n) a
    }

<-wellfounded : WellFounded _<_
<-wellfounded zero = acc λ _ → ⊥.rec ∘ ¬-<-zero
<-wellfounded (suc n) = acc-suc (<-wellfounded n)

<→≢ : n < m → ¬ n ≡ m
<→≢ {n} {m} p q = ¬m<m (subst (_< m) q p)

module _
    (b₀ : ℕ)
    (P : ℕ → Type₀)
    (base : ∀ n → n < suc b₀ → P n)
    (step : ∀ n → P n → P (suc b₀ + n))
  where
  open WFI (<-wellfounded)

  private
    dichotomy : ∀ b n → (n < b) ⊎ (Σ[ m ∈ ℕ ] n ≡ b + m)
    dichotomy b n
      = case n ≟ b return (λ _ → (n < b) ⊎ (Σ[ m ∈ ℕ ] n ≡ b + m)) of λ
      { (lt o) → inl o
      ; (eq p) → inr (0 , p ∙ sym (+-zero b))
      ; (gt (m , p)) → inr (suc m , sym p ∙ +-suc m b ∙ +-comm (suc m) b)
      }

    dichotomy<≡ : ∀ b n → (n<b : n < b) → dichotomy b n ≡ inl n<b
    dichotomy<≡ b n n<b
      = case dichotomy b n return (λ d → d ≡ inl n<b) of λ
      { (inl x) → cong inl (m≤n-isProp x n<b)
      ; (inr (m , p)) → ⊥.rec (<-asym n<b (m , sym (p ∙ +-comm b m)))
      }

    dichotomy+≡ : ∀ b m n → (p : n ≡ b + m) → dichotomy b n ≡ inr (m , p)
    dichotomy+≡ b m n p
      = case dichotomy b n return (λ d → d ≡ inr (m , p)) of λ
      { (inl n<b) → ⊥.rec (<-asym n<b (m , +-comm m b ∙ sym p))
      ; (inr (m' , q))
      → cong inr (Σ≡Prop (λ x → isSetℕ n (b + x)) (inj-m+ {m = b} (sym q ∙ p)))
      }

    b = suc b₀

    lemma₁ : ∀{x y z} → x ≡ suc z + y → y < x
    lemma₁ {y = y} {z} p = z , +-suc z y ∙ sym p

    subStep : (n : ℕ) → (∀ m → m < n → P m) → (n < b) ⊎ (Σ[ m ∈ ℕ ] n ≡ b + m) → P n
    subStep n _   (inl l) = base n l
    subStep n rec (inr (m , p))
      = transport (cong P (sym p)) (step m (rec m (lemma₁ p)))

    wfStep : (n : ℕ) → (∀ m → m < n → P m) → P n
    wfStep n rec = subStep n rec (dichotomy b n)

    wfStepLemma₀ : ∀ n (n<b : n < b) rec → wfStep n rec ≡ base n n<b
    wfStepLemma₀ n n<b rec = cong (subStep n rec) (dichotomy<≡ b n n<b)

    wfStepLemma₁ : ∀ n rec → wfStep (b + n) rec ≡ step n (rec n (lemma₁ refl))
    wfStepLemma₁ n rec
      = cong (subStep (b + n) rec) (dichotomy+≡ b n (b + n) refl)
      ∙ transportRefl _

  +induction : ∀ n → P n
  +induction = induction wfStep

  +inductionBase : ∀ n → (l : n < b) → +induction n ≡ base n l
  +inductionBase n l = induction-compute wfStep n ∙ wfStepLemma₀ n l _

  +inductionStep : ∀ n → +induction (b + n) ≡ step n (+induction n)
  +inductionStep n = induction-compute wfStep (b + n) ∙ wfStepLemma₁ n _

module <-Reasoning where
  -- TODO: would it be better to mirror the way it is done in the agda-stdlib?
  infixr 2 _<⟨_⟩_ _≤<⟨_⟩_ _≤⟨_⟩_ _<≤⟨_⟩_ _≡<⟨_⟩_ _≡≤⟨_⟩_ _<≡⟨_⟩_ _≤≡⟨_⟩_
  _<⟨_⟩_ : ∀ k → k < n → n < m → k < m
  _ <⟨ p ⟩ q = <-trans p q

  _≤<⟨_⟩_ : ∀ k → k ≤ n → n < m → k < m
  _ ≤<⟨ p ⟩ q = ≤<-trans p q

  _≤⟨_⟩_ : ∀ k → k ≤ n → n ≤ m → k ≤ m
  _ ≤⟨ p ⟩ q = ≤-trans p q

  _<≤⟨_⟩_ : ∀ k → k < n → n ≤ m → k < m
  _ <≤⟨ p ⟩ q = <≤-trans p q

  _≡≤⟨_⟩_ : ∀ k → k ≡ l → l ≤ m → k ≤ m
  _ ≡≤⟨ p ⟩ q = subst (λ k → k ≤ _) (sym p) q

  _≡<⟨_⟩_ : ∀ k → k ≡ l → l < m → k < m
  _ ≡<⟨ p ⟩ q = _ ≡≤⟨ cong suc p ⟩ q

  _≤≡⟨_⟩_ : ∀ k → k ≤ l → l ≡ m → k ≤ m
  _ ≤≡⟨ p ⟩ q = subst (λ l → _ ≤ l) q p

  _<≡⟨_⟩_ : ∀ k → k < l → l ≡ m → k < m
  _ <≡⟨ p ⟩ q = _ ≤≡⟨ p ⟩ q

max_stars_repo_name: L-TChen/cubical

max_issues_repo_name: L-TChen/cubical

max_forks_repo_name: L-TChen/cubical


text:
module O where

open import Data.Product
open import Function renaming (_∘_ to _○_)

open import Circle

------------------------------------------------------------------------------
-- Abstract interpretation:
-- natural numbers with paths equating all even numbers in one
-- connected component and all odd numbers in another connected
-- component

-- module with 0,1,2,3,4 ... this is the concrete domain

data N : Set where
  Zero  : N
  One   : N
  Two   : N
  Three : N
  Four  : N

recN : (C : Set) → C → C → C → C → C → N → C
recN C c0 c1 c2 c3 c4 Zero = c0
recN C c0 c1 c2 c3 c4 One = c1
recN C c0 c1 c2 c3 c4 Two = c2
recN C c0 c1 c2 c3 c4 Three = c3
recN C c0 c1 c2 c3 c4 Four = c4

-- module for the abstract domain {even, odd} except that we don't define it
-- this way: we simply add paths between the even elements and paths between
-- the odd elements

module Parity where

  private
    data N* : Set where
      Zero*  : N*
      One*   : N*
      Two*   : N*
      Three* : N*
      Four*  : N*

  NA : Set
  NA = N*

  zero : NA
  zero = Zero*

  one : NA
  one = One*

  two : NA
  two = Two*

  three : NA
  three = Three*

  four : NA
  four = Four*

  postulate
    even02 : Zero* ≡ Two*
    even04 : Zero* ≡ Four*
    odd13  : One* ≡ Three*

  recNA : (C : Set) → (c0 c1 c2 c3 c4 : C) →
    (ceven02 : c0 ≡ c2) → (ceven04 : c0 ≡ c4) → (codd13 : c1 ≡ c3) →
    NA → C
  recNA C c0 c1 c2 c3 c4 _ _ _ Zero* = c0
  recNA C c0 c1 c2 c3 c4 _ _ _ One* = c1
  recNA C c0 c1 c2 c3 c4 _ _ _ Two* = c2
  recNA C c0 c1 c2 c3 c4 _ _ _ Three* = c3
  recNA C c0 c1 c2 c3 c4 _ _ _ Four* = c4

open Parity

-- Now we define functions back and forth

abs : N → NA
abs = recN NA zero one two three four

con : NA → N
con = recNA N Two Three Two Three Two (refl Two) (refl Two) (refl Three)

-- Computations on N and NA can be related
-- Concrete computation

incN : N → N

incN Zero = One
incN One = Two
incN Two = Three
incN Three = Four
incN Four = Zero

-- we can apply an operation in the abstract domain and report the
-- approximate result

absF : (N → N) → (NA → NA)
absF f = abs ○ f ○ con

approx : (N → N) → (N → N)
approx f n = con ((absF f) (abs n))

test0 : approx incN Zero ≡ Three
test0 = refl Three

test1 : approx incN One ≡ Two
test1 = refl Two

test2 : approx incN Two ≡ Three
test2 = refl Three

test3 : approx incN Three ≡ Two
test3 = refl Two

test4 : approx incN Four ≡ Three
test4 = refl Three

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
{-# OPTIONS --prop #-}

{-# TERMINATING #-}
makeloop : {P : Prop} → P → P
makeloop p = makeloop p

postulate
  A : Set
  B C : A → Prop

record AB : Set where
  no-eta-equality  -- the problem goes away if this is left out
  constructor _,_
  field
    a : A
    b : B a
open AB public

-- -- Same problem if replacing the no-eta record by a datatype
-- data AB : Set where
--   _,_ : (a : A) → B a → AB

-- a : AB → A
-- a (x , y) = x

-- b : (z : AB) → B (a z)
-- b (x , y) = y

record ABC : Set where
  constructor _,_
  field
    ab : AB
    c : C (a ab)  -- the problem goes away if this field is left out
open ABC public

f : AB → ABC
f ab = (a ab , makeloop (b ab)) , {!!}

postulate
  P : ABC → Prop
  g : (ab : AB) → P (f ab)

works : (ab : AB) → P (f ab)
works ab = g ab

loops : (ab : AB) → P (f ab)
loops ab = g _

-- WAS: Agda loops while typechecking @loops@
-- SHOULD: succeed (with unsolved metas)


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

open import HoTT
open import groups.SuspAdjointLoop
open import groups.ToOmega
open import cohomology.Theory

{- A spectrum (family (Eₙ | n : ℤ) such that ΩEₙ₊₁ = Eₙ)
 - gives rise to a cohomology theory C with Cⁿ(S⁰) = π₁(Eₙ₊₁). -}

module cohomology.SpectrumModel
  {i} (E : ℤ → Ptd i) (spectrum : (n : ℤ) → ⊙Ω (E (succ n)) ⊙≃ E n) where

module SpectrumModel where

  {- Definition of cohomology group C -}
  module _ (n : ℤ) (X : Ptd i) where
    C : Group i
    C = Trunc-⊙→Ω-group X (E (succ n))

    {- convenient abbreviations -}
    CEl = Group.El C
    ⊙CEl = Group.⊙El C
    Cid = Group.ident C

    {- before truncation -}
    uCEl = X ⊙→ ⊙Ω (E (succ n))

  {- Cⁿ(X) is an abelian group -}
  C-is-abelian : (n : ℤ) (X : Ptd i) → is-abelian (C n X)
  C-is-abelian n X =
    iso-preserves-abelian (Trunc-⊙→Ω-group-emap-codom X (spectrum (succ n))) $
      Trunc-group-abelian (⊙→Ω-group-structure _ _) $ λ {(f , fpt) (g , gpt) →
        ⊙λ=' (λ x → Ω^2-∙-comm (f x) (g x)) (pt-lemma fpt gpt)}
    where
    pt-lemma : ∀ {i} {A : Type i} {x : A} {p q : idp {a = x} == idp {a = x}}
      (α : p == idp) (β : q == idp)
      →  ⊙∘-pt (fst ⊙Ω-∙) (⊙fanout-pt α β) idp
      == ⊙∘-pt (fst ⊙Ω-∙) (⊙fanout-pt β α) idp
       [ _== idp ↓ Ω^2-∙-comm p q ]
    pt-lemma idp idp = idp

  {- C-fmap, the functorial action of C:
   - contravariant functor from pointed spaces to abelian groups -}
  module _ (n : ℤ) {X Y : Ptd i} where

    C-fmap : X ⊙→ Y → (C n Y →ᴳ C n X)
    C-fmap f = Trunc-⊙→Ω-group-fmap-dom f (E (succ n))

    CEl-fmap : X ⊙→ Y → CEl n Y → CEl n X
    CEl-fmap F = GroupHom.f (C-fmap F)

    ⊙CEl-fmap : X ⊙→ Y → ⊙CEl n Y ⊙→ ⊙CEl n X
    ⊙CEl-fmap F = GroupHom.⊙f (C-fmap F)

  {- C-fmap is a functor from pointed spaces to abelian groups -}
  module _ (n : ℤ) {X : Ptd i} where

    C-fmap-idf : ∀ x → CEl-fmap n {X} {X} (⊙idf X) x == x
    C-fmap-idf x = ap (λ h → GroupHom.f h x) (Trunc-⊙→Ω-group-fmap-dom-idf (E (succ n)))

    C-fmap-∘ : {Y Z : Ptd i} (g : Y ⊙→ Z) (f : X ⊙→ Y)
      → ∀ x → CEl-fmap n (g ⊙∘ f) x == CEl-fmap n f (CEl-fmap n g x)
    C-fmap-∘ g f x = ap (λ h → GroupHom.f h x) (Trunc-⊙→Ω-group-fmap-dom-∘ g f (E (succ n)))

  -- Eilenberg-Steenrod Axioms

  {- Susp Axiom -}
  private
    C-Susp' : {E₁ E₀ : Ptd i} (iso : ⊙Ω E₁ ⊙≃ E₀) (X : Ptd i)
      → Trunc-⊙→Ω-group (⊙Susp X) E₁ ≃ᴳ Trunc-⊙→Ω-group X E₀
    C-Susp' {E₁ = E₁} iso X = Trunc-⊙→Ω-group-emap-codom X iso
                          ∘eᴳ Trunc-⊙→Ω-iso-Trunc-⊙→Ω X E₁

    -- This can be further simplified
    C-Susp-fmap' : {E₁ E₀ : Ptd i} (iso : ⊙Ω E₁ ⊙≃ E₀) {X Y : Ptd i} (f : X ⊙→ Y)
      → CommSquareᴳ
          (Trunc-⊙→Ω-group-fmap-dom (⊙Susp-fmap f) E₁)
          (Trunc-⊙→Ω-group-fmap-dom f E₀)
          (fst (C-Susp' iso Y)) (fst (C-Susp' iso X))
    C-Susp-fmap' {E₁} {E₀} iso {X} {Y} f = comm-sqrᴳ λ x →
        GroupHom.f (Trunc-⊙→Ω-group-fmap-codom X (fst iso))
          (GroupIso.f (Trunc-⊙→Ω-iso-Trunc-⊙→Ω X E₁)
            (GroupHom.f (Trunc-⊙→Ω-group-fmap-dom (⊙Susp-fmap f) E₁) x))
          =⟨ Trunc-⊙→Ω-iso-Trunc-⊙→Ω-nat-dom f E₁
            |in-ctx (λ h → GroupHom.f h x)
            |in-ctx GroupHom.f (Trunc-⊙→Ω-group-fmap-codom X (fst iso)) ⟩
        GroupHom.f (Trunc-⊙→Ω-group-fmap-codom X (fst iso))
          (GroupHom.f (Trunc-⊙→Ω-group-fmap-dom f (⊙Ω E₁))
            (GroupIso.f (Trunc-⊙→Ω-iso-Trunc-⊙→Ω Y E₁) x))
          =⟨ ! $ Trunc-⊙→Ω-group-fmap-nat f (fst iso)
            |in-ctx GroupHom.f
            |in-ctx (λ h → h (GroupIso.f (Trunc-⊙→Ω-iso-Trunc-⊙→Ω Y E₁) x)) ⟩
        GroupHom.f (Trunc-⊙→Ω-group-fmap-dom f E₀)
          (GroupHom.f (Trunc-⊙→Ω-group-fmap-codom Y (fst iso))
            (GroupIso.f (Trunc-⊙→Ω-iso-Trunc-⊙→Ω Y E₁) x))
          =∎

  C-Susp : (n : ℤ) (X : Ptd i) → C (succ n) (⊙Susp X) ≃ᴳ C n X
  C-Susp n X = C-Susp' (spectrum (succ n)) X

  C-Susp-fmap : (n : ℤ) {X Y : Ptd i} (f : X ⊙→ Y)
    → CommSquareᴳ
        (C-fmap (succ n) (⊙Susp-fmap f)) (C-fmap n f)
        (fst (C-Susp n Y)) (fst (C-Susp n X))
  C-Susp-fmap n f = C-Susp-fmap' (spectrum (succ n)) f

  {- Non-truncated Exactness Axiom -}
  module _ (n : ℤ) {X Y : Ptd i} where

    {- precomposing [⊙cfcod' f] and then [f] gives [0] -}
    im-sub-ker-lemma : (f : X ⊙→ Y) (g : uCEl n (⊙Cofiber f))
      → (g ⊙∘ ⊙cfcod' f) ⊙∘ f == ⊙cst
    im-sub-ker-lemma (f , fpt) (g , gpt) = ⊙λ='
      (λ x → ap g (! (cfglue' f x)) ∙ gpt)
      (↓-idf=cst-in
        (ap (g ∘ cfcod) fpt
         ∙ ap g (ap cfcod (! fpt) ∙ ! (cfglue (pt X))) ∙ gpt
           =⟨ lemma cfcod g fpt (! (cfglue (pt X))) gpt ⟩
         ap g (! (cfglue (pt X))) ∙ gpt
           =⟨ ! (∙-unit-r _) ⟩
         (ap g (! (cfglue (pt X))) ∙ gpt) ∙ idp ∎))
      where
      lemma : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k}
        {a₁ a₂ : A} {b : B} {c : C} (f : A → B) (g : B → C)
        (p : a₁ == a₂) (q : f a₁ == b) (r : g b == c)
        → ap (g ∘ f) p ∙ ap g (ap f (! p) ∙ q) ∙ r == ap g q ∙ r
      lemma f g idp idp idp = idp

    {- if g ⊙∘ f is constant then g factors as h ⊙∘ ⊙cfcod' f -}
    ker-sub-im-lemma : (f : X ⊙→ Y) (g : uCEl n Y)
      → g ⊙∘ f == ⊙cst
      → Σ (uCEl n (⊙Cofiber f)) (λ h → h ⊙∘ ⊙cfcod' f == g)
    ker-sub-im-lemma (f , fpt) (h , hpt) p =
      ((g , ! q ∙ hpt) ,
       pair= idp (! (∙-assoc q (! q) hpt) ∙ ap (_∙ hpt) (!-inv-r q)))
      where
      g : Cofiber f → Ω (E (succ n))
      g = CofiberRec.f idp h (! ∘ app= (ap fst p))

      q : h (pt Y) == g (cfbase' f)
      q = ap g (snd (⊙cfcod' (f , fpt)))

  {- Truncated Exactness Axiom -}
  module _ (n : ℤ) {X Y : Ptd i} where

    abstract
      C-im-sub-ker : (f : X ⊙→ Y)
        → im-propᴳ (C-fmap n (⊙cfcod' f)) ⊆ᴳ ker-propᴳ (C-fmap n f)
      C-im-sub-ker f =
        im-sub-ker-in (C-fmap n (⊙cfcod' f)) (C-fmap n f) $
          Trunc-elim
            (ap [_] ∘ im-sub-ker-lemma n f)

    abstract
      C-ker-sub-im : (f : X ⊙→ Y)
        → ker-propᴳ (C-fmap n f) ⊆ᴳ im-propᴳ (C-fmap n (⊙cfcod' f))
      C-ker-sub-im f =
        Trunc-elim
          {{λ _ → Π-level (λ _ → raise-level _ Trunc-level)}}
          (λ h tp → Trunc-rec (lemma h) (–> (Trunc=-equiv _ _) tp))
        where
        lemma : (h : uCEl n Y) → h ⊙∘ f == ⊙cst
          → Trunc -1 (Σ (CEl n (⊙Cofiber f))
                          (λ tk → fst (⊙CEl-fmap n (⊙cfcod' f)) tk == [ h ]))
        lemma h p = [ [ fst wit ] , ap [_] (snd wit) ]
          where
          wit : Σ (uCEl n (⊙Cofiber f)) (λ k → k ⊙∘ ⊙cfcod' f == h)
          wit = ker-sub-im-lemma n f h p

    C-exact : (f : X ⊙→ Y) → is-exact (C-fmap n (⊙cfcod' f)) (C-fmap n f)
    C-exact f = record {im-sub-ker = C-im-sub-ker f; ker-sub-im = C-ker-sub-im f}

  {- Additivity Axiom -}
  module _ (n : ℤ) {A : Type i} (X : A → Ptd i)
    (ac : has-choice 0 A i)
    where

    into : CEl n (⊙BigWedge X) → Trunc 0 (Π A (uCEl n ∘ X))
    into = Trunc-rec (λ H → [ (λ a → H ⊙∘ ⊙bwin a) ])

    module Out' (K : Π A (uCEl n ∘ X)) = BigWedgeRec
      idp
      (fst ∘ K)
      (! ∘ snd ∘ K)

    out : Trunc 0 (Π A (uCEl n ∘ X)) → CEl n (⊙BigWedge X)
    out = Trunc-rec (λ K → [ Out'.f K , idp ])

    into-out : ∀ y → into (out y) == y
    into-out = Trunc-elim
      (λ K → ap [_] (λ= (λ a → pair= idp $
        ap (Out'.f K) (! (bwglue a)) ∙ idp
          =⟨ ∙-unit-r _ ⟩
        ap (Out'.f K) (! (bwglue a))
          =⟨ ap-! (Out'.f K) (bwglue a) ⟩
        ! (ap (Out'.f K) (bwglue a))
          =⟨ ap ! (Out'.glue-β K a) ⟩
        ! (! (snd (K a)))
          =⟨ !-! (snd (K a)) ⟩
        snd (K a) ∎)))

    out-into : ∀ x → out (into x) == x
    out-into = Trunc-elim
      {P = λ tH → out (into tH) == tH}
      (λ {(h , hpt) → ap [_] $ ⊙λ=' (out-into-fst (h , hpt)) (↓-idf=cst-in (! (!-inv-l hpt)))})
      where
      lemma : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
        {a₁ a₂ : A} {b : B} (p : a₁ == a₂) (q : f a₁ == b)
        → ! q ∙ ap f p == ! (ap f (! p) ∙ q)
      lemma f idp idp = idp

      out-into-fst : (H : ⊙BigWedge X ⊙→ ⊙Ω (E (succ n)))
        → ∀ w → Out'.f (λ a → H ⊙∘ ⊙bwin a) w == fst H w
      out-into-fst (h , hpt) = BigWedge-elim
        (! hpt)
        (λ _ _ → idp)
        (λ a → ↓-='-in' $
           ! hpt ∙ ap h (bwglue a)
             =⟨ lemma h (bwglue a) hpt ⟩
           ! (ap h (! (bwglue a)) ∙ hpt)
             =⟨ ! (Out'.glue-β (λ a → (h , hpt) ⊙∘ ⊙bwin a) a) ⟩
           ap (Out'.f (λ a → (h , hpt) ⊙∘ ⊙bwin a)) (bwglue a) ∎)

    abstract
      C-additive-is-equiv : is-equiv (GroupHom.f (Πᴳ-fanout (C-fmap n ∘ ⊙bwin {X = X})))
      C-additive-is-equiv = transport is-equiv
        (λ= $ Trunc-elim
          (λ _ → idp))
        ((ac (uCEl n ∘ X)) ∘ise (is-eq into out into-out out-into))

open SpectrumModel

spectrum-cohomology : CohomologyTheory i
spectrum-cohomology = record {
  C = C;
  C-fmap = C-fmap;
  C-fmap-idf = C-fmap-idf;
  C-fmap-∘ = C-fmap-∘;
  C-is-abelian = C-is-abelian;
  C-Susp = C-Susp;
  C-Susp-fmap = C-Susp-fmap;
  C-exact = C-exact;
  C-additive-is-equiv = C-additive-is-equiv}

spectrum-C-S⁰ : (n : ℤ) → C n (⊙Lift ⊙S⁰) ≃ᴳ πS 0 (E (succ n))
spectrum-C-S⁰ n = Trunc-⊙Bool→Ω-iso-π₁ (E (succ n)) ∘eᴳ Trunc-⊙→Ω-group-emap-dom ⊙lift-equiv (E (succ n))

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Automatic solvers for equations over naturals
------------------------------------------------------------------------

-- See README.Nat for examples of how to use this solver

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

module Data.Nat.Solver where

import Algebra.Solver.Ring.Simple as Solver
import Algebra.Solver.Ring.AlmostCommutativeRing as ACR
open import Data.Nat using (_≟_)
open import Data.Nat.Properties

------------------------------------------------------------------------
-- A module for automatically solving propositional equivalences
-- containing _+_ and _*_

module +-*-Solver =
  Solver (ACR.fromCommutativeSemiring *-+-commutativeSemiring) _≟_


text:
module PreludeAll where
import PreludeBool public
import PreludeNat
import PreludeShow

open PreludeBool
open PreludeNat
open PreludeShow

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
open import Agda.Builtin.Equality

postulate
  X : Set
  rigid0 : ((@0 x : X) → X) → X

mutual
  H : ((@ω x : X) → X) → X
  H f = rigid0 _

  testω : (f : (@0 x : X) → X) → H (\ (@ω x) → f x) ≡ rigid0 (\ (@0 x) → f x)
  testω f = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- Small prelude
------------------------------------------------------------------------

module Prelude where

infixl 6 _+_
infixr 5 _∷_ _++_
infixr 3 _∨_
infix  2 ¬_

------------------------------------------------------------------------
-- Some "logic"

data ⊥ : Set where

¬_ : Set -> Set
¬ a = a -> ⊥

------------------------------------------------------------------------
-- Maybe and Dec

data Maybe (a : Set) : Set where
  just    : a -> Maybe a
  nothing :      Maybe a

data Dec (a : Set) : Set where
  yes :   a -> Dec a
  no  : ¬ a -> Dec a

------------------------------------------------------------------------
-- Lists

data [_] (a : Set) : Set where
  []  : [ a ]
  _∷_ : a -> [ a ] -> [ a ]

_++_ : forall {a} -> [ a ] -> [ a ] -> [ a ]
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

------------------------------------------------------------------------
-- Natural numbers

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

_+_ : ℕ -> ℕ -> ℕ
zero  + n = n
suc m + n = suc (m + n)

{-# BUILTIN NATURAL ℕ    #-}
{-# BUILTIN ZERO    zero #-}
{-# BUILTIN SUC     suc  #-}
{-# BUILTIN NATPLUS _+_  #-}

------------------------------------------------------------------------
-- Booleans

data Bool : Set where
  true  : Bool
  false : Bool

_∨_ : Bool -> Bool -> Bool
true  ∨ _ = true
false ∨ b = b

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
-- Functors from one category into another

module Control.Category.Functor where

open import Level using (suc; _⊔_)
open import Relation.Binary.PropositionalEquality

open import Control.Category
open Category using () renaming (Obj to obj; Hom to hom)

-- Operations of a functor.

-- Module T-FunctorOps C D F provides notation A ⇒ A' for homset C(A,A')
-- and notation B ⇉ B' for homset D(B,B') and the type T-map for the
-- functorial action.

module T-FunctorOps
  {co ch ce} (C : Category co ch ce)
  {δo dh de} (D : Category δo dh de)
             (F : obj C → obj D)
  where
  open HomSet (hom C) using (_⇒_)
  open HomSet (hom D) using () renaming (_⇒_ to _⇉_)

  -- Type of the map function.
  T-map = ∀ {A B} → (A ⇒ B) → F A ⇉ F B

-- Record FunctorOps C D F can be instantiated to define the functorial action
-- map of F.

record FunctorOps
  {co ch ce} (C : Category co ch ce)
  {δo dh de} (D : Category δo dh de) (F : obj C → obj D) : Set (co ⊔ ch ⊔ ce ⊔ δo ⊔ dh ⊔ de)
  where
  open T-FunctorOps C D F

  -- The functorial action (map function).
  field
    map  : T-map

-- Laws of a functor.

-- Module T-FunctorLaws ops provides notation...

module T-FunctorLaws
  {co ch ce} {C : Category co ch ce}
  {δo dh de} {D : Category δo dh de} {F : obj C → obj D}
  (ops : FunctorOps C D F) where

  open FunctorOps ops public

  open Category C using (_⇒_) renaming
    (Obj to ObjC; id to idC; _∘_ to _∘C_)

  open Category D using (_≈_) renaming
    (Obj to ObjD; _⇒_ to _⇉_; id to idD; _∘_ to _∘D_)

  -- First functor law: identity
  T-map-id = ∀ {A} →

      map (idC {A = A}) ≈ idD

  -- Second functor law: composition.
  T-map-∘  = ∀ {A B C} (f : A ⇒ B) {g : B ⇒ C} →

      map (g ∘C f) ≈ (map g ∘D map f)

record FunctorLaws
  {co ch ce} {C : Category co ch ce}
  {δo dh de} {D : Category δo dh de} {F : obj C → obj D}
  (ops : FunctorOps C D F) : Set ((co ⊔ ch ⊔ ce ⊔ δo ⊔ dh ⊔ de)) where
  open T-FunctorLaws ops

  field
    map-id : T-map-id
    map-∘  : T-map-∘

-- Functoriality.

record IsFunctor
  {co ch ce} {C : Category co ch ce}
  {δo dh de} {D : Category δo dh de} (F : obj C → obj D) : Set (co ⊔ ch ⊔ ce ⊔ δo ⊔ dh ⊔ de) where

  field
    ops  : FunctorOps  C D F
    laws : FunctorLaws ops

  open FunctorOps  ops  public
  open FunctorLaws laws public

-- -}

max_stars_repo_name: andreasabel/cubical

max_issues_repo_name: andreasabel/cubical

max_forks_repo_name: andreasabel/cubical


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

module Dodo.Binary.Trichotomous where

-- Stdlib imports
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; _≢_; refl; cong; subst; subst₂) renaming (sym to ≡-sym)
open import Level using (Level)
open import Function using (flip; _∘_; _∘₂_)
open import Data.Empty using (⊥-elim)
open import Data.Product using (_,_)
open import Relation.Unary using (Pred)
open import Relation.Binary using (Rel; Irreflexive; Trichotomous; Tri; tri<; tri≈; tri>)
open import Relation.Binary.Construct.Closure.Transitive using ([_])
-- Local imports
open import Dodo.Unary.Equality
open import Dodo.Binary.Equality
open import Dodo.Binary.Immediate
open import Dodo.Binary.Filter

-- # Definitions

tri-immˡ : {a ℓ₁ ℓ₂ : Level} {A : Set a} {_≈_ : Rel A ℓ₁} {R : Rel A ℓ₂}
  → Trichotomous _≈_ R → {x y z : A}
  → immediate R x z → immediate R y z
    ---------------------------------
  → x ≈ y
tri-immˡ triR {x} {y} {z} (Rxz , ¬∃y) (Ryz , ¬∃x) with triR x y
... | tri<  Rxy x≢y ¬Ryx = ⊥-elim (¬∃y (y , Rxy , [ Ryz ]))
... | tri≈ ¬Rxy x≡y ¬Ryx = x≡y
... | tri> ¬Rxy x≢y  Ryx = ⊥-elim (¬∃x (x , Ryx , [ Rxz ]))

tri-immʳ : {a ℓ₁ ℓ₂ : Level} {A : Set a} {_≈_ : Rel A ℓ₁} {R : Rel A ℓ₂}
  → Trichotomous _≈_ R → {x y z : A}
  → immediate R x y → immediate R x z
    ---------------------------------
  → y ≈ z
tri-immʳ triR {x} {y} {z} (Rxy , ¬∃z) (Rxz , ¬∃y) with triR y z
... | tri<  Ryz y≢z ¬Rzy = ⊥-elim (¬∃y (y , Rxy , [ Ryz ]))
... | tri≈ ¬Ryz y≡z ¬Rzy = y≡z
... | tri> ¬Ryz y≢z  Rzy = ⊥-elim (¬∃z (z , Rxz , [ Rzy ]))

tri-irreflexive : {a ℓ₁ ℓ₂ : Level} {A : Set a} {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂}
  → Trichotomous _≈_ _<_
    --------------------
  → Irreflexive _≈_ _<_
tri-irreflexive triR {x} {y} x≈y x<y with triR x y
... | tri< x<y x≉y x≯y = x≉y x≈y
... | tri≈ x≮y x≈y x≯y = x≮y x<y
... | tri> x≮y x≉y x>y = x≉y x≈y

tri-flip : ∀ {a ℓ : Level} {A : Set a} {R : Rel A ℓ}
  → {x y : A}
  → Tri (R x y) (x ≡ y) (R y x)
    -------------------------------------
  → Tri (flip R x y) (x ≡ y) (flip R y x)
tri-flip (tri<  Rxy x≢y ¬Ryx) = tri> ¬Ryx x≢y  Rxy
tri-flip (tri≈ ¬Rxy x≡y ¬Ryx) = tri≈ ¬Ryx x≡y ¬Rxy
tri-flip (tri> ¬Rxy x≢y  Ryx) = tri<  Ryx x≢y ¬Rxy

trichotomous-flip : ∀ {a ℓ : Level} {A : Set a} {R : Rel A ℓ}
  → Trichotomous _≡_ R
    -------------------------
  → Trichotomous _≡_ (flip R)
trichotomous-flip {R = R} triR = tri-flip {R = R} ∘₂ triR

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


text:
open import Data.Bool using (Bool; true; false; _∧_; _∨_; T)
open import Data.Bool.Properties using (∨-identityˡ; ∨-zeroˡ)
open import Data.List using (List; []; _∷_; any; map; foldl)
open import Data.List.Relation.Unary.Any using (Any; here; there; lookup; satisfied)
open import Data.Product as Prod using (∃; _,_; proj₁; proj₂)
open import Data.Unit using (⊤; tt)
open import Relation.Binary.PropositionalEquality
   using (_≡_; refl; cong; subst; sym; trans; module ≡-Reasoning)
open import Relation.Binary.PropositionalEquality as P
open ≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
open import Data.Nat using (ℕ; zero; suc)

≡→T : ∀ {b : Bool} → b ≡ true → T b
≡→T refl = tt

any-val : ∀ {a} {A : Set a} (f) (ns : List A)
        → any f ns ≡ true
        → Any (λ x → T (f x)) ns
any-val f (n ∷ ns) any-f-⟨n∷ns⟩≡true with f n | P.inspect f n
... | true  | P.[ fn≡t ] = here (≡→T fn≡t)
... | false | _          = there (any-val f ns any-f-⟨n∷ns⟩≡true)

get-val : ∀ {a} {A : Set a} {f} (ns : List A)
        → any f ns ≡ true
        → A
get-val {_} {_} {f} ns any≡true = lookup {xs = ns} (any-val f ns any≡true)

get-prop : ∀ {a} {A : Set a} {f} (ns : List A)
         → any f ns ≡ true
         → ∃ (λ x → T (f x))
get-prop {_} {_} {f} ns any≡true = satisfied {xs = ns} (any-val f ns any≡true)

is-not-zero : ℕ → Bool
is-not-zero zero = false
is-not-zero _ = true

eg1 : any is-not-zero (0 ∷ 0 ∷ 3 ∷ []) ≡ true
eg1 = refl
--proj₁ (get-prop {f = λ x → x} (true ∷ false ∷ []) _)
--proj₁ (get-prop {f = is-not-zero} (0 ∷ 0 ∷ 3 ∷ []) refl)

--data Singleton {a} {A : Set a} (x : A) : Set a where
--  _with≡_ : (y : A) → x ≡ y → Singleton x
--
--inspect : ∀ {a} {A : Set a} (x : A) → Singleton x
--inspect x = x with≡ refl

any-val' : ∀ {a} {A : Set a} (f : A → Bool) (ns : List A)
         → any f ns ≡ true
         → (∃ λ x → T (f x))
any-val' f [] ()
any-val' f (n ∷ ns) anyfnns≡true with f n | P.inspect f n
...   | true  | P.[ fn≡t ] = n , ≡→T fn≡t
...   | false | P.[ fn≡f ] = any-val' f ns anyfnns≡true
--  where
--    anyfns≡true =
--      begin
--        any f ns            ≡⟨ sym (∨-identityˡ (any f ns)) ⟩
--        false ∨ any f ns    ≡⟨ cong (_∨ any f ns) (sym ?) ⟩
--        f n ∨ any f ns      ≡⟨ anyfnns≡true ⟩
--        true
--      ∎


text:
------------------------------------------------------------------------------
-- Well-founded relation on lists based on their length
------------------------------------------------------------------------------

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

module FOTC.Data.List.WF-Relation.LT-Length where

open import FOTC.Base
open import FOTC.Data.List
open import FOTC.Data.Nat.Inequalities

------------------------------------------------------------------------------
-- Well-founded relation on lists based on their length.
LTL : D → D → Set
LTL xs ys = length xs < length ys

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- Forcing of parsers (can be used for inspection/debugging purposes)
------------------------------------------------------------------------

{-# OPTIONS --termination-depth=2 #-}

module TotalParserCombinators.Force where

open import Codata.Musical.Notation
import Data.List.Categorical as ListMonad
open import Data.Maybe hiding (_>>=_)
open import Data.Nat
open import Function
import Relation.Binary.PropositionalEquality as P

open import TotalParserCombinators.Congruence
open import TotalParserCombinators.Laws
open import TotalParserCombinators.Parser

-- force n p returns p, but with the first n layers of delay
-- constructors removed.

force : ∀ {Tok R xs} → ℕ → Parser Tok R xs → Parser Tok R xs
force zero    p                = p
force n       (return x)       = return x
force n       fail             = fail
force n       token            = token
force n       (p₁ ∣ p₂)        = force n p₁ ∣ force n p₂
force n       (f <$> p)        = f <$> force n p
force n       (nonempty p)     = nonempty (force n p)
force n       (cast xs₁≈xs₂ p) = cast xs₁≈xs₂ (force n p)
force (suc n) (p₁ ⊛ p₂)        with forced? p₁ | forced? p₂
... | just xs | nothing = force (suc n)   p₁  ⊛ force      n (♭ p₂)
... | just xs | just fs = force (suc n)   p₁  ⊛ force (suc n)   p₂
... | nothing | nothing = force      n (♭ p₁) ⊛ force      n (♭ p₂)
... | nothing | just fs =
  P.subst (Parser _ _) (ListMonad.Applicative.right-zero fs) $
                          force      n (♭ p₁) ⊛ force (suc n)   p₂
force (suc n) (p₁ >>= p₂)      with forced? p₁ | forced?′ p₂
... | just f  | nothing = force (suc n)   p₁  >>= λ x → force      n (♭ (p₂ x))
... | just f  | just xs = force (suc n)   p₁  >>= λ x → force (suc n)   (p₂ x)
... | nothing | nothing = force      n (♭ p₁) >>= λ x → force      n (♭ (p₂ x))
... | nothing | just xs =
  P.subst (Parser _ _) (ListMonad.MonadProperties.right-zero xs) $
                          force n (♭ p₁) >>= λ x → force (suc n) (p₂ x)

-- force preserves the semantics of its argument.

correct : ∀ {Tok R xs} (n : ℕ) (p : Parser Tok R xs) → force n p ≅P p
correct zero    p                = p ∎
correct (suc n) (return x)       = return x ∎
correct (suc n) fail             = fail ∎
correct (suc n) token            = token ∎
correct (suc n) (p₁ ∣ p₂)        = correct (suc n) p₁ ∣ correct (suc n) p₂
correct (suc n) (f <$> p)        = (λ _ → P.refl) <$> correct (suc n) p
correct (suc n) (nonempty p)     = nonempty (correct (suc n) p)
correct (suc n) (cast xs₁≈xs₂ p) = cast (correct (suc n) p)
correct (suc n) (p₁ ⊛ p₂)        with forced? p₁ | forced? p₂
... | just xs | nothing = [ ○ - ○ - ○ - ◌ ] correct (suc n)   p₁  ⊛ correct      n (♭ p₂)
... | just xs | just fs = [ ○ - ○ - ○ - ○ ] correct (suc n)   p₁  ⊛ correct (suc n)   p₂
... | nothing | nothing = [ ○ - ◌ - ○ - ◌ ] correct      n (♭ p₁) ⊛ correct      n (♭ p₂)
... | nothing | just fs =
  P.subst (Parser _ _) lemma forced  ≅⟨ Subst.correct lemma ⟩
  forced                             ≅⟨ [ ○ - ◌ - ○ - ○ ] correct n (♭ p₁) ⊛ correct (suc n) p₂ ⟩
  p₁ ⊛ p₂                            ∎
  where
  lemma  = ListMonad.Applicative.right-zero fs
  forced = force n (♭ p₁) ⊛ force (suc n) p₂
correct (suc n) (p₁ >>= p₂)      with forced? p₁ | forced?′ p₂
... | just f  | nothing = [ ○ - ○ - ○ - ◌ ] correct (suc n)   p₁  >>= λ x → correct      n (♭ (p₂ x))
... | just f  | just xs = [ ○ - ○ - ○ - ○ ] correct (suc n)   p₁  >>= λ x → correct (suc n)   (p₂ x)
... | nothing | nothing = [ ○ - ◌ - ○ - ◌ ] correct      n (♭ p₁) >>= λ x → correct      n (♭ (p₂ x))
... | nothing | just xs =
  P.subst (Parser _ _) lemma forced  ≅⟨ Subst.correct lemma ⟩
  forced                             ≅⟨ [ ○ - ◌ - ○ - ○ ] correct n (♭ p₁) >>= (λ x → correct (suc n) (p₂ x)) ⟩
  p₁ >>= p₂                          ∎
  where
  forced = force n (♭ p₁) >>= λ x → force (suc n) (p₂ x)
  lemma  = ListMonad.MonadProperties.right-zero xs

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
-- Christian Sattler, 2017-08-05
-- Nullary extended lambdas are useful in the interaction mode
-- for case splitting on the result inside an expression.
module NullaryExtendedLambda where

f : {A : Set} → A → A
f a = λ { → a }

g : {A : Set} → A → A
g a = λ where
  → a


text:
module binio where

open import Data.Word8
import Data.ByteString as BS
import Data.ByteString.IO as BSIO
open import Data.Fin using (Fin; toℕ)
open import Data.Vec using (Vec; toList; tabulate)
open import Data.List using (List)
open import Data.Colist using (Colist; fromList)
open import Agda.Builtin.Nat using (Nat; zero; suc; _<_)
open import IO
open import Coinduction using (♯_)

{-
instance
  finN<N : {n : Nat} {f : Fin n} → IsTrue (toℕ f < n)
  finN<N {.(suc _)} {Fin.zero} = itis
  finN<N {.(suc _)} {Fin.suc f} = finN<N {_} {f}

fin256 : Fin 256 → Word8
fin256 f = fromNat (toℕ f) {{finN<N {256} {f}}}

b256 : Colist Word8
b256 = fromList (toList (tabulate {256} fin256))
-}

fin256 : Fin 256 → Word8
fin256 f = primWord8fromNat (toℕ f)

b256 : List Word8
b256 = toList (tabulate {256} fin256)

b256′ : Colist Word8
b256′ = fromList b256

-- main = run (writeBinaryFile "256.bin" b256)
-- main = run (♯ readBinaryFile "256.bin" >>= λ x → ♯ writeBinaryFile "256'.bin" x)
-- main = run (readFile "256.bin")

main = run (BSIO.writeBinaryFile′ "256.bin" b256)
-- main = run (BS.IO.writeBinaryFile′ "256'.bin" b256′)

-- main = run (BS.IO.writeBinaryFile′ "256.bin" b256 >> BS.IO.writeBinaryFile′ "256'.bin" b256′)

max_stars_repo_name: semenov-vladyslav/bytes-agda

max_issues_repo_name: semenov-vladyslav/bytes-agda

max_forks_repo_name: semenov-vladyslav/bytes-agda


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Construction.Comma where

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

open import Categories.Category.Instance.One
open import Categories.Category using (Category; _[_,_]; _[_∘_])
open import Categories.Functor using (Functor)
open import Categories.Functor.Construction.Constant using (const!)
import Categories.Morphism.Reasoning as MR

private
  variable
    o₁ ℓ₁ e₁ o₂ ℓ₂ e₂ o₃ ℓ₃ e₃ : Level

-- things go odd with generalized variables for A B C, use anonymous module instead
module _ {A : Category o₁ ℓ₁ e₁}  {B : Category o₂ ℓ₂ e₂} {C : Category o₃ ℓ₃ e₃} where
  private
    module C = Category C
    module A = Category A
    module B = Category B

  record CommaObj (T : Functor A C) (S : Functor B C) : Set (o₁ ⊔ o₂ ⊔ ℓ₃) where
    open Category
    open Functor T renaming (F₀ to T₀)
    open Functor S renaming (F₀ to S₀)
    field
      {α} : Obj A
      {β} : Obj B
      f   : C [ T₀ α , S₀ β ]

  record Comma⇒ {T : Functor A C} {S : Functor B C} (X₁ X₂ : CommaObj T S) : Set (ℓ₁ ⊔ ℓ₂ ⊔ e₃) where
    open CommaObj X₁ renaming (α to α₁; β to β₁; f to f₁)
    open CommaObj X₂ renaming (α to α₂; β to β₂; f to f₂)
    open Functor T renaming (F₁ to T₁)
    open Functor S renaming (F₁ to S₁)

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

  Comma : Functor A C → Functor B C → Category _ _ _
  Comma T S = record
    { Obj         = CommaObj T S
    ; _⇒_         = Comma⇒
    ; _≈_         = λ a₁ a₂ → g a₁ A.≈ g a₂ × h a₁ B.≈ h a₂
    ; _∘_         = _∘′_
    ; id          = record { g = A.id ; h = B.id ; commute = id-comm }
    ; assoc       = A.assoc , B.assoc
    ; sym-assoc   = A.sym-assoc , B.sym-assoc
    ; identityˡ   = A.identityˡ , B.identityˡ
    ; identityʳ   = A.identityʳ , B.identityʳ
    ; identity²   = A.identity² , B.identity²
    ; equiv = record
      { refl  = A.Equiv.refl , B.Equiv.refl
      ; sym   = map A.Equiv.sym B.Equiv.sym
      ; trans = zip A.Equiv.trans B.Equiv.trans
      }
    ; ∘-resp-≈    = zip A.∘-resp-≈ B.∘-resp-≈
    } module Comma
    where
      module T = Functor T
      module S = Functor S

      open T using () renaming (F₀ to T₀; F₁ to T₁)
      open S using () renaming (F₀ to S₀; F₁ to S₁)
      open Comma⇒
      id-comm : {E : CommaObj T S} → let open CommaObj E in
         (S₁ B.id C.∘ f) C.≈ f C.∘ T₁ A.id
      id-comm {E} = begin
        (S₁ B.id C.∘ f) ≈⟨ S.identity ⟩∘⟨refl ⟩
        C.id C.∘ f      ≈⟨ id-comm-sym ⟩
        f C.∘ C.id      ≈˘⟨ refl⟩∘⟨ T.identity ⟩
        f C.∘ T₁ A.id ∎
        where
          open C.HomReasoning
          open CommaObj E
          open MR C

      _∘′_ : ∀ {X₁ X₂ X₃} → Comma⇒ X₂ X₃ → Comma⇒ X₁ X₂ → Comma⇒ X₁ X₃
      _∘′_ {X₁} {X₂} {X₃} a₁ a₂ = record
        { g = A [ g₁ ∘ g₂ ]
        ; h = B [ h₁ ∘ h₂ ]
        ; commute = begin
          S₁ (h₁ B.∘ h₂) C.∘ f₁      ≈⟨ S.homomorphism ⟩∘⟨refl ○ C.assoc ⟩
          S₁ h₁ C.∘  (S₁ h₂ C.∘ f₁)  ≈⟨  refl⟩∘⟨ commutes₂ ⟩
          S₁ h₁ C.∘  (f₂ C.∘ T₁ g₂)  ≈˘⟨  C.assoc ⟩
          (S₁ h₁ C.∘  f₂) C.∘ T₁ g₂  ≈⟨ commutes₁ ⟩∘⟨refl ⟩
          (f₃ C.∘ T₁ g₁) C.∘ T₁ g₂   ≈⟨ C.assoc ○ refl⟩∘⟨ ⟺ T.homomorphism ⟩
          f₃ C.∘ T₁ (g₁ A.∘ g₂) ∎
        }
        where
        open C.HomReasoning
        open Comma⇒ a₁ renaming (g to g₁; h to h₁; commute to commutes₁)
        open Comma⇒ a₂ renaming (g to g₂; h to h₂; commute to commutes₂)
        open CommaObj X₁ renaming (α to α₁; β to β₁; f to f₁)
        open CommaObj X₂ renaming (α to α₂; β to β₂; f to f₂)
        open CommaObj X₃ renaming (α to α₃; β to β₃; f to f₃)

  infix 4 _↓_
  _↓_ : (S : Functor A C) (T : Functor B C) → Category _ _ _
  S ↓ T = Comma S T

  Dom : (T : Functor A C) → (S : Functor B C) → Functor (Comma T S) A
  Dom T S = record
    { F₀ = CommaObj.α
    ; F₁ = Comma⇒.g
    ; identity = refl
    ; homomorphism = refl
    ; F-resp-≈ = proj₁
    }
   where
    open Comma T S
    open A.Equiv

  Cod : (T : Functor A C) → (S : Functor B C) → Functor (Comma T S) B
  Cod T S = record
    { F₀ = CommaObj.β
    ; F₁ = Comma⇒.h
    ; identity = refl
    ; homomorphism = refl
    ; F-resp-≈ = proj₂
    }
   where
    open Comma T S
    open B.Equiv

module _ {C : Category o₁ ℓ₁ e₁} {D : Category o₂ ℓ₂ e₂} where
  private
    module C = Category C

  infix 4 _↙_ _↘_
  _↙_ : (X : C.Obj) (T : Functor D C) → Category _ _ _
  X ↙ T = const! X ↓ T

  _↘_ : (S : Functor D C) (X : C.Obj) → Category _ _ _
  S ↘ X = S ↓ const! X

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
module Lib.Maybe where

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just    : A -> Maybe A

{-# COMPILED_DATA Maybe Maybe Nothing Just #-}


text:
-- A memoised implementation of the Fibonacci sequence, following
-- Hinze's "Memo functions, polytypically!".

module Issue2918 where

open import Agda.Builtin.IO
open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Size
open import Agda.Builtin.Unit

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

open _×_ public

mutual

  data Nat (i : Size) : Set where
    zero : Nat i
    suc  : Nat′ i → Nat i

  data Nat′ (i : Size) : Set where
    [_] : {j : Size< i} → Nat j → Nat′ i

mutual

  ℕ→Nat : ℕ → Nat ∞
  ℕ→Nat zero    = zero
  ℕ→Nat (suc n) = suc (ℕ→Nat′ n)

  ℕ→Nat′ : ℕ → Nat′ ∞
  ℕ→Nat′ n = [ ℕ→Nat n ]

mutual

  Nat′[_]→ : Size → Set → Set
  Nat′[ i ]→ A = A × Nat′[ i ]→′ A

  record Nat′[_]→′ (i : Size) (A : Set) : Set where
    coinductive
    field
      force : {j : Size< i} → Nat′[ j ]→ A

open Nat′[_]→′ public

tabulate : ∀ {i} {A : Set} → (Nat′ i → A) → Nat′[ i ]→′ A
force (tabulate f) = f [ zero ] , tabulate (λ n → f [ suc n ])

lookup : ∀ {i} {A : Set} → Nat′[ i ]→′ A → Nat′ i → A
lookup t [ zero  ] = proj₁ (force t)
lookup t [ suc n ] = lookup (proj₂ (force t)) n

memo-fix :
  {A : Set} →
  (∀ {i} → (Nat′ i → A) → (Nat i → A)) →
  ∀ {i} → Nat′ i → A
memo-fix f =
  wrapper λ { [ n ] → f (lookup (tabulate (memo-fix f))) n }
  where
  wrapper : ∀ {i} {A : Set} → (Nat′ i → A) → (Nat′ i → A)
  wrapper f [ n ] = f [ n ]

fib-step : ∀ {i} → (Nat′ i → ℕ) → (Nat i → ℕ)
fib-step fib zero            = 0
fib-step fib (suc [ zero ])  = 1
fib-step fib (suc [ suc n ]) = fib n + fib [ suc n ]

fib : ℕ → ℕ
fib n = memo-fix fib-step [ ℕ→Nat n ]

postulate
  crash-after-ten-seconds : ℕ → IO ⊤

{-# FOREIGN GHC
  import qualified Control.Exception
  import qualified System.Timeout

  crashAfterTenSeconds c = do
    r <- System.Timeout.timeout (10 * 10^6)
                                (Control.Exception.evaluate c)
    case r of
      Nothing -> error "The computation timed out"
      Just _  -> return ()
  #-}

{-# COMPILE GHC crash-after-ten-seconds = crashAfterTenSeconds #-}

main : IO ⊤
main = crash-after-ten-seconds (fib 300)


text:
{-# OPTIONS --cubical #-}
module leibniz where

open import Cubical.Data.Equality
open import Cubical.Foundations.Function using (_∘_)

module Martin-Löf {ℓ} {A : Set ℓ} where

  reflexive≡ : {a : A} → a ≡p a
  reflexive≡ = reflp

  symmetric≡ : {a b : A} → a ≡p b → b ≡p a
  symmetric≡ reflp = reflp

  transitive≡ : {a b c : A} → a ≡p b → b ≡p c → a ≡p c
  transitive≡ reflp reflp = reflp

open Martin-Löf public

ext : ∀ {ℓ ℓ′} {A : Set ℓ} {B : A → Set ℓ′} {f g : (a : A) → B a} →
            (∀ (a : A) → f a ≡p g a) → f ≡p g
ext p = ctop (funExt (ptoc ∘ p))

module Leibniz {A : Set} where

  _≐_ : (a b : A) → Set₁
  a ≐ b = (P : A → Set) → P a → P b

  reflexive≐ : {a : A} → a ≐ a
  reflexive≐ P Pa = Pa

  transitive≐ : {a b c : A} → a ≐ b → b ≐ c → a ≐ c
  transitive≐ a≐b b≐c P Pa = b≐c P (a≐b P Pa)

  symmetric≐ : {a b : A} → a ≐ b → b ≐ a
  symmetric≐ {a} {b} a≐b P = Qb
    where
      Q : A → Set
      Q c = P c → P a
      Qa : Q a
      Qa = reflexive≐ P
      Qb : Q b
      Qb = a≐b Q Qa

open Leibniz

T : Set → Set₁
T A = ∀ (X : Set) → (A → X) → X

module WarmUp (A : Set) where

  postulate
    paramT : (t : T A) → (X X′ : Set) (R : X → X′ → Set) →
             (k : A → X) (k′ : A → X′) (kR : (a : A) → R (k a) (k′ a)) →
             R (t X k) (t X′ k′)

  i : A → T A
  i a X k = k a

  id : A → A
  id a = a

  j : T A → A
  j t = t A id

  ji : (a : A) → (j (i a) ≡p a)
  ji a = reflp

  ijₑₓₜ : (t : T A) (X : Set) (k : A → X) → (i (j t) X k ≡p t X k)
  ijₑₓₜ t X k = paramT t A X R id k (λ a → reflp)
    where
      R : A → X → Set
      R a x = k a ≡p x

  ij : (t : T A) → (i (j t) ≡p t)
  ij t = ext (λ X → ext (λ k → ijₑₓₜ t X k))

module MainResult (A : Set) where

  postulate
    param≐ : {a b : A} (a≐b : a ≐ b) →
             (P P′ : A → Set) → (R : (c : A) → P c → P′ c → Set) →
                (Pa : P a) (P′a : P′ a) → R a Pa P′a →
                    R b (a≐b P Pa) (a≐b P′ P′a)

  i : {a b : A} (a≡b : a ≡p b) → a ≐ b
  i reflp P Pa = Pa

  j : {a b : A} → a ≐ b → a ≡p b
  j {a} {b} a≐b = Qb
    where
      Q : A → Set
      Q c = a ≡p c
      Qa : Q a
      Qa = reflexive≡
      Qb : Q b
      Qb = a≐b Q Qa

  ji : {a b : A} (a≡b : a ≡p b) → j (i a≡b) ≡p a≡b
  ji reflp = reflp

  ijₑₓₜ : {a b : A} (a≐b : a ≐ b) →
    (P : A → Set) (Pa : P a) → i (j a≐b) P Pa ≡p a≐b P Pa
  ijₑₓₜ {a} a≐b P Pa = param≐ a≐b Q P R reflp Pa reflp
    where
      Q : A → Set
      Q c = a ≡p c
      R : (c : A) (Qc : Q c) (Pc : P c) → Set
      R c Qc Pc = i Qc P Pa ≡p Pc
  ij : {a b : A} (a≐b : a ≐ b) → i (j a≐b) ≡p a≐b
  ij a≐b = ext (λ P → ext (ijₑₓₜ a≐b P))

max_stars_repo_name: guilhermehas/Equality

max_issues_repo_name: guilhermehas/Equality

max_forks_repo_name: guilhermehas/Equality


text:
import cedille-options

module to-string (options : cedille-options.options) where

open import lib
open import cedille-types
open import constants
open import syntax-util
open import ctxt
open import rename
open import general-util

data expr-side : Set where
  left : expr-side
  right : expr-side
  neither : expr-side

not-left : expr-side → 𝔹
not-left left = ff
not-left _ = tt
not-right : expr-side → 𝔹
not-right right = ff
not-right _ = tt

no-parens : {ed : exprd} → {ed' : exprd} → ⟦ ed ⟧ → ⟦ ed' ⟧ → expr-side → 𝔹
no-parens {_} {TERM} _ (IotaPair pi t t' og pi') lr = tt
no-parens {_} {TYPE} _ (TpEq _ t t' _) lr = tt
no-parens {_} {TERM} _ (Beta pi ot ot') lr = tt
no-parens {_} {TERM} _ (Phi pi eq t t' pi') right = tt
no-parens {_} {TERM} _ (Phi pi eq t t' pi') neither = tt
no-parens {_} {TERM} _ (Rho _ _ _ _ _ _) right = tt
no-parens {_} {TERM} _ (Chi _ _ _) right = tt
no-parens {_} {TERM} _ (Delta _ _ _) right = tt
no-parens {_} {TERM} _ (Let _ _ _) lr = tt
no-parens {_} {TERM} _ (Lam _ _ _ _ _ _) lr = tt
no-parens {_} {TERM} _ (Mu _ _ _ _ _ _ _) lr = tt
no-parens {_} {TERM} _ (Mu' _ _ _ _ _ _) lr = tt
no-parens {_} {TYPE} _ (TpLambda _ _ _ _ _) lr = tt
no-parens {_} {TYPE} _ (Abs _ _ _ _ _ _) lr = tt
no-parens {_} {KIND} _ (KndPi _ _ _ _ _) lr = tt
no-parens {_} {TYPE} _ (Iota _ _ _ _ _) lr = tt
no-parens {_} {LIFTINGTYPE} _ (LiftPi _ _ _ _) lr = tt
no-parens{TERM} (App t me t') p lr = is-term-level-app p && not-right lr
no-parens{TERM} (AppTp t T) p lr = is-term-level-app p && not-right lr
no-parens{TERM} (Beta pi ot ot') p lr = tt
no-parens{TERM} (Chi pi mT t) p lr = ff
no-parens{TERM} (Delta pi mT t) p lr = ff
no-parens{TERM} (Epsilon pi lr' m t) p lr = is-eq-op p
no-parens{TERM} (Hole pi) p lr = tt
no-parens{TERM} (IotaPair pi t t' og pi') p lr = tt
no-parens{TERM} (IotaProj t n pi) p lr = tt
no-parens{TERM} (Lam pi l' pi' x oc t) p lr = ff
no-parens{TERM} (Let pi dtT t) p lr = ff
no-parens{TERM} (Open _ _ _) p lr = tt
no-parens{TERM} (Parens pi t pi') p lr = tt
no-parens{TERM} (Phi pi eq t t' pi') p lr = ff
no-parens{TERM} (Rho pi op on eq og t) p lr = ff
no-parens{TERM} (Sigma pi t) p lr = is-eq-op p
no-parens{TERM} (Theta pi theta t lts) p lr = ff
no-parens{TERM} (Var pi x) p lr = tt
no-parens{TERM} (Mu _ _ _ _ _ _ _) p lr = tt
no-parens{TERM} (Mu' _ _ _ _ _ _)  p lr = tt
no-parens{TYPE} (Abs pi b pi' x Tk T) p lr = is-arrow p && not-left lr
no-parens{TYPE} (Iota pi pi' x oT T) p lr = ff
no-parens{TYPE} (Lft pi pi' x t lT) p lr = ff
no-parens{TYPE} (NoSpans T pi) p lr = tt
no-parens{TYPE} (TpApp T T') p lr = is-arrow p || (is-type-level-app p && not-right lr)
no-parens{TYPE} (TpAppt T t) p lr = is-arrow p || (is-type-level-app p && not-right lr)
no-parens{TYPE} (TpArrow T a T') p lr = is-arrow p && not-left lr
no-parens{TYPE} (TpEq _ t t' _) p lr = tt
no-parens{TYPE} (TpHole pi) p lr = tt
no-parens{TYPE} (TpLambda pi pi' x Tk T) p lr = ff
no-parens{TYPE} (TpParens pi T pi') p lr = tt
no-parens{TYPE} (TpVar pi x) p lr = tt
no-parens{TYPE} (TpLet _ _ _) _ _ = ff
no-parens{KIND} (KndArrow k k') p lr = is-arrow p && not-left lr
no-parens{KIND} (KndParens pi k pi') p lr = tt
no-parens{KIND} (KndPi pi pi' x Tk k) p lr = is-arrow p && not-left lr
no-parens{KIND} (KndTpArrow T k) p lr = is-arrow p && not-left lr
no-parens{KIND} (KndVar pi x as) p lr = tt
no-parens{KIND} (Star pi) p lr = tt
no-parens{LIFTINGTYPE} (LiftArrow lT lT') p lr = is-arrow p && not-left lr
no-parens{LIFTINGTYPE} (LiftParens pi lT pi') p lr = tt
no-parens{LIFTINGTYPE} (LiftPi pi x T lT) p lr = is-arrow p && not-left lr
no-parens{LIFTINGTYPE} (LiftStar pi) p lr = tt
no-parens{LIFTINGTYPE} (LiftTpArrow T lT) p lr = is-arrow p && not-left lr
no-parens{TK} _ _ _ = tt
no-parens{QUALIF} _ _ _ = tt
no-parens{ARG} _ _ _ = tt

pattern ced-ops-drop-spine = cedille-options.options.mk-options _ _ _ _ ff _ ff
pattern ced-ops-conv-arr = cedille-options.options.mk-options _ _ _ _ _ _ ff
pattern ced-ops-conv-abs = cedille-options.options.mk-options _ _ _ _ _ _ tt

drop-spine : cedille-options.options → {ed : exprd} → ctxt → ⟦ ed ⟧ → ⟦ ed ⟧
drop-spine ced-ops-drop-spine = h
  where
  drop-mod-args : ctxt → maybeErased → spineApp → spineApp
  drop-mod-args Γ me (v , as) =
    let qv = unqual-all (ctxt-get-qualif Γ) v in qv ,
    maybe-else' (maybe-if (~ v =string qv) ≫maybe ctxt-qualif-args-length Γ me qv)
      as (λ n → reverse (drop n (reverse as)))

  h : {ed : exprd} → ctxt → ⟦ ed ⟧ → ⟦ ed ⟧
  h {TERM} Γ t = maybe-else' (term-to-spapp t) t (spapp-term ∘ drop-mod-args Γ Erased)
  h {TYPE} Γ T = maybe-else' (type-to-spapp T) T (spapp-type ∘ drop-mod-args Γ NotErased)
  h Γ x = x
drop-spine ops Γ x = x

to-string-rewrite : {ed : exprd} → ctxt → cedille-options.options → ⟦ ed ⟧ → Σi exprd ⟦_⟧
to-string-rewrite{TERM} Γ ops (Parens _ t _) = to-string-rewrite Γ ops t
to-string-rewrite{TYPE} Γ ops (TpParens _ T _) = to-string-rewrite Γ ops T
to-string-rewrite{KIND} Γ ops (KndParens _ k _) = to-string-rewrite Γ ops k
to-string-rewrite{LIFTINGTYPE} Γ ops (LiftParens _ lT _) = to-string-rewrite Γ ops lT
to-string-rewrite{TK} Γ ops (Tkt T) = to-string-rewrite Γ ops T
to-string-rewrite{TK} Γ ops (Tkk k) = to-string-rewrite Γ ops k
to-string-rewrite{TYPE} Γ ced-ops-conv-arr (Abs _ me _ ignored-var (Tkt T) T') = , TpArrow T me T'
to-string-rewrite{KIND} Γ ced-ops-conv-arr (KndPi _ _ ignored-var (Tkt T) k) = , KndTpArrow T k
to-string-rewrite{KIND} Γ ced-ops-conv-arr (KndPi _ _ ignored-var (Tkk k) k') = , KndArrow k k'
to-string-rewrite{LIFTINGTYPE} Γ ced-ops-conv-arr (LiftPi _ ignored-var T lT) = , LiftTpArrow T lT
to-string-rewrite{TYPE} Γ ced-ops-conv-abs (TpArrow T me T') = , Abs posinfo-gen me posinfo-gen ignored-var (Tkt T) T'
to-string-rewrite{KIND} Γ ced-ops-conv-abs (KndTpArrow T k) = , KndPi posinfo-gen posinfo-gen ignored-var (Tkt T) k
to-string-rewrite{KIND} Γ ced-ops-conv-abs (KndArrow k k') = , KndPi posinfo-gen posinfo-gen ignored-var (Tkk k) k'
to-string-rewrite{LIFTINGTYPE} Γ ced-ops-conv-abs (LiftTpArrow T lT) = , LiftPi posinfo-gen ignored-var T lT
to-string-rewrite{TERM} Γ ops (Sigma pi (Sigma pi' t)) = to-string-rewrite Γ ops t
to-string-rewrite Γ ops x = , drop-spine ops Γ x

-------------------------------
strM : Set
strM = ∀ {ed} → rope → ℕ → 𝕃 tag → ctxt → maybe ⟦ ed ⟧ → expr-side → rope × ℕ × 𝕃 tag

to-stringh : {ed : exprd} → ⟦ ed ⟧ → strM

strM-Γ : (ctxt → strM) → strM
strM-Γ f s n ts Γ = f Γ s n ts Γ

infixr 4 _≫str_

_≫str_ : strM → strM → strM
(m ≫str m') s n ts Γ pe lr with m s n ts Γ pe lr
(m ≫str m') s n ts Γ pe lr | s' , n' , ts' = m' s' n' ts' Γ pe lr

strAdd : string → strM
strAdd s s' n ts Γ pe lr = s' ⊹⊹ [[ s ]] , n + string-length s , ts

strΓ' : defScope → var → strM → strM
strΓ' ds v m s n ts Γ@(mk-ctxt (fn , mn , ps , q) syms i symb-occs d) pe =
  let gl = ds iff globalScope
      v' = if gl then (mn # v) else v in
  m s n ts (mk-ctxt
      (fn , mn , ps , qualif-insert-params q v' (unqual-local v) (if gl then ps else ParamsNil))
      syms (trie-insert i v' (var-decl , ("missing" , "missing"))) symb-occs d) pe

strΓ : var → strM → strM
strΓ x m s n ts Γ = m s n ts (ctxt-var-decl x Γ)

ctxt-get-file-id : ctxt → (filename : string) → ℕ
ctxt-get-file-id (mk-ctxt mod (syms , mn-fn , mn-ps , ids , id) is os _) =
  trie-lookup-else 0 ids

make-loc-tag : ctxt → (filename start-to end-to : string) → (start-from end-from : ℕ) → tag
make-loc-tag Γ fn s e = make-tag "loc"
  (("fn" , [[ ℕ-to-string (ctxt-get-file-id Γ fn) ]]) ::
   ("s" , [[ s ]]) :: ("e" , [[ e ]]) :: [])

var-loc-tag : ctxt → location → var → (start-from end-from : ℕ) → 𝕃 tag
var-loc-tag Γ ("missing" , "missing") x start end = []
var-loc-tag Γ (fn , pos) x start end =
  [ make-loc-tag Γ fn pos (posinfo-plus-str pos (unqual-local x)) start end ]

var-tags : ctxt → qvar → var → ℕ → ℕ → 𝕃 tag
var-tags Γ qv uqv s e with qv =string (qualif-var Γ uqv)
...| tt = var-loc-tag Γ (ctxt-var-location Γ qv) uqv s e
...| ff = make-tag "shadowed" [] s e :: var-loc-tag Γ (ctxt-var-location Γ qv) uqv s e

strVar : var → strM
strVar v s n ts Γ pe lr =
  let uqv = unqual-local $ unqual-all (ctxt-get-qualif Γ) v
      uqv' = if cedille-options.options.show-qualified-vars options then v else uqv
      n' = n + (string-length uqv') in
  s ⊹⊹ [[ uqv' ]] , n' , var-tags Γ (qualif-var Γ v) uqv n n' ++ ts

-- Only necessary to unqual-local because of module parameters
strBvar : var → (class body : strM) → strM
strBvar v cm bm = strAdd (unqual-local v) ≫str cm ≫str strΓ v bm

strMetaVar : var → span-location → strM
strMetaVar x (fn , pi , pi') s n ts Γ pe lr =
  let n' = n + string-length x in
  s ⊹⊹ [[ x ]] , n' , make-loc-tag Γ fn pi pi' n n' :: ts

strEmpty : strM
strEmpty s n ts Γ pe lr = s , n , ts

{-# TERMINATING #-}
term-to-stringh : term → strM
type-to-stringh : type → strM
kind-to-stringh : kind → strM
liftingType-to-stringh : liftingType → strM
tk-to-stringh : tk → strM
constructors-to-string : dataConsts → strM

params-to-string : params → strM
params-to-string' : strM → params → strM
file-to-string : start → strM
cmds-to-string : cmds → strM → strM
cmd-to-string : cmd → strM → strM
optTerm-to-string : optTerm → string → string → strM
optClass-to-string : optClass → strM
optGuide-to-string : optGuide → strM
optNums-to-string : optNums → strM
optType-to-string : optType → strM
maybeCheckType-to-string : optType → strM
lterms-to-string : lterms → strM
arg-to-string : arg → strM
args-to-string : args → strM
binder-to-string : maybeErased → string
opacity-to-string : opacity → string
maybeErased-to-string : maybeErased → string
lam-to-string : maybeErased → string
leftRight-to-string : leftRight → string
vars-to-string : vars → strM
nums-to-string : nums → strM
theta-to-string : theta → strM
arrowtype-to-string : maybeErased → string
maybeMinus-to-string : maybeMinus → string
optPlus-to-string : optPlus → string
optPublic-to-string : optPublic → string
optAs-to-string : optAs → strM

to-string-ed : {ed : exprd} → ⟦ ed ⟧ → strM
to-string-ed{TERM} = term-to-stringh
to-string-ed{TYPE} = type-to-stringh
to-string-ed{KIND} = kind-to-stringh
to-string-ed{LIFTINGTYPE} = liftingType-to-stringh
to-string-ed{TK} = tk-to-stringh
to-string-ed{ARG} = arg-to-string
to-string-ed{QUALIF} q = strEmpty

to-stringh' : {ed : exprd} → expr-side → ⟦ ed ⟧ → strM
to-stringh' {ed} lr t {ed'} s n ts Γ mp lr' =
  elim-Σi (to-string-rewrite Γ options t) λ t' →
  parens-unless (~ isJust (mp ≫=maybe λ pe → maybe-if (~ no-parens t' pe lr)))
    (to-string-ed t') s n ts Γ (just t') lr
  where
  parens-unless : 𝔹 → strM → strM
  parens-unless p s = if p then s else (strAdd "(" ≫str s ≫str strAdd ")")

to-stringl : {ed : exprd} → ⟦ ed ⟧ → strM
to-stringr : {ed : exprd} → ⟦ ed ⟧ → strM
to-stringl = to-stringh' left
to-stringr = to-stringh' right
to-stringh = to-stringh' neither

constructors-to-string DataNull                        = strEmpty
constructors-to-string (DataCons (DataConst _ x t) ds) =
  strAdd "  | "  ≫str
  strAdd x      ≫str
  strAdd " : "  ≫str
  type-to-stringh  t ≫str
  constructors-to-string ds

tk-to-stringh (Tkt T) = to-stringh T
tk-to-stringh (Tkk k) = to-stringh k

term-to-stringh (App t me t') = to-stringl t ≫str strAdd (" " ^ maybeErased-to-string me) ≫str to-stringr t'
term-to-stringh (AppTp t T) = to-stringl t ≫str strAdd " · " ≫str to-stringr T
term-to-stringh (Beta pi ot ot') = strAdd "β" ≫str optTerm-to-string ot " < " " >" ≫str optTerm-to-string ot' " { " " }"
term-to-stringh (Chi pi mT t) = strAdd "χ" ≫str optType-to-string mT ≫str strAdd " - " ≫str to-stringr t
term-to-stringh (Delta pi mT t) = strAdd "δ" ≫str optType-to-string mT ≫str strAdd " - " ≫str to-stringr t
term-to-stringh (Epsilon pi lr m t) = strAdd "ε" ≫str strAdd (leftRight-to-string lr) ≫str strAdd (maybeMinus-to-string m) ≫str to-stringh t
term-to-stringh (Hole pi) = strAdd "●"
term-to-stringh (IotaPair pi t t' og pi') = strAdd "[ " ≫str to-stringh t ≫str strAdd " , " ≫str to-stringh t' ≫str optGuide-to-string og ≫str strAdd " ]"
term-to-stringh (IotaProj t n pi) = to-stringh t ≫str strAdd ("." ^ n)
term-to-stringh (Lam pi l pi' x oc t) = strAdd (lam-to-string l) ≫str strAdd " " ≫str strBvar x (optClass-to-string oc) (strAdd " . " ≫str to-stringr t)
term-to-stringh (Let pi dtT t) with dtT
...| DefTerm pi' x m t' = strAdd "[ " ≫str strBvar x (maybeCheckType-to-string m ≫str strAdd " = " ≫str to-stringh t' ≫str strAdd " ] - ") (to-stringh t)
...| DefType pi' x k t' = strAdd "[ " ≫str strBvar x (strAdd " ◂ " ≫str to-stringh k ≫str strAdd " = " ≫str to-stringh t' ≫str strAdd " ] - ") (to-stringh t)
term-to-stringh (Open pi x t) = strAdd "open " ≫str strVar x ≫str strAdd " - " ≫str to-stringh t
term-to-stringh (Parens pi t pi') = to-stringh t
term-to-stringh (Phi pi eq t t' pi') = strAdd "φ " ≫str to-stringl eq ≫str strAdd " - " ≫str to-stringh t ≫str strAdd " {" ≫str to-stringr t' ≫str strAdd "}"
term-to-stringh (Rho pi op on eq og t) = strAdd "ρ" ≫str strAdd (optPlus-to-string op) ≫str optNums-to-string on ≫str strAdd " " ≫str to-stringl eq ≫str optGuide-to-string og ≫str strAdd " - " ≫str to-stringr t
term-to-stringh (Sigma pi t) = strAdd "ς " ≫str to-stringh t
term-to-stringh (Theta pi theta t lts) = theta-to-string theta ≫str to-stringh t ≫str lterms-to-string lts
term-to-stringh (Var pi x) = strVar x
term-to-stringh (Mu pi x t ot pi' cs pi'') = strAdd "μ " ≫str strBvar x (strAdd " . " ≫str to-stringh t) strEmpty ≫str optType-to-string ot ≫str strAdd "TODO"
term-to-stringh (Mu' pi t ot pi' cs pi'')  = strAdd "μ' " ≫str to-stringh t ≫str strAdd " . " ≫str optType-to-string ot ≫str strAdd "TODO"

type-to-stringh (Abs pi b pi' x Tk T) = strAdd (binder-to-string b ^ " ") ≫str strBvar x (strAdd " : " ≫str tk-to-stringh Tk ≫str strAdd " . ") (to-stringh T)
type-to-stringh (Iota pi pi' x T T') = strAdd "ι " ≫str strBvar x (strAdd " : " ≫str to-stringh T ≫str strAdd " . ") (to-stringh T')
type-to-stringh (Lft pi pi' x t lT) = strAdd "↑ " ≫str strBvar x (strAdd " . ") (to-stringh t) ≫str strAdd " : " ≫str to-stringh lT
type-to-stringh (NoSpans T pi) = to-string-ed T
type-to-stringh (TpApp T T') = to-stringl T ≫str strAdd " · " ≫str to-stringr T'
type-to-stringh (TpAppt T t) = to-stringl T ≫str strAdd " " ≫str to-stringr t
type-to-stringh (TpArrow T a T') = to-stringl T ≫str strAdd (arrowtype-to-string a) ≫str to-stringr T'
type-to-stringh (TpEq _ t t' _) = strAdd "{ " ≫str to-stringh (erase-term t) ≫str strAdd " ≃ " ≫str to-stringh (erase-term t') ≫str strAdd " }"
type-to-stringh (TpHole pi) = strAdd "●"
type-to-stringh (TpLambda pi pi' x Tk T) = strAdd "λ " ≫str strBvar x (strAdd " : " ≫str tk-to-stringh Tk ≫str strAdd " . ") (to-stringr T)
type-to-stringh (TpParens pi T pi') = to-stringh T
type-to-stringh (TpVar pi x) = strVar x
type-to-stringh (TpLet pi dtT t) with dtT
...| DefTerm pi' x m t' = strAdd "[ " ≫str strBvar x (maybeCheckType-to-string m ≫str strAdd " = " ≫str to-stringh t' ≫str strAdd " ] - ") (to-stringh t)
...| DefType pi' x k t' = strAdd "[ " ≫str strBvar x (strAdd " ◂ " ≫str to-stringh k ≫str strAdd " = " ≫str to-stringh t' ≫str strAdd " ] - ") (to-stringh t)

kind-to-stringh (KndArrow k k') = to-stringl k ≫str strAdd " ➔ " ≫str to-stringr k'
kind-to-stringh (KndParens pi k pi') = to-stringh k
kind-to-stringh (KndPi pi pi' x Tk k) = strAdd "Π " ≫str strBvar x (strAdd " : " ≫str tk-to-stringh Tk ≫str strAdd " . ") (to-stringh k)
kind-to-stringh (KndTpArrow T k) = to-stringl T ≫str strAdd " ➔ " ≫str to-stringr k
kind-to-stringh (KndVar pi x as) = strVar x ≫str args-to-string as
kind-to-stringh (Star pi) = strAdd "★"

liftingType-to-stringh (LiftArrow lT lT') = to-stringl lT ≫str strAdd " ➔↑ " ≫str to-stringr lT'
liftingType-to-stringh (LiftParens pi lT pi') = strAdd "(" ≫str to-string-ed lT ≫str strAdd ")"
liftingType-to-stringh (LiftPi pi x T lT) = strAdd "Π↑ " ≫str strBvar x (strAdd " : " ≫str to-stringh T ≫str strAdd " . ") (to-stringh lT)
liftingType-to-stringh (LiftStar pi) = strAdd "☆"
liftingType-to-stringh (LiftTpArrow T lT) = to-stringl T ≫str strAdd " ➔↑ " ≫str to-stringr lT
optTerm-to-string NoTerm c1 c2 = strEmpty
optTerm-to-string (SomeTerm t _) c1 c2 = strAdd c1 ≫str to-stringh (erase-term t) ≫str strAdd c2
optClass-to-string NoClass = strEmpty
optClass-to-string (SomeClass Tk) = strAdd " : " ≫str tk-to-stringh Tk
optGuide-to-string NoGuide = strEmpty
optGuide-to-string (Guide pi v T) = strAdd " @ " ≫str strBvar v (strAdd " . ") (to-stringh T)
optType-to-string NoType = strEmpty
optType-to-string (SomeType T) = strAdd " " ≫str to-stringh T
maybeCheckType-to-string NoType = strEmpty
maybeCheckType-to-string (SomeType T) = strAdd " ◂ " ≫str to-stringh T
lterms-to-string (LtermsCons m t ts) = strAdd (" " ^ maybeErased-to-string m) ≫str to-stringh t ≫str lterms-to-string ts
lterms-to-string (LtermsNil _) = strEmpty
arg-to-string (TermArg me t) = strAdd (maybeErased-to-string me) ≫str to-stringh t
arg-to-string (TypeArg T) = strAdd "· " ≫str to-stringh T
args-to-string (ArgsCons t ts) = strAdd " " ≫str arg-to-string t ≫str args-to-string ts
args-to-string ArgsNil = strEmpty
binder-to-string All = "∀"
binder-to-string Pi = "Π"
opacity-to-string OpacOpaque = "opaque "
opacity-to-string OpacTrans = ""
maybeErased-to-string Erased = "-"
maybeErased-to-string NotErased = ""
lam-to-string Erased = "Λ"
lam-to-string NotErased = "λ"
leftRight-to-string Left = "l"
leftRight-to-string Right = "r"
leftRight-to-string Both = ""
vars-to-string (VarsStart v) = strVar v
vars-to-string (VarsNext v vs) = strVar v ≫str strAdd " " ≫str vars-to-string vs
theta-to-string Abstract = strAdd "θ "
theta-to-string AbstractEq = strAdd "θ+ "
theta-to-string (AbstractVars vs) = strAdd "θ<" ≫str vars-to-string vs ≫str strAdd "> "
nums-to-string (NumsStart n) = strAdd n
nums-to-string (NumsNext n ns) = strAdd n ≫str strAdd " " ≫str nums-to-string ns
optNums-to-string NoNums = strEmpty
optNums-to-string (SomeNums ns) = strAdd "<" ≫str nums-to-string ns ≫str strAdd ">"
arrowtype-to-string NotErased = " ➔ "
arrowtype-to-string Erased = " ➾ "
maybeMinus-to-string EpsHnf = ""
maybeMinus-to-string EpsHanf = "-"
optPlus-to-string RhoPlain = ""
optPlus-to-string RhoPlus = "+"
optPublic-to-string NotPublic = ""
optPublic-to-string IsPublic = "public "
optAs-to-string NoOptAs = strEmpty
optAs-to-string (SomeOptAs _ x) = strAdd " as " ≫str strAdd x

braceL : maybeErased → string
braceL Erased = "{"
braceL NotErased = "("

braceR : maybeErased → string
braceR Erased = "}"
braceR NotErased = ")"

param-to-string : decl → strM → strM
param-to-string (Decl _ pi me v atk _) f =
  strAdd (braceL me) ≫str
  strAdd (unqual-local v) ≫str
  strAdd " : " ≫str
  tk-to-stringh atk ≫str
  strAdd (braceR me) ≫str
  strΓ' localScope v f
params-to-string' f ParamsNil = f
params-to-string' f (ParamsCons p ParamsNil) = param-to-string p f
params-to-string' f (ParamsCons p ps) = param-to-string p (strAdd " " ≫str params-to-string' f ps)

params-to-string = params-to-string' strEmpty

file-to-string (File _ is _ _ mn ps cs _) =
   cmds-to-string (imps-to-cmds is)
  (strAdd "module " ≫str
   strAdd mn ≫str
   strAdd " " ≫str
   params-to-string'
  (strAdd "." ≫str strAdd "\n" ≫str
   cmds-to-string cs strEmpty) ps)

cmds-to-string CmdsStart f = f
cmds-to-string (CmdsNext c cs) f =
   strAdd "\n" ≫str
   cmd-to-string c
  (strAdd "\n" ≫str
   cmds-to-string cs f)

cmd-to-string (DefTermOrType op (DefTerm pi x mcT t) _) f =
  strM-Γ λ Γ →
  let ps = ctxt-get-current-params Γ in
  strAdd (opacity-to-string op) ≫str
  strAdd x ≫str
  maybeCheckType-to-string (case mcT of λ where
     NoType → NoType
     (SomeType T) → SomeType (abs-expand-type ps T)) ≫str
  strAdd " = " ≫str
  to-stringh (lam-expand-term ps t) ≫str
  strAdd " ." ≫str
  strΓ' globalScope x f
cmd-to-string (DefTermOrType op (DefType pi x k T) _) f =
  strM-Γ λ Γ →
  let ps = ctxt-get-current-params Γ in
  strAdd (opacity-to-string op) ≫str
  strAdd x ≫str
  strAdd " ◂ " ≫str
  to-stringh (abs-expand-kind ps k) ≫str
  strAdd " = " ≫str
  to-stringh (lam-expand-type ps T) ≫str
  strAdd " ." ≫str
  strΓ' globalScope x f
cmd-to-string (DefKind pi x ps k _) f =
  strM-Γ λ Γ →
  let ps' = ctxt-get-current-params Γ in
  strAdd x ≫str
  params-to-string (append-params ps' ps) ≫str
  strAdd " = " ≫str
  to-stringh k ≫str
  strAdd " ." ≫str
  strΓ' globalScope x f
cmd-to-string (ImportCmd (Import _ op _ fn oa as _)) f =
  strAdd "import " ≫str
  strAdd (optPublic-to-string op) ≫str
  strAdd fn ≫str
  optAs-to-string oa ≫str
  args-to-string as ≫str
  strAdd " ." ≫str
  f
cmd-to-string (DefDatatype (Datatype pi pix x ps k cs pi') pi'') f =
  strAdd "data " ≫str
  strAdd x ≫str
  strAdd " " ≫str
  params-to-string ps ≫str
  strAdd " : " ≫str
  kind-to-stringh k ≫str
  strAdd " = " ≫str
  constructors-to-string cs ≫str
  strΓ' globalScope x f

strRun : ctxt → strM → rope
strRun Γ m = fst (m {TERM} [[]] 0 [] Γ nothing neither)

strRunTag : (name : string) → ctxt → strM → tagged-val
strRunTag name Γ m with m {TERM} [[]] 0 [] Γ nothing neither
...| s , n , ts = name , s , ts

to-string-tag : {ed : exprd} → string → ctxt → ⟦ ed ⟧ → tagged-val
to-string-tag name Γ t = strRunTag name Γ
  (to-stringh
    (if cedille-options.options.erase-types options
       then erase t
       else t))

to-string : {ed : exprd} → ctxt → ⟦ ed ⟧ → rope
to-string Γ t = strRun Γ (to-stringh t)

tk-to-string : ctxt → tk → rope
tk-to-string Γ atk = strRun Γ (tk-to-stringh atk)

params-to-string-tag : string → ctxt → params → tagged-val
params-to-string-tag name Γ ps = strRunTag name Γ (params-to-string ps)

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


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

open import Polynomial.Parameters

module Polynomial.Homomorphism.Semantics
  {c r₁ r₂ r₃}
  (homo : Homomorphism c r₁ r₂ r₃)
  where

open import Data.Product    using (_,_)
open import Data.List       using ([])
open import Data.Vec as Vec using (Vec)
open import Data.Fin        using (Fin)

open import Function

open import Polynomial.Homomorphism.Lemmas homo
open import Polynomial.NormalForm homo
open Homomorphism homo
open import Polynomial.Reasoning ring

open import Polynomial.Exponentiation rawRing

κ-hom : ∀ {n}
      → (x : Raw.Carrier)
      → (Ρ : Vec Carrier n)
      → ⟦ κ x ⟧ Ρ ≈ ⟦ x ⟧ᵣ
κ-hom x _ = refl

ι-hom : ∀ {n} → (i : Fin n) → (Ρ : Vec Carrier n) → ⟦ ι i ⟧ Ρ ≈ Vec.lookup Ρ i
ι-hom i Ρ′ =
  let (ρ , Ρ) = drop-1 (Fin⇒≤ i) Ρ′
  in
  begin
    ⟦ (κ Raw.1# Δ 1 ∷↓ []) Π↓ Fin⇒≤ i ⟧ Ρ′
  ≈⟨ Π↓-hom (κ Raw.1# Δ 1 ∷↓ []) (Fin⇒≤ i) Ρ′ ⟩
    Σ?⟦ κ Raw.1# Δ 1 ∷↓ [] ⟧ (ρ , Ρ)
  ≈⟨ ∷↓-hom-s (κ Raw.1#) 0 [] ρ Ρ  ⟩
    ρ * ⟦ κ Raw.1# ⟧ Ρ
  ≈⟨ *≫ 1-homo ⟩
    ρ * 1#
  ≈⟨ *-identityʳ ρ ⟩
    ρ
  ≡⟨ drop-1⇒lookup i Ρ′ ⟩
    Vec.lookup Ρ′ i
  ∎

max_stars_repo_name: mckeankylej/agda-ring-solver

max_issues_repo_name: mckeankylej/agda-ring-solver

max_forks_repo_name: mckeankylej/agda-ring-solver