text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of n-ary products
------------------------------------------------------------------------

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

module Data.Product.N-ary.Properties where

open import Data.Nat.Base hiding (_^_)
open import Data.Product
open import Data.Product.N-ary
open import Data.Vec using (Vec; _∷_)
open import Function.Inverse using (_↔_; inverse)
open import Relation.Binary.PropositionalEquality as P
open ≡-Reasoning

------------------------------------------------------------------------
-- Basic proofs

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

  cons-head-tail-identity : ∀ n (as : A ^ suc n) → cons n (head n as) (tail n as) ≡ as
  cons-head-tail-identity 0       as = P.refl
  cons-head-tail-identity (suc n) as = P.refl

  head-cons-identity : ∀ n a (as : A ^ n) → head n (cons n a as) ≡ a
  head-cons-identity 0       a as = P.refl
  head-cons-identity (suc n) a as = P.refl

  tail-cons-identity : ∀ n a (as : A ^ n) → tail n (cons n a as) ≡ as
  tail-cons-identity 0       a as = P.refl
  tail-cons-identity (suc n) a as = P.refl

  append-cons-commute : ∀ m n a (xs : A ^ m) ys →
    append (suc m) n (cons m a xs) ys ≡ cons (m + n) a (append m n xs ys)
  append-cons-commute 0       n a xs ys = P.refl
  append-cons-commute (suc m) n a xs ys = P.refl

  append-splitAt-identity : ∀ m n (as : A ^ (m + n)) → uncurry (append m n) (splitAt m n as) ≡ as
  append-splitAt-identity 0       n as = P.refl
  append-splitAt-identity (suc m) n as = begin
    let x         = head (m + n) as in
    let (xs , ys) = splitAt m n (tail (m + n) as) in
    append (suc m) n (cons m (head (m + n) as) xs) ys
      ≡⟨ append-cons-commute m n x xs ys ⟩
    cons (m + n) x (append m n xs ys)
      ≡⟨ P.cong (cons (m + n) x) (append-splitAt-identity m n (tail (m + n) as)) ⟩
    cons (m + n) x (tail (m + n) as)
      ≡⟨ cons-head-tail-identity (m + n) as ⟩
    as
      ∎

------------------------------------------------------------------------
-- Conversion to and from Vec

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

  toVec : ∀ n → A ^ n → Vec A n
  toVec 0       _  = Vec.[]
  toVec (suc n) xs = head n xs Vec.∷ toVec n (tail n xs)

  fromVec : ∀ {n} → Vec A n → A ^ n
  fromVec         Vec.[]       = []
  fromVec {suc n} (x Vec.∷ xs) = cons n x (fromVec xs)

  fromVec∘toVec : ∀ n (xs : A ^ n) → fromVec (toVec n xs) ≡ xs
  fromVec∘toVec 0       _  = P.refl
  fromVec∘toVec (suc n) xs = begin
    cons n (head n xs) (fromVec (toVec n (tail n xs)))
      ≡⟨ P.cong (cons n (head n xs)) (fromVec∘toVec n (tail n xs)) ⟩
    cons n (head n xs) (tail n xs)
      ≡⟨ cons-head-tail-identity n xs ⟩
    xs ∎

  toVec∘fromVec : ∀ {n} (xs : Vec A n) → toVec n (fromVec xs) ≡ xs
  toVec∘fromVec         Vec.[]       = P.refl
  toVec∘fromVec {suc n} (x Vec.∷ xs) = begin
    head n (cons n x (fromVec xs)) Vec.∷ toVec n (tail n (cons n x (fromVec xs)))
      ≡⟨ P.cong₂ (λ x xs → x Vec.∷ toVec n xs) hd-prf tl-prf ⟩
    x Vec.∷ toVec n (fromVec xs)
      ≡⟨ P.cong (x Vec.∷_) (toVec∘fromVec xs) ⟩
    x Vec.∷ xs
      ∎ where

      hd-prf = head-cons-identity n x (fromVec xs)
      tl-prf = tail-cons-identity n x (fromVec xs)

  ↔Vec : ∀ n → A ^ n ↔ Vec A n
  ↔Vec n = inverse (toVec n) fromVec (fromVec∘toVec n) toVec∘fromVec


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

module Cubical.Data.Fin where

open import Cubical.Data.Fin.Base       public
open import Cubical.Data.Fin.Properties public
open import Cubical.Data.Fin.Literals   public

ext: agda

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

open import lib.Basics
open import lib.types.FunctionSeq
open import lib.types.TLevel
open import lib.types.Pi
open import lib.types.Pointed
open import lib.types.Sigma
open import lib.NType2

module lib.types.Truncation where

module _ {i} where

  postulate  -- HIT
    Trunc : (n : ℕ₋₂) (A : Type i) → Type i
    [_] : {n : ℕ₋₂} {A : Type i} → A → Trunc n A
    instance Trunc-level : {n : ℕ₋₂} {A : Type i} → has-level n (Trunc n A)

  module TruncElim {n : ℕ₋₂} {A : Type i} {j} {P : Trunc n A → Type j}
    {{p : (x : Trunc n A) → has-level n (P x)}} (d : (a : A) → P [ a ]) where

    postulate  -- HIT
      f : Π (Trunc n A) P
      [_]-β : ∀ a → f [ a ] ↦ d a
    {-# REWRITE [_]-β #-}

open TruncElim public renaming (f to Trunc-elim)

module TruncRec {i j} {n : ℕ₋₂} {A : Type i} {B : Type j} {{p : has-level n B}}
  (d : A → B) where

  private
    module M = TruncElim {{λ x → p}} d

  f : Trunc n A → B
  f = M.f

open TruncRec public renaming (f to Trunc-rec)

module TruncRecType {i j} {n : ℕ₋₂} {A : Type i} (d : A → n -Type j) where

  open TruncRec {{n -Type-level j}} d public

  flattening-Trunc : Σ (Trunc (S n) A) (fst ∘ f) ≃ Trunc (S n) (Σ A (fst ∘ d))
  flattening-Trunc = equiv to from to-from from-to where

    to-aux : (x : Trunc (S n) A) → (fst (f x) → Trunc (S n) (Σ A (fst ∘ d)))
    to-aux = Trunc-elim (λ a b → [ (a , b) ])

    to : Σ (Trunc (S n) A) (fst ∘ f) → Trunc (S n) (Σ A (fst ∘ d))
    to (x , y) = to-aux x y

    from-aux : Σ A (fst ∘ d) → Σ (Trunc (S n) A) (fst ∘ f)
    from-aux (a , b) = ([ a ] , b)

    from : Trunc (S n) (Σ A (fst ∘ d)) → Σ (Trunc (S n) A) (fst ∘ f)
    from = Trunc-rec {{Σ-level ⟨⟩ (λ x → raise-level _ (snd (f x)))}}
                     from-aux  where

    to-from : (x : Trunc (S n) (Σ A (fst ∘ d))) → to (from x) == x
    to-from = Trunc-elim (λ _ → idp)

    from-to-aux : (a : Trunc (S n) A) (b : fst (f a)) → from (to-aux a b) == (a , b)
    from-to-aux = Trunc-elim {{λ _ → Π-level (λ _ → =-preserves-level (Σ-level ⟨⟩ (λ x → raise-level _ (snd (f x)))))}}
                             (λ a b → idp)

    from-to : (x : Σ (Trunc (S n) A) (fst ∘ f)) → from (to x) == x
    from-to (a , b) = from-to-aux a b

⊙Trunc : ∀ {i} → ℕ₋₂ → Ptd i → Ptd i
⊙Trunc n ⊙[ A , a ] = ⊙[ Trunc n A , [ a ] ]

⊙Trunc-rec : ∀ {i j} {n : ℕ₋₂} {X : Ptd i} {Y : Ptd j} {{Y-level : has-level n (de⊙ Y)}}
  → X ⊙→ Y
  → ⊙Trunc n X ⊙→ Y
⊙Trunc-rec {{Y-level}} f = Trunc-rec {{Y-level}} (fst f) , snd f

⊙Trunc-rec-post-⊙∘ : ∀ {i j k} {n : ℕ₋₂} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  {{Y-level : has-level n (de⊙ Y)}} {{Z-level : has-level n (de⊙ Z)}}
  (g : Y ⊙→ Z) (f : X ⊙→ Y)
  → ⊙Trunc-rec {n = n} {{Z-level}} (g ⊙∘ f) == g ⊙∘ ⊙Trunc-rec {{Y-level}} f
⊙Trunc-rec-post-⊙∘ {{Y-level}} {{Z-level}} g f =
  ⊙λ=' (Trunc-elim {{λ x → =-preserves-level Z-level}} (λ x → idp)) idp

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

  [_]₀ : A → Trunc 0 A
  [_]₀ = [_] {n = 0}

  [_]₁ : A → Trunc 1 A
  [_]₁ = [_] {n = 1}

  [_]₂ : A → Trunc 2 A
  [_]₂ = [_] {n = 2}

module _ {i} {n : ℕ₋₂} {A : Type i} where

  private
    Trunc= : (a b : Trunc (S n) A) → n -Type i
    Trunc= = Trunc-elim (λ a → Trunc-elim ((λ b → (Trunc n (a == b) , Trunc-level))))

  {- t is for truncated -}
  _=ₜ_ : (a b : Trunc (S n) A) → Type i
  _=ₜ_ a b = fst (Trunc= a b)

  =ₜ-level : (a b : Trunc (S n) A) → has-level n (a =ₜ b)
  =ₜ-level a b = snd (Trunc= a b)

  =ₜ-refl : (a : Trunc (S n) A) → a =ₜ a
  =ₜ-refl = Trunc-elim {{λ x → raise-level _ (=ₜ-level x x)}}
                       (λ a → [ idp ])

  =ₜ-equiv : (a b : Trunc (S n) A) → (a == b) ≃ (a =ₜ b)
  =ₜ-equiv a b = to a b , to-is-equiv a b where

    to : (a b : Trunc (S n) A) → (a == b → a =ₜ b)
    to a b p = transport (λ c → a =ₜ c) p (=ₜ-refl a)

    from-aux : (a b : A) → a == b → [ a ] == [ b ] :> Trunc (S n) A
    from-aux _ _ = ap [_]

    from : (a b : Trunc (S n) A) → a =ₜ b → a == b
    from = Trunc-elim (λ a → Trunc-elim (λ b → Trunc-rec (from-aux a b)))

    to-from-aux : (a b : A) → (p : a == b) → to _ _ (from-aux a b p) == [ p ]
    to-from-aux a .a idp = idp

    to-from : (a b : Trunc (S n) A) (x : a =ₜ b) → to a b (from a b x) == x
    to-from = Trunc-elim {{λ x → Π-level (λ y → Π-level (λ _ → =-preserves-level (raise-level _ (=ₜ-level x y))))}}
              (λ a → Trunc-elim {{λ x → Π-level (λ _ → =-preserves-level (raise-level _ (=ₜ-level [ a ] x)))}}
              (λ b → Trunc-elim
              (to-from-aux a b)))

    from-to-aux : (a : Trunc (S n) A) → from a a (=ₜ-refl a) == idp
    from-to-aux = Trunc-elim (λ _ → idp)

    from-to : (a b : Trunc (S n) A) (p : a == b) → from a b (to a b p) == p
    from-to a .a idp = from-to-aux a

    adj : (ta tb : Trunc (S n) A) (p : ta == tb)
      → ap (to ta tb) (from-to ta tb p) == to-from ta tb (to ta tb p)
    adj ta .ta idp =
      Trunc-elim {P = λ ta → ap (to ta ta) (from-to ta ta idp) == to-from ta ta (to ta ta idp)}
                 {{λ x → =-preserves-level $ =-preserves-level $ raise-level _ $ =ₜ-level x x}}
                 (λ _ → idp)
                 ta

    to-is-equiv : ∀ a b → is-equiv (to a b)
    to-is-equiv a b =
      record
      { g = from a b
      ; f-g = to-from a b
      ; g-f = from-to a b
      ; adj = adj a b
      }

  =ₜ-path : (a b : Trunc (S n) A) → (a == b) == (a =ₜ b)
  =ₜ-path a b = ua (=ₜ-equiv a b)

{- Universal property -}

abstract
  Trunc-rec-is-equiv : ∀ {i j} (n : ℕ₋₂) (A : Type i) (B : Type j)
    {{p : has-level n B}} → is-equiv (Trunc-rec {{p}} :> ((A → B) → (Trunc n A → B)))
  Trunc-rec-is-equiv n A B {{p}} = is-eq _ (λ f → f ∘ [_])
    (λ f → λ= (Trunc-elim (λ a → idp))) (λ f → idp)

Trunc-preserves-level : ∀ {i} {A : Type i} {n : ℕ₋₂} (m : ℕ₋₂)
 → has-level n A → has-level n (Trunc m A)
Trunc-preserves-level {n = ⟨-2⟩} _ p = has-level-in
  ([ contr-center p ] , Trunc-elim (λ a → ap [_] (contr-path p a)))
Trunc-preserves-level ⟨-2⟩ _ = contr-has-level Trunc-level
Trunc-preserves-level {n = (S n)} (S m) c = has-level-in (λ t₁ t₂ →
  Trunc-elim
    {{λ s₁ → prop-has-level-S {A = has-level n (s₁ == t₂)} has-level-is-prop}}
    (λ a₁ → Trunc-elim
      {{λ s₂ → prop-has-level-S {A = has-level n ([ a₁ ] == s₂)} has-level-is-prop}}
      (λ a₂ → equiv-preserves-level
      ((=ₜ-equiv [ a₁ ] [ a₂ ])⁻¹)
               {{Trunc-preserves-level {n = n} m (has-level-apply c a₁ a₂)}})
              t₂)
    t₁)

{- an n-type is equivalent to its n-truncation -}
unTrunc-equiv : ∀ {i} {n : ℕ₋₂} (A : Type i)
  {{_ : has-level n A}} → Trunc n A ≃ A
unTrunc-equiv A = equiv f [_] (λ _ → idp) g-f where
  f = Trunc-rec (idf _)
  g-f = Trunc-elim (λ _ → idp)

⊙unTrunc-equiv : ∀ {i} {n : ℕ₋₂} (X : Ptd i)
  {{_ : has-level n (de⊙ X)}} → ⊙Trunc n X ⊙≃ X
⊙unTrunc-equiv {n = n} X = ≃-to-⊙≃ (unTrunc-equiv (de⊙ X)) idp

-- Equivalence associated to the universal property
Trunc-extend-equiv : ∀ {i j} (n : ℕ₋₂) (A : Type i) (B : Type j)
  {{p : has-level n B}} → (A → B) ≃ (Trunc n A → B)
Trunc-extend-equiv n A B = (Trunc-rec , Trunc-rec-is-equiv n A B)

Trunc-fmap : ∀ {i j} {n : ℕ₋₂} {A : Type i} {B : Type j} → ((A → B) → (Trunc n A → Trunc n B))
Trunc-fmap f = Trunc-rec ([_] ∘ f)

⊙Trunc-fmap : ∀ {i j} {n : ℕ₋₂} {X : Ptd i} {Y : Ptd j} → ((X ⊙→ Y) → (⊙Trunc n X ⊙→ ⊙Trunc n Y))
⊙Trunc-fmap F = Trunc-fmap (fst F) , ap [_] (snd F)

–>-unTrunc-equiv-natural : ∀ {i} {j} {n : ℕ₋₂}
  {A : Type i} {B : Type j} (f : A → B)
  {{_ : has-level n A}} {{_ : has-level n B}}
  → –> (unTrunc-equiv {n = n} B) ∘ Trunc-fmap f ∼
    f ∘ –> (unTrunc-equiv {n = n} A)
–>-unTrunc-equiv-natural f = Trunc-elim (λ a → idp)

⊙–>-⊙unTrunc-equiv-natural : ∀ {i} {j} {n : ℕ₋₂}
  {X : Ptd i} {Y : Ptd j} (f : X ⊙→ Y)
  {{_ : has-level n (de⊙ X)}} {{_ : has-level n (de⊙ Y)}}
  → ⊙–> (⊙unTrunc-equiv {n = n} Y) ⊙∘ ⊙Trunc-fmap f ==
    f ⊙∘ ⊙–> (⊙unTrunc-equiv {n = n} X)
⊙–>-⊙unTrunc-equiv-natural (f' , idp) =
  ⊙λ=' (–>-unTrunc-equiv-natural f') idp

⊙–>-⊙unTrunc-equiv-natural-=⊙∘ : ∀ {i} {n : ℕ₋₂}
  {X Y : Ptd i} (f : X ⊙→ Y)
  {{_ : has-level n (de⊙ X)}} {{_ : has-level n (de⊙ Y)}}
  → ⊙–> (⊙unTrunc-equiv {n = n} Y) ◃⊙∘
    ⊙Trunc-fmap f ◃⊙idf
    =⊙∘
    f ◃⊙∘
    ⊙–> (⊙unTrunc-equiv {n = n} X) ◃⊙idf
⊙–>-⊙unTrunc-equiv-natural-=⊙∘ f =
  =⊙∘-in (⊙–>-⊙unTrunc-equiv-natural f)

Trunc-fmap2 : ∀ {i j k} {n : ℕ₋₂} {A : Type i} {B : Type j} {C : Type k}
  → ((A → B → C) → (Trunc n A → Trunc n B → Trunc n C))
Trunc-fmap2 f = Trunc-rec (λ a → Trunc-fmap (f a))

⊙Trunc-rec-⊙Trunc-fmap : ∀ {i j k} {n : ℕ₋₂} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  {{Z-level : has-level n (de⊙ Z)}}
  (g : Y ⊙→ Z) (f : X ⊙→ Y)
  → ⊙Trunc-rec {n = n} {{Z-level}} g ⊙∘ ⊙Trunc-fmap f ==
    ⊙Trunc-rec {n = n} {{Z-level}} (g ⊙∘ f)
⊙Trunc-rec-⊙Trunc-fmap {{Z-level}} g f =
  ⊙λ=' (Trunc-elim {{λ tx → =-preserves-level Z-level}} (λ x → idp)) $
  ap (_∙ snd g) (∘-ap (Trunc-elim (fst g)) [_] (snd f))

-- XXX What is the naming convention?
Trunc-fpmap : ∀ {i j} {n : ℕ₋₂} {A : Type i} {B : Type j} {f g : A → B}
  → f ∼ g → Trunc-fmap {n = n} f ∼ Trunc-fmap g
Trunc-fpmap h = Trunc-elim (ap [_] ∘ h)

Trunc-fmap-idf : ∀ {i} {n : ℕ₋₂} {A : Type i}
  → ∀ x → Trunc-fmap {n = n} (idf A) x == x
Trunc-fmap-idf = Trunc-elim (λ _ → idp)

⊙Trunc-fmap-⊙idf : ∀ {i} {n : ℕ₋₂} {X : Ptd i}
  → ⊙Trunc-fmap (⊙idf X) ⊙∼ ⊙idf (⊙Trunc n X)
⊙Trunc-fmap-⊙idf = Trunc-fmap-idf , idp

transport-Trunc : ∀ {i} {n : ℕ₋₂} {A B : Type i}
  (p : A == B)
  → transport (Trunc n) p == Trunc-fmap (coe p)
transport-Trunc p@idp = ! (λ= Trunc-fmap-idf)

⊙transport-⊙Trunc : ∀ {i} {n : ℕ₋₂} {X Y : Ptd i}
  (p : X == Y)
  → ⊙transport (⊙Trunc n) p == ⊙Trunc-fmap (⊙coe p)
⊙transport-⊙Trunc p@idp = ! (⊙λ= ⊙Trunc-fmap-⊙idf)

Trunc-fmap-cst : ∀ {i} {j} {n : ℕ₋₂} {A : Type i} {B : Type j}
  → ∀ (b : B) → Trunc-fmap {n = n} {A = A} (cst b) ∼ cst [ b ]
Trunc-fmap-cst b = Trunc-elim (λ a → idp)

⊙Trunc-fmap-cst : ∀ {i} {j} {n : ℕ₋₂} {X : Ptd i} {Y : Ptd j}
  → ⊙Trunc-fmap {n = n} (⊙cst {X = X} {Y = Y}) ⊙∼ ⊙cst
⊙Trunc-fmap-cst {Y = Y} = Trunc-fmap-cst (pt Y) , idp

Trunc-fmap-∘ : ∀ {i j k} {n : ℕ₋₂} {A : Type i} {B : Type j} {C : Type k}
  (g : B → C) (f : A → B)
  → ∀ x → Trunc-fmap {n = n} g (Trunc-fmap f x) == Trunc-fmap (g ∘ f) x
Trunc-fmap-∘ g f = Trunc-elim (λ _ → idp)

⊙Trunc-fmap-⊙∘ : ∀ {i j k} {n : ℕ₋₂} {A : Ptd i} {B : Ptd j} {C : Ptd k}
  (g : B ⊙→ C) (f : A ⊙→ B)
  → ⊙Trunc-fmap {n = n} g ⊙∘ ⊙Trunc-fmap f ⊙∼ ⊙Trunc-fmap (g ⊙∘ f)
⊙Trunc-fmap-⊙∘ {n = n} g f =
  Trunc-fmap-∘ (fst g) (fst f) , pres-pt-path
  where
  pres-pt-path : snd (⊙Trunc-fmap {n = n} g ⊙∘ ⊙Trunc-fmap f) == snd (⊙Trunc-fmap (g ⊙∘ f))
  pres-pt-path =
    ap (Trunc-fmap (fst g)) (ap [_] (snd f)) ∙ ap [_] (snd g)
      =⟨ ap (_∙ ap [_] (snd g))
            (∘-ap (Trunc-fmap (fst g)) [_] (snd f) ∙
             ap-∘ [_] (fst g) (snd f)) ⟩
    ap [_] (ap (fst g) (snd f)) ∙ ap [_] (snd g)
      =⟨ ∙-ap [_] (ap (fst g) (snd f)) (snd g) ⟩
    ap [_] (ap (fst g) (snd f) ∙ snd g) =∎

⊙Trunc-fmap-seq : ∀ {i} {n : ℕ₋₂} {X Y : Ptd i}
  → X ⊙–→ Y
  → ⊙Trunc n X ⊙–→ ⊙Trunc n Y
⊙Trunc-fmap-seq ⊙idf-seq = ⊙idf-seq
⊙Trunc-fmap-seq (f ◃⊙∘ fs) = ⊙Trunc-fmap f ◃⊙∘ ⊙Trunc-fmap-seq fs

⊙Trunc-fmap-seq-⊙∘ : ∀ {i} {n : ℕ₋₂} {X Y : Ptd i} (fs : X ⊙–→ Y)
  → ⊙Trunc-fmap {n = n} (⊙compose fs) ◃⊙idf =⊙∘ ⊙Trunc-fmap-seq fs
⊙Trunc-fmap-seq-⊙∘ ⊙idf-seq = =⊙∘-in (⊙λ= (⊙Trunc-fmap-⊙idf))
⊙Trunc-fmap-seq-⊙∘ (f ◃⊙∘ fs) = =⊙∘-in $
  ⊙Trunc-fmap (f ⊙∘ ⊙compose fs)
    =⟨ ! $ ⊙λ= $ ⊙Trunc-fmap-⊙∘ f (⊙compose fs) ⟩
  ⊙Trunc-fmap f ⊙∘ ⊙Trunc-fmap (⊙compose fs)
    =⟨ ap (⊙Trunc-fmap f ⊙∘_) (=⊙∘-out (⊙Trunc-fmap-seq-⊙∘ fs)) ⟩
  ⊙Trunc-fmap f ⊙∘ ⊙compose (⊙Trunc-fmap-seq fs) =∎

⊙Trunc-fmap-seq-=⊙∘ : ∀ {i} {n : ℕ₋₂} {X Y : Ptd i} {fs gs : X ⊙–→ Y}
  → fs =⊙∘ gs
  → ⊙Trunc-fmap-seq {n = n} fs =⊙∘ ⊙Trunc-fmap-seq {n = n} gs
⊙Trunc-fmap-seq-=⊙∘ {fs = fs} {gs = gs} p =
  ⊙Trunc-fmap-seq fs
    =⊙∘⟨ !⊙∘ (⊙Trunc-fmap-seq-⊙∘ fs) ⟩
  ⊙Trunc-fmap (⊙compose fs) ◃⊙idf
    =⊙∘₁⟨ ap ⊙Trunc-fmap (=⊙∘-out p) ⟩
  ⊙Trunc-fmap (⊙compose gs) ◃⊙idf
    =⊙∘⟨ ⊙Trunc-fmap-seq-⊙∘ gs ⟩
  ⊙Trunc-fmap-seq gs ∎⊙∘

Trunc-csmap : ∀ {i₀ i₁ j₀ j₁} {n : ℕ₋₂}
  {A₀ : Type i₀} {A₁ : Type i₁} {B₀ : Type j₀} {B₁ : Type j₁}
  {f : A₀ → B₀} {g : A₁ → B₁} {hA : A₀ → A₁} {hB : B₀ → B₁}
  → CommSquare f g hA hB
  → CommSquare (Trunc-fmap {n = n} f) (Trunc-fmap g) (Trunc-fmap hA) (Trunc-fmap hB)
Trunc-csmap (comm-sqr cs) = comm-sqr $ Trunc-elim (ap [_] ∘ cs)

{- Pushing concatenatation through _=ₜ_ -}
module _ {i} {n : ℕ₋₂} {A : Type i} where

  {- concatenation in _=ₜ_ -}
  _∙ₜ_ : {ta tb tc : Trunc (S n) A}
    → ta =ₜ tb → tb =ₜ tc → ta =ₜ tc
  _∙ₜ_ {ta = ta} {tb = tb} {tc = tc} =
    Trunc-elim {P = λ ta → C ta tb tc}
      {{λ ta → level ta tb tc}}
      (λ a → Trunc-elim {P = λ tb → C [ a ] tb tc}
         {{λ tb → level [ a ] tb tc}}
         (λ b → Trunc-elim {P = λ tc → C [ a ] [ b ] tc}
                  {{λ tc → level [ a ] [ b ] tc}}
                  (λ c → Trunc-fmap2 _∙_)
                  tc)
         tb)
      ta
    where
    C : (ta tb tc : Trunc (S n) A) → Type i
    C ta tb tc = ta =ₜ tb → tb =ₜ tc → ta =ₜ tc
    level : (ta tb tc : Trunc (S n) A) → has-level (S n) (C ta tb tc)
    level ta tb tc =
      raise-level _ $
      Π-level $ λ _ →
      Π-level $ λ _ →
      =ₜ-level ta tc

  {- inversion in _=ₜ_ -}
  !ₜ : {ta tb : Trunc (S n) A}
    → ta =ₜ tb
    → tb =ₜ ta
  !ₜ {ta = ta} {tb = tb} =
    Trunc-elim {P = λ ta → C ta tb}
      {{λ ta → level ta tb}}
      (λ a → Trunc-elim {P = λ tb → C [ a ] tb}
        {{λ tb → level [ a ] tb}}
        (λ b → Trunc-fmap !)
        tb)
      ta
    where
    C : (ta tb : Trunc (S n) A) → Type i
    C ta tb = ta =ₜ tb → tb =ₜ ta
    level : (ta tb : Trunc (S n) A) → has-level (S n) (C ta tb)
    level ta tb = raise-level _ $ Π-level $ λ _ → =ₜ-level tb ta

  ∙ₜ-assoc : {ta tb tc td : Trunc (S n) A}
    (tp : ta =ₜ tb) (tq : tb =ₜ tc) (tr : tc =ₜ td)
    → _∙ₜ_ {ta} (_∙ₜ_ {ta} tp tq) tr
      == _∙ₜ_ {ta} tp (_∙ₜ_ {tb} tq tr)
  ∙ₜ-assoc {ta = ta} {tb = tb} {tc = tc} {td = td} =
    Trunc-elim {P = λ ta → C ta tb tc td}
      {{λ ta → C-level ta tb tc td}}
      (λ a → Trunc-elim {P = λ tb → C [ a ] tb tc td}
        {{λ tb → C-level [ a ] tb tc td}}
        (λ b → Trunc-elim {P = λ tc → C [ a ] [ b ] tc td}
          {{λ tc → C-level [ a ] [ b ] tc td}}
          (λ c → Trunc-elim {P = λ td → C [ a ] [ b ] [ c ] td}
            {{λ td → C-level [ a ] [ b ] [ c ] td}}
            (λ d tp tq tr → Trunc-elim
              {P = λ tp → D [ a ] [ b ] [ c ] [ d ] tp tq tr}
              {{λ tp → D-level [ a ] [ b ] [ c ] [ d ] tp tq tr}}
              (λ p → Trunc-elim
                {P = λ tq → D [ a ] [ b ] [ c ] [ d ] [ p ] tq tr}
                {{λ tq → D-level [ a ] [ b ] [ c ] [ d ] [ p ] tq tr}}
                (λ q → Trunc-elim
                  {P = λ tr → D [ a ] [ b ] [ c ] [ d ] [ p ] [ q ] tr}
                  {{λ tr → D-level [ a ] [ b ] [ c ] [ d ] [ p ] [ q ] tr}}
                  (λ r → ap [_] (∙-assoc p q r))
                  tr)
                tq)
              tp)
            td)
          tc)
        tb)
      ta
    where
    D : (ta tb tc td : Trunc (S n) A)
      → ta =ₜ tb → tb =ₜ tc → tc =ₜ td
      → Type i
    D ta tb tc td tp tq tr =
         _∙ₜ_ {ta} (_∙ₜ_ {ta} tp tq) tr
      == _∙ₜ_ {ta} tp (_∙ₜ_ {tb} tq tr)
    C : (ta tb tc td : Trunc (S n) A) → Type i
    C ta tb tc td = ∀ tp tq tr → D ta tb tc td tp tq tr
    D-level : (ta tb tc td : Trunc (S n) A)
      (tp : ta =ₜ tb) (tq : tb =ₜ tc) (tr : tc =ₜ td)
      → has-level n (D ta tb tc td tp tq tr)
    D-level ta tb tc td tp tq tr = =-preserves-level (=ₜ-level ta td)
    C-level : (ta tb tc td : Trunc (S n) A) → has-level (S n) (C ta tb tc td)
    C-level ta tb tc td =
      raise-level _ $
      Π-level $ λ tp →
      Π-level $ λ tq →
      Π-level $ λ tr →
      D-level ta tb tc td tp tq tr

  abstract
    ∙ₜ-assoc-pentagon : {ta tb tc td te : Trunc (S n) A}
      (tp : ta =ₜ tb) (tq : tb =ₜ tc) (tr : tc =ₜ td) (ts : td =ₜ te)
      → ∙ₜ-assoc {ta} (_∙ₜ_ {ta} tp tq) tr ts ◃∙
        ∙ₜ-assoc {ta} tp tq (_∙ₜ_ {tc} tr ts) ◃∎
        =ₛ
        ap (λ u → _∙ₜ_ {ta} u ts) (∙ₜ-assoc {ta} tp tq tr) ◃∙
        ∙ₜ-assoc {ta} tp (_∙ₜ_ {tb} tq tr) ts ◃∙
        ap (_∙ₜ_ {ta} tp) (∙ₜ-assoc {tb} tq tr ts) ◃∎
    ∙ₜ-assoc-pentagon {ta} {tb} {tc} {td} {te} = core ta tb tc td te
      where
      P : (ta tb tc td te : Trunc (S n) A)
        (tp : ta =ₜ tb) (tq : tb =ₜ tc) (tr : tc =ₜ td) (ts : td =ₜ te)
        → Type i
      P ta tb tc td te tp tq tr ts =
        ∙ₜ-assoc {ta} (_∙ₜ_ {ta} tp tq) tr ts ◃∙
        ∙ₜ-assoc {ta} tp tq (_∙ₜ_ {tc} tr ts) ◃∎
        =ₛ
        ap (λ u → _∙ₜ_ {ta} u ts) (∙ₜ-assoc {ta} tp tq tr) ◃∙
        ∙ₜ-assoc {ta} tp (_∙ₜ_ {tb} tq tr) ts ◃∙
        ap (_∙ₜ_ {ta} tp) (∙ₜ-assoc {tb} tq tr ts) ◃∎
      P-level : ∀ ta tb tc td te →
        (tp : ta =ₜ tb) (tq : tb =ₜ tc) (tr : tc =ₜ td) (ts : td =ₜ te)
        → has-level n (P ta tb tc td te tp tq tr ts)
      P-level ta tb tc td te tp tq tr ts =
        =ₛ-level $ raise-level _ $ raise-level _ $ =ₜ-level ta te
      Q : (ta tb tc td te : Trunc (S n) A) → Type i
      Q ta tb tc td te = ∀ tp tq tr ts → P ta tb tc td te tp tq tr ts
      Q-level : ∀ ta tb tc td te → has-level (S n) (Q ta tb tc td te)
      Q-level ta tb tc td te =
        raise-level n $
        Π-level $ λ tp →
        Π-level $ λ tq →
        Π-level $ λ tr →
        Π-level $ λ ts →
        P-level ta tb tc td te tp tq tr ts
      core' : ∀ {a} {b} {c} {d} {e} p q r s → P [ a ] [ b ] [ c ] [ d ] [ e ] [ p ] [ q ] [ r ] [ s ]
      core' idp idp r s = =ₛ-in idp
      core : ∀ ta tb tc td te → Q ta tb tc td te
      core ta tb tc td te =
        Trunc-elim {P = λ ta → Q ta tb tc td te} {{λ ta → Q-level ta tb tc td te}} (λ a →
          Trunc-elim {P = λ tb → Q [ a ] tb tc td te} {{λ tb → Q-level [ a ] tb tc td te}} (λ b →
            Trunc-elim {P = λ tc → Q [ a ] [ b ] tc td te} {{λ tc → Q-level [ a ] [ b ] tc td te}} (λ c →
              Trunc-elim {P = λ td → Q [ a ] [ b ] [ c ] td te} {{λ td → Q-level [ a ] [ b ] [ c ] td te}} (λ d →
                Trunc-elim {P = λ te → Q [ a ] [ b ] [ c ] [ d ] te} {{λ te → Q-level [ a ] [ b ] [ c ] [ d ] te}} (λ e →
                  let R = P [ a ] [ b ] [ c ] [ d ] [ e ]
                      R-level = P-level [ a ] [ b ] [ c ] [ d ] [ e ]
                  in λ tp tq tr ts →
                  Trunc-elim {P = λ tp → R tp tq tr ts} {{λ tp → R-level tp tq tr ts }} (λ p →
                    Trunc-elim {P = λ tq → R [ p ] tq tr ts} {{λ tq → R-level [ p ] tq tr ts}} (λ q →
                      Trunc-elim {P = λ tr → R [ p ] [ q ] tr ts} {{λ tr → R-level [ p ] [ q ] tr ts}} (λ r →
                        Trunc-elim {P = λ ts → R [ p ] [ q ] [ r ] ts} {{λ ts → R-level [ p ] [ q ] [ r ] ts}} (λ s →
                          core' p q r s
                        ) ts
                      ) tr
                    ) tq
                  ) tp
                ) te
              ) td
            ) tc
          ) tb
        ) ta

  –>-=ₜ-equiv-pres-∙ : {ta tb tc : Trunc (S n) A}
    (p : ta == tb) (q : tb == tc)
    →  –> (=ₜ-equiv ta tc) (p ∙ q)
       ==
       _∙ₜ_ {ta = ta} (–> (=ₜ-equiv ta tb) p) (–> (=ₜ-equiv tb tc) q)
  –>-=ₜ-equiv-pres-∙ {ta = ta} idp idp =
    Trunc-elim
      {P = λ ta → –> (=ₜ-equiv ta ta) idp
              == _∙ₜ_ {ta = ta} (–> (=ₜ-equiv ta ta) idp)
                                (–> (=ₜ-equiv ta ta) idp)}
      {{λ ta → raise-level _ $ =-preserves-level $ =ₜ-level ta ta}}
      (λ a → idp)
      ta

  !ₜ-=ₜ-refl : ∀ (ta : Trunc (S n) A)
    → !ₜ {ta = ta} (=ₜ-refl ta) == =ₜ-refl ta
  !ₜ-=ₜ-refl =
    Trunc-elim
      {P = λ ta → !ₜ {ta = ta} (=ₜ-refl ta) == =ₜ-refl ta}
      {{λ ta → raise-level _ $ =-preserves-level $ =ₜ-level ta ta}}
      (λ a → idp)

  –>-=ₜ-equiv-pres-! : {ta tb : Trunc (S n) A}
    (p : ta == tb)
    → –> (=ₜ-equiv tb ta) (! p) == !ₜ {ta = ta} (–> (=ₜ-equiv ta tb) p)
  –>-=ₜ-equiv-pres-! {ta = ta} p@idp = ! (!ₜ-=ₜ-refl ta)

  abstract
    –>-=ₜ-equiv-pres-∙-coh : {ta tb tc td : Trunc (S n) A}
      (p : ta == tb) (q : tb == tc) (r : tc == td)
      → –>-=ₜ-equiv-pres-∙ (p ∙ q) r ◃∙
        ap (λ u → _∙ₜ_ {ta = ta} u (–> (=ₜ-equiv tc td) r)) (–>-=ₜ-equiv-pres-∙ p q) ◃∙
        ∙ₜ-assoc {ta = ta} (–> (=ₜ-equiv ta tb) p) (–> (=ₜ-equiv tb tc) q) (–> (=ₜ-equiv tc td) r) ◃∎
        =ₛ
        ap (–> (=ₜ-equiv ta td)) (∙-assoc p q r) ◃∙
        –>-=ₜ-equiv-pres-∙ p (q ∙ r) ◃∙
        ap (_∙ₜ_ {ta = ta} (–> (=ₜ-equiv ta tb) p)) (–>-=ₜ-equiv-pres-∙ q r) ◃∎
    –>-=ₜ-equiv-pres-∙-coh {ta = ta} idp idp idp =
      Trunc-elim
        {P = λ ta → P ta ta ta ta idp idp idp}
        {{λ ta → =ₛ-level $ raise-level (S (S n)) $ raise-level (S n) $ raise-level n $ =ₜ-level ta ta}}
        (λ a → =ₛ-in idp)
        ta
      where
      P : (ta tb tc td : Trunc (S n) A) (p : ta == tb) (q : tb == tc) (r : tc == td) → Type i
      P ta tb tc td p q r =
        –>-=ₜ-equiv-pres-∙ (p ∙ q) r ◃∙
        ap (λ u → _∙ₜ_ {ta = ta} u (–> (=ₜ-equiv tc td) r)) (–>-=ₜ-equiv-pres-∙ p q) ◃∙
        ∙ₜ-assoc {ta = ta} (–> (=ₜ-equiv ta tb) p) (–> (=ₜ-equiv tb tc) q) (–> (=ₜ-equiv tc td) r) ◃∎
        =ₛ
        ap (–> (=ₜ-equiv ta td)) (∙-assoc p q r) ◃∙
        –>-=ₜ-equiv-pres-∙ p (q ∙ r) ◃∙
        ap (_∙ₜ_ {ta = ta} (–> (=ₜ-equiv ta tb) p)) (–>-=ₜ-equiv-pres-∙ q r) ◃∎

{- naturality of =ₜ-equiv -}

module _ {i j} {n : ℕ₋₂} {A : Type i} {B : Type j} (f : A → B) where
  =ₜ-fmap : ∀ (a₀ a₁ : Trunc (S n) A)
    → a₀ =ₜ a₁ → Trunc-fmap f a₀ =ₜ Trunc-fmap f a₁
  =ₜ-fmap = Trunc-elim
    {P = λ a₀ → ∀ a₁ → a₀ =ₜ a₁ → Trunc-fmap f a₀ =ₜ Trunc-fmap f a₁}
    {{λ a₀ → Π-level λ a₁ → Π-level λ _ → raise-level _ $ =ₜ-level (Trunc-fmap f a₀) (Trunc-fmap f a₁)}}
    (λ a₀ → Trunc-elim
      {P = λ a₁ → [ a₀ ] =ₜ a₁ → [ f a₀ ] =ₜ Trunc-fmap f a₁}
      {{λ a₁ → Π-level λ _ → raise-level _ $ =ₜ-level [ f a₀ ] (Trunc-fmap f a₁)}}
      (λ a₁ → Trunc-fmap (ap f)))

module _ {i j} {n : ℕ₋₂} {A : Type i} {B : Type j} (f : A → B) where
  =ₜ-equiv-nat : ∀ (a₀ a₁ : Trunc (S n) A) (p : a₀ == a₁)
     →  –> (=ₜ-equiv (Trunc-fmap f a₀) (Trunc-fmap f a₁)) (ap (Trunc-fmap f) p)
     == =ₜ-fmap f a₀ a₁ (–> (=ₜ-equiv a₀ a₁) p)
  =ₜ-equiv-nat a₀ .a₀ idp =
    Trunc-elim
      {P = λ a
        →  –> (=ₜ-equiv (Trunc-fmap f a) (Trunc-fmap f a)) idp
        == =ₜ-fmap f a a (–> (=ₜ-equiv a a) idp)}
      {{λ a → raise-level _ $ =-preserves-level $ =ₜ-level (Trunc-fmap f a) (Trunc-fmap f a)}}
      (λ _ → idp)
      a₀

{- Truncation preserves equivalences - more convenient than univalence+ap
 - when we need to know the forward or backward function explicitly -}
module _ {i j} {n : ℕ₋₂} {A : Type i} {B : Type j} where

  Trunc-isemap : {f : A → B} → is-equiv f → is-equiv (Trunc-fmap {n = n} f)
  Trunc-isemap {f-orig} ie = is-eq f g f-g g-f where
    f = Trunc-fmap f-orig
    g = Trunc-fmap (is-equiv.g ie)

    f-g : ∀ tb → f (g tb) == tb
    f-g = Trunc-elim (ap [_] ∘ is-equiv.f-g ie)

    g-f : ∀ ta → g (f ta) == ta
    g-f = Trunc-elim (ap [_] ∘ is-equiv.g-f ie)

  Trunc-emap : A ≃ B → Trunc n A ≃ Trunc n B
  Trunc-emap (f , f-ie) = Trunc-fmap f , Trunc-isemap f-ie

Trunc-csemap : ∀ {i₀ i₁ j₀ j₁} {n : ℕ₋₂}
  {A₀ : Type i₀} {A₁ : Type i₁} {B₀ : Type j₀} {B₁ : Type j₁}
  {f : A₀ → B₀} {g : A₁ → B₁} {hA : A₀ → A₁} {hB : B₀ → B₁}
  → CommSquareEquiv f g hA hB
  → CommSquareEquiv (Trunc-fmap {n = n} f) (Trunc-fmap g) (Trunc-fmap hA) (Trunc-fmap hB)
Trunc-csemap (cs , hA-ise , hB-ise) = Trunc-csmap cs , Trunc-isemap hA-ise , Trunc-isemap hB-ise

transport-Trunc' : ∀ {i j} {A : Type i} {n : ℕ₋₂} (P : A → Type j)
  {x y : A} (p : x == y) (b : P x)
  → transport (Trunc n ∘ P) p [ b ] == [ transport P p b ]
transport-Trunc' _ idp _ = idp

Trunc-fuse : ∀ {i} (A : Type i) (m n : ℕ₋₂)
  → Trunc m (Trunc n A) ≃ Trunc (minT m n) A
Trunc-fuse A m n = equiv
  (Trunc-rec {{raise-level-≤T (minT≤l m n) Trunc-level}}
    (Trunc-rec {{raise-level-≤T (minT≤r m n) Trunc-level}}
      [_]))
  (Trunc-rec ([_] ∘ [_]))
  (Trunc-elim (λ _ → idp))
  (Trunc-elim (Trunc-elim
       {{λ _ → =-preserves-level (Trunc-preserves-level _ Trunc-level)}}
       (λ _ → idp)))
  where
      instance
        l : has-level (minT m n) (Trunc m (Trunc n A))
        l with (minT-out m n)
        l | inl p = transport (λ k → has-level k (Trunc m (Trunc n A)))
                              (! p) Trunc-level
        l | inr q = Trunc-preserves-level _
                      (transport (λ k → has-level k (Trunc n A))
                                 (! q) Trunc-level)

Trunc-fuse-≤ : ∀ {i} (A : Type i) {m n : ℕ₋₂} (m≤n : m ≤T n)
  → Trunc m (Trunc n A) ≃ Trunc m A
Trunc-fuse-≤ A m≤n = equiv
  (Trunc-rec (Trunc-rec {{raise-level-≤T m≤n Trunc-level}}
      [_]))
  (Trunc-rec ([_] ∘ [_]))
  (Trunc-elim (λ _ → idp))
  (Trunc-elim (Trunc-elim
       {{λ _ → =-preserves-level (Trunc-preserves-level _ Trunc-level)}}
       (λ _ → idp)))

{- Truncating a binary product is equivalent to truncating its components -}
Trunc-×-econv : ∀ {i} {j} (n : ℕ₋₂) (A : Type i) (B : Type j)
  → Trunc n (A × B) ≃ Trunc n A × Trunc n B
Trunc-×-econv n A B = equiv f g f-g g-f
  where
  f : Trunc n (A × B) → Trunc n A × Trunc n B
  f = Trunc-rec (λ {(a , b) → [ a ] , [ b ]})

  g : Trunc n A × Trunc n B → Trunc n (A × B)
  g (ta , tb) = Trunc-rec (λ a → Trunc-rec (λ b → [ a , b ]) tb) ta

  f-g : ∀ p → f (g p) == p
  f-g (ta , tb) = Trunc-elim
    {P = λ ta → f (g (ta , tb)) == (ta , tb)}
    (λ a → Trunc-elim
      {P = λ tb → f (g ([ a ] , tb)) == ([ a ] , tb)}
      (λ b → idp)
      tb)
    ta

  g-f : ∀ tab → g (f tab) == tab
  g-f = Trunc-elim
    {P = λ tab → g (f tab) == tab}
    (λ ab → idp)

Trunc-×-conv : ∀ {i} {j} (n : ℕ₋₂) (A : Type i) (B : Type j)
  → Trunc n (A × B) == Trunc n A × Trunc n B
Trunc-×-conv n A B = ua (Trunc-×-econv n A B)

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


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

module Definition.Typed.Consequences.Canonicity where

open import Definition.Untyped

open import Definition.Typed
open import Definition.Typed.Weakening
open import Definition.Typed.Properties
open import Definition.Typed.EqRelInstance
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Fundamental.Reducibility

open import Tools.Embedding
open import Tools.Empty
open import Tools.Nat
open import Tools.Product

-- Turns a natural number into its term representation
sucᵏ : Nat → Term
sucᵏ 0 = zero
sucᵏ (1+ n) = suc (sucᵏ n)

-- Helper function for canonicity for reducible natural properties
canonicity″ : ∀ {t}
              → Natural-prop ε t
              → ∃ λ k → ε ⊢ t ≡ sucᵏ k ∷ ℕ
canonicity″ (sucᵣ (ℕₜ n₁ d n≡n prop)) =
  let a , b = canonicity″ prop
  in  1+ a , suc-cong (trans (subset*Term (redₜ d)) b)
canonicity″ zeroᵣ = 0 , refl (zeroⱼ ε)
canonicity″ (ne (neNfₜ neK ⊢k k≡k)) = ⊥-elim (noNe ⊢k neK)

-- Helper function for canonicity for specific reducible natural numbers
canonicity′ : ∀ {t l}
             → ([ℕ] : ε ⊩⟨ l ⟩ℕ ℕ)
             → ε ⊩⟨ l ⟩ t ∷ ℕ / ℕ-intr [ℕ]
             → ∃ λ k → ε ⊢ t ≡ sucᵏ k ∷ ℕ
canonicity′ (noemb [ℕ]) (ιx (ℕₜ n d n≡n prop)) =
  let a , b = canonicity″ prop
  in  a , trans (subset*Term (redₜ d)) b
canonicity′ (emb 0<1 [ℕ]) (ιx [t]) = canonicity′ [ℕ] [t]

-- Canonicity of natural numbers
canonicity : ∀ {t} → ε ⊢ t ∷ ℕ → ∃ λ k → ε ⊢ t ≡ sucᵏ k ∷ ℕ
canonicity ⊢t with reducibleTerm ⊢t
canonicity ⊢t | [ℕ] , [t] =
  canonicity′ (ℕ-elim [ℕ]) (irrelevanceTerm [ℕ] (ℕ-intr (ℕ-elim [ℕ])) [t])

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
open import Level                      using (Level)
open import Function                   using (_∘_; id; flip)
open import Data.Fin     as Fin        using (fromℕ)
open import Data.Nat     as Nat        using (ℕ; suc; zero; pred; _+_; _⊔_)
open import Data.Nat.Properties using (≤-decTotalOrder)
open import Data.List    as List       using (List; []; _∷_; [_]; concatMap; _++_; length; map)
open import Data.Vec     as Vec        using (Vec; []; _∷_; _∷ʳ_; reverse; initLast; toList)
open import Data.Product as Prod       using (∃; _×_; _,_; proj₁; proj₂)
open import Data.Maybe   as Maybe      using (Maybe; just; nothing; maybe)
open import Data.Sum     as Sum        using (_⊎_; inj₁; inj₂)
open import Data.Integer as Int        using (ℤ; -[1+_]; +_) renaming (_≟_ to _≟-Int_)
open import Relation.Nullary           using (Dec; yes; no)
open import Relation.Nullary.Decidable using (map′)
open import Relation.Binary            using (module DecTotalOrder)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym)
open import Reflection renaming (Term to AgTerm; _≟_ to _≟-AgTerm_)

module Auto.Core where

  open DecTotalOrder ≤-decTotalOrder using (total)

  private
    ∃-syntax : ∀ {a b} {A : Set a} → (A → Set b) → Set (b Level.⊔ a)
    ∃-syntax = ∃
    syntax ∃-syntax (λ x → B) = ∃[ x ] B

  -- define error messages that may occur when the `auto` function is
  -- called.
  data Message : Set where
    searchSpaceExhausted : Message
    unsupportedSyntax    : Message

  -- define our own instance of the error functor based on the either
  -- monad, and use it to propagate one of several error messages
  private
    Error : ∀ {a} (A : Set a) → Set a
    Error A = Message ⊎ A

    _⟨$⟩_ : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) → Error A → Error B
    f ⟨$⟩ inj₁ x = inj₁ x
    f ⟨$⟩ inj₂ y = inj₂ (f y)

  -- define term names for the term language we'll be using for proof
  -- search; we use standard Agda names, together with term-variables
  -- and Agda implications/function types.
  data TermName : Set₀ where
    name   : (n : Name) → TermName
    var    : (i : ℤ)    → TermName
    impl   : TermName

  tname-injective : ∀ {x y} → TermName.name x ≡ TermName.name y → x ≡ y
  tname-injective refl = refl

  tvar-injective : ∀ {i j} → TermName.var i ≡ TermName.var j → i ≡ j
  tvar-injective refl = refl

  _≟-TermName_ : (x y : TermName) → Dec (x ≡ y)
  (name x) ≟-TermName (name  y) with x ≟-Name y
  (name x) ≟-TermName (name .x) | yes refl = yes refl
  (name x) ≟-TermName (name  y) | no  x≠y  = no (x≠y ∘ tname-injective)
  (name _) ≟-TermName (var   _) = no (λ ())
  (name _) ≟-TermName (impl   ) = no (λ ())
  (var  _) ≟-TermName (name  _) = no (λ ())
  (var  i) ≟-TermName (var   j) with i ≟-Int j
  (var  i) ≟-TermName (var  .i) | yes refl = yes refl
  (var  i) ≟-TermName (var   j) | no i≠j = no (i≠j ∘ tvar-injective)
  (var  _) ≟-TermName (impl   ) = no (λ ())
  (impl  ) ≟-TermName (name  _) = no (λ ())
  (impl  ) ≟-TermName (var   _) = no (λ ())
  (impl  ) ≟-TermName (impl   ) = yes refl

  -- define rule names for the proof terms/rules that our proof search will
  -- return/use; we'll use standard Agda names, together with rule-variables.
  data RuleName : Set where
    name  : Name → RuleName
    var   : ℕ    → RuleName

  name-injective : ∀ {x y} → RuleName.name x ≡ name y → x ≡ y
  name-injective refl = refl

  rvar-injective : ∀ {x y} → RuleName.var x ≡ var y → x ≡ y
  rvar-injective refl = refl

  _≟-RuleName_ : (x y : RuleName) → Dec (x ≡ y)
  name x ≟-RuleName name y = map′ (cong name) name-injective (x ≟-Name y)
  name x ≟-RuleName var  y = no (λ ())
  var  x ≟-RuleName name y = no (λ ())
  var  x ≟-RuleName var  y = map′ (cong var) rvar-injective (x Nat.≟ y)

  -- now we can load the definitions from proof search
  open import ProofSearch RuleName TermName _≟-TermName_ Literal _≟-Lit_
    as PS public renaming (Term to PsTerm; module Extensible to PsExtensible)

  -- next up, converting the terms returned by Agda's reflection
  -- mechanism to terms in our proof search's language!

  -- dictionary for the treatment of variables in conversion from Agda
  -- terms to terms to be used in proof search.
  ConvertVar  : Set
  ConvertVar  = (depth index : ℕ) → ∃ PsTerm

  -- conversion dictionary for rule-terms, which turns every variable
  -- that is within the scope of the term (i.e. is defined within the
  -- term by lambda abstraction) into a variable, and every variable
  -- which is defined out of scope into a Skolem constant (which
  -- blocks unification).
  convertVar4Term : ConvertVar
  convertVar4Term = fromVar
    where
      fromVar : (depth index : ℕ) → ∃ PsTerm
      fromVar d i with total i d
      fromVar d i | inj₁ i≤d = (suc (Δ i≤d) , var (fromℕ (Δ i≤d)))
      fromVar d i | inj₂ i>d = (0 , con (var (-[1+ Δ i>d ])) [])

  -- conversion dictionary for goal-terms, which turns all variables
  -- into Skolem constants which blocks all unification.
  convertVar4Goal : ConvertVar
  convertVar4Goal = fromVar
    where
      fromVar : (depth index : ℕ) → ∃ PsTerm
      fromVar d i with total i d
      fromVar d i | inj₁ i≤d = (0 , con (var (+ Δ i≤d)) [])
      fromVar d i | inj₂ i>d = (0 , con (var (-[1+ Δ i>d ])) [])

  -- helper function for converting definitions or constructors to
  -- proof terms.
  fromDefOrCon : (s : Name) → ∃[ n ] List (PsTerm n) → ∃ PsTerm
  fromDefOrCon f (n , ts) = n , con (name f) ts

  -- specialised function to convert literals of natural numbers
  -- (since they have a representation using Agda names)
  convertℕ : ∀ {k} → ℕ → PsTerm k
  convertℕ  zero   = con (name (quote zero)) []
  convertℕ (suc n) = con (name (quote suc)) (convertℕ n ∷ [])

  -- convert an Agda term to a term, abstracting over the treatment of
  -- variables with an explicit dictionary of the type `ConvertVar`---
  -- passing in `ConvertVar4Term` or `ConvertVar4Goal` will result in
  -- rule-terms or goal-terms, respectively.

  convert : ConvertVar → (depth : ℕ) → AgTerm → Error (∃ PsTerm)
  convertChildren :
    ConvertVar → ℕ → List (Arg AgTerm) → Error (∃[ n ] List (PsTerm n))

  convert cv d (lit (nat n)) = inj₂ (0 , convertℕ n)
  convert cv d (lit l)       = inj₂ (0 , lit l)
  convert cv d (var i [])    = inj₂ (cv d i)
  convert cv d (var i args)  = inj₁ unsupportedSyntax
  convert cv d (con c args)  = fromDefOrCon c ⟨$⟩ convertChildren cv d args
  convert cv d (def f args)  = fromDefOrCon f ⟨$⟩ convertChildren cv d args
  convert cv d (pi (arg (arg-info visible _) t₁) (abs _ t₂)) with convert cv d t₁ | convert cv (suc d) t₂
  ... | inj₁ msg | _        = inj₁ msg
  ... | _        | inj₁ msg = inj₁ msg
  ... | inj₂ (n₁ , p₁) | inj₂ (n₂ , p₂)
    with match p₁ p₂
  ... | (p₁′ , p₂′) = inj₂ (n₁ ⊔ n₂ , con impl (p₁′ ∷ p₂′ ∷ []))
  convert cv d (pi (arg _ _) (abs _ t₂)) = convert cv (suc d) t₂
  convert cv d (lam _ _)     = inj₁ unsupportedSyntax
  convert cv d (pat-lam _ _) = inj₁ unsupportedSyntax
  convert cv d (sort _)      = inj₁ unsupportedSyntax
  convert cv d unknown       = inj₁ unsupportedSyntax
  convert cv d (meta x args) = inj₁ unsupportedSyntax

  convertChildren cv d [] = inj₂ (0 , [])
  convertChildren cv d (arg (arg-info visible _) t ∷ ts)
    with convert cv d t | convertChildren cv d ts
  ... | inj₁ msg      | _              = inj₁ msg
  ... | _             | inj₁ msg       = inj₁ msg
  ... | inj₂ (m , p)  | inj₂ (n , ps) with match p ps
  ... | (p′ , ps′)                      = inj₂ (m ⊔ n , p′ ∷ ps′)
  convertChildren cv d (arg _ _ ∷ ts)   = convertChildren cv d ts

  -- convert an Agda term to a rule-term.
  agda2term : AgTerm → Error (∃ PsTerm)
  agda2term t = convert convertVar4Term 0 t

  -- split a term at every occurrence of the `impl` constructor---
  -- equivalent to splitting at every occurrence of the _→_ symbol in
  -- an Agda term.
  split : ∀ {n} → PsTerm n → ∃[ k ] Vec (PsTerm n) (suc k)
  split (con impl (t₁ ∷ t₂ ∷ [])) = Prod.map suc (λ ts → t₁ ∷ ts) (split t₂)
  split t = zero , t ∷ []

  -- convert an Agda term to a goal-term, together with a `HintDB`
  -- representing the premises of the rule---this means that for a
  -- term of the type `A → B` this function will generate a goal of
  -- type `B` and a premise of type `A`.
  agda2goal×premises : AgTerm → Error (∃ PsTerm × Rules)
  agda2goal×premises t with convert convertVar4Goal 0 t
  ... | inj₁ msg            = inj₁ msg
  ... | inj₂ (n , p)        with split p
  ... | (k , ts)            with initLast ts
  ... | (prems , goal , _)  = inj₂ ((n , goal) , toPremises (pred k) prems)
    where
      toPremises : ∀ {k} → ℕ → Vec (PsTerm n) k → Rules
      toPremises i [] = []
      toPremises i (t ∷ ts) = (n , rule (var i) t []) ∷ toPremises (pred i) ts

  -- convert an Agda name to an rule-term.
  name2term : Name → TC (Error (∃ PsTerm))
  name2term nm = bindTC (getType nm) (λ tp → returnTC (agda2term tp))

  -- convert an Agda name to a rule.
  name2ruleHelper : Name → (Error (∃ PsTerm)) → TC (Error (∃ Rule))
  name2ruleHelper nm name2term_nm with name2term_nm
  ... | inj₁ msg             = returnTC (inj₁ msg)
  ... | inj₂ (n , t)         with split t
  ... | (k , ts)             with initLast ts
  ... | (prems , concl , _)  =  returnTC (inj₂ (n , rule (name nm) concl (toList prems)))

  -- convert an Agda name to a rule.
  name2rule : Name → TC (Error (∃ Rule))
  name2rule nm = bindTC (name2term nm) (name2ruleHelper nm)

  -- function which reifies untyped proof terms (from the
  -- `ProofSearch` module) to untyped Agda terms.

  reify : Proof → TC AgTerm
  reifyChildren : List Proof → TC (List (Arg AgTerm))

  reify (con (var i) ps) = returnTC ((var i []))
  reify (con (name n) ps) =
    bindTC (getDefinition n) (λ
      { (function x) → bindTC (reifyChildren ps) (λ rc → returnTC (def n rc))
      ; (data-type pars cs) →  bindTC (reifyChildren ps) ((λ rc → returnTC (con n rc)))
      ; (record′ c _) → returnTC unknown
      ; (constructor′ d ) → returnTC unknown
      ; axiom → returnTC unknown
      ; primitive′ → returnTC unknown} )

  reifyChildren [] = returnTC []
  reifyChildren (p ∷ ps) =
    bindTC (reify p)
    (λ rp → bindTC (reifyChildren ps) (λ rcps → returnTC (toArg rp ∷ rcps)))
    where
      toArg : AgTerm → Arg AgTerm
      toArg = arg (arg-info visible relevant)

  -- data-type `Exception` which is used to unquote error messages to
  -- the type-level so that `auto` can generate descriptive type-errors.

  data Exception : Message → Set where
    throw : (msg : Message) → Exception msg

  quoteError : Message → AgTerm
  quoteError (searchSpaceExhausted) = quoteTerm (throw searchSpaceExhausted)
  quoteError (unsupportedSyntax)    = quoteTerm (throw unsupportedSyntax)

max_stars_repo_name: wenkokke/AutoInAgda

max_issues_repo_name: wenkokke/AutoInAgda

max_forks_repo_name: wenkokke/AutoInAgda


text:
open import Categories
open import Functors
open import RMonads

module RMonads.RKleisli.Adjunction {a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}
                                   {J : Fun C D}(M : RMonad J) where

open import Library
open import RMonads.RKleisli M
open import RAdjunctions
open import RMonads.RKleisli.Functors M
open Cat
open Fun
open RMonad M

KlAdj : RAdj J Kl
KlAdj = record{
  L = RKlL;
  R = RKlR;
  left     = id;
  right    = id;
  lawa     = λ _ → refl;
  lawb     = λ _ → refl;
  natleft  = lem;
  natright = lem}
  where
   lem = λ {X}{X'}{Y}{Y'} (f : Hom C X' X) (g : Hom D (OMap J Y) (T Y')) h →
    proof
    comp D (bind g) (comp D h (HMap J f))
    ≅⟨ cong (λ h₁ → comp D (bind g) (comp D h₁ (HMap J f))) (sym law2) ⟩
    comp D (bind g) (comp D (comp D (bind h) η) (HMap J f))
    ≅⟨ cong (comp D (bind g)) (ass D) ⟩
    comp D (bind g) (comp D (bind h) (comp D η (HMap J f)))
    ∎

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
open import Data.ByteString using ( ByteString ; Style ; strict ; lazy )
open import Data.ByteString.Primitive using ( strict₁ ; strict₂ ; lazy₁ ; lazy₂ )
open import Data.Bool using ( Bool )
open import Data.Char using ( Char )
open import Data.Nat using ( ℕ )
open import Data.Natural using ( Natural ; % )
open import Data.Product using ( _×_ ; _,_ )
open import Data.String using ( String )

open import Data.ByteString.UTF8.Primitive

module Data.ByteString.UTF8 where

toString : {s : Style} → (ByteString s) → String
toString {lazy}   = toStringLazy
toString {strict} = toStringStrict

fromString : {s : Style} → String → (ByteString s)
fromString {lazy}   = fromStringLazy
fromString {strict} = fromStringStrict

length : {s : Style} → (ByteString s) → Natural
length {lazy}   = lengthLazy
length {strict} = lengthStrict

size : {s : Style} → (ByteString s) → ℕ
size bs = % (length bs)

span : {s : Style} → (Char → Bool) → (ByteString s) → (ByteString s × ByteString s)
span {lazy}   φ bs with spanLazy φ bs
span {lazy}   φ bs | bs² = (lazy₁ bs² , lazy₂ bs²)
span {strict} φ bs with spanStrict φ bs
span {strict} φ bs | bs² = (strict₁ bs² , strict₂ bs²)

break : {s : Style} → (Char → Bool) → (ByteString s) → (ByteString s × ByteString s)
break {lazy}   φ bs with breakLazy φ bs
break {lazy}   φ bs | bs² = (lazy₁ bs² , lazy₂ bs²)
break {strict} φ bs with breakStrict φ bs
break {strict} φ bs | bs² = (strict₁ bs² , strict₂ bs²)

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io


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

module hott.types.nat where

open import hott.core.universe
open import hott.core.equality
open import hott.functions

data ℕ : Type₀ where
  zero : ℕ
  succ : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

-- Addition.
_+_   : ℕ → ℕ → ℕ
0       + y = y
succ x  + y = succ (x + y)

-- Multiplication
_*_   : ℕ → ℕ → ℕ
zero   * y = zero
succ x * y = y + (x * y)

-- The interated fucntion
iterate : ∀{ℓ} {A : Type ℓ} → (A → A) → ℕ → A → A
iterate _ zero     = id
iterate f (succ n) = f ∘ iterate f n

max_stars_repo_name: piyush-kurur/hott

max_issues_repo_name: piyush-kurur/hott

max_forks_repo_name: piyush-kurur/hott


text:
-- The "intro" command manages to refine goals of type ∞ A with the
-- term ♯ ?.

{-# OPTIONS --universe-polymorphism #-}

module IntroSharp where

postulate
  Level : Set
  zero : Level
  suc  : (i : Level) → Level
  _⊔_ : Level -> Level -> Level

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO zero  #-}
{-# BUILTIN LEVELSUC  suc   #-}
{-# BUILTIN LEVELMAX  _⊔_   #-}

postulate
  ∞  : ∀ {a} (A : Set a) → Set a
  ♯_ : ∀ {a} {A : Set a} → A → ∞ A
  ♭  : ∀ {a} {A : Set a} → ∞ A → A

{-# BUILTIN INFINITY ∞  #-}
{-# BUILTIN SHARP    ♯_ #-}
{-# BUILTIN FLAT     ♭  #-}

Foo : ∞ Set
Foo = ?

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
data _≡_ {A : Set}(x : A) : A → Set where
  refl : x ≡ x

data * : Set where ! : *

postulate
  prop : ∀ x → x ≡ !

record StrictTotalOrder : Set where
  field compare : *

open StrictTotalOrder

module M (Key : StrictTotalOrder) where

    postulate
      intersection′-₁ : ∀ x → x ≡ compare Key

    -- Doesn't termination check, but shouldn't get __IMPOSSIBLE__
    -- when termination checking!
    to-∈-intersection′  : * → * → Set
    to-∈-intersection′ x h with intersection′-₁ x
    to-∈-intersection′ ._ h   | refl with prop h
    to-∈-intersection′ ._ ._  | refl    | refl = to-∈-intersection′ ! !

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module 04-inductive-types where

import 03-natural-numbers
open 03-natural-numbers public

-- Section 4.2 The unit type

-- Definition 4.2.1

data unit : UU lzero where
  star : unit

𝟙 = unit

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

-- Section 4.3 The empty type

-- Definition 4.3.1

data empty : UU lzero where

𝟘 = empty

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

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

ex-falso' : {i : Level} {A : UU i} → empty → A
ex-falso' = ex-falso

-- Definition 4.3.2

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

-- Section 4.4 The booleans

-- Definition 4.4.1

data bool : UU lzero where
  true false : bool

-- Example 4.4.2

neg-𝟚 : bool → bool
neg-𝟚 true = false
neg-𝟚 false = true

conjunction-𝟚 : bool → (bool → bool)
conjunction-𝟚 true true = true
conjunction-𝟚 true false = false
conjunction-𝟚 false true = false
conjunction-𝟚 false false = false

disjunction-𝟚 : bool → (bool → bool)
disjunction-𝟚 true true = true
disjunction-𝟚 true false = true
disjunction-𝟚 false true = true
disjunction-𝟚 false false = false

-- Section 4.5 Coproducts and the type of integers

-- Definition 4.5.1

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

ind-coprod : {i j k : Level} {A : UU i} {B : UU j} (C : coprod A B → UU k) →
  ((x : A) → C (inl x)) → ((y : B) → C (inr y)) →
  (t : coprod A B) → C t
ind-coprod C f g (inl x) = f x
ind-coprod C f g (inr x) = g x

-- Definition 4.5.2

-- The type of integers

ℤ : UU lzero
ℤ = coprod ℕ (coprod unit ℕ)

-- Inclusion of the negative integers

in-neg : ℕ → ℤ
in-neg n = inl n

-- Negative one

neg-one-ℤ : ℤ
neg-one-ℤ = in-neg zero-ℕ

-- Zero

zero-ℤ : ℤ
zero-ℤ = inr (inl star)

-- One

one-ℤ : ℤ
one-ℤ = inr (inr zero-ℕ)

-- Inclusion of the positive integers

in-pos : ℕ → ℤ
in-pos n = inr (inr n)

-- Lemma 4.5.3

{- We prove an induction principle for the integers. -}

ind-ℤ : {i : Level} (P : ℤ → UU i) → P neg-one-ℤ → ((n : ℕ) → P (inl n) → P (inl (succ-ℕ n))) → P zero-ℤ → P one-ℤ → ((n : ℕ) → P (inr (inr (n))) → P (inr (inr (succ-ℕ n)))) → (k : ℤ) → P k
ind-ℤ P p-1 p-S p0 p1 pS (inl zero-ℕ) = p-1
ind-ℤ P p-1 p-S p0 p1 pS (inl (succ-ℕ x)) = p-S x (ind-ℤ P p-1 p-S p0 p1 pS (inl x))
ind-ℤ P p-1 p-S p0 p1 pS (inr (inl star)) = p0
ind-ℤ P p-1 p-S p0 p1 pS (inr (inr zero-ℕ)) = p1
ind-ℤ P p-1 p-S p0 p1 pS (inr (inr (succ-ℕ x))) = pS x (ind-ℤ P p-1 p-S p0 p1 pS (inr (inr (x))))

-- Definition 4.5.4

succ-ℤ : ℤ → ℤ
succ-ℤ (inl zero-ℕ) = zero-ℤ
succ-ℤ (inl (succ-ℕ x)) = inl x
succ-ℤ (inr (inl star)) = one-ℤ
succ-ℤ (inr (inr x)) = inr (inr (succ-ℕ x))

-- Section 4.6 Dependent pair types

-- Definition 4.6.1

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

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

-- Definition 4.6.2

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

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

-- Section 4.7 Cartesian products

-- Definition 4.7.1

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

pair' :
  {i j : Level} {A : UU i} {B : UU j} → A → B → prod A B
pair' = pair

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

-- Exercises

-- Exercise 4.2

{- In this exercise we were asked to show that (A + ¬A) implies (¬¬A → A). In
   other words, we get double negation elimination for the types that are
   decidable. -}

is-decidable : {l : Level} (A : UU l) → UU l
is-decidable A = coprod A (¬ A)

double-negation-elim-is-decidable :
  {i : Level} (A : UU i) → is-decidable A → (¬ (¬ A) → A)
double-negation-elim-is-decidable A (inl x) p = x
double-negation-elim-is-decidable A (inr x) p = ind-empty (p x)

neg-triple-neg : {l : Level} (A : UU l) → (¬ (¬ (¬ A))) → (¬ A)
neg-triple-neg A f a = f (λ g → g a)

-- Exercise 4.3

exclusive-disjunction-𝟚 : bool → (bool → bool)
exclusive-disjunction-𝟚 true true = false
exclusive-disjunction-𝟚 true false = true
exclusive-disjunction-𝟚 false true = true
exclusive-disjunction-𝟚 false false = false

implication-𝟚 : bool → (bool → bool)
implication-𝟚 true true = true
implication-𝟚 true false = false
implication-𝟚 false true = true
implication-𝟚 false false = true

bi-implication-𝟚 : bool → (bool → bool)
bi-implication-𝟚 true true = true
bi-implication-𝟚 true false = false
bi-implication-𝟚 false true = false
bi-implication-𝟚 false false = true

peirce-arrow-𝟚 : bool → (bool → bool)
peirce-arrow-𝟚 true true = false
peirce-arrow-𝟚 true false = false
peirce-arrow-𝟚 false true = false
peirce-arrow-𝟚 false false = true

sheffer-stroke-𝟚 : bool → (bool → bool)
sheffer-stroke-𝟚 true true = false
sheffer-stroke-𝟚 true false = true
sheffer-stroke-𝟚 false true = true
sheffer-stroke-𝟚 false false = true

-- Exercise 4.4

pred-ℤ : ℤ → ℤ
pred-ℤ (inl x) = inl (succ-ℕ x)
pred-ℤ (inr (inl star)) = inl zero-ℕ
pred-ℤ (inr (inr zero-ℕ)) = inr (inl star)
pred-ℤ (inr (inr (succ-ℕ x))) = inr (inr x)

-- Exercise 4.5

-- Addition on ℤ

add-ℤ : ℤ → ℤ → ℤ
add-ℤ (inl zero-ℕ) l = pred-ℤ l
add-ℤ (inl (succ-ℕ x)) l = pred-ℤ (add-ℤ (inl x) l)
add-ℤ (inr (inl star)) l = l
add-ℤ (inr (inr zero-ℕ)) l = succ-ℤ l
add-ℤ (inr (inr (succ-ℕ x))) l = succ-ℤ (add-ℤ (inr (inr x)) l)

-- The negative of an integer

neg-ℤ : ℤ → ℤ
neg-ℤ (inl x) = inr (inr x)
neg-ℤ (inr (inl star)) = inr (inl star)
neg-ℤ (inr (inr x)) = inl x

-- Multiplication on ℤ

mul-ℤ : ℤ → ℤ → ℤ
mul-ℤ (inl zero-ℕ) l = neg-ℤ l
mul-ℤ (inl (succ-ℕ x)) l = add-ℤ (neg-ℤ l) (mul-ℤ (inl x) l)
mul-ℤ (inr (inl star)) l = zero-ℤ
mul-ℤ (inr (inr zero-ℕ)) l = l
mul-ℤ (inr (inr (succ-ℕ x))) l = add-ℤ l (mul-ℤ (inr (inr x)) l)

-- Exercise 4.6

Fibonacci-ℤ : ℤ → ℤ
Fibonacci-ℤ (inl zero-ℕ) = one-ℤ
Fibonacci-ℤ (inl (succ-ℕ zero-ℕ)) = neg-one-ℤ
Fibonacci-ℤ (inl (succ-ℕ (succ-ℕ x))) =
  add-ℤ (Fibonacci-ℤ (inl x)) (neg-ℤ (Fibonacci-ℤ (inl (succ-ℕ x))))
Fibonacci-ℤ (inr (inl star)) = zero-ℤ
Fibonacci-ℤ (inr (inr zero-ℕ)) = one-ℤ
Fibonacci-ℤ (inr (inr (succ-ℕ zero-ℕ))) = one-ℤ
Fibonacci-ℤ (inr (inr (succ-ℕ (succ-ℕ x)))) =
  add-ℤ (Fibonacci-ℤ (inr (inr x))) (Fibonacci-ℤ (inr (inr (succ-ℕ x))))

-- Exercise 4.7

{- In this exercise we were asked to show that 1 + 1 satisfies the induction
   principle of the booleans. In other words, type theory cannot distinguish
   the booleans from the type 1 + 1. We will see later that they are indeed
   equivalent types. -}

t0 : coprod unit unit
t0 = inl star

t1 : coprod unit unit
t1 = inr star

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

-- Exercise 4.8

-- Exercise 4.8(a)

data list {l : Level} (A : UU l) : UU l where
  nil : list A
  cons : A → list A → list A

in-list : {l : Level} {A : UU l} → A → list A
in-list a = cons a nil

-- Exercise 4.8(b)

fold-list :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (b : B) (μ : A → (B → B)) →
  list A → B
fold-list b μ nil = b
fold-list b μ (cons a l) = μ a (fold-list b μ l)

-- Exercise 4.8(c)

length-list :
  {l : Level} {A : UU l} → list A → ℕ
length-list = fold-list zero-ℕ (λ a → succ-ℕ)

-- Exercise 4.8(d)

sum-list-ℕ :
  list ℕ → ℕ
sum-list-ℕ = fold-list zero-ℕ add-ℕ

-- Exercise 4.8(e)

concat-list :
  {l : Level} {A : UU l} → list A → (list A → list A)
concat-list {l} {A} = fold-list id (λ a f → (cons a) ∘ f)

-- Exercise 4.8(f)

flatten-list :
  {l : Level} {A : UU l} → list (list A) → list A
flatten-list = fold-list nil concat-list

-- Exercise 4.8 (g)

reverse-list :
  {l : Level} {A : UU l} → list A → list A
reverse-list nil = nil
reverse-list (cons a l) = concat-list (reverse-list l) (in-list a)

max_stars_repo_name: hemangandhi/HoTT-Intro

max_issues_repo_name: hemangandhi/HoTT-Intro

max_forks_repo_name: hemangandhi/HoTT-Intro


text:
module Category where

open import Logic.Equivalence
open import Logic.Relations

open Equivalence using () renaming (_==_ to eq)

record Cat : Set2 where
  field
    Obj     : Set1
    _─→_    : Obj -> Obj -> Set
    id      : {A : Obj} -> A ─→ A
    _∘_     : {A B C : Obj} -> B ─→ C -> A ─→ B -> A ─→ C
    Eq      : {A B : Obj} -> Equivalence (A ─→ B)
    cong    : {A B C : Obj}{f₁ f₂ : B ─→ C}{g₁ g₂ : A ─→ B} ->
              eq Eq f₁ f₂ -> eq Eq g₁ g₂ -> eq Eq (f₁ ∘ g₁) (f₂ ∘ g₂)
    idLeft  : {A B : Obj}{f : A ─→ B} -> eq Eq (id ∘ f) f
    idRight : {A B : Obj}{f : A ─→ B} -> eq Eq (f ∘ id) f
    assoc   : {A B C D : Obj}{f : C ─→ D}{g : B ─→ C}{h : A ─→ B} ->
              eq Eq ((f ∘ g) ∘ h) (f ∘ (g ∘ h))

module Category (ℂ : Cat) where

  private module CC = Cat ℂ
  open CC public hiding (_─→_; _∘_)

  private module Eq {A B : Obj} = Equivalence (Eq {A}{B})
  open Eq public hiding (_==_)

  infix	 20 _==_
  infixr 30 _─→_
  infixr 90 _∘_

  _─→_ = CC._─→_

  _==_ : {A B : Obj} -> Rel (A ─→ B)
  _==_ = Eq._==_

  _∘_ : {A B C : Obj} -> B ─→ C -> A ─→ B -> A ─→ C
  _∘_ = CC._∘_

  congL : {A B C : Obj}{f₁ f₂ : B ─→ C}{g : A ─→ B} ->
	  f₁ == f₂ -> f₁ ∘ g == f₂ ∘ g
  congL p = cong p refl

  congR : {A B C : Obj}{f : B ─→ C}{g₁ g₂ : A ─→ B} ->
	  g₁ == g₂ -> f ∘ g₁ == f ∘ g₂
  congR p = cong refl p

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

module Magma.Bundles where

open import Algebra.Bundles
open import Algebra.Core
open import Magma.Structures
open import Relation.Binary
open import Level

record IdempotentMagma c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _∙_     : Op₂ Carrier
    isIdempotentMagma  : IsIdempotentMagma _≈_ _∙_

  open IsIdempotentMagma isIdempotentMagma public

  magma : Magma c ℓ
  magma = record { isMagma = isMagma }

  open Magma magma public
    using (rawMagma)

record AlternateMagma c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _∙_     : Op₂ Carrier
    isAlternateMagma  : IsAlternateMagma _≈_ _∙_

  open IsAlternateMagma isAlternateMagma public

  magma : Magma c ℓ
  magma = record { isMagma = isMagma }

  open Magma magma public
    using (rawMagma)

record FlexibleMagma c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _∙_     : Op₂ Carrier
    isFlexibleMagma  : IsFlexibleMagma _≈_ _∙_

  open IsFlexibleMagma isFlexibleMagma public

  magma : Magma c ℓ
  magma = record { isMagma = isMagma }

  open Magma magma public
    using (rawMagma)

record MedialMagma c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _∙_     : Op₂ Carrier
    isMedialMagma  : IsMedialMagma _≈_ _∙_

  open IsMedialMagma isMedialMagma public

  magma : Magma c ℓ
  magma = record { isMagma = isMagma }

  open Magma magma public
    using (rawMagma)

record SemimedialMagma c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _∙_     : Op₂ Carrier
    isSemimedialMagma  : IsSemimedialMagma _≈_ _∙_

  open IsSemimedialMagma isSemimedialMagma public

  magma : Magma c ℓ
  magma = record { isMagma = isMagma }

  open Magma magma public
    using (rawMagma)

record LeftUnitalMagma c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier  : Set c
    _≈_      : Rel Carrier ℓ
    _∙_      : Op₂ Carrier
    ε        : Carrier
    isLeftUnitalMagma  : IsLeftUnitalMagma _≈_ _∙_ ε

  open IsLeftUnitalMagma isLeftUnitalMagma public

  magma : Magma c ℓ
  magma = record { isMagma = isMagma }

  open Magma magma public
    using (rawMagma)

record RightUnitalMagma c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier  : Set c
    _≈_      : Rel Carrier ℓ
    _∙_      : Op₂ Carrier
    ε        : Carrier
    isRightUnitalMagma  : IsRightUnitalMagma _≈_ _∙_ ε

  open IsRightUnitalMagma isRightUnitalMagma public

  magma : Magma c ℓ
  magma = record { isMagma = isMagma }

  open Magma magma public
    using (rawMagma)


text:
------------------------------------------------------------------------------
-- Exercises for Type Theory CM0859 (Prof. Andreas Abel).
-- http://www1.eafit.edu.co/asr/courses/type-theory-CM0859/exercises.pdf
------------------------------------------------------------------------------

open import Data.PropFormula 2 public

ex1 : ∀ {φ}
    → ∅ ⊢ φ ⊃ φ

ex1 {φ} = ⊃-intro (assume {Γ = ∅} φ)

ex2 : ∀ {φ ψ}
    → ∅ ⊢ (φ ∧ (φ ⊃ ψ)) ⊃ ψ

ex2 {φ}{ψ} =
  ⊃-intro $
    ⊃-elim
      (∧-proj₂ $ assume {Γ = ∅} (φ ∧ (φ ⊃ ψ)))
      (∧-proj₁ $ assume {Γ = ∅} (φ ∧ (φ ⊃ ψ)))

ex3 : ∀ {φ ψ γ}
    → ∅ ⊢ (φ ∧ (ψ ∨ γ)) ⊃ ((φ ∧ ψ) ∨ (φ ∧ γ))

ex3 {φ}{ψ}{γ} =
  ⊃-intro $
    ⊃-elim
      (⊃-intro $
        ∨-elim {Γ = ∅ , (φ ∧ (ψ ∨ γ))}
          (∨-intro₁ (φ ∧ γ) $
            ∧-intro
              (∧-proj₁ $ weaken ψ $ assume {Γ = ∅} (φ ∧ (ψ ∨ γ)))
              (assume {Γ = ∅ , (φ ∧ (ψ ∨ γ)) } ψ))
          (∨-intro₂ (φ ∧ ψ) $
            ∧-intro
              (∧-proj₁ $ weaken γ $ assume {Γ = ∅} (φ ∧ (ψ ∨ γ)))
              (assume {Γ = ∅ , (φ ∧ (ψ ∨ γ))} γ )))
    (∧-proj₂ $ assume {Γ = ∅} (φ ∧ (ψ ∨ γ)))

ex4 : ∀ {φ ψ}
    → ∅ ⊢ (¬ φ ∨ ψ) ⊃ (φ ⊃ ψ)

ex4 {φ}{ψ} =
  ⊃-intro $
    ∨-elim {Γ = ∅}
      (⊃-intro $
        ⊥-elim {Γ = ∅ , ¬ φ , φ} ψ
          (¬-elim
            (weaken φ $
              assume {Γ = ∅} (¬ φ))
            (assume {Γ = ∅ , ¬ φ} φ)))
      (⊃-intro $
        weaken φ $
          assume {Γ = ∅} ψ)

ex5 : ∀ {φ ψ}
    → ∅ ⊢ ¬ (φ ∨ ψ) ⊃ (¬ φ ∧ ¬ ψ)

ex5 {φ}{ψ} =
  ⊃-intro $
    ∧-intro
      (¬-intro $
        ¬-elim
          (weaken φ $
            assume {Γ = ∅} (¬ (φ ∨ ψ)))
          (∨-intro₁ ψ $
            assume {Γ = ∅ , ¬ (φ ∨ ψ)} φ))
      (¬-intro $
        ¬-elim
          (weaken ψ $
            assume {Γ = ∅} (¬ (φ ∨ ψ)))
          (∨-intro₂ φ $
            assume {Γ = ∅ , ¬ (φ ∨ ψ)} ψ))

¬¬EM : ∀ {Γ} {φ}
     → Γ ⊢ ¬ ¬ (φ ∨ ¬ φ)

¬¬EM {Γ}{φ} =
  ¬-intro $
    ¬-elim
      (assume {Γ = Γ} (¬ (φ ∨ ¬ φ)))
      PEM

RAA⊃EM
  : ∀ {Γ} {φ}
  → Γ ⊢ φ ∨ ¬ φ

RAA⊃EM {Γ}{φ} =
  RAA
    (¬-elim
      (¬¬EM {Γ = Γ , ¬ (φ ∨ ¬ φ)} )
      (assume {Γ = Γ} (¬ (φ ∨ ¬ φ))))

EM⊃Pierce
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ ((φ ⊃ ψ) ⊃ φ) ⊃ φ

EM⊃Pierce {Γ}{φ}{ψ} =
  ⊃-elim
    (⊃-intro
      (∨-elim {Γ = Γ}
        (⊃-intro
          (weaken ((φ ⊃ ψ) ⊃ φ)
            (assume {Γ = Γ} φ)))
        (⊃-intro
          (⊃-elim
            (assume {Γ = Γ , ¬ φ} ((φ ⊃ ψ) ⊃ φ))
              (⊃-intro
                (⊥-elim
                  ψ
                  (¬-elim
                  (weaken φ
                    (weaken ((φ ⊃ ψ) ⊃ φ)
                      (assume {Γ = Γ} (¬ φ))))
                      (assume {Γ = Γ , ¬ φ , (φ ⊃ ψ) ⊃ φ} φ))))
            ))))
      PEM

postulate
  RAA'
    : ∀ {Γ} {φ}
    → Γ ⊢ ( ¬ φ ⊃ φ) ⊃ φ

RAA'⊃RAA : ∀ {Γ}{φ}
         → Γ ⊢ ¬ (¬ φ) ⊃ φ

RAA'⊃RAA {Γ}{φ} =
  ⊃-intro
    (⊃-elim
      RAA'
      (⊃-intro
        (⊥-elim
          φ
          (¬-elim
            (weaken (¬ φ) (assume  {Γ = Γ } ( ¬ (¬ φ))))
            (assume  {Γ = Γ , ¬ (¬ φ) } (¬ φ)))
         )))

postulate
  Pierce : ∀ {Γ} {φ} {ψ}
         → Γ ⊢ ((φ ⊃ ψ) ⊃ φ) ⊃ φ

Pierce⊃RAA' : ∀ {Γ}{φ}
            → Γ ⊢ ( ¬ φ ⊃ φ ) ⊃ φ

Pierce⊃RAA' {Γ}{φ} =
  ⊃-intro $
    ⊃-elim
      (Pierce {Γ = Γ , ¬ φ ⊃ φ} {φ = φ} {ψ = ⊥})
      (⊃-intro $
        ⊃-elim
          (weaken (φ ⊃ ⊥) $
            assume {Γ = Γ} ((¬ φ) ⊃ φ))
          (¬-equiv₂ $
            assume {Γ = Γ , (¬ φ) ⊃ φ}
              (φ ⊃ ⊥)
          )
      )

max_stars_repo_name: jonaprieto/agda-prop

max_issues_repo_name: jonaprieto/agda-prop

max_forks_repo_name: jonaprieto/agda-prop


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

module Relation.Nullary.Decidable where

open import Relation.Nullary.Decidable.Base public

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
module Selective.Examples.TestChannel where

open import Selective.Libraries.Channel
open import Prelude

open import Debug
open import Data.Nat.Show using (show)

ℕ-ReplyMessage : MessageType
ℕ-ReplyMessage = ValueType UniqueTag ∷ [ ValueType ℕ ]ˡ

ℕ-Reply : InboxShape
ℕ-Reply = [ ℕ-ReplyMessage ]ˡ

ℕ×ℕ→ℕ-Message : MessageType
ℕ×ℕ→ℕ-Message = ValueType UniqueTag ∷ ReferenceType ℕ-Reply ∷ ValueType ℕ ∷ [ ValueType ℕ ]ˡ

Calculate : InboxShape
Calculate = [ ℕ×ℕ→ℕ-Message ]ˡ

CalculateProtocol : ChannelInitiation
CalculateProtocol = record
                       { request = Calculate
                       ; response = record {
                         channel-shape = ℕ-Reply
                         ; all-tagged = (HasTag _) ∷ []
                         }
                       ; request-tagged = [ HasTag+Ref _ ]ᵃ
                       }

ℕ×ℕ→ℕ-ci : ChannelInitiation
ℕ×ℕ→ℕ-ci = record {
  request = Calculate
  ; response = record { channel-shape = ℕ-Reply ; all-tagged = (HasTag _) ∷ [] }
  ; request-tagged = (HasTag+Ref _) ∷ [] }

Calculator : InboxShape
Calculator = ℕ×ℕ→ℕ-Message ∷ [ ℕ×ℕ→ℕ-Message ]ˡ

calculator-actor : ∀ {i} → ∞ActorM (↑ i) Calculator (Lift (lsuc lzero) ⊤) [] (λ _ → [])
calculator-actor .force = receive ∞>>= λ {
  (Msg Z (tag ∷ _ ∷ n ∷ m ∷ [])) .force →
    Z ![t: Z ] (lift tag ∷ [ lift (n + m) ]ᵃ) ∞>> (do
    strengthen []
    calculator-actor)
  ; (Msg (S Z) (tag ∷ _ ∷ n ∷ m ∷ [])) .force →
    (Z ![t: Z ] (lift tag ∷ ([ lift (n * m) ]ᵃ))) ∞>> (do
    (strengthen [])
    calculator-actor)
  ; (Msg (S (S ())) _)
  }

TestBox : InboxShape
TestBox = ℕ-Reply

calculator-test-actor : ∀{i} → ∞ActorM i TestBox (Lift (lsuc lzero) ℕ) [] (λ _ → [])
calculator-test-actor = do
  spawn∞ calculator-actor
  let add-request = (record {
    var = Z
    ; chosen-field = Z
    ; fields = lift 32 ∷ [ lift 10 ]ᵃ
    ; session = record {
      can-request = [ Z ]ᵐ -- Pick add method
      ; response-session = record {
        can-receive = [ Z ]ᵐ
        ; tag = 0
        }
      }
    })
    add-rs = add-request .session .response-session
  initiate-channel _ add-request
  Msg Z (_ ∷ n ∷ []) ← from-channel (CalculateProtocol .response) add-rs
    where
      Msg (S ()) _
  let mult-request = (record {
    var = Z
    ; chosen-field = Z
    ; fields = lift n ∷ [ lift 10 ]ᵃ
    ; session = record {
      can-request = [ S Z ]ᵐ -- Pick multiply method
      ; response-session = record {
        can-receive = [ Z ]ᵐ
        ; tag = 1
        }
      }
    })
    mult-rs = add-rs = mult-request .session .response-session
  Msg Z (_ ∷ m ∷ []) ← from-channel (CalculateProtocol .response) mult-rs
    where
      Msg (S ()) _
  debug (show m) (strengthen [])
  return m

max_stars_repo_name: Zalastax/thesis

max_issues_repo_name: Zalastax/singly-typed-actors

max_forks_repo_name: Zalastax/singly-typed-actors


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.Polynomials.Multivariate.EquivCarac.A[X]X-A where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism

open import Cubical.Data.Nat
open import Cubical.Data.Vec
open import Cubical.Data.Sigma
open import Cubical.Data.FinData

open import Cubical.Algebra.DirectSum.DirectSumHIT.Base
open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.FGIdeal
open import Cubical.Algebra.CommRing.QuotientRing

open import Cubical.Algebra.CommRing.Instances.Int renaming (ℤCommRing to ℤCR)
open import Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly
     renaming (PolyCommRing to A[X1,···,Xn] ; Poly to A[x1,···,xn])
open import Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly-Quotient
open import Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly-notationZ

open import Cubical.Relation.Nullary

open import Cubical.HITs.SetQuotients as SQ
open import Cubical.HITs.PropositionalTruncation as PT

private variable
  ℓ : Level

-----------------------------------------------------------------------------
-- Functions

module Properties-Equiv-QuotientXn-A
  (Ar@(A , Astr) : CommRing ℓ)
  where

  private
    A[X] : CommRing ℓ
    A[X] = A[X1,···,Xn] Ar 1

    A[x] : Type ℓ
    A[x] = A[x1,···,xn] Ar 1

    A[X]/X : CommRing ℓ
    A[X]/X = A[X1,···,Xn]/<Xkʲ> Ar 1 0 1

    A[x]/x : Type ℓ
    A[x]/x = A[x1,···,xn]/<xkʲ> Ar 1 0 1

  open CommRingStr Astr using ()
    renaming
    ( 0r        to 0A
    ; 1r        to 1A
    ; _+_       to _+A_
    ; -_        to -A_
    ; _·_       to _·A_
    ; +Assoc    to +AAssoc
    ; +IdL      to +AIdL
    ; +IdR      to +AIdR
    ; +InvL     to +AInvL
    ; +InvR     to +AInvR
    ; +Comm     to +AComm
    ; ·Assoc    to ·AAssoc
    ; ·IdL      to ·AIdL
    ; ·IdR      to ·AIdR
    ; ·DistR+   to ·ADistR+
    ; ·DistL+   to ·ADistL+
    ; is-set    to isSetA     )

  open CommRingStr (snd A[X] ) using ()
    renaming
    ( 0r        to 0PA
    ; 1r        to 1PA
    ; _+_       to _+PA_
    ; -_        to -PA_
    ; _·_       to _·PA_
    ; +Assoc    to +PAAssoc
    ; +IdL      to +PAIdL
    ; +IdR      to +PAIdR
    ; +InvL     to +PAInvL
    ; +InvR     to +PAInvR
    ; +Comm     to +PAComm
    ; ·Assoc    to ·PAAssoc
    ; ·IdL      to ·PAIdL
    ; ·IdR      to ·PAIdR
    ; ·Comm     to ·PAComm
    ; ·DistR+   to ·PADistR+
    ; ·DistL+   to ·PADistL+
    ; is-set    to isSetPA     )

  open CommRingStr (snd A[X]/X) using ()
    renaming
    ( 0r        to 0PAI
    ; 1r        to 1PAI
    ; _+_       to _+PAI_
    ; -_        to -PAI_
    ; _·_       to _·PAI_
    ; +Assoc    to +PAIAssoc
    ; +IdL      to +PAIIdL
    ; +IdR      to +PAIIdR
    ; +InvL     to +PAIInvL
    ; +InvR     to +PAIInvR
    ; +Comm     to +PAIComm
    ; ·Assoc    to ·PAIAssoc
    ; ·IdL      to ·PAIIdL
    ; ·IdR      to ·PAIIdR
    ; ·DistR+   to ·PAIDistR+
    ; ·DistL+   to ·PAIDistL+
    ; is-set    to isSetPAI     )

  open RingTheory

-----------------------------------------------------------------------------
-- Direct sens

  A[x]→A : A[x] → A
  A[x]→A = DS-Rec-Set.f _ _ _ _ isSetA
          0A
          base-trad
          _+A_
          +AAssoc
          +AIdR
          +AComm
          base-neutral-eq
          base-add-eq

       where
       base-trad : _
       base-trad (zero ∷ []) a = a
       base-trad (suc k ∷ []) a = 0A

       base-neutral-eq : _
       base-neutral-eq (zero ∷ []) = refl
       base-neutral-eq (suc k ∷ []) = refl

       base-add-eq : _
       base-add-eq (zero ∷ []) a b = refl
       base-add-eq (suc k ∷ []) a b = +AIdR _

  A[x]→A-pres1 : A[x]→A 1PA ≡ 1A
  A[x]→A-pres1 = refl

  A[x]→A-pres+ : (x y : A[x]) → (A[x]→A (x +PA y)) ≡ A[x]→A x +A A[x]→A y
  A[x]→A-pres+ x y = refl

  A[x]→A-pres· : (x y : A[x]) → (A[x]→A (x ·PA y)) ≡ A[x]→A x ·A A[x]→A y
  A[x]→A-pres· = DS-Ind-Prop.f _ _ _ _
               (λ x u v i y → isSetA _ _ (u y) (v y) i)
               (λ y → sym (0LeftAnnihilates (CommRing→Ring Ar) _))
               (λ v a → DS-Ind-Prop.f _ _ _ _ (λ _ → isSetA _ _)
                         (sym (0RightAnnihilates (CommRing→Ring Ar) _))
                         (λ v' a' → base-eq a a' v v')
                         (λ {U V} ind-U ind-V → cong₂ _+A_ ind-U ind-V ∙ sym (·ADistR+ _ _ _)))
               λ {U V} ind-U ind-V y → cong₂ _+A_ (ind-U y) (ind-V y) ∙ sym (·ADistL+ _ _ _)
            where
            base-eq : (a a' : A) → (v v' : Vec ℕ 1) → (A[x]→A (base v a ·PA base v' a')) ≡ A[x]→A (base v a) ·A A[x]→A (base v' a')
            base-eq a a' (zero ∷ []) (zero ∷ []) = refl
            base-eq a a' (zero ∷ []) (suc k' ∷ []) = sym (0RightAnnihilates (CommRing→Ring Ar) _)
            base-eq a a' (suc k ∷ []) (k' ∷ []) = sym (0LeftAnnihilates (CommRing→Ring Ar) _)

  A[X]→A : CommRingHom A[X] Ar
  fst A[X]→A = A[x]→A
  snd A[X]→A = makeIsRingHom A[x]→A-pres1 A[x]→A-pres+ A[x]→A-pres·

  A[x]→A-cancel : (k : Fin 1) → A[x]→A (<Xkʲ> Ar 1 0 1 k) ≡ 0A
  A[x]→A-cancel zero = refl

  A[X]/X→A : CommRingHom A[X]/X Ar
  A[X]/X→A = Quotient-FGideal-CommRing-CommRing.inducedHom A[X] Ar A[X]→A (<Xkʲ> Ar 1 0 1) A[x]→A-cancel

  A[x]/x→A : A[x]/x → A
  A[x]/x→A = fst A[X]/X→A

-----------------------------------------------------------------------------
-- Converse sens

  A→A[x] : A → A[x]
  A→A[x] a = base (0 ∷ []) a

  A→A[x]-pres+ : (a a' : A) → A→A[x] (a +A a') ≡ A→A[x] a +PA A→A[x] a'
  A→A[x]-pres+ a a' = sym (base-add (0 ∷ []) a a')

  A→A[x]/x : A → A[x]/x
  A→A[x]/x = [_] ∘ A→A[x]

  A→A[x]/x-pres+ : (a a' : A) → A→A[x]/x (a +A a') ≡ A→A[x]/x a +PAI A→A[x]/x a'
  A→A[x]/x-pres+ a a' = cong [_] (A→A[x]-pres+ a a')

-----------------------------------------------------------------------------
-- Section sens

  e-sect : (a : A) → A[x]→A (A→A[x] a) ≡ a
  e-sect a = refl

-----------------------------------------------------------------------------
-- Retraction sens

  open IsRing

  e-retr : (x : A[x]/x) → A→A[x]/x (A[x]/x→A x) ≡ x
  e-retr = SQ.elimProp (λ x → isSetPAI _ _)
           (DS-Ind-Prop.f _ _ _ _ (λ x → isSetPAI _ _)
           (cong [_] (base-neutral _))
           (λ v a → base-eq a v)
           λ {U V} ind-U ind-V → cong [_] ((A→A[x]-pres+ _ _)) ∙ cong₂ _+PAI_ ind-U ind-V)

         where
         base-eq : (a : A) → (v : Vec ℕ 1) → A→A[x]/x (A[x]/x→A [ (base v a) ]) ≡ [ (base v a) ]
         base-eq a (zero ∷ []) = cong [_] refl
         base-eq a (suc k ∷ []) = eq/ (base (0 ∷ []) 0A) (base (suc k ∷ []) a) ∣ ((λ x → base (k ∷ []) (-A a)) , helper) ∣₁
           where
           helper : _
           helper = cong (λ X → X +PA base (suc k ∷ []) (-A a)) (base-neutral _)
                     ∙ +PAIdL _
                     ∙ sym (+PAIdR _
                            ∙ cong₂ base
                                    (cong (λ X → X ∷ []) (+-suc _ _ ∙ +-zero _))
                                    (·AIdR _))

module _
  (Ar@(A , Astr) : CommRing ℓ)
  where

  open Iso
  open Properties-Equiv-QuotientXn-A Ar

  Equiv-A[X]/X-A : CommRingEquiv (A[X1,···,Xn]/<Xkʲ> Ar 1 0 1) Ar
  fst Equiv-A[X]/X-A = isoToEquiv is
    where
    is : Iso (A[x1,···,xn]/<xkʲ> Ar 1 0 1) A
    fun is = A[x]/x→A
    inv is = A→A[x]/x
    rightInv is = e-sect
    leftInv is = e-retr
  snd Equiv-A[X]/X-A = snd A[X]/X→A

Equiv-ℤ[X]/X-ℤ : RingEquiv (CommRing→Ring ℤ[X]/X) (CommRing→Ring ℤCR)
Equiv-ℤ[X]/X-ℤ = Equiv-A[X]/X-A ℤCR

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
open import x1-Base

module x4-Nat where

data ℕ : Set where
  zero :     ℕ
  suc  : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}

data _≤_ : Rel ℕ where
  z≤n : ∀ {x}   → zero ≤ x
  s≤s : ∀ {x y} →     x ≤     y
                → suc x ≤ suc y

≤-suc : ∀ {x y} → suc x ≤ suc y
                →     x ≤     y
≤-suc (s≤s x≤y) = x≤y

_≤?_ : Decidable _≤_
zero  ≤? _      = left  z≤n
suc _ ≤? zero   = right λ()
suc x ≤? suc y with x ≤? y
... | left  x≤y = left  (s≤s x≤y)
... | right x>y = right (λ sx≤sy → x>y (≤-suc sx≤sy))

open import x3-PropositionalEquality using (_≡_; refl; cong; equivalence)

antisym : ∀ {x y} → x ≤ y → y ≤ x → x ≡ y
antisym  z≤n       z≤n      = refl
antisym (s≤s x≤y) (s≤s y≤x) = cong suc (antisym x≤y y≤x)

trans : ∀ {x y z} → x ≤ y → y ≤ z → x ≤ z
trans  z≤n             _  = z≤n
trans (s≤s x≤y) (s≤s y≤z) = s≤s (trans x≤y y≤z)

total : ∀ x y → Either (x ≤ y) (y ≤ x)
total  zero        _ = left  z≤n
total (suc x)   zero = right z≤n
total (suc x) (suc y) with total x y
... | left  x≤y      = left  (s≤s x≤y)
... | right y≤x      = right (s≤s y≤x)

reflexive : ∀ {x y} → x ≡ y → x ≤ y
reflexive {zero}  refl = z≤n
reflexive {suc _} refl = s≤s (reflexive refl)

totalOrder : TotalOrder _≡_ _≤_
totalOrder = record
  { antisym     = antisym
  ; trans       = trans
  ; total       = total
  ; reflexive   = reflexive
  ; equivalence = equivalence
  }

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


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

module Control.Monad.Levels.Zipping where

open import Prelude
open import Control.Monad.Levels.Definition
open import Control.Monad.Levels.Eliminators
open import Data.Bag
open import Path.Reasoning

open import Cubical.Foundations.HLevels using (isOfHLevelΠ)

zip₂-alg : Levels-ϕ[ A ](⟅ A ⟆ → (Levels A → Levels A) → Levels A)
[ zip₂-alg ]-set = isOfHLevelΠ 2 λ _ → isOfHLevelΠ 2 λ _ → trunc
[ zip₂-alg ] y ∷ ys ⟨ _ ⟩ x xs = (x ∪ y) ∷ xs ys
[ zip₂-alg ][] x xs = x ∷ xs []
[ zip₂-alg ]-trail i x xs = ∪-idʳ x i ∷ xs []

zip₂-alg-id : Levels-ψ[ xs ⦂ A ]≡ ((zip₂-alg ↓ xs) [] id ⊜ xs)
⟦ zip₂-alg-id ⟧≡ x ∷ xs ⟨ Pxs ⟩ = refl
⟦ zip₂-alg-id ⟧≡[] = trail

zip-alg : Levels-ϕ[ A ] (Levels A → Levels A)
[ zip-alg ]-set = isOfHLevelΠ 2 λ _ → trunc
[ zip-alg ] x ∷ _ ⟨ k ⟩ ys = (zip₂-alg ↓ ys) x k
[ zip-alg ][] ys = ys
[ zip-alg ]-trail = funExt (zip₂-alg-id ⇓≡_)

zip : Levels A → Levels A → Levels A
zip xs = zip-alg ↓ xs

zip-idʳ : Levels-ψ[ xs ⦂ A ]≡ zip xs [] ⊜ xs
⟦ zip-idʳ ⟧≡ x ∷ xs ⟨ Pxs ⟩ = cong (x ∷_) Pxs
⟦ zip-idʳ ⟧≡[] = refl

mutual
  zip₂-comm : (x : ⟅ A ⟆) (xs : Levels A) (pxs : ∀ ys → zip xs ys ≡ zip ys xs) → Levels-ψ[ ys ⦂ A ]≡  (zip (x ∷ xs) ys ⊜ zip ys (x ∷ xs))
  ⟦ zip₂-comm x xs pxs ⟧≡[] = zip-idʳ ⇓≡ (x ∷ xs)
  ⟦ zip₂-comm x xs pxs ⟧≡ y ∷ ys ⟨ Pys ⟩ = cong₂ _∷_ (∪-comm x y) (pxs ys)

  zip-comm : Levels-ψ[ xs ⦂ A ] (∀ ys → zip xs ys ≡ zip ys xs)
  ∥ zip-comm ∥-prop = isOfHLevelΠ 1 λ _ → trunc _ _
  ∥ zip-comm ∥[] ys = sym (zip-idʳ ⇓≡ ys)
  ∥ zip-comm ∥ x ∷ xs ⟨ Pxs ⟩ ys = zip₂-comm x xs Pxs ⇓≡ ys

zip₃-assoc : (x : ⟅ A ⟆) (xs : Levels A) (pxs : ∀ ys zs → zip (zip xs ys) zs ≡ zip xs (zip ys zs)) →
             (y : ⟅ A ⟆) (ys : Levels A) →
             Levels-ψ[ zs ⦂ A ]≡ (zip (zip (x ∷ xs) (y ∷ ys)) zs ⊜ zip (x ∷ xs) (zip (y ∷ ys) zs))
⟦ zip₃-assoc x xs pxs y ys ⟧≡[] = (zip-idʳ ⇓≡ (zip (x ∷ xs) (y ∷ ys))) ; cong (zip (x ∷ xs)) (sym (zip-idʳ ⇓≡ (y ∷ ys)))
⟦ zip₃-assoc x xs pxs y ys ⟧≡ z ∷ zs ⟨ _ ⟩ = cong₂ _∷_ (∪-assoc x y z) (pxs ys zs)

zip₂-assoc : (x : ⟅ A ⟆) (xs : Levels A) (pxs : ∀ ys zs → zip (zip xs ys) zs ≡ zip xs (zip ys zs)) →
             Levels-ψ[ ys ⦂ A ] (∀ zs → zip (zip (x ∷ xs) ys) zs ≡ zip (x ∷ xs) (zip ys zs))
∥ zip₂-assoc x xs pxs ∥-prop = isOfHLevelΠ 1 λ _ → trunc _ _
∥ zip₂-assoc x xs pxs ∥[] zs = cong (λ xs → zip xs zs) (zip-idʳ ⇓≡ (x ∷ xs))
∥ zip₂-assoc x xs pxs ∥ y ∷ ys ⟨ _ ⟩ zs = zip₃-assoc x xs pxs y ys ⇓≡ zs

zip-assoc : Levels-ψ[ xs ⦂ A ] (∀ ys zs → zip (zip xs ys) zs ≡ zip xs (zip ys zs))
∥ zip-assoc ∥-prop = isOfHLevelΠ 1 λ _ → isOfHLevelΠ 1 λ _ → trunc _ _
∥ zip-assoc ∥ x ∷ xs ⟨ Pxs ⟩ ys zs = ∥ zip₂-assoc x xs Pxs ∥⇓ ys zs
∥ zip-assoc ∥[] _ _ = refl

open import Algebra

module _ {a} {A : Type a} where
  levels-cmon : CommutativeMonoid a
  Monoid.𝑆 (CommutativeMonoid.monoid levels-cmon) = Levels A
  Monoid._∙_ (CommutativeMonoid.monoid levels-cmon) = zip
  Monoid.ε (CommutativeMonoid.monoid levels-cmon) = []
  Monoid.assoc (CommutativeMonoid.monoid levels-cmon) = ∥ zip-assoc ∥⇓
  Monoid.ε∙ (CommutativeMonoid.monoid levels-cmon) _ = refl
  Monoid.∙ε (CommutativeMonoid.monoid levels-cmon) xs = zip-idʳ ⇓≡ xs
  CommutativeMonoid.comm levels-cmon = ∥ zip-comm ∥⇓

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


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

module Data.Binary where

open import Data.Binary.Base public
  using (𝔹; ⟦_⇑⟧; ⟦_⇓⟧; _+_; _*_; _-_)


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

open import Functions.Definition
open import Groups.Definition
open import Groups.Homomorphisms.Definition
open import Setoids.Setoids
open import Sets.EquivalenceRelations
open import Groups.Lemmas
open import Groups.QuotientGroup.Definition
open import Groups.Homomorphisms.Lemmas

module Groups.QuotientGroup.Lemmas {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+A_ : A → A → A} {_+B_ : B → B → B} (G : Group S _+A_) (H : Group T _+B_) {f : A → B} (fHom : GroupHom G H f) where

quotientGroupLemma : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} → {underf : A → B} → (f : GroupHom G H underf) → {x y : A} → Setoid._∼_ T (underf x) (underf y) → Setoid._∼_ (quotientGroupSetoid G f) x y
quotientGroupLemma {S = S} {T = T} G {H = H} fHom {x} {y} fx=fy = transitive (GroupHom.groupHom fHom) (transitive (Group.+WellDefined H (Equivalence.reflexive (Setoid.eq T)) (homRespectsInverse fHom)) (transferToRight'' H fx=fy))
  where
    open Group G
    open Setoid T
    open Equivalence eq

quotientGroupLemma' : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} → {underf : A → B} → (f : GroupHom G H underf) → {x y : A} → Setoid._∼_ (quotientGroupSetoid G f) x y → Setoid._∼_ T (underf x) (underf y)
quotientGroupLemma' {S = S} {T = T} G {H = H} f fx=fy = transferToRight H (transitive (transitive (Group.+WellDefined H (Equivalence.reflexive (Setoid.eq T)) (symmetric (homRespectsInverse f))) (symmetric (GroupHom.groupHom f))) fx=fy)
  where
    open Group G
    open Setoid T
    open Equivalence eq

projectionMapIsGroupHom : GroupHom G (quotientGroupByHom G fHom) id
GroupHom.groupHom projectionMapIsGroupHom {x} {y} = quotientGroupLemma G fHom (Equivalence.reflexive (Setoid.eq T))
GroupHom.wellDefined projectionMapIsGroupHom x=y = quotientGroupLemma G fHom (GroupHom.wellDefined fHom x=y)


text:
-- {-# OPTIONS -v import:10 -v scope:10 #-}

module Issue1078 where

import Common.Level
import Issue1078.A
import Issue1078.B

-- Was: weird scope error in Issue1078.B

-- Should give error:
-- You tried to load Issue1078/B.agda
-- which defines the module Issue1078.A. However, according to the
-- include path this module should be defined in Issue1078/A.agda.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- Laws related to return⋆
------------------------------------------------------------------------

module TotalParserCombinators.Laws.ReturnStar where

open import Algebra
open import Category.Monad
open import Codata.Musical.Notation
open import Data.List
import Data.List.Categorical
open import Data.List.Relation.Binary.BagAndSetEquality as Eq
  using (bag) renaming (_∼[_]_ to _List-∼[_]_)
open import Function
open import Level

private
  module BagMonoid {A : Set} =
    CommutativeMonoid (Eq.commutativeMonoid bag A)
  open module ListMonad =
    RawMonad {f = zero} Data.List.Categorical.monad
    using () renaming (_⊛_ to _⊛′_; _>>=_ to _>>=′_)

open import TotalParserCombinators.Derivative using (D)
open import TotalParserCombinators.Congruence
  hiding (fail)
import TotalParserCombinators.Laws.AdditiveMonoid as AdditiveMonoid
open import TotalParserCombinators.Laws.Derivative
open import TotalParserCombinators.Lib
open import TotalParserCombinators.Parser

-- return⋆ preserves equality.

cong : ∀ {k Tok R} {xs₁ xs₂ : List R} →
       xs₁ List-∼[ k ] xs₂ → return⋆ {Tok = Tok} xs₁ ∼[ k ]P return⋆ xs₂
cong {xs₁ = xs₁} {xs₂} xs₁≈xs₂ = xs₁≈xs₂ ∷ λ t → ♯ (
  D t (return⋆ xs₁)  ≅⟨ D-return⋆ xs₁ ⟩
  fail               ≅⟨ sym $ D-return⋆ xs₂ ⟩
  D t (return⋆ xs₂)  ∎)

-- return⋆ is homomorphic with respect to _++_/_∣_.

distrib-∣ :
  ∀ {Tok R} (xs₁ xs₂ : List R) →
  return⋆ {Tok = Tok} (xs₁ ++ xs₂) ≅P return⋆ xs₁ ∣ return⋆ xs₂
distrib-∣ xs₁ xs₂ =
  BagMonoid.refl ∷ λ t → ♯ (
    D t (return⋆ (xs₁ ++ xs₂))             ≅⟨ D-return⋆ (xs₁ ++ xs₂) ⟩
    fail                                   ≅⟨ sym $ AdditiveMonoid.left-identity fail ⟩
    fail ∣ fail                            ≅⟨ sym $ D-return⋆ xs₁ ∣ D-return⋆ xs₂ ⟩
    D t (return⋆ xs₁) ∣ D t (return⋆ xs₂)  ∎)

-- return⋆ is homomorphic with respect to _⊛′_/_⊛_.

distrib-⊛ :
  ∀ {Tok R₁ R₂} (fs : List (R₁ → R₂)) xs →
  return⋆ {Tok = Tok} (fs ⊛′ xs) ≅P return⋆ fs ⊛ return⋆ xs
distrib-⊛ fs xs =
  BagMonoid.refl ∷ λ t → ♯ (
    D t (return⋆ (fs ⊛′ xs))         ≅⟨ D-return⋆ (fs ⊛′ xs) ⟩

    fail                             ≅⟨ sym $ AdditiveMonoid.left-identity fail ⟩

    fail ∣ fail                      ≅⟨ sym $ left-zero-⊛ (return⋆ xs) ∣
                                              right-zero-⊛ (return⋆ fs) ⟩
    fail ⊛ return⋆ xs ∣
    return⋆ fs ⊛ fail                ≅⟨ sym $ [ ○ - ○ - ○ - ○ ] D-return⋆ fs ⊛ (return⋆ xs ∎) ∣
                                              [ ○ - ○ - ○ - ○ ] return⋆ fs ∎ ⊛ D-return⋆ xs ⟩
    D t (return⋆ fs) ⊛ return⋆ xs ∣
    return⋆ fs ⊛ D t (return⋆ xs)    ≅⟨ sym $ D-⊛ (return⋆ fs) (return⋆ xs) ⟩

    D t (return⋆ fs ⊛ return⋆ xs)    ∎)

-- return⋆ is homomorphic with respect to _>>=′_/_>>=_.

distrib->>= :
  ∀ {Tok R₁ R₂} xs (f : R₁ → List R₂) →
  return⋆ {Tok = Tok} (xs >>=′ f) ≅P return⋆ xs >>= (return⋆ ∘ f)
distrib->>= xs f =
  BagMonoid.refl ∷ λ t → ♯ (
    D t (return⋆ (xs >>=′ f))                   ≅⟨ D-return⋆ (xs >>=′ f) ⟩

    fail                                        ≅⟨ sym $ AdditiveMonoid.left-identity fail ⟩

    fail ∣ fail                                 ≅⟨ sym $ left-zero->>=  (return⋆ ∘ f) ∣
                                                         right-zero->>= (return⋆ xs) ⟩
    fail >>= (return⋆ ∘ f) ∣
    return⋆ xs >>= (λ _ → fail)                 ≅⟨ sym $ [ ○ - ○ - ○ - ○ ] D-return⋆ xs >>= (λ x → return⋆ (f x) ∎) ∣
                                                         [ ○ - ○ - ○ - ○ ] return⋆ xs ∎ >>= (λ x → D-return⋆ (f x)) ⟩
    D t (return⋆ xs) >>= (return⋆ ∘ f) ∣
    return⋆ xs >>= (λ x → D t (return⋆ (f x)))  ≅⟨ sym $ D->>= (return⋆ xs) (return⋆ ∘ f) ⟩

    D t (return⋆ xs >>= (return⋆ ∘ f))          ∎)

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators