text:
------------------------------------------------------------------------------
-- ABP Lemma 2
------------------------------------------------------------------------------

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

-- From Dybjer and Sander's paper: The second lemma states that given
-- a state of the latter kind (see Lemma 1) we will arrive at a new
-- start state, which is identical to the old start state except that
-- the bit has alternated and the first item in the input stream has
-- been removed.

module FOTC.Program.ABP.Lemma2I where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Base.List.PropertiesI
open import FOTC.Base.Loop
open import FOTC.Base.PropertiesI
open import FOTC.Data.Bool
open import FOTC.Data.Bool.PropertiesI
open import FOTC.Data.List
open import FOTC.Data.List.PropertiesI
open import FOTC.Program.ABP.ABP
open import FOTC.Program.ABP.Fair.Type
open import FOTC.Program.ABP.Fair.PropertiesI
open import FOTC.Program.ABP.PropertiesI
open import FOTC.Program.ABP.Terms

------------------------------------------------------------------------------
-- Helper function for Lemma 2.
helper₂ : ∀ {b i' is' os₁' os₂' as' bs' cs' ds' js'} →
          Bit b →
          Fair os₁' →
          S' b i' is' os₁' os₂' as' bs' cs' ds' js' →
          ∀ ft₂ os₂'' → F*T ft₂ → Fair os₂'' → os₂' ≡ ft₂ ++ os₂'' →
          ∃[ os₁'' ] ∃[ os₂'' ] ∃[ as'' ] ∃[ bs'' ] ∃[ cs'' ] ∃[ ds'' ]
            Fair os₁''
            ∧ Fair os₂''
            ∧ S (not b) is' os₁'' os₂'' as'' bs'' cs'' ds'' js'
helper₂ {b} {i'} {is'} {os₁'} {os₂'} {as'} {bs'} {cs'} {ds'} {js'}
       Bb Fos₁' (as'S' , bs'S' , cs'S' , ds'S' , js'S')
       .(T ∷ []) os₂'' f*tnil Fos₂'' os₂'-eq =
       os₁' , os₂'' , as'' , bs'' , cs'' , ds''
       , Fos₁' , Fos₂''
       , as''-eq , bs''-eq ,  cs''-eq , refl , js'-eq
  where
  os₂'-eq-helper : os₂' ≡ T ∷ os₂''
  os₂'-eq-helper =
    os₂'              ≡⟨ os₂'-eq ⟩
    (T ∷ []) ++ os₂'' ≡⟨ ++-∷ T [] os₂'' ⟩
    T ∷ [] ++ os₂''   ≡⟨ ∷-rightCong (++-leftIdentity os₂'') ⟩
    T ∷ os₂''         ∎

  ds'' : D
  ds'' = corrupt os₂'' · cs'

  ds'-eq : ds' ≡ ok b ∷ ds''
  ds'-eq =
    ds' ≡⟨ ds'S' ⟩
    corrupt os₂' · (b ∷ cs')
      ≡⟨ ·-leftCong (corruptCong os₂'-eq-helper) ⟩
    corrupt (T ∷ os₂'') · (b ∷ cs')
      ≡⟨ corrupt-T os₂'' b cs' ⟩
    ok b ∷ corrupt os₂'' · cs'
       ≡⟨ refl ⟩
    ok b ∷ ds'' ∎

  as'' : D
  as'' = as'

  as''-eq : as'' ≡ send (not b) · is' · ds''
  as''-eq =
    as''                         ≡⟨ as'S' ⟩
    await b i' is' ds'           ≡⟨ awaitCong₄ ds'-eq ⟩
    await b i' is' (ok b ∷ ds'') ≡⟨ await-ok≡ b b i' is' ds'' refl ⟩
    send (not b) · is' · ds''    ∎

  bs'' : D
  bs'' = bs'

  bs''-eq : bs'' ≡ corrupt os₁' · as'
  bs''-eq = bs'S'

  cs'' : D
  cs'' = cs'

  cs''-eq : cs'' ≡ ack (not b) · bs'
  cs''-eq = cs'S'

  js'-eq : js' ≡ out (not b) · bs''
  js'-eq = js'S'

helper₂ {b} {i'} {is'} {os₁'} {os₂'} {as'} {bs'} {cs'} {ds'} {js'}
        Bb Fos₁' (as'S' , bs'S' , cs'S' , ds'S' , js'S')
        .(F ∷ ft₂) os₂'' (f*tcons {ft₂} FTft₂) Fos₂'' os₂'-eq =
        helper₂ Bb (tail-Fair Fos₁') ihS' ft₂ os₂'' FTft₂ Fos₂'' refl
  where
  os₁^ : D
  os₁^ = tail₁ os₁'

  os₂^ : D
  os₂^ = ft₂ ++ os₂''

  os₂'-eq-helper : os₂' ≡ F ∷ os₂^
  os₂'-eq-helper = os₂'               ≡⟨ os₂'-eq ⟩
                   (F ∷ ft₂) ++ os₂'' ≡⟨ ++-∷ _ _ _ ⟩
                   F ∷ ft₂ ++ os₂''   ≡⟨ refl ⟩
                   F ∷ os₂^           ∎

  ds^ : D
  ds^ = corrupt os₂^ · cs'

  ds'-eq : ds' ≡ error ∷ ds^
  ds'-eq =
    ds'
      ≡⟨ ds'S' ⟩
    corrupt os₂' · (b ∷ cs')
      ≡⟨ ·-leftCong (corruptCong os₂'-eq-helper) ⟩
    corrupt (F ∷ os₂^) · (b ∷ cs')
      ≡⟨ corrupt-F _ _ _ ⟩
    error ∷ corrupt os₂^ · cs'
      ≡⟨ refl ⟩
    error ∷ ds^ ∎

  as^ : D
  as^ = await b i' is' ds^

  as'-eq : as' ≡ < i' , b > ∷ as^
  as'-eq = as'                             ≡⟨ as'S' ⟩
           await b i' is' ds'              ≡⟨ awaitCong₄ ds'-eq ⟩
           await b i' is' (error ∷ ds^)    ≡⟨ await-error _ _ _ _ ⟩
           < i' , b > ∷ await b i' is' ds^ ≡⟨ refl ⟩
           < i' , b > ∷ as^                ∎

  bs^ : D
  bs^ = corrupt os₁^ · as^

  bs'-eq-helper₁ : os₁' ≡ T ∷ tail₁ os₁' → bs' ≡ ok < i' , b > ∷ bs^
  bs'-eq-helper₁ h =
    bs'
      ≡⟨ bs'S' ⟩
    corrupt os₁' · as'
      ≡⟨ subst₂ (λ t t' → corrupt os₁' · as' ≡ corrupt t · t')
                h
                as'-eq
                refl
      ⟩
    corrupt (T ∷ tail₁ os₁') · (< i' , b > ∷ as^)
      ≡⟨ corrupt-T _ _ _ ⟩
    ok < i' , b > ∷ corrupt (tail₁ os₁') · as^
       ≡⟨ refl ⟩
    ok < i' , b > ∷ bs^ ∎

  bs'-eq-helper₂ : os₁' ≡ F ∷ tail₁ os₁' → bs' ≡ error ∷ bs^
  bs'-eq-helper₂ h =
    bs'
      ≡⟨ bs'S' ⟩
    corrupt os₁' · as'
      ≡⟨ subst₂ (λ t t' → corrupt os₁' · as' ≡ corrupt t · t')
                h
                as'-eq
                refl
      ⟩
    corrupt (F ∷ tail₁ os₁') · (< i' , b > ∷ as^)
      ≡⟨ corrupt-F _ _ _ ⟩
    error ∷ corrupt (tail₁ os₁') · as^
      ≡⟨ refl ⟩
    error ∷ bs^ ∎

  bs'-eq : bs' ≡ ok < i' , b > ∷ bs^ ∨ bs' ≡ error ∷ bs^
  bs'-eq = case (λ h → inj₁ (bs'-eq-helper₁ h))
                (λ h → inj₂ (bs'-eq-helper₂ h))
                (head-tail-Fair Fos₁')

  cs^ : D
  cs^ = ack (not b) · bs^

  cs'-eq-helper₁ : bs' ≡ ok < i' , b > ∷ bs^ → cs' ≡ b ∷ cs^
  cs'-eq-helper₁ h =
    cs'                                 ≡⟨ cs'S' ⟩
    ack (not b) · bs'                   ≡⟨ ·-rightCong h ⟩
    ack (not b) · (ok < i' , b > ∷ bs^) ≡⟨ ack-ok≢ _ _ _ _ (not-x≢x Bb) ⟩
    not (not b) ∷ ack (not b) · bs^     ≡⟨ ∷-leftCong (not-involutive Bb) ⟩
    b ∷ ack (not b) · bs^               ≡⟨ refl ⟩
    b ∷ cs^                             ∎

  cs'-eq-helper₂ : bs' ≡ error ∷ bs^ → cs' ≡ b ∷ cs^
  cs'-eq-helper₂ h =
    cs'                             ≡⟨ cs'S' ⟩
    ack (not b) · bs'               ≡⟨ ·-rightCong h ⟩
    ack (not b) · (error ∷ bs^)     ≡⟨ ack-error _ _ ⟩
    not (not b) ∷ ack (not b) · bs^ ≡⟨ ∷-leftCong (not-involutive Bb) ⟩
    b ∷ ack (not b) · bs^           ≡⟨ refl ⟩
    b ∷ cs^                         ∎

  cs'-eq : cs' ≡ b ∷ cs^
  cs'-eq = case cs'-eq-helper₁ cs'-eq-helper₂ bs'-eq

  js'-eq-helper₁ : bs' ≡ ok < i' , b > ∷ bs^ → js' ≡ out (not b) · bs^
  js'-eq-helper₁ h  =
    js'
      ≡⟨ js'S' ⟩
    out (not b) · bs'
      ≡⟨ ·-rightCong h ⟩
    out (not b) · (ok < i' , b > ∷ bs^)
      ≡⟨ out-ok≢ (not b) b i' bs^ (not-x≢x Bb) ⟩
    out (not b) · bs^ ∎

  js'-eq-helper₂ : bs' ≡ error ∷ bs^ → js' ≡ out (not b) · bs^
  js'-eq-helper₂ h  =
    js'                         ≡⟨ js'S' ⟩
    out (not b) · bs'           ≡⟨ ·-rightCong h ⟩
    out (not b) · (error ∷ bs^) ≡⟨ out-error (not b) bs^ ⟩
    out (not b) · bs^           ∎

  js'-eq : js' ≡ out (not b) · bs^
  js'-eq = case js'-eq-helper₁ js'-eq-helper₂ bs'-eq

  ds^-eq : ds^ ≡ corrupt os₂^ · (b ∷ cs^)
  ds^-eq = ·-rightCong cs'-eq

  ihS' : S' b i' is' os₁^ os₂^ as^ bs^ cs^ ds^ js'
  ihS' = refl , refl , refl , ds^-eq , js'-eq

-- From Dybjer and Sander's paper: From the assumption that
-- os₂' ∈ Fair and hence by unfolding Fair, we conclude that there are
-- ft₂ : F*T and os₂'' : Fair, such that os₂' = ft₂ ++ os₂''.
--
-- We proceed by induction on ft₂ : F*T using helper.

lemma₂ : ∀ {b i' is' os₁' os₂' as' bs' cs' ds' js'} →
         Bit b →
         Fair os₁' →
         Fair os₂' →
         S' b i' is' os₁' os₂' as' bs' cs' ds' js' →
         ∃[ os₁'' ] ∃[ os₂'' ] ∃[ as'' ] ∃[ bs'' ] ∃[ cs'' ] ∃[ ds'' ]
         Fair os₁''
         ∧ Fair os₂''
         ∧ S (not b) is' os₁'' os₂'' as'' bs'' cs'' ds'' js'
lemma₂ {b} {is' = is'} {os₂' = os₂'} {js' = js'} Bb Fos₁' Fos₂' s' =
  helper₁ (Fair-out Fos₂')
  where
  helper₁ : (∃[ ft₂ ] ∃[ os₂'' ] F*T ft₂ ∧ os₂' ≡ ft₂ ++ os₂'' ∧ Fair os₂'') →
            ∃[ os₁'' ] ∃[ os₂'' ] ∃[ as'' ] ∃[ bs'' ] ∃[ cs'' ] ∃[ ds'' ]
              Fair os₁''
              ∧ Fair os₂''
              ∧ S (not b) is' os₁'' os₂'' as'' bs'' cs'' ds'' js'
  helper₁ (ft₂ , os₂'' , FTft₂ , os₂'-eq , Fos₂'') =
    helper₂ Bb Fos₁' s' ft₂ os₂'' FTft₂ Fos₂'' os₂'-eq

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

open import HoTT
open import homotopy.CoHSpace

module homotopy.Cogroup where

record CogroupStructure {i} (X : Ptd i) : Type i where
  field
    co-h-struct : CoHSpaceStructure X
    ⊙inv : X ⊙→ X
  open CoHSpaceStructure co-h-struct public

  inv : de⊙ X → de⊙ X
  inv = fst ⊙inv

  field
    ⊙inv-l : ⊙Wedge-rec ⊙inv (⊙idf X) ⊙∘ ⊙coμ ⊙∼ ⊙cst
    ⊙assoc : ⊙–> (⊙∨-assoc X X X) ⊙∘ ⊙∨-fmap ⊙coμ (⊙idf X) ⊙∘ ⊙coμ
          ⊙∼ ⊙∨-fmap (⊙idf X) ⊙coμ ⊙∘ ⊙coμ

{-
module _ {i j : ULevel} {X : Ptd i} (CGS : CogroupStructure X) where

  open CogroupStructure CGS

  private
    lemma-inv : ⊙Wedge-rec (⊙Lift-fmap ⊙inv) (⊙idf (⊙Lift {j = j} X))
             ⊙∘ ⊙∨-fmap (⊙lift {j = j}) (⊙lift {j = j})
             ⊙∘ ⊙coμ
             ⊙∘ ⊙lower {j = j}
             == ⊙cst
  abstract
    lemma-inv =
        ! (⊙λ= (⊙∘-assoc
             (⊙Wedge-rec (⊙Lift-fmap ⊙inv) (⊙idf (⊙Lift {j = j} X)))
             (⊙∨-fmap ⊙lift ⊙lift)
             (⊙coμ ⊙∘ ⊙lower)))
      ∙ ap (_⊙∘ ⊙coμ ⊙∘ ⊙lower) (⊙λ= (⊙Wedge-rec-fmap (⊙Lift-fmap ⊙inv) (⊙idf _) ⊙lift ⊙lift))
      ∙ ap (_⊙∘ ⊙coμ ⊙∘ ⊙lower) (! (⊙λ= (⊙Wedge-rec-post∘ ⊙lift ⊙inv (⊙idf _))))
      ∙ ⊙λ= (⊙∘-assoc ⊙lift (⊙Wedge-rec ⊙inv (⊙idf X)) (⊙coμ ⊙∘ ⊙lower))
      ∙ ap ⊙Lift-fmap (⊙λ= ⊙inv-l)

  private
    ⊙coμ' : ⊙Lift {j = j} X ⊙→ ⊙Lift {j = j} X ⊙∨ ⊙Lift {j = j} X
    ⊙coμ' = ⊙∨-fmap (⊙lift {j = j}) (⊙lift {j = j}) ⊙∘ ⊙coμ ⊙∘ ⊙lower {j = j}

  private
    lemma-assoc' :
         ⊙–> (⊙∨-assoc (⊙Lift {j = j} X) (⊙Lift {j = j} X) (⊙Lift {j = j} X))
         ⊙∘ ⊙∨-fmap ⊙coμ' (⊙idf (⊙Lift {j = j} X))
         ⊙∘ ⊙∨-fmap (⊙lift {j = j}) (⊙lift {j = j}) ⊙∘ ⊙coμ
      == ⊙∨-fmap (⊙idf (⊙Lift {j = j} X)) ⊙coμ'
         ⊙∘ ⊙∨-fmap (⊙lift {j = j}) (⊙lift {j = j}) ⊙∘ ⊙coμ
  abstract
    lemma-assoc' =
      ⊙–> (⊙∨-assoc (⊙Lift X) (⊙Lift X) (⊙Lift X))
      ⊙∘ ⊙∨-fmap ⊙coμ' (⊙idf (⊙Lift {j = j} X))
      ⊙∘ ⊙∨-fmap ⊙lift ⊙lift ⊙∘ ⊙coμ
        =⟨ ! $ ap (⊙–> (⊙∨-assoc _ _ _) ⊙∘_) $ ⊙λ= $
             ⊙∘-assoc
              (⊙∨-fmap ⊙coμ' (⊙idf (⊙Lift X)))
              (⊙∨-fmap ⊙lift ⊙lift)
              ⊙coμ ⟩
      ⊙–> (⊙∨-assoc (⊙Lift X) (⊙Lift X) (⊙Lift X))
      ⊙∘ (⊙∨-fmap ⊙coμ' (⊙idf (⊙Lift X)) ⊙∘ ⊙∨-fmap ⊙lift ⊙lift)
      ⊙∘ ⊙coμ
        =⟨ ap (λ f → ⊙–> (⊙∨-assoc _ _ _ ) ⊙∘ f ⊙∘ ⊙coμ) $
               ! (⊙λ= $ ⊙∨-fmap-∘ ⊙coμ' ⊙lift (⊙idf (⊙Lift X)) ⊙lift)
               ∙ (⊙λ= $ ⊙∨-fmap-∘ (⊙∨-fmap ⊙lift ⊙lift) ⊙coμ ⊙lift (⊙idf X)) ⟩
      ⊙–> (⊙∨-assoc (⊙Lift X) (⊙Lift X) (⊙Lift X))
      ⊙∘ (⊙∨-fmap (⊙∨-fmap ⊙lift ⊙lift) ⊙lift ⊙∘ ⊙∨-fmap ⊙coμ (⊙idf X))
      ⊙∘ ⊙coμ
        =⟨ ap (⊙–> (⊙∨-assoc _ _ _ ) ⊙∘_) $ ⊙λ= $
            ⊙∘-assoc
              (⊙∨-fmap (⊙∨-fmap ⊙lift ⊙lift) ⊙lift)
              (⊙∨-fmap ⊙coμ (⊙idf X))
              ⊙coμ ⟩
      ⊙–> (⊙∨-assoc (⊙Lift X) (⊙Lift X) (⊙Lift X))
      ⊙∘ ⊙∨-fmap (⊙∨-fmap ⊙lift ⊙lift) ⊙lift
      ⊙∘ ⊙∨-fmap ⊙coμ (⊙idf X) ⊙∘ ⊙coμ
        =⟨ ! $ ⊙λ= $
            ⊙∘-assoc
              (⊙–> (⊙∨-assoc (⊙Lift X) (⊙Lift X) (⊙Lift X)))
              (⊙∨-fmap (⊙∨-fmap ⊙lift ⊙lift) ⊙lift)
              (⊙∨-fmap ⊙coμ (⊙idf X) ⊙∘ ⊙coμ) ⟩
      (⊙–> (⊙∨-assoc (⊙Lift X) (⊙Lift X) (⊙Lift X)) ⊙∘ ⊙∨-fmap (⊙∨-fmap ⊙lift ⊙lift) ⊙lift)
      ⊙∘ ⊙∨-fmap ⊙coμ (⊙idf X) ⊙∘ ⊙coμ
        =⟨ ap (_⊙∘ ⊙∨-fmap ⊙coμ (⊙idf X) ⊙∘ ⊙coμ) $
            ⊙λ= $ ⊙∨-assoc-nat ⊙lift ⊙lift ⊙lift ⟩
      (⊙∨-fmap ⊙lift (⊙∨-fmap ⊙lift ⊙lift) ⊙∘ ⊙–> (⊙∨-assoc X X X))
      ⊙∘ ⊙∨-fmap ⊙coμ (⊙idf X) ⊙∘ ⊙coμ
        =⟨ ⊙λ= $ ⊙∘-assoc
            (⊙∨-fmap ⊙lift (⊙∨-fmap ⊙lift ⊙lift))
            (⊙–> (⊙∨-assoc X X X))
            (⊙∨-fmap ⊙coμ (⊙idf X) ⊙∘ ⊙coμ) ⟩
      ⊙∨-fmap ⊙lift (⊙∨-fmap ⊙lift ⊙lift)
      ⊙∘ ⊙–> (⊙∨-assoc X X X) ⊙∘ ⊙∨-fmap ⊙coμ (⊙idf X) ⊙∘ ⊙coμ
        =⟨ ap (⊙∨-fmap ⊙lift (⊙∨-fmap ⊙lift ⊙lift) ⊙∘_) $ ⊙λ= ⊙assoc ⟩
      ⊙∨-fmap ⊙lift (⊙∨-fmap ⊙lift ⊙lift)
      ⊙∘ ⊙∨-fmap (⊙idf X) ⊙coμ ⊙∘ ⊙coμ
        =⟨ ! $ ⊙λ= $ ⊙∘-assoc
            (⊙∨-fmap ⊙lift (⊙∨-fmap ⊙lift ⊙lift))
            (⊙∨-fmap (⊙idf X) ⊙coμ)
            ⊙coμ ⟩
      (⊙∨-fmap ⊙lift (⊙∨-fmap ⊙lift ⊙lift)
       ⊙∘ ⊙∨-fmap (⊙idf X) ⊙coμ)
      ⊙∘ ⊙coμ
        =⟨ ap (_⊙∘ ⊙coμ) $
             ! (⊙λ= $ ⊙∨-fmap-∘ ⊙lift (⊙idf X) (⊙∨-fmap ⊙lift ⊙lift) ⊙coμ)
             ∙ (⊙λ= $ ⊙∨-fmap-∘ (⊙idf (⊙Lift X)) ⊙lift ⊙coμ' ⊙lift) ⟩
      (⊙∨-fmap (⊙idf (⊙Lift X)) ⊙coμ' ⊙∘ ⊙∨-fmap ⊙lift ⊙lift) ⊙∘ ⊙coμ
        =⟨ ⊙λ= $ ⊙∘-assoc (⊙∨-fmap (⊙idf (⊙Lift X)) ⊙coμ') (⊙∨-fmap ⊙lift ⊙lift) ⊙coμ ⟩
      ⊙∨-fmap (⊙idf (⊙Lift X)) ⊙coμ' ⊙∘ ⊙∨-fmap ⊙lift ⊙lift ⊙∘ ⊙coμ
        =∎

  private
    lemma-assoc :
         ⊙–> (⊙∨-assoc (⊙Lift {j = j} X) (⊙Lift {j = j} X) (⊙Lift {j = j} X))
         ⊙∘ ⊙∨-fmap ⊙coμ' (⊙idf (⊙Lift {j = j} X)) ⊙∘ ⊙coμ'
      == ⊙∨-fmap (⊙idf (⊙Lift {j = j} X)) ⊙coμ' ⊙∘ ⊙coμ'
  abstract
    lemma-assoc = ap (_⊙∘ ⊙lower) lemma-assoc'

  Lift-cogroup-structure : CogroupStructure (⊙Lift {j = j} X)
  Lift-cogroup-structure = record
    { co-h-struct = Lift-co-h-space-structure {j = j} co-h-struct
    ; ⊙inv = ⊙lift ⊙∘ ⊙inv ⊙∘ ⊙lower
    ; ⊙inv-l = ⊙app= lemma-inv
    ; ⊙assoc = ⊙app= lemma-assoc
    }
-}

module _ {i j} {X : Ptd i} (cogroup-struct : CogroupStructure X) (Y : Ptd j) where

  private
    module CGS = CogroupStructure cogroup-struct
    ⊙coμ = CGS.⊙coμ

    comp : (X ⊙→ Y) → (X ⊙→ Y) → (X ⊙→ Y)
    comp f g = ⊙Wedge-rec f g ⊙∘ ⊙coμ

    inv : (X ⊙→ Y) → (X ⊙→ Y)
    inv = _⊙∘ CGS.⊙inv

    abstract
      unit-l : ∀ f → comp ⊙cst f == f
      unit-l f =
        ⊙Wedge-rec ⊙cst f ⊙∘ ⊙coμ
          =⟨ ap2 (λ f g → ⊙Wedge-rec f g ⊙∘ ⊙coμ) (! $ ⊙λ= (⊙∘-cst-r f)) (! $ ⊙λ= (⊙∘-unit-r f)) ⟩
        ⊙Wedge-rec (f ⊙∘ ⊙cst) (f ⊙∘ ⊙idf X) ⊙∘ ⊙coμ
          =⟨ ap (_⊙∘ ⊙coμ) (! $ ⊙λ= $ ⊙Wedge-rec-post∘ f ⊙cst (⊙idf X)) ⟩
        (f ⊙∘ ⊙Wedge-rec ⊙cst (⊙idf X)) ⊙∘ ⊙coμ
          =⟨ ⊙λ= $ ⊙∘-assoc f (⊙Wedge-rec ⊙cst (⊙idf X)) ⊙coμ ⟩
        f ⊙∘ (⊙Wedge-rec ⊙cst (⊙idf X) ⊙∘ ⊙coμ)
          =⟨ ap (f ⊙∘_) (⊙λ= CGS.⊙unit-l) ⟩
        f ⊙∘ ⊙idf X
          =⟨ ⊙λ= (⊙∘-unit-r f) ⟩
        f
          =∎

      assoc : ∀ f g h → comp (comp f g) h == comp f (comp g h)
      assoc f g h =
        ⊙Wedge-rec (⊙Wedge-rec f g ⊙∘ ⊙coμ) h ⊙∘ ⊙coμ
          =⟨ ! $ ⊙λ= (⊙∘-unit-r h) |in-ctx (λ h → ⊙Wedge-rec (⊙Wedge-rec f g ⊙∘ ⊙coμ) h ⊙∘ ⊙coμ) ⟩
        ⊙Wedge-rec (⊙Wedge-rec f g ⊙∘ ⊙coμ) (h ⊙∘ ⊙idf X) ⊙∘ ⊙coμ
          =⟨ ! $ ⊙λ= (⊙Wedge-rec-fmap (⊙Wedge-rec f g) h ⊙coμ (⊙idf X)) |in-ctx _⊙∘ ⊙coμ ⟩
        (⊙Wedge-rec (⊙Wedge-rec f g) h ⊙∘ ⊙∨-fmap ⊙coμ (⊙idf X)) ⊙∘ ⊙coμ
          =⟨ ⊙λ= $ ⊙∘-assoc (⊙Wedge-rec (⊙Wedge-rec f g) h) (⊙∨-fmap ⊙coμ (⊙idf X)) ⊙coμ ⟩
        ⊙Wedge-rec (⊙Wedge-rec f g) h ⊙∘ ⊙∨-fmap ⊙coμ (⊙idf X) ⊙∘ ⊙coμ
          =⟨ ⊙λ= (⊙Wedge-rec-assoc f g h) |in-ctx _⊙∘ ⊙∨-fmap ⊙coμ (⊙idf X) ⊙∘ ⊙coμ ⟩
        (⊙Wedge-rec f (⊙Wedge-rec g h) ⊙∘ ⊙–> (⊙∨-assoc X X X)) ⊙∘ ⊙∨-fmap ⊙coμ (⊙idf X) ⊙∘ ⊙coμ
          =⟨ ⊙λ= $ ⊙∘-assoc (⊙Wedge-rec f (⊙Wedge-rec g h)) (⊙–> (⊙∨-assoc X X X)) (⊙∨-fmap ⊙coμ (⊙idf X) ⊙∘ ⊙coμ) ⟩
        ⊙Wedge-rec f (⊙Wedge-rec g h) ⊙∘ ⊙–> (⊙∨-assoc X X X) ⊙∘ ⊙∨-fmap ⊙coμ (⊙idf X) ⊙∘ ⊙coμ
          =⟨ ⊙λ= CGS.⊙assoc |in-ctx ⊙Wedge-rec f (⊙Wedge-rec g h) ⊙∘_ ⟩
        ⊙Wedge-rec f (⊙Wedge-rec g h) ⊙∘ ⊙∨-fmap (⊙idf X) ⊙coμ ⊙∘ ⊙coμ
          =⟨ ! $ ⊙λ= $ ⊙∘-assoc (⊙Wedge-rec f (⊙Wedge-rec g h)) (⊙∨-fmap (⊙idf X) ⊙coμ) ⊙coμ ⟩
        (⊙Wedge-rec f (⊙Wedge-rec g h) ⊙∘ ⊙∨-fmap (⊙idf X) ⊙coμ) ⊙∘ ⊙coμ
          =⟨ ⊙λ= (⊙Wedge-rec-fmap f (⊙Wedge-rec g h) (⊙idf X) ⊙coμ) |in-ctx _⊙∘ ⊙coμ  ⟩
        ⊙Wedge-rec (f ⊙∘ ⊙idf X) (⊙Wedge-rec g h ⊙∘ ⊙coμ) ⊙∘ ⊙coμ
          =⟨ ⊙λ= (⊙∘-unit-r f) |in-ctx (λ f → ⊙Wedge-rec f (⊙Wedge-rec g h ⊙∘ ⊙coμ) ⊙∘ ⊙coμ) ⟩
        ⊙Wedge-rec f (⊙Wedge-rec g h ⊙∘ ⊙coμ) ⊙∘ ⊙coμ
          =∎

      inv-l : ∀ f → comp (inv f) f == ⊙cst
      inv-l f =
        ⊙Wedge-rec (f ⊙∘ CGS.⊙inv) f ⊙∘ ⊙coμ
          =⟨ ap (λ g → ⊙Wedge-rec (f ⊙∘ CGS.⊙inv) g ⊙∘ ⊙coμ) (! $ ⊙λ= (⊙∘-unit-r f)) ⟩
        ⊙Wedge-rec (f ⊙∘ CGS.⊙inv) (f ⊙∘ ⊙idf X) ⊙∘ ⊙coμ
          =⟨ ap (_⊙∘ ⊙coμ) (! $ ⊙λ= $ ⊙Wedge-rec-post∘ f CGS.⊙inv (⊙idf X)) ⟩
        (f ⊙∘ ⊙Wedge-rec CGS.⊙inv (⊙idf X)) ⊙∘ ⊙coμ
          =⟨ ⊙λ= $ ⊙∘-assoc f (⊙Wedge-rec CGS.⊙inv (⊙idf X)) ⊙coμ ⟩
        f ⊙∘ (⊙Wedge-rec CGS.⊙inv (⊙idf X) ⊙∘ ⊙coμ)
          =⟨ ap (f ⊙∘_) (⊙λ= CGS.⊙inv-l) ⟩
        f ⊙∘ ⊙cst
          =⟨ ⊙λ= (⊙∘-cst-r f) ⟩
        ⊙cst
          =∎

  cogroup⊙→-group-structure : GroupStructure (X ⊙→ Y)
  cogroup⊙→-group-structure = record
    { ident = ⊙cst
    ; inv = inv
    ; comp = comp
    ; unit-l = unit-l
    ; assoc = assoc
    ; inv-l = inv-l
    }

ext: agda

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
{-# OPTIONS --without-K #-}
module Common.Integer where

open import Agda.Builtin.Int public renaming (Int to Integer)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --without-K #-}
module sets.nat.ordering.lt.level where

open import sum
open import equality.core
open import hott.level.core
open import hott.level.closure
open import sets.nat.core
open import sets.nat.ordering.lt.core
open import sets.nat.ordering.leq.level
open import sets.empty
open import container.core
open import container.w

<-level : ∀ {m n} → h 1 (m < n)
<-level = ≤-level

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
{-# OPTIONS --without-K --safe #-}
open import Categories.Category.Core
open import Categories.Category.Monoidal.Core

module Categories.Object.Monoid {o ℓ e} {𝒞 : Category o ℓ e} (C : Monoidal 𝒞) where

open import Level

-- a monoid object is a generalization of the idea from algebra of a monoid,
-- extended into any monoidal category

open Category 𝒞
open Monoidal C

record IsMonoid (M : Obj) : Set (ℓ ⊔ e) where
  field
    μ : M ⊗₀ M ⇒ M
    η : unit ⇒ M

  field
    assoc : μ ∘ μ ⊗₁ id ≈ μ ∘ id ⊗₁ μ ∘ associator.from
    identityˡ : unitorˡ.from ≈ μ ∘ η ⊗₁ id
    identityʳ : unitorʳ.from ≈ μ ∘ id ⊗₁ η

record Monoid : Set (o ⊔ ℓ ⊔ e) where
  field
    Carrier : Obj
    isMonoid : IsMonoid Carrier

  open IsMonoid isMonoid public

open Monoid

record Monoid⇒ (M M′ : Monoid) : Set (ℓ ⊔ e) where
  field
    arr : Carrier M ⇒ Carrier M′
    preserves-μ : arr ∘ μ M ≈ μ M′ ∘ arr ⊗₁ arr
    preserves-η : arr ∘ η M ≈ η M′

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
module AKS.Everything where

open import AKS.Binary
open import AKS.Exponentiation
open import AKS.Extended
open import AKS.Fin
-- open import AKS.Modular.Quotient
-- open import AKS.Polynomial
open import AKS.Primality
open import AKS.Nat
open import AKS.Nat.GCD

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


text:
------------------------------------------------------------------------
-- Quotiented queues: any two queues representing the same sequence
-- are equal
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --safe #-}

import Equality.Path as P

module Queue.Quotiented
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq

open import Prelude

open import Bijection equality-with-J using (_↔_)
open import Equality.Path.Isomorphisms eq
import Equivalence equality-with-J as Eq
open import Function-universe equality-with-J hiding (id; _∘_)
open import H-level.Closure equality-with-J
open import List equality-with-J as L hiding (map)
import Queue equality-with-J as Q
open import Quotient eq as Quotient
open import Sum equality-with-J

private
  variable
    a b             : Level
    A B             : Type a
    s s′ s₁ s₂      : Is-set A
    q q₁ q₂ x x₁ x₂ : A
    f g             : A → B
    xs              : List A

------------------------------------------------------------------------
-- Queues

-- The queue type family is parametrised.

module _
  -- The underlying queue type family.
  (Q : ∀ {ℓ} → Type ℓ → Type ℓ)

  -- Note that the predicate is required to be trivial. Perhaps the
  -- code could be made more general, but I have not found a use for
  -- such generality.
  ⦃ is-queue : ∀ {ℓ} → Q.Is-queue Q (λ _ → ↑ _ ⊤) ℓ ⦄
  where

  abstract

    private

      -- The quotienting relation: Two queues are seen as equal if
      -- they represent the same list.

      _∼_ : {A : Type a} (_ _ : Q A) → Type a
      q₁ ∼ q₂ = Q.to-List _ q₁ ≡ Q.to-List _ q₂

    -- Queues.
    --
    -- The type is abstract to ensure that a change to a different
    -- underlying queue type family does not break code that uses this
    -- module.
    --
    -- Ulf Norell suggested to me that I could use parametrisation
    -- instead of abstract. (Because if the underlying queue type
    -- family is a parameter, then the underlying queues do not
    -- compute.) I decided to use both. (Because I want to have the
    -- flexibility that comes with parametrisation, but I do not want
    -- to force users to work in a parametrised setting.)

    Queue : Type a → Type a
    Queue A = Q A / _∼_

-- The remainder of the code uses an implicit underlying queue type
-- family parameter, and an extra instance argument.

module _
  {Q : ∀ {ℓ} → Type ℓ → Type ℓ}
  ⦃ is-queue : ∀ {ℓ} → Q.Is-queue Q (λ _ → ↑ _ ⊤) ℓ ⦄
  ⦃ is-queue-with-map : ∀ {ℓ₁ ℓ₂} → Q.Is-queue-with-map Q ℓ₁ ℓ₂ ⦄
  where

  abstract

    -- Queue A is a set.

    Queue-is-set : Is-set (Queue Q A)
    Queue-is-set = /-is-set

------------------------------------------------------------------------
-- Conversion functions

  abstract

    -- Converts queues to lists. (The carrier type is required to be a
    -- set.)

    to-List : Is-set A → Queue Q A → List A
    to-List s = Quotient.rec λ where
      .[]ʳ                   → Q.to-List _
      .[]-respects-relationʳ → id
      .is-setʳ               → H-level-List 0 s

    -- Converts lists to queues.

    from-List : List A → Queue Q A
    from-List = [_] ∘ Q.from-List

    -- The function from-List is a right inverse of to-List s.

    to-List-from-List : to-List s (from-List q) ≡ q
    to-List-from-List = Q.to-List-from-List

    -- The function from-List is a left inverse of to-List s.

    from-List-to-List :
      (q : Queue Q A) → _≡_ {A = Queue Q A} (from-List (to-List s q)) q
    from-List-to-List = Quotient.elim-prop λ where
      .[]ʳ q → []-respects-relation (
        Q.to-List ⦃ is-queue = is-queue ⦄ _
          (Q.from-List (Q.to-List _ q))      ≡⟨ Q.to-List-from-List ⟩∎

        Q.to-List _ q                        ∎)
      .is-propositionʳ _ → Queue-is-set

  -- If A is a set, then there is a bijection between Queue Q A and
  -- List A.

  Queue↔List : Is-set A → Queue Q A ↔ List A
  Queue↔List s = record
    { surjection = record
      { logical-equivalence = record
        { to   = to-List s
        ; from = from-List
        }
      ; right-inverse-of = λ _ → to-List-from-List
      }
    ; left-inverse-of = from-List-to-List
    }

------------------------------------------------------------------------
-- Queue operations

  abstract

    private

      -- Helper functions that can be used to define unary functions
      -- on queues.

      unary :
        {A : Type a} {B : Type b}
        (f : List A → List B)
        (g : Q A → Q B) →
        (∀ {q} → Q.to-List _ (g q) ≡ f (Q.to-List _ q)) →
        Queue Q A → Queue Q B
      unary f g h =
        g /-map λ q₁ q₂ q₁∼q₂ →
          Q.to-List _ (g q₁)  ≡⟨ h ⟩
          f (Q.to-List _ q₁)  ≡⟨ cong f q₁∼q₂ ⟩
          f (Q.to-List _ q₂)  ≡⟨ sym h ⟩∎
          Q.to-List _ (g q₂)  ∎

      to-List-unary :
        ∀ {h : ∀ {q} → _} q →
        to-List s₁ (unary f g (λ {q} → h {q = q}) q) ≡ f (to-List s₂ q)
      to-List-unary {s₁ = s₁} {f = f} {g = g} {s₂ = s₂} {h = h} =
        Quotient.elim-prop λ where
          .[]ʳ q →
            to-List s₁ (unary f g h [ q ])  ≡⟨⟩
            Q.to-List _ (g q)               ≡⟨ h ⟩
            f (Q.to-List _ q)               ≡⟨⟩
            f (to-List s₂ [ q ])            ∎
          .is-propositionʳ _ → H-level-List 0 s₁

      -- Generalisations of the functions above.

      unary′ :
        {A : Type a} {F : Type a → Type b} →
        (∀ {A} → Is-set A → Is-set (F A)) →
        (map : ∀ {A B} → (A → B) → F A → F B) →
        (∀ {A} {x : F A} → map id x ≡ x) →
        (∀ {A B C} {f : B → C} {g : A → B} x →
         map (f ∘ g) x ≡ map f (map g x)) →
        (f : List A → F (List B))
        (g : Q A → F (Q B)) →
        (∀ {q} → map (Q.to-List _) (g q) ≡ f (Q.to-List _ q)) →
        Is-set B →
        Queue Q A → F (Queue Q B)
      unary′ F-set map map-id map-∘ f g h s = Quotient.rec λ where
          .[]ʳ → map [_] ∘ g

          .[]-respects-relationʳ {x = q₁} {y = q₂} q₁∼q₂ → lemma₂ (
            map (to-List s) (map [_] (g q₁))  ≡⟨ sym $ map-∘ _ ⟩
            map (Q.to-List _) (g q₁)          ≡⟨ h ⟩
            f (Q.to-List _ q₁)                ≡⟨ cong f q₁∼q₂ ⟩
            f (Q.to-List _ q₂)                ≡⟨ sym h ⟩
            map (Q.to-List _) (g q₂)          ≡⟨ map-∘ _ ⟩∎
            map (to-List s) (map [_] (g q₂))  ∎)

          .is-setʳ → F-set Queue-is-set
        where
        lemma₁ : map from-List (map (to-List s) x) ≡ x
        lemma₁ {x = x} =
          map from-List (map (to-List s) x)  ≡⟨ sym $ map-∘ _ ⟩
          map (from-List ∘ to-List s) x      ≡⟨ cong (flip map x) $ ⟨ext⟩ $ _↔_.left-inverse-of (Queue↔List s) ⟩
          map id x                           ≡⟨ map-id ⟩∎
          x                                  ∎

        lemma₂ :
          map (to-List s) x₁ ≡ map (to-List s) x₂ →
          x₁ ≡ x₂
        lemma₂ {x₁ = x₁} {x₂ = x₂} eq =
          x₁                                  ≡⟨ sym lemma₁ ⟩
          map from-List (map (to-List s) x₁)  ≡⟨ cong (map from-List) eq ⟩
          map from-List (map (to-List s) x₂)  ≡⟨ lemma₁ ⟩∎
          x₂                                  ∎

      to-List-unary′ :
        {F      : Type a → Type b}
        (F-set  : ∀ {A} → Is-set A → Is-set (F A))
        (map    : ∀ {A B} → (A → B) → F A → F B)
        (map-id : ∀ {A} {x : F A} → map id x ≡ x)
        (map-∘  : ∀ {A B C} {f : B → C} {g : A → B} x →
                  map (f ∘ g) x ≡ map f (map g x))
        (f : List A → F (List B))
        (g : Q A → F (Q B))
        (h : ∀ {q} → map (Q.to-List _) (g q) ≡ f (Q.to-List _ q))
        (s : Is-set B) →
        ∀ q →
        map (to-List s) (unary′ F-set map map-id map-∘ f g h s q) ≡
        f (to-List s′ q)
      to-List-unary′ {s′ = s′} F-set map map-id map-∘ f g h s =
        Quotient.elim-prop λ where
          .[]ʳ q →
            map (to-List s)
                (unary′ F-set map map-id map-∘ f g h s [ q ])  ≡⟨⟩

            map (to-List s) (map [_] (g q))                    ≡⟨ sym $ map-∘ _ ⟩

            map (Q.to-List _) (g q)                            ≡⟨ h ⟩

            f (Q.to-List _ q)                                  ≡⟨⟩

            f (to-List s′ [ q ])                               ∎
          .is-propositionʳ _ → F-set (H-level-List 0 s)

    -- Enqueues an element.

    enqueue : A → Queue Q A → Queue Q A
    enqueue x = unary (_++ x ∷ []) (Q.enqueue x) Q.to-List-enqueue

    to-List-enqueue : to-List s (enqueue x q) ≡ to-List s q ++ x ∷ []
    to-List-enqueue {q = q} = to-List-unary q

    -- Dequeues an element, if possible. (The carrier type is required
    -- to be a set.)

    dequeue : Is-set A → Queue Q A → Maybe (A × Queue Q A)
    dequeue s = unary′
      (Maybe-closure 0 ∘ ×-closure 2 s)
      (λ f → ⊎-map id (Σ-map id f))
      ⊎-map-id
      ⊎-map-∘
      (_↔_.to List↔Maybe[×List])
      (Q.dequeue _)
      Q.to-List-dequeue
      s

    to-List-dequeue :
      ⊎-map id (Σ-map id (to-List s)) (dequeue s q) ≡
      _↔_.to List↔Maybe[×List] (to-List s q)
    to-List-dequeue {q = q} = to-List-unary′
      (Maybe-closure 0 ∘ ×-closure 2 _)
      (λ f → ⊎-map id (Σ-map id f))
      ⊎-map-id
      ⊎-map-∘
      _
      (Q.dequeue _)
      _
      _
      q

    -- The "inverse" of the dequeue operation.

    dequeue⁻¹ : Maybe (A × Queue Q A) → Queue Q A
    dequeue⁻¹ nothing        = [ Q.empty ]
    dequeue⁻¹ (just (x , q)) = unary (x ∷_) (Q.cons x) Q.to-List-cons q

    to-List-dequeue⁻¹ :
      to-List s (dequeue⁻¹ x) ≡
      _↔_.from List↔Maybe[×List] (⊎-map id (Σ-map id (to-List s)) x)
    to-List-dequeue⁻¹ {x = nothing}      = Q.to-List-empty
    to-List-dequeue⁻¹ {x = just (_ , q)} = to-List-unary q

    -- A map function.

    map : (A → B) → Queue Q A → Queue Q B
    map f = unary (L.map f) (Q.map f) Q.to-List-map

    to-List-map : to-List s₁ (map f q) ≡ L.map f (to-List s₂ q)
    to-List-map {q = q} = to-List-unary q

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Right-biased universe-sensitive functor and monad instances for These.
--
-- To minimize the universe level of the RawFunctor, we require that
-- elements of B are "lifted" to a copy of B at a higher universe level
-- (a ⊔ b).
-- See the Data.Product.Categorical.Examples for how this is done in a
-- Product-based similar setting.
------------------------------------------------------------------------

-- This functor can be understood as a notion of computation which can
-- either fail (that), succeed (this) or accumulate warnings whilst
-- delivering a successful computation (these).

-- It is a good alternative to Data.Product.Categorical when the notion
-- of warnings does not have a neutral element (e.g. List⁺).

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

open import Level
open import Algebra

module Data.These.Categorical.Right (a : Level) {c ℓ} (W : Semigroup c ℓ) where

open Semigroup W
open import Data.These.Categorical.Right.Base a Carrier public

open import Data.These
open import Category.Applicative
open import Category.Monad

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

applicative : RawApplicative Theseᵣ
applicative = record
  { pure = this
  ; _⊛_  = ap
  } where

  ap : ∀ {A B}→ Theseᵣ (A → B) → Theseᵣ A → Theseᵣ B
  ap (this f)    t = map₁ f t
  ap (that w)    t = that w
  ap (these f w) t = map f (w ∙_) t

monad : RawMonad Theseᵣ
monad = record
  { return = this
  ; _>>=_  = bind
  } where

  bind : ∀ {A B} → Theseᵣ A → (A → Theseᵣ B) → Theseᵣ B
  bind (this t)    f = f t
  bind (that w)    f = that w
  bind (these t w) f = map₂ (w ∙_) (f t)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Choosing between elements based on the result of applying a function
------------------------------------------------------------------------

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

open import Algebra

module Algebra.Construct.LiftedChoice where

open import Algebra.Consequences.Base
open import Relation.Binary
open import Relation.Nullary using (¬_; yes; no)
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_])
open import Data.Product using (_×_; _,_)
open import Level using (Level; _⊔_)
open import Function.Base using (id; _on_)
open import Function.Injection using (Injection)
open import Function.Equality using (Π)
open import Relation.Binary using (Setoid; _Preserves_⟶_)
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Unary using (Pred)
open import Relation.Nullary.Negation using (contradiction)

import Relation.Binary.Reasoning.Setoid as EqReasoning

private
  variable
    a b p ℓ : Level
    A : Set a
    B : Set b

------------------------------------------------------------------------
-- Definition

module _ (_≈_ : Rel B ℓ) (_•_ : Op₂ B) where

  Lift : Selective _≈_ _•_ → (A → B) → Op₂ A
  Lift ∙-sel f x y with ∙-sel (f x) (f y)
  ... | inj₁ _ = x
  ... | inj₂ _ = y

------------------------------------------------------------------------
-- Algebraic properties

module _ {_≈_ : Rel B ℓ} {_∙_ : Op₂ B}
         (∙-isSelectiveMagma : IsSelectiveMagma _≈_ _∙_) where

  private module M = IsSelectiveMagma ∙-isSelectiveMagma
  open M hiding (sel; isMagma)
  open EqReasoning setoid

  module _ (f : A → B) where

    private
      _◦_ = Lift _≈_ _∙_ M.sel f

    sel-≡ : Selective _≡_ _◦_
    sel-≡ x y with M.sel (f x) (f y)
    ... | inj₁ _ = inj₁ P.refl
    ... | inj₂ _ = inj₂ P.refl

    distrib : ∀ x y → ((f x) ∙ (f y)) ≈ f (x ◦ y)
    distrib x y with M.sel (f x) (f y)
    ... | inj₁ fx∙fy≈fx = fx∙fy≈fx
    ... | inj₂ fx∙fy≈fy = fx∙fy≈fy

  module _ (f : A → B) {_≈′_ : Rel A ℓ}
           (≈-reflexive : _≡_ ⇒ _≈′_) where

    private
      _◦_ = Lift _≈_ _∙_ M.sel f

    sel : Selective _≈′_ _◦_
    sel x y = Sum.map ≈-reflexive ≈-reflexive (sel-≡ f x y)

    idem : Idempotent _≈′_ _◦_
    idem = sel⇒idem _≈′_ sel

  module _ {f : A → B} {_≈′_ : Rel A ℓ}
           (f-injective : ∀ {x y} → f x ≈ f y → x ≈′ y)
           where

    private
      _◦_ = Lift _≈_ _∙_ M.sel f

    cong : f Preserves _≈′_ ⟶ _≈_ → Congruent₂ _≈′_ _◦_
    cong f-cong {x} {y} {u} {v} x≈y u≈v
      with M.sel (f x) (f u) | M.sel (f y) (f v)
    ... | inj₁ fx∙fu≈fx | inj₁ fy∙fv≈fy = x≈y
    ... | inj₂ fx∙fu≈fu | inj₂ fy∙fv≈fv = u≈v
    ... | inj₁ fx∙fu≈fx | inj₂ fy∙fv≈fv = f-injective (begin
      f x       ≈⟨ sym fx∙fu≈fx ⟩
      f x ∙ f u ≈⟨ ∙-cong (f-cong x≈y) (f-cong u≈v) ⟩
      f y ∙ f v ≈⟨ fy∙fv≈fv ⟩
      f v       ∎)
    ... | inj₂ fx∙fu≈fu | inj₁ fy∙fv≈fy = f-injective (begin
      f u       ≈⟨ sym fx∙fu≈fu ⟩
      f x ∙ f u ≈⟨ ∙-cong (f-cong x≈y) (f-cong u≈v) ⟩
      f y ∙ f v ≈⟨ fy∙fv≈fy ⟩
      f y       ∎)

    assoc : Associative _≈_ _∙_ → Associative _≈′_ _◦_
    assoc ∙-assoc x y z = f-injective (begin
      f ((x ◦ y) ◦ z)   ≈˘⟨ distrib f (x ◦ y) z ⟩
      f (x ◦ y) ∙ f z   ≈˘⟨ ∙-congʳ (distrib f x y) ⟩
      (f x ∙ f y) ∙ f z ≈⟨  ∙-assoc (f x) (f y) (f z) ⟩
      f x ∙ (f y ∙ f z) ≈⟨  ∙-congˡ (distrib f y z) ⟩
      f x ∙ f (y ◦ z)   ≈⟨  distrib f x (y ◦ z) ⟩
      f (x ◦ (y ◦ z))   ∎)

    comm : Commutative _≈_ _∙_ → Commutative _≈′_ _◦_
    comm ∙-comm x y = f-injective (begin
      f (x ◦ y) ≈˘⟨ distrib f x y ⟩
      f x ∙ f y ≈⟨  ∙-comm (f x) (f y) ⟩
      f y ∙ f x ≈⟨  distrib f y x ⟩
      f (y ◦ x) ∎)

------------------------------------------------------------------------
-- Algebraic structures

  module _ {_≈′_ : Rel A ℓ} {f : A → B}
           (f-injective : ∀ {x y} → f x ≈ f y → x ≈′ y)
           (f-cong : f Preserves _≈′_ ⟶ _≈_)
           (≈′-isEquivalence : IsEquivalence _≈′_)
           where

    private
      module E = IsEquivalence ≈′-isEquivalence
      _◦_ = Lift _≈_ _∙_ M.sel f

    isMagma : IsMagma _≈′_ _◦_
    isMagma = record
      { isEquivalence = ≈′-isEquivalence
      ; ∙-cong        = cong (λ {x y} → f-injective {x} {y}) f-cong
      }

    isSemigroup : Associative _≈_ _∙_ → IsSemigroup _≈′_ _◦_
    isSemigroup ∙-assoc = record
      { isMagma = isMagma
      ; assoc   = assoc (λ {x y} → f-injective {x} {y}) ∙-assoc
      }

    isBand : Associative _≈_ _∙_ → IsBand _≈′_ _◦_
    isBand ∙-assoc = record
      { isSemigroup = isSemigroup ∙-assoc
      ; idem        = idem f E.reflexive
      }

    isSemilattice : Associative _≈_ _∙_ → Commutative _≈_ _∙_ →
                    IsSemilattice _≈′_ _◦_
    isSemilattice ∙-assoc ∙-comm = record
      { isBand = isBand ∙-assoc
      ; comm   = comm (λ {x y} → f-injective {x} {y}) ∙-comm
      }

    isSelectiveMagma : IsSelectiveMagma _≈′_ _◦_
    isSelectiveMagma = record
      { isMagma = isMagma
      ; sel     = sel f E.reflexive
      }

------------------------------------------------------------------------
-- Other properties

  module _ {P : Pred A p} (f : A → B) where

    private
      _◦_ = Lift _≈_ _∙_ M.sel f

    preservesᵒ : (∀ {x y} → P x → (f x ∙ f y) ≈ f y → P y) →
                 (∀ {x y} → P y → (f x ∙ f y) ≈ f x → P x) →
                 ∀ x y → P x ⊎ P y → P (x ◦ y)
    preservesᵒ left right x y (inj₁ px) with M.sel (f x) (f y)
    ... | inj₁ _        = px
    ... | inj₂ fx∙fy≈fx = left px fx∙fy≈fx
    preservesᵒ left right x y (inj₂ py) with M.sel (f x) (f y)
    ... | inj₁ fx∙fy≈fy = right py fx∙fy≈fy
    ... | inj₂ _        = py

    preservesʳ : (∀ {x y} → P y → (f x ∙ f y) ≈ f x → P x) →
                 ∀ x {y} → P y → P (x ◦ y)
    preservesʳ right x {y} Py with M.sel (f x) (f y)
    ... | inj₁ fx∙fy≈fx = right Py fx∙fy≈fx
    ... | inj₂ fx∙fy≈fy = Py

    preservesᵇ : ∀ {x y} → P x → P y → P (x ◦ y)
    preservesᵇ {x} {y} Px Py with M.sel (f x) (f y)
    ... | inj₁ _ = Px
    ... | inj₂ _ = Py

    forcesᵇ : (∀ {x y} → P x → (f x ∙ f y) ≈ f x → P y) →
              (∀ {x y} → P y → (f x ∙ f y) ≈ f y → P x) →
              ∀ x y → P (x ◦ y) → P x × P y
    forcesᵇ presˡ presʳ x y P[x∙y] with M.sel (f x) (f y)
    ... | inj₁ fx∙fy≈fx = P[x∙y] , presˡ P[x∙y] fx∙fy≈fx
    ... | inj₂ fx∙fy≈fy = presʳ P[x∙y] fx∙fy≈fy , P[x∙y]


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

open import LogicalFormulae
open import Setoids.Setoids
open import Sets.EquivalenceRelations
open import Rings.IntegralDomains.Definition
open import Rings.Definition

module Rings.Irreducibles.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} (intDom : IntegralDomain R) where

open import Rings.Irreducibles.Definition intDom
open import Rings.Divisible.Definition R
open import Rings.Units.Definition R

open Setoid S
open Equivalence eq
open Ring R

dividesIrreducibleImpliesUnit : {r c : A} → Irreducible r → c ∣ r → (r ∣ c → False) → Unit c
dividesIrreducibleImpliesUnit {r} {c} irred (x , cx=r) notAssoc = Irreducible.irreducible irred x c (transitive *Commutative cx=r) nonunit
  where
    nonunit : Unit x → False
    nonunit (a , xa=1) = notAssoc (a , transitive (transitive (transitive (transitive (*WellDefined (symmetric cx=r) reflexive) (symmetric *Associative)) *Commutative) (*WellDefined xa=1 reflexive)) identIsIdent)


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}

module Cubical.Algebra.Group.EilenbergMacLane.CupProduct where

open import Cubical.Algebra.Group.EilenbergMacLane.Base renaming (elim to EM-elim)
open import Cubical.Algebra.Group.EilenbergMacLane.WedgeConnectivity
open import Cubical.Algebra.Group.EilenbergMacLane.GroupStructure
open import Cubical.Algebra.Group.EilenbergMacLane.Properties
open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Properties

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.GroupoidLaws renaming (assoc to ∙assoc)
open import Cubical.Foundations.Path
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Transport

open import Cubical.Foundations.Pointed.Homogeneous

open import Cubical.Functions.Morphism

open import Cubical.Homotopy.Loopspace

open import Cubical.HITs.Truncation as Trunc renaming (rec to trRec; elim to trElim)
open import Cubical.HITs.EilenbergMacLane1 renaming (rec to EMrec)
open import Cubical.Algebra.AbGroup.Base
open import Cubical.Data.Empty
  renaming (rec to ⊥-rec)
open import Cubical.HITs.Truncation
  renaming (elim to trElim ; rec to trRec ; rec2 to trRec2)
open import Cubical.Data.Nat hiding (_·_) renaming (elim to ℕelim)
open import Cubical.HITs.Susp

open import Cubical.Algebra.AbGroup.TensorProduct
open import Cubical.Algebra.Group

open AbGroupStr renaming (_+_ to _+Gr_ ; -_ to -Gr_)

open PlusBis

private
  variable
    ℓ ℓ' ℓ'' : Level

-- Lemma for distributativity of cup product (used later)
pathType : ∀ {ℓ} {G : AbGroup ℓ} (n : ℕ) (x : EM G (2 + n)) (p : 0ₖ (2 + n) ≡ x) → Type ℓ
pathType n x p = sym (rUnitₖ (2 + n) x) ∙ (λ i → x +ₖ p i)
               ≡ sym (lUnitₖ (2 + n) x) ∙ λ i → p i +ₖ x

pathTypeMake : ∀ {ℓ} {G : AbGroup ℓ} (n : ℕ) (x : EM G (2 + n)) (p : 0ₖ (2 + n) ≡ x)
    → pathType n x p
pathTypeMake n x = J (λ x p → pathType n x p) refl

-- Definition of cup product (⌣ₖ, given by ·₀ when first argument is in K(G,0))
module _ {G' : AbGroup ℓ} {H' : AbGroup ℓ'} where
   private
     G = fst G'
     H = fst H'

     strG = snd G'
     strH = snd H'

     0G = 0g strG
     0H = 0g strH

     _+G_ = _+Gr_ strG
     _+H_ = _+Gr_ strH

     -H_ = -Gr_ strH
     -G_ = -Gr_ strG

   ·₀' : H → (m : ℕ) → EM G' m → EM (G' ⨂ H') m
   ·₀' h =
     elim+2
       (_⊗ h)
       (elimGroupoid _ (λ _ → emsquash)
         embase
         (λ g → emloop (g ⊗ h))
         λ g l →
           compPathR→PathP
             (sym (∙assoc _ _ _
                ∙∙ cong₂ _∙_ (sym (emloop-comp _ _ _)
                            ∙ cong emloop (sym (⊗DistL+⊗ g l h))) refl
                ∙∙ rCancel _)))
       λ n f → trRec (isOfHLevelTrunc (4 + n))
                        λ { north → 0ₖ (suc (suc n))
                          ; south → 0ₖ (suc (suc n))
                          ; (merid a i) → EM→ΩEM+1 (suc n) (f (EM-raw→EM _ _ a)) i}

   ·₀ : G → (m : ℕ) → EM H' m → EM (G' ⨂ H') m
   ·₀ g =
     elim+2 (λ h → g ⊗ h)
               (elimGroupoid _ (λ _ → emsquash)
                 embase
                 (λ h → emloop (g ⊗ h))
                 λ h l → compPathR→PathP
                   (sym (∙assoc _ _ _
                      ∙∙ cong₂ _∙_ (sym (emloop-comp _ _ _) ∙ cong emloop (sym (⊗DistR+⊗ g h l))) refl
                      ∙∙ rCancel _)))
               λ n f
               → trRec (isOfHLevelTrunc (4 + n))
                        λ { north → 0ₖ (suc (suc n))
                          ; south → 0ₖ (suc (suc n))
                          ; (merid a i) → EM→ΩEM+1 (suc n) (f (EM-raw→EM _ _ a)) i}

   ·₀-distr : (g h : G) → (m : ℕ)  (x : EM H' m) → ·₀ (g +G h) m x ≡ ·₀ g m x +ₖ ·₀ h m x
   ·₀-distr g h =
     elim+2
       (⊗DistL+⊗ g h)
       (elimSet _ (λ _ → emsquash _ _)
         refl
         (λ w → compPathR→PathP (sym ((λ i → emloop (⊗DistL+⊗ g h w i)
                               ∙ (lUnit (sym (cong₂+₁ (emloop (g ⊗ w)) (emloop (h ⊗ w)) i)) (~ i)))
              ∙∙ cong₂ _∙_ (emloop-comp _ (g ⊗ w) (h ⊗ w)) refl
              ∙∙ rCancel _))))
       λ m ind →
         trElim (λ _ → isOfHLevelTruncPath)
                λ { north → refl
                  ; south → refl
                  ; (merid a i) k → z m ind a k i}

      where
      z : (m : ℕ) → ((x : EM H' (suc m))
        → ·₀ (g +G h) (suc m) x
         ≡ ·₀ g (suc m) x +ₖ ·₀ h (suc m) x) → (a : EM-raw H' (suc m))
        → cong (·₀ (g +G h) (suc (suc m))) (cong ∣_∣ₕ (merid a)) ≡
          cong₂ _+ₖ_
            (cong (·₀ g (suc (suc m))) (cong ∣_∣ₕ (merid a)))
            (cong (·₀ h (suc (suc m))) (cong ∣_∣ₕ (merid a)))
      z m ind a = (λ i → EM→ΩEM+1 _ (ind (EM-raw→EM _ _ a) i))
               ∙∙ EM→ΩEM+1-hom _ (·₀ g (suc m) (EM-raw→EM H' (suc m) a))
                                  (·₀ h (suc m) (EM-raw→EM H' (suc m) a))
               ∙∙ sym (cong₂+₂ m (cong (·₀ g (suc (suc m))) (cong ∣_∣ₕ (merid a)))
                                 (cong (·₀ h (suc (suc m))) (cong ∣_∣ₕ (merid a))))

   ·₀0 : (m : ℕ) → (g : G) → ·₀ g m (0ₖ m) ≡ 0ₖ m
   ·₀0 zero = ⊗AnnihilR
   ·₀0 (suc zero) g = refl
   ·₀0 (suc (suc m)) g = refl

   ·₀'0 : (m : ℕ) (h : H) → ·₀' h m (0ₖ m) ≡ 0ₖ m
   ·₀'0 zero = ⊗AnnihilL
   ·₀'0 (suc zero) g = refl
   ·₀'0 (suc (suc m)) g = refl

   0·₀ : (m : ℕ) → (x : _) → ·₀ 0G m x ≡ 0ₖ m
   0·₀ =
     elim+2 ⊗AnnihilL
       (elimSet _ (λ _ → emsquash _ _)
         refl
         λ g → compPathR→PathP ((sym (emloop-1g _)
                                ∙ cong emloop (sym (⊗AnnihilL g)))
                                ∙∙ (λ i → rUnit (rUnit (cong (·₀ 0G 1) (emloop g)) i) i)
                                ∙∙ sym (∙assoc _ _ _)))
       λ n f → trElim (λ _ → isOfHLevelTruncPath)
                       λ { north → refl
                         ; south → refl
                         ; (merid a i) j → (cong (EM→ΩEM+1 (suc n)) (f (EM-raw→EM _ _ a))
                                           ∙ EM→ΩEM+1-0ₖ _) j i}

   0·₀' : (m : ℕ) (g : _) → ·₀' 0H m g ≡ 0ₖ m
   0·₀' =
     elim+2
       ⊗AnnihilR
       (elimSet _ (λ _ → emsquash _ _)
         refl
         λ g → compPathR→PathP (sym (∙assoc _ _ _
                              ∙∙ sym (rUnit _) ∙ sym (rUnit _)
                              ∙∙ (cong emloop (⊗AnnihilR g)
                                ∙ emloop-1g _))))
       λ n f → trElim (λ _ → isOfHLevelTruncPath)
                       λ { north → refl
                         ; south → refl
                         ; (merid a i) j → (cong (EM→ΩEM+1 (suc n)) (f (EM-raw→EM _ _ a))
                                           ∙ EM→ΩEM+1-0ₖ _) j i}

-- Definition of the cup product
   cup∙ : ∀ n m → EM G' n → EM∙ H' m →∙ EM∙ (G' ⨂ H') (n +' m)
   cup∙ =
     ℕelim
       (λ m g → (·₀ g m) , ·₀0 m g)
         λ n f →
           ℕelim
             (λ g → (λ h → ·₀' h (suc n) g) , 0·₀' (suc n) g)
             λ m _ → main n m f

     where
     main : (n m : ℕ) (ind : ((m : ℕ) → EM G' n → EM∙ H' m →∙ EM∙ (G' ⨂ H') (n +' m)))
         → EM G' (suc n) →  EM∙ H' (suc m) →∙ EM∙ (G' ⨂ H') (suc (suc (n + m)))
     main zero m ind =
       elimGroupoid _ (λ _ → isOfHLevel↑∙ _ _)
         ((λ _ → 0ₖ (2 + m)) , refl)
         (f m)
         λ n h → finalpp m n h
       where
       f : (m : ℕ) → G → typ (Ω (EM∙ H' (suc m) →∙ EM∙ (G' ⨂ H') (suc (suc m)) ∙))
       fst (f m g i) x = EM→ΩEM+1 _ (·₀ g _ x) i
       snd (f zero g i) j = EM→ΩEM+1-0ₖ (suc zero) j i
       snd (f (suc m) g i) j = EM→ΩEM+1-0ₖ (suc (suc m)) j i

       f-hom-fst : (m : ℕ) (g h : G) → cong fst (f m (g +G h)) ≡ cong fst (f m g ∙ f m h)
       f-hom-fst m g h =
            (λ i j x → EM→ΩEM+1 _ (·₀-distr g h (suc m) x i) j)
         ∙∙ (λ i j x → EM→ΩEM+1-hom _ (·₀ g (suc m) x) (·₀ h (suc m) x) i j)
         ∙∙ sym (cong-∙ fst (f m g) (f m h))

       f-hom : (m : ℕ) (g h : G) → f m (g +G h) ≡ f m g ∙ f m h
       f-hom m g h = →∙Homogeneous≡Path (isHomogeneousEM _) _ _ (f-hom-fst m g h)

       finalpp : (m : ℕ) (g h : G) → PathP (λ i → f m g i ≡ f m (g +G h) i) refl (f m h)
       finalpp m g h =
         compPathR→PathP (sym (rCancel _)
                       ∙∙ cong (_∙ sym (f m (g +G h))) (f-hom m g h)
                       ∙∙ sym (∙assoc _ _ _))

     main (suc n) m ind =
       trElim (λ _ → isOfHLevel↑∙ (2 + n) m)
         λ { north → (λ _ → 0ₖ (3 + (n + m))) , refl
           ; south → (λ _ → 0ₖ (3 + (n + m))) , refl
           ; (merid a i) → Iso.inv (ΩfunExtIso _ _)
                             (EM→ΩEM+1∙ _ ∘∙ ind (suc m) (EM-raw→EM _ _ a)) i}

   _⌣ₖ_ : {n m : ℕ} (x : EM G' n) (y : EM H' m) → EM (G' ⨂ H') (n +' m)
   _⌣ₖ_ x y = cup∙ _ _ x .fst y

   ⌣ₖ-0ₖ : (n m : ℕ) (x : EM G' n) → (x ⌣ₖ 0ₖ m) ≡ 0ₖ (n +' m)
   ⌣ₖ-0ₖ n m x = cup∙ n m x .snd

   0ₖ-⌣ₖ : (n m : ℕ) (x : EM H' m) → ((0ₖ n) ⌣ₖ x) ≡ 0ₖ (n +' m)
   0ₖ-⌣ₖ zero m = 0·₀ _
   0ₖ-⌣ₖ (suc zero) zero x = refl
   0ₖ-⌣ₖ (suc (suc n)) zero x = refl
   0ₖ-⌣ₖ (suc zero) (suc m) x = refl
   0ₖ-⌣ₖ (suc (suc n)) (suc m) x = refl

module LeftDistributivity {G' : AbGroup ℓ} {H' : AbGroup ℓ'} where
   private
     distrl1 : (n m : ℕ) → EM H' m → EM H' m
             → EM∙ G' n →∙ EM∙ (G' ⨂ H') (n +' m)
     fst (distrl1 n m x y) z = z ⌣ₖ (x +ₖ y)
     snd (distrl1 n m x y) = 0ₖ-⌣ₖ n m _

     distrl2 : (n m : ℕ) → EM H' m → EM H' m
             → EM∙ G' n →∙ EM∙ (G' ⨂ H') (n +' m)
     fst (distrl2 n m x y) z = (z ⌣ₖ x) +ₖ (z ⌣ₖ y)
     snd (distrl2 n m x y) =
       cong₂ _+ₖ_ (0ₖ-⌣ₖ n m x) (0ₖ-⌣ₖ n m y) ∙ rUnitₖ _ (0ₖ (n +' m))

   hLevLem : (n m : ℕ) → isOfHLevel (suc (suc m)) (EM∙ G' (suc n) →∙ EM∙ (G' ⨂ H') ((suc n) +' m))
   hLevLem n m =
     subst (isOfHLevel (suc (suc m)))
           (λ i → EM∙ G' (suc n) →∙ EM∙ (G' ⨂ H')
           ((cong suc (+-comm m n) ∙ sym (+'≡+ (suc n) m)) i)) (isOfHLevel↑∙ m n)

   mainDistrL : (n m : ℕ) (x y : EM H' (suc m))
     → distrl1 (suc n) (suc m) x y ≡ distrl2 (suc n) (suc m) x y
   mainDistrL n zero =
     wedgeConEM.fun H' H' 0 0
       (λ _ _ → hLevLem _ _ _ _)
       (λ x → →∙Homogeneous≡ (isHomogeneousEM _)
              (funExt λ z → l x z))
       (λ y → →∙Homogeneous≡ (isHomogeneousEM _)
              (funExt λ z → r y z ))
       λ i → →∙Homogeneous≡ (isHomogeneousEM (suc (suc (n + 0))))
                               (funExt (λ z → l≡r z i))
     where
     l : (x : EM H' 1) (z : _)
       → (distrl1 (suc n) 1 embase x .fst z) ≡ (distrl2 (suc n) 1 embase x .fst z)
     l x z = cong (z ⌣ₖ_) (lUnitₖ _ x)
            ∙∙ sym (lUnitₖ _ (z ⌣ₖ x))
            ∙∙ λ i → (⌣ₖ-0ₖ (suc n) (suc zero) z (~ i)) +ₖ (z ⌣ₖ x)

     r : (z : EM H' 1) (x : EM G' (suc n))
       → (distrl1 (suc n) 1 z embase .fst x) ≡ (distrl2 (suc n) 1 z embase .fst x)
     r y z = cong (z ⌣ₖ_) (rUnitₖ _ y)
            ∙∙ sym (rUnitₖ _ (z ⌣ₖ y))
            ∙∙ λ i → (z ⌣ₖ y) +ₖ (⌣ₖ-0ₖ (suc n) (suc zero) z (~ i))

     l≡r : (z : EM G' (suc n)) → l embase z ≡ r embase z
     l≡r z = sym (pathTypeMake _ _ (sym (⌣ₖ-0ₖ (suc n) (suc zero) z)))

   mainDistrL n (suc m) =
     elim2 (λ _ _ → isOfHLevelPath (4 + m) (hLevLem _ _) _ _)
           (wedgeConEM.fun H' H' (suc m) (suc m)
             (λ x y p q → isOfHLevelPlus {n = suc (suc m)} (suc m)
                             (hLevLem n (suc (suc m))
                               (distrl1 (suc n) (suc (suc m)) ∣ x ∣ ∣ y ∣)
                               (distrl2 (suc n) (suc (suc m)) ∣ x ∣ ∣ y ∣) p q))
             (λ x → →∙Homogeneous≡ (isHomogeneousEM _)
               (funExt (l x)))
             (λ x → →∙Homogeneous≡ (isHomogeneousEM _)
               (funExt (r x)))
             λ i → →∙Homogeneous≡ (isHomogeneousEM _)
                     (funExt (λ z → l≡r z i)))
    where
    l : (x : EM-raw H' (suc (suc m))) (z : EM G' (suc n))
     → (distrl1 (suc n) (suc (suc m)) (0ₖ _) ∣ x ∣ₕ .fst z)
      ≡ (distrl2 (suc n) (suc (suc m)) (0ₖ _) ∣ x ∣ₕ .fst z)
    l x z = cong (z ⌣ₖ_) (lUnitₖ (suc (suc m)) ∣ x ∣)
         ∙∙ sym (lUnitₖ _ (z ⌣ₖ ∣ x ∣))
         ∙∙ λ i → (⌣ₖ-0ₖ (suc n) (suc (suc m)) z (~ i)) +ₖ (z ⌣ₖ ∣ x ∣)

    r : (x : EM-raw H' (suc (suc m))) (z : EM G' (suc n))
      → (distrl1 (suc n) (suc (suc m)) ∣ x ∣ₕ (0ₖ _) .fst z)
       ≡ (distrl2 (suc n) (suc (suc m)) ∣ x ∣ₕ (0ₖ _) .fst z)
    r x z = cong (z ⌣ₖ_) (rUnitₖ (suc (suc m)) ∣ x ∣)
         ∙∙ sym (rUnitₖ _ (z ⌣ₖ ∣ x ∣))
         ∙∙ λ i → (z ⌣ₖ ∣ x ∣) +ₖ (⌣ₖ-0ₖ (suc n) (suc (suc m)) z (~ i))

    l≡r : (z : EM G' (suc n)) → l north z ≡ r north z
    l≡r z = sym (pathTypeMake _ _ (sym (⌣ₖ-0ₖ (suc n) (suc (suc m)) z)))

module RightDistributivity {G' : AbGroup ℓ} {H' : AbGroup ℓ'} where
   private
     G = fst G'
     H = fst H'

     strG = snd G'
     strH = snd H'

     0G = 0g strG
     0H = 0g strH

     _+G_ = _+Gr_ strG
     _+H_ = _+Gr_ strH

     -H_ = -Gr_ strH
     -G_ = -Gr_ strG

     distrr1 : (n m : ℕ) → EM G' n → EM G' n → EM∙ H' m →∙ EM∙ (G' ⨂ H') (n +' m)
     fst (distrr1 n m x y) z = (x +ₖ y) ⌣ₖ z
     snd (distrr1 n m x y) = ⌣ₖ-0ₖ n m _

     distrr2 : (n m : ℕ) → EM G' n → EM G' n → EM∙ H' m →∙ EM∙ (G' ⨂ H') (n +' m)
     fst (distrr2 n m x y) z = (x ⌣ₖ z) +ₖ (y ⌣ₖ z)
     snd (distrr2 n m x y) = cong₂ _+ₖ_ (⌣ₖ-0ₖ n m x) (⌣ₖ-0ₖ n m y) ∙ rUnitₖ _ (0ₖ (n +' m))

   mainDistrR : (n m : ℕ) (x y : EM G' (suc n))
     → distrr1 (suc n) (suc m) x y ≡ distrr2 (suc n) (suc m) x y
   mainDistrR zero m =
     wedgeConEM.fun G' G' 0 0
       (λ _ _ → isOfHLevel↑∙ 1 m _ _)
       (λ x → →∙Homogeneous≡ (isHomogeneousEM _)
                        (funExt (l x)))
       (λ x → →∙Homogeneous≡ (isHomogeneousEM _)
                        (funExt (r x)))
       λ i → →∙Homogeneous≡ (isHomogeneousEM _)
                        (funExt λ z → l≡r z i)
     where
     l : (x : _) (z : _) → _ ≡ _
     l x z =
          (λ i → (lUnitₖ 1 x i) ⌣ₖ z)
       ∙∙ sym (lUnitₖ _ (x ⌣ₖ z))
       ∙∙ λ i → 0ₖ-⌣ₖ _ _ z (~ i) +ₖ (x ⌣ₖ z)

     r : (x : _) (z : _) → _ ≡ _
     r x z =
          ((λ i → (rUnitₖ 1 x i) ⌣ₖ z))
       ∙∙ sym (rUnitₖ _ _)
       ∙∙ λ i → (_⌣ₖ_ {n = 1} {m = suc m} x z) +ₖ 0ₖ-⌣ₖ (suc zero) (suc m) z (~ i)

     l≡r : (z : _) → l embase z ≡ r embase z
     l≡r z = pathTypeMake _ _ _

   mainDistrR (suc n) m =
     elim2 (λ _ _ → isOfHLevelPath (4 + n)
                      (isOfHLevel↑∙ (2 + n) m) _ _)
           (wedgeConEM.fun _ _ _ _
             (λ x y → isOfHLevelPath ((2 + n) + (2 + n))
                       (transport (λ i → isOfHLevel (((λ i → (+-comm n 2 (~ i) + (2 + n)))
                                                         ∙ sym (+-assoc n 2 (2 + n))) (~ i))
                                  (EM∙ H' (suc m) →∙ EM∙ ((fst (AbGroupPath (G' ⨂ H') (H' ⨂ G'))) ⨂-comm (~ i))
                                  ((+'-comm (suc m) (suc (suc n))) i)))
                                  (isOfHLevelPlus n
                                    (LeftDistributivity.hLevLem m (suc (suc n))))) _ _)
             (λ x → →∙Homogeneous≡ (isHomogeneousEM _)
                        (funExt (l x)))
             (λ x → →∙Homogeneous≡ (isHomogeneousEM _)
                        (funExt (r x)))
             λ i → →∙Homogeneous≡ (isHomogeneousEM _)
                        (funExt λ z → r≡l z i))
     where
     l : (x : _) (z : _) → _ ≡ _
     l x z = (λ i → (lUnitₖ _ ∣ x ∣ i) ⌣ₖ z)
        ∙∙ sym (lUnitₖ _ (∣ x ∣ ⌣ₖ z))
        ∙∙ λ i → 0ₖ-⌣ₖ _ _ z (~ i) +ₖ (∣ x ∣ ⌣ₖ z)

     r : (x : _) (z : _) → _ ≡ _
     r x z = (λ i → (rUnitₖ _ ∣ x ∣ i) ⌣ₖ z)
           ∙∙ sym (rUnitₖ _ (∣ x ∣ ⌣ₖ z))
           ∙∙ λ i → (∣ x ∣ ⌣ₖ z) +ₖ 0ₖ-⌣ₖ _ _ z (~ i)

     r≡l : (z : _) → l north z ≡ r north z
     r≡l z = pathTypeMake _ _ _

-- TODO: Summarise distributivity proofs
-- TODO: Associativity and graded commutativity, following Cubical.ZCohomology.RingStructure
-- The following lemmas will be needed to make the types match up.

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

module Axiom.LEM where
  open import Basics
  open import Flat
  open import lib.Basics

  postulate LEM : {@♭ i : ULevel} (@♭ P : PropT i) → Dec (P holds)

max_stars_repo_name: glangmead/formalization

max_issues_repo_name: glangmead/formalization

max_forks_repo_name: glangmead/formalization


text:
module Generic.Test.Reify where

open import Generic.Core
open import Generic.Property.Reify
open import Generic.Test.Data.Fin
open import Generic.Test.Data.Vec

open import Data.Fin renaming (Fin to StdFin)
open import Data.Vec renaming (Vec to StdVec)

xs : Vec (Fin 4) 3
xs = fsuc (fsuc (fsuc fzero)) ∷ᵥ fzero ∷ᵥ fsuc fzero ∷ᵥ []ᵥ

xs′ : StdVec (StdFin 4) 3
xs′ = suc (suc (suc zero)) ∷ zero ∷ (suc zero) ∷ []

test : reflect xs ≡ xs′
test = refl

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
{-# OPTIONS --cubical --no-import-sorts --safe --experimental-lossy-unification #-}
module Cubical.ZCohomology.Groups.Prelims where

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.Properties
open import Cubical.ZCohomology.GroupStructure

open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Foundations.Path
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws

open import Cubical.HITs.Sn
open import Cubical.HITs.Susp
open import Cubical.HITs.S1

open import Cubical.Homotopy.Loopspace
open import Cubical.Data.Sigma
open import Cubical.Data.Int renaming (_+_ to _+ℤ_; +-comm to +ℤ-comm ; +-assoc to +ℤ-assoc)
open import Cubical.Data.Nat
open import Cubical.HITs.Truncation renaming (elim to trElim ; map to trMap ; rec to trRec)
open import Cubical.HITs.SetTruncation renaming (elim to sElim ; map to sMap ; rec to sRec)

infixr 33 _⋄_

_⋄_ : _
_⋄_ = compIso

-- We strengthen the elimination rule for Hⁿ(S¹). We show that we only need to work with elements ∣ f ∣₂ (definitionally) sending loop to some loop p
-- and sending base to 0
elimFunS¹ : (n : ℕ) → (p : typ (Ω (coHomK-ptd (suc n)))) → S¹ → coHomK (suc n)
elimFunS¹ n  p base = ∣ ptSn (suc n) ∣
elimFunS¹ n  p (loop i) = p i

coHomPointedElimS¹ : ∀ {ℓ} (n : ℕ) {B : coHom (suc n) S¹ → Type ℓ}
                 → ((x : coHom (suc n) S¹) → isProp (B x))
                 → ((p : typ (Ω (coHomK-ptd (suc n)))) → B ∣ elimFunS¹ n p ∣₂)
                 → (x : coHom (suc n) S¹) → B x
coHomPointedElimS¹ n {B = B} x p =
  coHomPointedElim n base x
    λ f Id → subst B
              (cong ∣_∣₂ (funExt (λ {base → sym Id ; (loop i) j → doubleCompPath-filler (sym Id) (cong f loop) Id (~ j) i})))
              (p (sym Id ∙∙ (cong f loop) ∙∙ Id))

coHomPointedElimS¹2 : ∀ {ℓ} (n : ℕ) {B : (x y : coHom (suc n) S¹) → Type ℓ}
                 → ((x y : coHom (suc n) S¹) → isProp (B x y))
                 → ((p q : typ (Ω (coHomK-ptd (suc n)))) → B ∣ elimFunS¹ n p ∣₂ ∣ elimFunS¹ n q ∣₂)
                 → (x y : coHom (suc n) S¹) → B x y
coHomPointedElimS¹2 n {B = B} x p =
  coHomPointedElim2 _ base x λ f g fId gId
    → subst2 B (cong ∣_∣₂ (funExt (λ {base → sym fId ; (loop i) j → doubleCompPath-filler (sym (fId)) (cong f loop) fId (~ j) i})))
                (cong ∣_∣₂ (funExt (λ {base → sym gId ; (loop i) j → doubleCompPath-filler (sym (gId)) (cong g loop) gId (~ j) i})))
                (p (sym fId ∙∙ cong f loop ∙∙ fId) (sym gId ∙∙ cong g loop ∙∙ gId))

-- We do the same thing for Sⁿ, n ≥ 2.
elimFunSⁿ : (n m : ℕ) (p : S₊ (suc m) → typ (Ω (coHomK-ptd (suc n))))
         → (S₊ (2 + m)) → coHomK (suc n)
elimFunSⁿ n m p north = ∣ ptSn (suc n) ∣
elimFunSⁿ n m p south = ∣ ptSn (suc n) ∣
elimFunSⁿ n m p (merid a i) = p a i

coHomPointedElimSⁿ : ∀ {ℓ} (n m : ℕ) {B : (x : coHom (suc n) (S₊ (2 + m))) → Type ℓ}
                 → ((x : coHom (suc n) (S₊ (2 + m))) → isProp (B x))
                 → ((p : _) → B ∣ elimFunSⁿ n m p ∣₂)
                 → (x : coHom (suc n) (S₊ (2 + m))) → B x
coHomPointedElimSⁿ n m {B = B} isprop ind =
  coHomPointedElim n north isprop
    λ f fId → subst B (cong ∣_∣₂ (funExt (λ {north → sym fId
                                           ; south → sym fId ∙' cong f (merid (ptSn (suc m)))
                                           ; (merid a i) j → hcomp (λ k → λ {(i = i0) → fId (~ j ∧ k)
                                                                             ; (i = i1) → compPath'-filler (sym fId)
                                                                                (cong f (merid (ptSn (suc m)))) k j
                                                                             ; (j = i1) → f (merid a i)})
                                                                    (hcomp (λ k → λ {(i = i0) → f north ;
                                                                                (i = i1) → f (merid (ptSn (suc m)) (j ∨ ~ k)) ;
                                                                                (j = i1) → f (merid a i)})
                                                                           (f (merid a i)))})))
                       (ind λ a → sym fId ∙∙ cong f (merid a) ∙ cong f (sym (merid (ptSn (suc m)))) ∙∙ fId)

0₀ = 0ₖ 0
0₁ = 0ₖ 1
0₂ = 0ₖ 2
0₃ = 0ₖ 3
0₄ = 0ₖ 4

S¹map : hLevelTrunc 3 S¹ → S¹
S¹map = trRec isGroupoidS¹ (idfun _)

S¹map-id : (x : hLevelTrunc 3 S¹) → Path (hLevelTrunc 3 S¹) ∣ S¹map x ∣ x
S¹map-id = trElim (λ _ → isOfHLevelPath 3 (isOfHLevelTrunc 3) _ _)
                  λ a → refl

-- We prove that (S¹ → ∥ S¹ ∥) ≃ S¹ × ℤ (Needed for H¹(S¹)). Note that the truncation doesn't really matter, since S¹ is a groupoid.
-- Given a map f : S¹ → S¹, the idea is to send this to (f(base) , winding (f(loop))). For this to be
-- well-typed, we need to translate f(loop) into an element in Ω(S¹,base).

S¹→S¹≡S¹×Int : Iso (S¹ → hLevelTrunc 3 S¹) (S¹ × Int)
Iso.fun S¹→S¹≡S¹×Int f = S¹map (f base)
                 , winding (basechange2⁻ (S¹map (f base)) λ i → S¹map (f (loop i)))
Iso.inv S¹→S¹≡S¹×Int (s , int) base = ∣ s ∣
Iso.inv S¹→S¹≡S¹×Int (s , int) (loop i) = ∣ basechange2 s (intLoop int) i ∣
Iso.rightInv S¹→S¹≡S¹×Int (s , int) = ΣPathP (refl , ((λ i → winding (basechange2-retr s (λ i → intLoop int i) i))
                                                      ∙ windingIntLoop int))
Iso.leftInv S¹→S¹≡S¹×Int f = funExt λ { base → S¹map-id (f base)
                                      ; (loop i) j → helper j i}
  where
  helper : PathP (λ i → S¹map-id (f base) i ≡ S¹map-id (f base) i)
                  (λ i → ∣ basechange2 (S¹map (f base))
                             (intLoop (winding (basechange2⁻ (S¹map (f base)) (λ i₁ → S¹map (f (loop i₁)))))) i ∣)
                  (cong f loop)
  helper i j =
    hcomp (λ k → λ { (i = i0) → cong ∣_∣ (basechange2 (S¹map (f base))
                                           (intLoop (winding (basechange2⁻ (S¹map (f base)) (λ i₁ → S¹map (f (loop i₁))))))) j
                    ; (i = i1) → S¹map-id (f (loop j)) k
                    ; (j = i0) → S¹map-id (f base) (i ∧ k)
                    ; (j = i1) → S¹map-id (f base) (i ∧ k)})
          (helper2 i j)
    where
    helper2 : Path (Path (hLevelTrunc 3 _) _ _)
                   (cong ∣_∣ (basechange2 (S¹map (f base))
                                         (intLoop
                                           (winding
                                             (basechange2⁻ (S¹map (f base))
                                                           (λ i₁ → S¹map (f (loop i₁))))))))
                   λ i → ∣ S¹map (f (loop i)) ∣
    helper2 i j =
         ∣ ((cong (basechange2 (S¹map (f base)))
                   (decodeEncode base (basechange2⁻ (S¹map (f base))
                                                    (λ i₁ → S¹map (f (loop i₁)))))
            ∙ basechange2-sect (S¹map (f base))
                               (λ i → S¹map (f (loop i)))) i) j ∣

{- Proof that (S¹ → K₁) ≃ K₁ × ℤ. Needed for H¹(T²) -}
S1→K₁≡S1×Int : Iso ((S₊ 1) → coHomK 1) (coHomK 1 × Int)
S1→K₁≡S1×Int = S¹→S¹≡S¹×Int ⋄ prodIso (invIso (truncIdempotentIso 3 (isGroupoidS¹))) idIso

module _ (key : Unit') where
  module P = lockedCohom key
  private
    _+K_ : {n : ℕ} → coHomK n → coHomK n → coHomK n
    _+K_ {n = n} = P.+K n

    -K_ : {n : ℕ} → coHomK n → coHomK n
    -K_ {n = n} = P.-K n

    _-K_ : {n : ℕ} → coHomK n → coHomK n → coHomK n
    _-K_ {n = n} = P.-Kbin n

  infixr 55 _+K_
  infixr 55 -K_
  infixr 56 _-K_

  {- Proof that S¹→K2 is isomorphic to K2×K1 (as types). Needed for H²(T²)  -}
  S1→K2≡K2×K1' : Iso (S₊ 1 → coHomK 2) (coHomK 2 × coHomK 1)
  Iso.fun S1→K2≡K2×K1' f = f base , ΩKn+1→Kn 1 (sym (P.rCancelK 2 (f base))
                                             ∙∙ cong (λ x → (f x) -K f base) loop
                                             ∙∙ P.rCancelK 2 (f base))
  Iso.inv S1→K2≡K2×K1' = invmap
    where
    invmap : (∥ Susp S¹ ∥ 4) × (∥ S¹ ∥ 3) → S¹ → ∥ Susp S¹ ∥ 4
    invmap (a , b) base = a +K 0₂
    invmap (a , b) (loop i) = a +K Kn→ΩKn+1 1 b i
  Iso.rightInv S1→K2≡K2×K1' (a , b) = ΣPathP ((P.rUnitK 2 a)
                                           , (cong (ΩKn+1→Kn 1) (doubleCompPath-elim' (sym (P.rCancelK 2 (a +K 0₂)))
                                             (λ i → (a +K Kn→ΩKn+1 1 b i) -K (a +K 0₂))
                                             (P.rCancelK 2 (a +K 0₂)))
                                          ∙∙ cong (ΩKn+1→Kn 1) (congHelper2 (Kn→ΩKn+1 1 b) (λ x → (a +K x) -K (a +K 0₂))
                                                               (funExt (λ x → sym (cancelHelper a x)))
                                                               (P.rCancelK 2 (a +K 0₂)))
                                          ∙∙ Iso.leftInv (Iso-Kn-ΩKn+1 1) b))

      module _ where
      cancelHelper : (a b : coHomK 2) → (a +K b) -K (a +K 0₂) ≡ b
      cancelHelper a b = cong (λ x → (a +K b) -K x) (P.rUnitK 2 a)
                       ∙ P.-cancelLK 2 a b

      congHelper2 : (p : 0₂ ≡ 0₂) (f : coHomK 2 → coHomK 2) (id : (λ x → x) ≡ f) → (q : (f 0₂) ≡ 0₂)
                  → (sym q) ∙ cong f p ∙ q ≡ p
      congHelper2 p f = J (λ f _ → (q : (f 0₂) ≡ 0₂) → (sym q) ∙ cong f p ∙ q ≡ p)
                         λ q → (cong (sym q ∙_) (isCommΩK 2 p _) ∙∙ assoc _ _ _ ∙∙ cong (_∙ p) (lCancel q))
                              ∙ sym (lUnit p)

      conghelper3 : (x : coHomK 2) (p : x ≡ x) (f : coHomK 2 → coHomK 2) (id : (λ x → x) ≡ f) (q : f x ≡ x)
                  → (sym q) ∙ cong f p ∙ q ≡ p
      conghelper3 x p f = J (λ f _ → (q : (f x) ≡ x) → (sym q) ∙ cong f p ∙ q ≡ p)
                            λ q → (cong (sym q ∙_) (isCommΩK-based 2 x p _) ∙∙ assoc _ _ _ ∙∙ cong (_∙ p) (lCancel q))
                                      ∙  sym (lUnit p)
  Iso.leftInv S1→K2≡K2×K1' a i base = P.rUnitK _ (a base) i
  Iso.leftInv S1→K2≡K2×K1' a i (loop j) = loop-helper i j
    where
    loop-helper : PathP (λ i → P.rUnitK _ (a base) i ≡ P.rUnitK _ (a base) i)
                     (cong (a base +K_) (Kn→ΩKn+1 1 (ΩKn+1→Kn 1 ((sym (P.rCancelK 2 (a base))
                           ∙∙ (λ i → a (loop i) -K (a (base)))
                           ∙∙ P.rCancelK 2 (a base))))))
                     (cong a loop)
    loop-helper i j =
      hcomp (λ k → λ { (i = i0) → (G (doubleCompPath-elim'
                                        (sym rP) (λ i₁ → a (loop i₁) -K a base) rP (~ k))) j
                      ; (i = i1) → cong a loop j
                      ; (j = i0) → P.rUnitK 2 (a base) i
                      ; (j = i1) → P.rUnitK 2 (a base) i})
             (loop-helper2 i j)

       where
       F : typ (Ω (coHomK-ptd 2)) → a base +K snd (coHomK-ptd 2) ≡ a base +K snd (coHomK-ptd 2)
       F = cong (_+K_ {n = 2} (a base))

       G : 0ₖ 2 ≡ 0ₖ 2 → a base +K snd (coHomK-ptd 2) ≡ a base +K snd (coHomK-ptd 2)
       G p = F (Kn→ΩKn+1 1 (ΩKn+1→Kn 1 p))

       rP : P.+K 2 (a base) (P.-K 2 (a base)) ≡ 0ₖ 2
       rP = P.rCancelK 2 (a base)

       lem : (x : coHomK 2) (p : x ≡ x) (q : 0₂ ≡ x)
           → Kn→ΩKn+1 1 (ΩKn+1→Kn 1 (q ∙ p ∙ sym q)) ≡ q ∙ p ∙ sym q
       lem x p q = Iso.rightInv (Iso-Kn-ΩKn+1 1) (q ∙ p ∙ sym q)

       subtr-lem : (a b : hLevelTrunc 4 (S₊ 2)) → a +K (b -K a) ≡ b
       subtr-lem a b = P.commK 2 a (b -K a) ∙ P.-+cancelK 2 b a

       subtr-lem-coher : PathP (λ i → subtr-lem (a base) (a base) i ≡ subtr-lem (a base) (a base) i)
                           (cong (a base +K_) (λ i₁ → a (loop i₁) -K a base))
                           λ i → a (loop i)
       subtr-lem-coher i j = subtr-lem (a base) (a (loop j)) i

       abstract
         helperFun2 : {A : Type₀} {0A a b : A} (main : 0A ≡ 0A) (start : b ≡ b) (p : a ≡ a) (q : a ≡ b) (r : b ≡ 0A) (Q : a ≡ 0A)
                      (R : PathP (λ i → Q i ≡ Q i) p main)
                      → start ≡ sym q ∙ p ∙ q
                      → isComm∙ (A , 0A)
                      → sym r ∙ start ∙ r ≡ main
         helperFun2 main start p q r Q R startId comm =
             sym r ∙ start ∙ r                                            ≡[ i ]⟨ sym r ∙ startId i ∙ r ⟩
             sym r ∙ (sym q ∙ p ∙ q) ∙ r                                  ≡[ i ]⟨ sym r ∙ assoc (sym q) (p ∙ q) r (~ i) ⟩
             sym r ∙ sym q ∙ (p ∙ q) ∙ r                                  ≡[ i ]⟨ sym r ∙ sym q ∙ assoc p q r (~ i) ⟩
             sym r ∙ sym q ∙ p ∙ q ∙ r                                    ≡[ i ]⟨ assoc (sym r) (rUnit (sym q) i) (p ∙ lUnit (q ∙ r) i) i ⟩
             (sym r ∙ sym q ∙ refl) ∙ p ∙ refl ∙ q ∙ r                    ≡[ i ]⟨ (sym r ∙ sym q ∙ λ j → Q (i ∧ j)) ∙ R i ∙ (λ j → Q ( i ∧ (~ j))) ∙ q ∙ r ⟩
             (sym r ∙ sym q ∙ Q) ∙ main ∙ sym Q ∙ q ∙ r                   ≡[ i ]⟨ (sym r ∙ sym q ∙ Q) ∙ main ∙ sym Q ∙ symDistr (sym r) (sym q) (~ i) ⟩
             (sym r ∙ sym q ∙ Q) ∙ main ∙ sym Q ∙ sym (sym r ∙ sym q)     ≡[ i ]⟨ (assoc (sym r) (sym q) Q i) ∙ main ∙ symDistr (sym r ∙ sym q) Q (~ i) ⟩
             ((sym r ∙ sym q) ∙ Q) ∙ main ∙ sym ((sym r ∙ sym q) ∙ Q)     ≡[ i ]⟨ ((sym r ∙ sym q) ∙ Q) ∙ comm main (sym ((sym r ∙ sym q) ∙ Q)) i ⟩
             ((sym r ∙ sym q) ∙ Q) ∙ sym ((sym r ∙ sym q) ∙ Q) ∙ main     ≡⟨ assoc ((sym r ∙ sym q) ∙ Q) (sym ((sym r ∙ sym q) ∙ Q)) main  ⟩
             (((sym r ∙ sym q) ∙ Q) ∙ sym ((sym r ∙ sym q) ∙ Q)) ∙ main   ≡[ i ]⟨ rCancel (((sym r ∙ sym q) ∙ Q)) i ∙ main ⟩
             refl ∙ main                                                  ≡⟨ sym (lUnit main) ⟩
             main ∎

         congFunct₃ : ∀ {A B : Type₀} {a b c d : A} (f : A → B) (p : a ≡ b) (q : b ≡ c) (r : c ≡ d)
                      → cong f (p ∙ q ∙ r) ≡ cong f p ∙ cong f q ∙ cong f r
         congFunct₃ f p q r = congFunct f p (q ∙ r) ∙ cong (cong f p ∙_) (congFunct f q r)

         lem₀ : G (sym rP ∙ (λ i₁ → a (loop i₁) -K a base) ∙ rP)
                 ≡ F (sym rP ∙ (λ i₁ → a (loop i₁) -K a base) ∙ rP)
         lem₀ = cong F (lem (a base -K (a base))
                               (λ i₁ → a (loop i₁) -K a base)
                               (sym (P.rCancelK 2 (a base))))

         lem₁ : G (sym rP ∙ (λ i₁ → a (loop i₁) -K a base) ∙ rP)
                ≡ sym (λ i₁ → a base +K P.rCancelK 2 (a base) i₁) ∙
                      cong (a base +K_) (λ i₁ → a (loop i₁) -K a base) ∙
                      (λ i₁ → a base +K P.rCancelK 2 (a base) i₁)
         lem₁ = lem₀ ∙ congFunct₃ (a base +K_) (sym rP)
                                                    (λ i₁ → a (loop i₁) -K a base)
                                                    rP

         loop-helper2 : PathP (λ i → P.rUnitK _ (a base) i ≡ P.rUnitK _ (a base) i)
                       (cong (a base +K_) (Kn→ΩKn+1 1 (ΩKn+1→Kn 1 ((sym (P.rCancelK 2 (a base))
                             ∙ (λ i → a (loop i) -K (a (base)))
                             ∙ P.rCancelK 2 (a base))))))
                       (cong a loop)
         loop-helper2 = compPathL→PathP (helperFun2 (cong a loop) _ _
                                                  (cong (a base +K_) (P.rCancelK 2 (a base))) _ _
                                                  subtr-lem-coher
                                                  lem₁
                                                  (isCommΩK-based 2 (a base)))

S1→K2≡K2×K1 : Iso (S₊ 1 → coHomK 2) (coHomK 2 × coHomK 1)
S1→K2≡K2×K1 = S1→K2≡K2×K1' unlock

max_stars_repo_name: L-TChen/cubical

max_issues_repo_name: L-TChen/cubical

max_forks_repo_name: L-TChen/cubical


text:
module Everything where

import Algebra.Structures.Field
import Algebra.Structures.Bundles.Field

import Algebra.Linear.Core

import Algebra.Linear.Space
import Algebra.Linear.Space.Hom
import Algebra.Linear.Space.Product
import Algebra.Linear.Space.FiniteDimensional
import Algebra.Linear.Space.FiniteDimensional.Hom
import Algebra.Linear.Space.FiniteDimensional.Product

import Algebra.Linear.Construct
import Algebra.Linear.Construct.Vector
import Algebra.Linear.Construct.Matrix

import Algebra.Linear.Morphism
import Algebra.Linear.Morphism.Definitions
import Algebra.Linear.Morphism.VectorSpace
import Algebra.Linear.Morphism.Bundles
import Algebra.Linear.Morphism.Bundles.VectorSpace

import Algebra.Linear.Structures
import Algebra.Linear.Structures.VectorSpace
import Algebra.Linear.Structures.FiniteDimensional
import Algebra.Linear.Structures.Bundles
import Algebra.Linear.Structures.Bundles.FiniteDimensional

max_stars_repo_name: felko/linear-algebra

max_issues_repo_name: felko/linear-algebra

max_forks_repo_name: felko/linear-algebra


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Pointwise lifting of relations to maybes
------------------------------------------------------------------------

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

module Data.Maybe.Relation.Binary.Pointwise where

open import Level
open import Data.Maybe.Base using (Maybe; just; nothing)
open import Function.Equivalence using (_⇔_; equivalence)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec

------------------------------------------------------------------------
-- Definition

data Pointwise
       {a b ℓ} {A : Set a} {B : Set b}
       (R : REL A B ℓ) : REL (Maybe A) (Maybe B) (a ⊔ b ⊔ ℓ) where
  just    : ∀ {x y} → R x y → Pointwise R (just x) (just y)
  nothing : Pointwise R nothing nothing

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

module _ {a b ℓ} {A : Set a} {B : Set b} {R : REL A B ℓ} where

  drop-just : ∀ {x y} → Pointwise R (just x) (just y) → R x y
  drop-just (just p) = p

  just-equivalence : ∀ {x y} → R x y ⇔ Pointwise R (just x) (just y)
  just-equivalence = equivalence just drop-just

------------------------------------------------------------------------
-- Relational properties

module _ {a r} {A : Set a} {R : Rel A r} where

  refl : Reflexive R → Reflexive (Pointwise R)
  refl R-refl {just _}  = just R-refl
  refl R-refl {nothing} = nothing

  reflexive : _≡_ ⇒ R → _≡_ ⇒ Pointwise R
  reflexive reflexive P.refl = refl (reflexive P.refl)

module _ {a b r₁ r₂} {A : Set a} {B : Set b}
         {R : REL A B r₁} {S : REL B A r₂} where

  sym : Sym R S → Sym (Pointwise R) (Pointwise S)
  sym R-sym (just p) = just (R-sym p)
  sym R-sym nothing  = nothing

module _ {a b c r₁ r₂ r₃} {A : Set a} {B : Set b} {C : Set c}
         {R : REL A B r₁} {S : REL B C r₂} {T : REL A C r₃} where

  trans : Trans R S T → Trans (Pointwise R) (Pointwise S) (Pointwise T)
  trans R-trans (just p) (just q) = just (R-trans p q)
  trans R-trans nothing  nothing  = nothing

module _ {a r} {A : Set a} {R : Rel A r} where

  dec : Decidable R → Decidable (Pointwise R)
  dec R-dec (just x) (just y) = Dec.map just-equivalence (R-dec x y)
  dec R-dec (just x) nothing  = no (λ ())
  dec R-dec nothing  (just y) = no (λ ())
  dec R-dec nothing  nothing  = yes nothing

  isEquivalence : IsEquivalence R → IsEquivalence (Pointwise R)
  isEquivalence R-isEquivalence = record
    { refl  = refl R.refl
    ; sym   = sym R.sym
    ; trans = trans R.trans
    } where module R = IsEquivalence R-isEquivalence

  isDecEquivalence : IsDecEquivalence R → IsDecEquivalence (Pointwise R)
  isDecEquivalence R-isDecEquivalence = record
    { isEquivalence = isEquivalence R.isEquivalence
    ; _≟_           = dec R._≟_
    } where module R = IsDecEquivalence R-isDecEquivalence

module _ {c ℓ} where

  setoid : Setoid c ℓ → Setoid c (c ⊔ ℓ)
  setoid S = record
    { isEquivalence = isEquivalence S.isEquivalence
    } where module S = Setoid S

  decSetoid : DecSetoid c ℓ → DecSetoid c (c ⊔ ℓ)
  decSetoid S = record
    { isDecEquivalence = isDecEquivalence S.isDecEquivalence
    } where module S = DecSetoid S


text:
module _ where

open import Agda.Builtin.Equality

postulate
  A : Set
  P : A → Set

data Flat (@♭ A : Set) : Set where
  con : (@♭ x : A) → Flat A

-- it should not be able to unify x and y,
-- because the equality is not @♭.
test4 : (@♭ x : A) (@♭ y : A) → (x ≡ y) → P x → P y
test4 x y refl p = {!!}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import Base

module Homotopy.Pointed where

open import Integers
open import Homotopy.Truncation
open import Homotopy.Connected

record pType (i : Level) : Set (suc i) where
  constructor ⋆[_,_]
  field
    ∣_∣ : Set i  -- \|
    ⋆ : ∣_∣  -- \*
open pType public

pType₀ : Set₁
pType₀ = pType zero

_→⋆_ : ∀ {i j} → (pType i → pType j → pType (max i j))
_→⋆_ A B = ⋆[ Σ (∣ A ∣ → ∣ B ∣) (λ f → f (⋆ A) ≡ ⋆ B), ((λ _ → ⋆ B) , refl) ]

τ⋆ : ∀ {i} → (ℕ₋₂ → pType i → pType i)
τ⋆ n ⋆[ X , x ] = ⋆[ τ n X , proj x ]

is-contr⋆ : ∀ {i} → (pType i → Set i)
is-contr⋆ ⋆[ X , x ] = is-contr X

is-connected⋆ : ∀ {i} → ℕ₋₂ → (pType i → Set i)
is-connected⋆ n ⋆[ X , x ] = is-connected n X

connected⋆-lt : ∀ {i} (k n : ℕ) (lt : k < S n) (X : pType i)
  → (is-connected⋆ ⟨ n ⟩ X → is-contr⋆ (τ⋆ ⟨ k ⟩ X))
connected⋆-lt .n n <n X p = p
connected⋆-lt k O (<S ()) X p
connected⋆-lt k (S n) (<S lt) X p =
  connected⋆-lt k n lt X (connected-S-is-connected ⟨ n ⟩ p)

_≃⋆_ : ∀ {i j} → (pType i → pType j → Set (max i j))
⋆[ X , x ] ≃⋆ ⋆[ Y , y ] = Σ (X ≃ Y) (λ f → π₁ f x ≡ y)

id-equiv⋆ : ∀ {i} (X : pType i) → X ≃⋆ X
id-equiv⋆ ⋆[ X , x ] = (id-equiv X , refl)

equiv-compose⋆ : ∀ {i j k} {A : pType i} {B : pType j} {C : pType k}
  → (A ≃⋆ B → B ≃⋆ C → A ≃⋆ C)
equiv-compose⋆ (f , pf) (g , pg) = (equiv-compose f g , (ap (π₁ g) pf ∘ pg))

pType-eq-raw : ∀ {i} {X Y : pType i} (p : ∣ X ∣ ≡ ∣ Y ∣)
  (q : transport (λ X → X) p (⋆ X) ≡ ⋆ Y) → X ≡ Y
pType-eq-raw {i} {⋆[ X , x ]} {⋆[ .X , .x ]} refl refl = refl

pType-eq : ∀ {i} {X Y : pType i} → (X ≃⋆ Y → X ≡ Y)
pType-eq (e , p) = pType-eq-raw (eq-to-path e) (trans-id-eq-to-path e _ ∘ p)

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


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

module Algebra.Construct.Free.Semilattice.Definition where

open import Prelude

infixr 5 _∷_
data 𝒦 (A : Type a) : Type a where
  []   : 𝒦 A
  _∷_  : A → 𝒦 A → 𝒦 A
  com   : ∀ x y xs → x ∷ y ∷ xs ≡ y ∷ x ∷ xs
  dup   : ∀ x xs → x ∷ x ∷ xs ≡ x ∷ xs
  trunc : isSet (𝒦 A)

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
{-# OPTIONS --without-K #-}
open import HoTT.Base
open import HoTT.Equivalence

module HoTT.Identity.Universe {i} {A B : 𝒰 i} where

-- Axiom 2.10.3 - univalence
postulate
  idtoeqv-equiv : isequiv (idtoeqv {A = A} {B = B})

=𝒰-equiv : (A == B) ≃ (A ≃ B)
=𝒰-equiv = idtoeqv , idtoeqv-equiv

module _ where
  open qinv (isequiv→qinv idtoeqv-equiv)
  abstract
    ua : A ≃ B → A == B
    ua = g
    =𝒰-η : ua ∘ idtoeqv ~ id
    =𝒰-η = η
    =𝒰-β : idtoeqv ∘ ua ~ id
    =𝒰-β = ε

_=𝒰_ = _≃_

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott


text:
module hott.types.int where

open import hott.functions
open import hott.core
import hott.types.nat as nat

open nat using (ℕ)

data ℤ : Type₀ where
  zero : ℤ
  +ve  : ℕ → ℤ
  -ve  : ℕ → ℤ

fromNat : ℕ → ℤ
fromNat nat.zero = zero
fromNat (nat.succ n) = +ve n

neg : ℤ → ℤ
neg zero = zero
neg (+ve n) = -ve n
neg (-ve n) = +ve n

suc : ℤ → ℤ
suc zero                 = +ve 0
suc (+ve x)              = +ve (nat.succ x)
suc (-ve 0)              = zero
suc (-ve (nat.succ x))   = -ve x

pred : ℤ → ℤ
pred zero                 = -ve 0
pred (-ve x)              = -ve (nat.succ x)
pred (+ve 0)              = zero
pred (+ve (nat.succ x))   = +ve x

suc∘pred~id : suc ∘ pred ~ id
suc∘pred~id zero               = refl
suc∘pred~id (+ve 0)            = refl
suc∘pred~id (+ve (nat.succ x)) = refl
suc∘pred~id (-ve x)            = refl

pred∘suc~id : pred ∘ suc ~ id
pred∘suc~id zero               = refl
pred∘suc~id (+ve x)            = refl
pred∘suc~id (-ve 0)            = refl
pred∘suc~id (-ve (nat.succ x)) = refl

max_stars_repo_name: piyush-kurur/hott

max_issues_repo_name: piyush-kurur/hott

max_forks_repo_name: piyush-kurur/hott


text:
------------------------------------------------------------------------
-- Second-order abstract syntax
--
-- Examples of the formalisation framework in use
------------------------------------------------------------------------

module Examples where

-- | Algebraic structures

-- Monoids
import Monoid.Signature
import Monoid.Syntax
import Monoid.Equality

-- Commutative monoids
import CommMonoid.Signature
import CommMonoid.Syntax
import CommMonoid.Equality

-- Groups
import Group.Signature
import Group.Syntax
import Group.Equality

-- Commutative groups
import CommGroup.Signature
import CommGroup.Syntax
import CommGroup.Equality

-- Group actions
import GroupAction.Signature
import GroupAction.Syntax
import GroupAction.Equality

-- Semirings
import Semiring.Signature
import Semiring.Syntax
import Semiring.Equality

-- Rings
import Ring.Signature
import Ring.Syntax
import Ring.Equality

-- Commutative rings
import CommRing.Signature
import CommRing.Syntax
import CommRing.Equality

-- | Logic

-- Propositional logic
import PropLog.Signature
import PropLog.Syntax
import PropLog.Equality

-- First-order logic (with example proofs)
import FOL.Signature
import FOL.Syntax
import FOL.Equality

-- | Computational calculi

-- Combinatory logic
import Combinatory.Signature
import Combinatory.Syntax
import Combinatory.Equality

-- Untyped λ-calculus
import UTLC.Signature
import UTLC.Syntax
import UTLC.Equality

-- Simply-typed λ-calculus (with operational semantics and environment model)
import STLC.Signature
import STLC.Syntax
import STLC.Equality
import STLC.Model

-- Typed λ-calculus with product and sum types, and naturals (with example derivation)
import TLC.Signature
import TLC.Syntax
import TLC.Equality

-- PCF
import PCF.Signature
import PCF.Syntax
import PCF.Equality

-- | Miscellaneous

-- Lenses
import Lens.Signature
import Lens.Syntax
import Lens.Equality

-- Inception algebras
import Inception.Signature
import Inception.Syntax
import Inception.Equality

-- Substitution algebras
import Sub.Signature
import Sub.Syntax
import Sub.Equality

-- Partial differentiation (with some example proofs)
import PDiff.Signature
import PDiff.Syntax
import PDiff.Equality

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


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

module Experiment.Zero where

open import Level using (_⊔_)

-- Empty type
data ⊥ : Set where

-- Unit type
record ⊤ : Set where
  constructor tt

-- Boolean
data Bool : Set where
  true false : Bool

-- Natural number
data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

-- Propositional Equality
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x

-- Sum type
data _⊎_ {a} {b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  inj₁ : A → A ⊎ B
  inj₂ : B → A ⊎ B

-- Dependent Product type
record Σ {a} {b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    fst : A
    snd : B fst

-- Induction
⊤-ind : ∀ {p} {P : ⊤ → Set p} → P tt → ∀ x → P x
⊤-ind P⊤ tt = P⊤

⊥-ind : ∀ {p} {P : ⊥ → Set p} → ∀ x → P x
⊥-ind ()

Bool-ind : ∀ {p} {P : Bool → Set p} → P true → P false → ∀ x → P x
Bool-ind t e true  = t
Bool-ind t e false = e

ℕ-ind : ∀ {p} {P : ℕ → Set p} → P zero → (∀ m → P m → P (suc m)) → ∀ n → P n
ℕ-ind P0 Ps zero    = P0
ℕ-ind P0 Ps (suc n) = Ps n (ℕ-ind P0 Ps n)

≡-ind : ∀ {a p} {A : Set a}
        (P : (x y : A) → x ≡ y → Set p) →
        (∀ x → P x x refl) →
        ∀ x y (eq : x ≡ y) → P x y eq
≡-ind P Pr x .x refl = Pr x

⊎-ind : ∀ {a b p} {A : Set a} {B : Set b} {P : A ⊎ B → Set p} →
        (∀ x → P (inj₁ x)) → (∀ y → P (inj₂ y)) → ∀ s → P s
⊎-ind i1 i2 (inj₁ x) = i1 x
⊎-ind i1 i2 (inj₂ y) = i2 y

Σ-ind : ∀ {a b p} {A : Set a} {B : A → Set b} {P : Σ A B → Set p} →
        (∀ x y → P (x , y)) → ∀ p → P p
Σ-ind f (x , y) = f x y


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

module Dodo.Binary.Intersection where

-- Stdlib imports
open import Level using (Level; _⊔_)
open import Data.Product as P
open import Data.Product using (_×_; _,_; swap; proj₁; proj₂)
open import Relation.Binary using (REL)
-- Local imports
open import Dodo.Binary.Equality

-- # Definitions

infixl 30 _∩₂_

_∩₂_ : {a b ℓ₁ ℓ₂ : Level} {A : Set a} {B : Set b}
  → REL A B ℓ₁
  → REL A B ℓ₂
  → REL A B (ℓ₁ ⊔ ℓ₂)
_∩₂_ P Q x y = P x y × Q x y

-- # Properties

module _ {a b ℓ : Level} {A : Set a} {B : Set b} {R : REL A B ℓ} where

  ∩₂-idem : (R ∩₂ R) ⇔₂ R
  ∩₂-idem = ⇔: ⊆-proof ⊇-proof
    where
    ⊆-proof : (R ∩₂ R) ⊆₂' R
    ⊆-proof _ _ = proj₁
    ⊇-proof : R ⊆₂' (R ∩₂ R)
    ⊇-proof _ _ Rxy = (Rxy , Rxy)

module _ {a b ℓ₁ ℓ₂ : Level} {A : Set a} {B : Set b}
  {P : REL A B ℓ₁} {Q : REL A B ℓ₂} where

  ∩₂-comm : (P ∩₂ Q) ⇔₂ (Q ∩₂ P)
  ∩₂-comm = ⇔: (λ _ _ → swap) (λ _ _ → swap)

module _ {a b ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a} {B : Set b}
  {P : REL A B ℓ₁} {Q : REL A B ℓ₂} {R : REL A B ℓ₃} where

  ∩₂-assoc : P ∩₂ (Q ∩₂ R) ⇔₂ (P ∩₂ Q) ∩₂ R
  ∩₂-assoc = ⇔: ⊆-proof ⊇-proof
    where
    ⊆-proof : P ∩₂ (Q ∩₂ R) ⊆₂' (P ∩₂ Q) ∩₂ R
    ⊆-proof _ _ (Pxy , (Qxy , Rxy)) = ((Pxy , Qxy) , Rxy)
    ⊇-proof : (P ∩₂ Q) ∩₂ R ⊆₂' P ∩₂ (Q ∩₂ R)
    ⊇-proof _ _ ((Pxy , Qxy) , Rxy) = (Pxy , (Qxy , Rxy))

-- # Operations

-- ## Operations: ⊆₂

module _ {a b ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a} {B : Set b}
    {P : REL A B ℓ₁} {Q : REL A B ℓ₂} {R : REL A B ℓ₃} where

  ∩₂-combine-⊆₂ : P ⊆₂ Q → P ⊆₂ R → P ⊆₂ (Q ∩₂ R)
  ∩₂-combine-⊆₂ (⊆: P⊆Q) (⊆: P⊆R) = ⊆: (λ x y Pxy → (P⊆Q x y Pxy , P⊆R x y Pxy))

module _ {a b ℓ₁ ℓ₂ : Level} {A : Set a} {B : Set b}
    {P : REL A B ℓ₁} {Q : REL A B ℓ₂} where

  ∩₂-introˡ-⊆₂ : (P ∩₂ Q) ⊆₂ Q
  ∩₂-introˡ-⊆₂ = ⊆: λ _ _ → proj₂

  ∩₂-introʳ-⊆₂ : (P ∩₂ Q) ⊆₂ P
  ∩₂-introʳ-⊆₂ = ⊆: λ _ _ → proj₁

module _ {a b ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a} {B : Set b}
    {P : REL A B ℓ₁} {Q : REL A B ℓ₂} {R : REL A B ℓ₃} where

  ∩₂-elimˡ-⊆₂ : P ⊆₂ (Q ∩₂ R) → P ⊆₂ R
  ∩₂-elimˡ-⊆₂ (⊆: P⊆[Q∩R]) = ⊆: (λ x y Pxy → proj₂ (P⊆[Q∩R] x y Pxy))

  ∩₂-elimʳ-⊆₂ : P ⊆₂ (Q ∩₂ R) → P ⊆₂ Q
  ∩₂-elimʳ-⊆₂ (⊆: P⊆[Q∩R]) = ⊆: (λ x y Pxy → proj₁ (P⊆[Q∩R] x y Pxy))

module _ {a b ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a} {B : Set b}
    {P : REL A B ℓ₁} {Q : REL A B ℓ₂} {R : REL A B ℓ₃} where

  ∩₂-substˡ-⊆₂ : P ⊆₂ Q → (P ∩₂ R) ⊆₂ (Q ∩₂ R)
  ∩₂-substˡ-⊆₂ (⊆: P⊆Q) = ⊆: (λ x y → P.map₁ (P⊆Q x y))

  ∩₂-substʳ-⊆₂ : P ⊆₂ Q → (R ∩₂ P) ⊆₂ (R ∩₂ Q)
  ∩₂-substʳ-⊆₂ (⊆: P⊆Q) = ⊆: (λ x y → P.map₂ (P⊆Q x y))

-- ## Operations: ⇔₂

module _ {a b ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a} {B : Set b}
    {P : REL A B ℓ₁} {Q : REL A B ℓ₂} {R : REL A B ℓ₃} where

  ∩₂-substˡ : P ⇔₂ Q → (P ∩₂ R) ⇔₂ (Q ∩₂ R)
  ∩₂-substˡ = ⇔₂-compose ∩₂-substˡ-⊆₂ ∩₂-substˡ-⊆₂

  ∩₂-substʳ : P ⇔₂ Q → (R ∩₂ P) ⇔₂ (R ∩₂ Q)
  ∩₂-substʳ = ⇔₂-compose ∩₂-substʳ-⊆₂ ∩₂-substʳ-⊆₂

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


text:
-- Andreas, 2015-12-10, issue reported by Andrea Vezzosi

open import Common.Equality
open import Common.Bool

id : Bool → Bool
id true  = true
id false = false

is-id : ∀ x → x ≡ id x
is-id true  = refl
is-id false = refl

postulate
  P : Bool → Set
  b : Bool
  p : P (id b)

proof : P b
proof rewrite is-id b = p


text:
module Selective where

open import Prelude.Equality
open import Agda.Builtin.TrustMe

-----------------------------------------------------------------
-- id : ∀ {a} {A : Set a} → A → A
-- id x = x

id : ∀ {A : Set} → A → A
id x = x
{-# INLINE id #-}

infixl -10 id
syntax id {A = A} x = x ofType A

const : ∀ {a b} {A : Set a} {B : Set b} → A → B → A
const x _ = x
{-# INLINE const #-}

flip : ∀ {a b c} {A : Set a} {B : Set b} {C : A → B → Set c} →
      (∀ x y → C x y) → ∀ y x → C x y
flip f x y = f y x
{-# INLINE flip #-}

infixr 9 _∘_
_∘_ : ∀ {a b c} {A : Set a} {B : A → Set b} {C : ∀ x → B x → Set c}
        (f : ∀ {x} (y : B x) → C x y) (g : ∀ x → B x) →
        ∀ x → C x (g x)
(f ∘ g) x = f (g x)
{-# INLINE _∘_ #-}

infixr -20 _$_
_$_ : ∀ {a b} {A : Set a} {B : A → Set b} → (∀ x → B x) → ∀ x → B x
f $ x = f x

------------------------------------------------------------------
data Either (A : Set) (B : Set) : Set where
  left  : A → Either A B
  right : B → Either A B

either : ∀ {A : Set} {B : Set} {C : Set} →
           (A → C) → (B → C) → Either A B → C
either f g (left  x) = f x
either f g (right x) = g x

data Pair (a b : Set) : Set where
  _×_ : a → b → Pair a b
------------------------------------------------------------------
record Functor (F : Set → Set) : Set₁ where
  infixl 5 _<$>_
  field
    fmap : ∀ {A B} → (A → B) → F A → F B

    -- Functor laws
    fmap-id      : ∀ {A} {x : F A} → fmap id x ≡ id x
    fmap-compose : ∀ {A B C} {f : A → B} {g : B → C} {x : F A} →
                   fmap (g ∘ f) x ≡ (fmap g ∘ fmap f) x

  _<$>_ = fmap

open Functor {{...}} public

instance
  FunctorFunction : {X : Set} → Functor (λ Y → (X → Y))
  fmap {{FunctorFunction}} f g = λ x → (f ∘ g) x
  fmap-id {{FunctorFunction}} = refl
  fmap-compose {{FunctorFunction}} = refl

record Applicative (F : Set → Set) : Set₁ where
  infixl 5 _<*>_ _<*_ _*>_
  field
    overlap {{functor}} : Functor F
    pure  : ∀ {A} → A → F A
    _<*>_ : ∀ {A B} → F (A → B) → F A → F B

    -- Applicative laws
    ap-identity     : ∀ {A B} {f : F (A → B)} → (pure id <*> f) ≡ f
    ap-homomorphism : ∀ {A B} {x : A} {f : A → B} →
                      pure f <*> pure x ≡ pure (f x)
    ap-interchange  : ∀ {A B} {x : A} {f : F (A → B)} →
                      f <*> pure x ≡ pure (_$ x) <*> f
    -- ap-composition  : ∀ {A B C} {x : F A} {f : F (A → B)} {g : F (B → C)} →
    --                   (pure (_∘_) <*> g <*> f <*> x) ≡ (g <*> (f <*> x))
    fmap-pure-ap : ∀ {A B} {x : F A} {f : A → B} →
                   f <$> x ≡ pure f <*> x

  _<*_ : ∀ {A B} → F A → F B → F A
  a <* b = ⦇ const a b ⦈

  _*>_ : ∀ {A B} → F A → F B → F B
  a *> b = ⦇ (const id) a b ⦈

open Applicative {{...}} public

instance
  ApplicativeFunction : {X : Set} → Applicative (λ Y → (X → Y))
  pure {{ApplicativeFunction}} f = const f
  _<*>_ {{ApplicativeFunction}} f g = λ x → f x (g x)

  -- Applicative laws
  ap-identity {{ApplicativeFunction}} = refl
  ap-homomorphism {{ApplicativeFunction}} = refl
  ap-interchange {{ApplicativeFunction}} = refl
  fmap-pure-ap {{ApplicativeFunction}} {_} {_} {x} {f} = primTrustMe
    -- f <$> x -- f <$> x
    --   ≡⟨ {!!} ⟩
    -- pure f <*> x
    --   ∎

record Bifunctor (P : Set → Set → Set)  : Set₁ where
  field
    bimap : ∀ {A B C D} → (A → B) → (C → D) → P A C → P B D

    first : ∀ {A B C} → (A -> B) -> P A C -> P B C

    second : ∀ {A B C} → (B -> C) -> P A B -> P A C

open Bifunctor {{...}} public

instance
  BifunctorEither : Bifunctor Either
  bimap {{BifunctorEither}} f _ (left a)  = left (f a)
  bimap {{BifunctorEither}} _ g (right b) = right (g b)

  first {{BifunctorEither}} f = bimap f id

  second {{BifunctorEither}} = bimap id

record Selective (F : Set → Set) : Set₁ where
  field
    overlap {{applicative}} : Applicative F
    handle : ∀ {A B} → F (Either A B) → F (A → B) → F B

    -- Laws:
    -- (F1) Apply a pure function to the result:
    f1 : ∀ {A B C} {f : B → C} {x : F (Either A B)} {y : F (A → B)} →
         (f <$> (handle x y)) ≡ handle (second f <$> x) ((f ∘_) <$> y)

    -- (F2) Apply a pure function to the left (error) branch:
    f2 : ∀ {A B C} {f : A -> C} {x : F (Either A B)} {y : F (C → B)} →
         handle (first f <$> x) y ≡ handle x ((_∘ f) <$> y)

    -- (F3) Apply a pure function to the handler:
    f3 : ∀ {A B C} {f : C → A → B} {x : F (Either A B)} {y : F C} →
         (handle x (f <$> y)) ≡ handle (first (flip f) <$> x) (flip (_$_) <$> y)

    -- (P1) Apply a pure handler:
    p1 : ∀ {A B} {x : F (Either A B)} {y : A → B} →
         handle x (pure y) ≡ (either y id <$> x)

    -- (P2) Handle a pure error:
    p2 : ∀ {A B} {x : A} {y : F (A → B)} →
         handle (pure (left x)) y ≡ ((_$ x) <$> y)

    -- -- (A1) Associativity
    -- a1 : ∀ {A B C} {x : F (Either A B)}
    --                {y : F (Either C (A → B))}
    --                {z : F (C → A → B)} →
    --      handle x (handle y z) ≡
    --      handle (handle ((λ x → right x) <$> x) (λ a → bimap (λ x → (x × a)) (_$ a) y))

-- A1: handle x (handle y z) = handle (handle (f <$> x) (g <$> y)) (h <$> z)
--       where f x = Right <$> x
--             g y = \a -> bimap (,a) ($a) y
--             h z = uncurry z
-- a1 :: Selective f => f (Either a b) -> f (Either c (a -> b)) -> f (c -> a -> b) -> f b
-- a1 x y z = handle x (handle y z) === handle (handle (f <$> x) (g <$> y)) (h <$> z)
--   where
--     f x = Right <$> x
--     g y = \a -> bimap (,a) ($a) y
--     h z = uncurry z

open Selective {{...}} public

-- | 'Selective' is more powerful than 'Applicative': we can recover the
-- application operator '<*>'. In particular, the following 'Applicative' laws
-- hold when expressed using 'apS':
--
-- * Identity     : pure id <*> v = v
-- * Homomorphism : pure f <*> pure x = pure (f x)
-- * Interchange  : u <*> pure y = pure ($y) <*> u
-- * Composition  : (.) <$> u <*> v <*> w = u <*> (v <*> w)
apS : ∀ {A B : Set} {F : Set → Set} {{_ : Selective F}} →
      F (A → B) → F A → F B
apS f x = handle (left <$> f) (flip (_$_) <$> x)
---------------------------------------------------------------------

max_stars_repo_name: tuura/selective-theory-agda

max_issues_repo_name: tuura/selective-theory-agda

max_forks_repo_name: tuura/selective-theory-agda


text:
module SizedIO.ConsoleObject where

open import Size

open import SizedIO.Console
open import SizedIO.Object
open import SizedIO.IOObject

-- A console object is an IO object for the IO interface  of console
ConsoleObject : (i : Size)  → (iface : Interface) → Set
ConsoleObject i iface = IOObject consoleI iface i

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
module Acc where

data Rel(A : Set) : Set1 where
  rel : (A -> A -> Set) -> Rel A

_is_than_ : {A : Set} -> A -> Rel A -> A -> Set
x is rel f than y = f x y

data Acc {A : Set} (less : Rel A) (x : A)  : Set where
  acc : ((y : A) -> x is less than y -> Acc less y) -> Acc less x

data WO {A : Set} (less : Rel A) : Set where
  wo : ((x : A) -> Acc less x) -> WO less

data False : Set where
data True : Set where
  tt : True

data Nat : Set where
  Z : Nat
  S : Nat -> Nat

data ∏ {A : Set} (f : A -> Set) : Set where
  ∏I : ((z : A) -> f z) -> ∏ f

data Ord : Set  where
  z : Ord
  lim : (Nat -> Ord) -> Ord

zp  : Ord -> Ord
zp z = z
zp (lim f) = lim (\x -> zp (f x))

_<_ : Ord -> Ord -> Set
z < _ = True
lim _ < z = False
lim f < lim g = ∏ \(n : Nat) -> f n < g n

ltNat : Nat -> Nat -> Set
ltNat Z Z = False
ltNat Z (S n) = True
ltNat (S m) (S n) = ltNat m n
ltNat (S m) Z = False

ltNatRel : Rel Nat
ltNatRel = rel ltNat

postulate woltNat : WO ltNatRel

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --cumulativity #-}

open import Agda.Builtin.Equality

mutual
  X : Set
  X = _

  Y : Set₁
  Y = Set

  test : _≡_ {A = Set₁} X Y
  test = refl


text:
------------------------------------------------------------------------
-- Potentially cyclic precedence graphs
------------------------------------------------------------------------

module Mixfix.Cyclic.PrecedenceGraph where

open import Data.Fin using (Fin)
open import Data.Nat using (ℕ)
open import Data.Vec as Vec using (allFin)
open import Data.List using (List)
open import Data.Product using (∃)

open import Mixfix.Fixity
open import Mixfix.Operator
open import Mixfix.Expr hiding (module PrecedenceGraph)

-- Precedence graphs are represented by the number of precedence
-- levels, plus functions mapping node identifiers (precedences) to
-- node contents and successor precedences.

record PrecedenceGraph : Set where
  field
    -- The number of precedence levels.
    levels : ℕ

  -- Precedence levels.
  Precedence : Set
  Precedence = Fin levels

  field
    -- The precedence level's operators.
    ops : Precedence → (fix : Fixity) → List (∃ (Operator fix))

    -- The immediate successors of the precedence level.
    ↑ : Precedence → List Precedence

  -- All precedence levels.
  anyPrecedence : List Precedence
  anyPrecedence = Vec.toList (allFin levels)

-- Potentially cyclic precedence graphs.

cyclic : PrecedenceGraphInterface
cyclic = record
  { PrecedenceGraph = PrecedenceGraph
  ; Precedence      = PrecedenceGraph.Precedence
  ; ops             = PrecedenceGraph.ops
  ; ↑               = PrecedenceGraph.↑
  ; anyPrecedence   = PrecedenceGraph.anyPrecedence
  }

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators