text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Propertiers of any for containers
------------------------------------------------------------------------

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

module Data.Container.Relation.Unary.Any.Properties where

open import Level
open import Algebra
open import Data.Product as Prod using (∃; _×_; ∃₂; _,_; proj₂)
open import Data.Product.Function.NonDependent.Propositional using (_×-cong_)
import Data.Product.Function.Dependent.Propositional as Σ
open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_])
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence using (equivalence)
open import Function.HalfAdjointEquivalence using (_≃_; ↔→≃)
open import Function.Inverse as Inv using (_↔_; inverse; module Inverse)
open import Function.Related as Related using (Related; SK-sym)
open import Function.Related.TypeIsomorphisms
open import Relation.Unary using (Pred ; _∪_ ; _∩_)
open import Relation.Binary using (REL)
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; _≗_; refl)

open Related.EquationalReasoning hiding (_≡⟨_⟩_)
private
  module ×⊎ {k ℓ} = CommutativeSemiring (×-⊎-commutativeSemiring k ℓ)

open import Data.Container.Core
import Data.Container.Combinator as C
open import Data.Container.Combinator.Properties
open import Data.Container.Related
open import Data.Container.Relation.Unary.Any as Any using (◇; any)
open import Data.Container.Membership

module _ {s p} (C : Container s p) {x} {X : Set x} {ℓ} {P : Pred X ℓ} where

-- ◇ can be unwrapped to reveal the Σ type

  ↔Σ : ∀ {xs : ⟦ C ⟧ X} → ◇ C P xs ↔ ∃ λ p → P (proj₂ xs p)
  ↔Σ {xs} = inverse ◇.proof any (λ _ → P.refl) (λ _ → P.refl)

-- ◇ can be expressed using _∈_.

  ↔∈ : ∀ {xs : ⟦ C ⟧ X} → ◇ C P xs ↔ (∃ λ x → x ∈ xs × P x)
  ↔∈ {xs} = inverse to from (λ _ → P.refl) (to∘from) where

    to : ◇ C P xs → ∃ λ x → x ∈ xs × P x
    to (any (p , Px)) = (proj₂ xs p , (any (p , P.refl)) , Px)

    from : (∃ λ x → x ∈ xs × P x) → ◇ C P xs
    from (.(proj₂ xs p) , (any (p , refl)) , Px) = any (p , Px)

    to∘from : to ∘ from ≗ id
    to∘from (.(proj₂ xs p) , any (p , refl) , Px) = P.refl

module _ {s p} {C : Container s p} {x} {X : Set x}
         {ℓ₁ ℓ₂} {P₁ : Pred X ℓ₁} {P₂ : Pred X ℓ₂} where
-- ◇ is a congruence for bag and set equality and related preorders.

  cong : ∀ {k} {xs₁ xs₂ : ⟦ C ⟧ X} →
         (∀ x → Related k (P₁ x) (P₂ x)) → xs₁ ∼[ k ] xs₂ →
         Related k (◇ C P₁ xs₁) (◇ C P₂ xs₂)
  cong {k} {xs₁} {xs₂} P₁↔P₂ xs₁≈xs₂ =
    ◇ C P₁ xs₁               ↔⟨ ↔∈ C ⟩
    (∃ λ x → x ∈ xs₁ × P₁ x) ∼⟨ Σ.cong Inv.id (xs₁≈xs₂ ×-cong P₁↔P₂ _) ⟩
    (∃ λ x → x ∈ xs₂ × P₂ x) ↔⟨ SK-sym (↔∈ C) ⟩
    ◇ C P₂ xs₂               ∎

-- Nested occurrences of ◇ can sometimes be swapped.

module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s₂ p₂}
         {x y} {X : Set x} {Y : Set y} {r} {P : REL X Y r} where

  swap : {xs : ⟦ C₁ ⟧ X} {ys : ⟦ C₂ ⟧ Y} →
         let ◈ : ∀ {s p} {C : Container s p} {x} {X : Set x} {ℓ} → ⟦ C ⟧ X → Pred X ℓ → Set (p ⊔ ℓ)
             ◈ = λ {_} {_} → flip (◇ _) in
         ◈ xs (◈ ys ∘ P) ↔ ◈ ys (◈ xs ∘ flip P)
  swap {xs} {ys} =
    ◇ _ (λ x → ◇ _ (P x) ys) xs                ↔⟨ ↔∈ C₁ ⟩
    (∃ λ x → x ∈ xs × ◇ _ (P x) ys)            ↔⟨ Σ.cong Inv.id $ Σ.cong Inv.id $ ↔∈ C₂ ⟩
    (∃ λ x → x ∈ xs × ∃ λ y → y ∈ ys × P x y)  ↔⟨ Σ.cong Inv.id (λ {x} → ∃∃↔∃∃ (λ _ y → y ∈ ys × P x y)) ⟩
    (∃₂ λ x y → x ∈ xs × y ∈ ys × P x y)       ↔⟨ ∃∃↔∃∃ (λ x y → x ∈ xs × y ∈ ys × P x y) ⟩
    (∃₂ λ y x → x ∈ xs × y ∈ ys × P x y)       ↔⟨ Σ.cong Inv.id (λ {y} → Σ.cong Inv.id (λ {x} →
      (x ∈ xs × y ∈ ys × P x y)                     ↔⟨ SK-sym Σ-assoc ⟩
      ((x ∈ xs × y ∈ ys) × P x y)                   ↔⟨ Σ.cong (×-comm _ _) Inv.id ⟩
      ((y ∈ ys × x ∈ xs) × P x y)                   ↔⟨ Σ-assoc ⟩
      (y ∈ ys × x ∈ xs × P x y)                     ∎)) ⟩
    (∃₂ λ y x → y ∈ ys × x ∈ xs × P x y)       ↔⟨ Σ.cong Inv.id (λ {y} → ∃∃↔∃∃ {B = y ∈ ys} (λ x _ → x ∈ xs × P x y)) ⟩
    (∃ λ y → y ∈ ys × ∃ λ x → x ∈ xs × P x y)  ↔⟨ Σ.cong Inv.id (Σ.cong Inv.id (SK-sym (↔∈ C₁))) ⟩
    (∃ λ y → y ∈ ys × ◇ _ (flip P y) xs)       ↔⟨ SK-sym (↔∈ C₂) ⟩
    ◇ _ (λ y → ◇ _ (flip P y) xs) ys           ∎

-- Nested occurrences of ◇ can sometimes be flattened.

module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s₂ p₂}
         {x} {X : Set x} {ℓ} (P : Pred X ℓ) where

  flatten : ∀ (xss : ⟦ C₁ ⟧ (⟦ C₂ ⟧ X)) →
            ◇ C₁ (◇ C₂ P) xss ↔
            ◇ (C₁ C.∘ C₂) P (Inverse.from (Composition.correct C₁ C₂) ⟨$⟩ xss)
  flatten xss = inverse t f (λ _ → P.refl) (λ _ → P.refl) where

    ◇₁ = ◇ C₁; ◇₂ = ◇ C₂; ◇₁₂ = ◇ (C₁ C.∘ C₂)
    open Inverse

    t : ◇₁ (◇₂ P) xss → ◇₁₂ P (from (Composition.correct C₁ C₂) ⟨$⟩ xss)
    t (any (p₁ , (any (p₂ , p)))) = any (any (p₁ , p₂) , p)

    f : ◇₁₂ P (from (Composition.correct C₁ C₂) ⟨$⟩ xss) → ◇₁ (◇₂ P) xss
    f (any (any (p₁ , p₂) , p)) = any (p₁ , any (p₂ , p))

-- Sums commute with ◇ (for a fixed instance of a given container).

module _ {s p} {C : Container s p} {x} {X : Set x}
         {ℓ ℓ′} {P : Pred X ℓ} {Q : Pred X ℓ′} where

  ◇⊎↔⊎◇ : ∀ {xs : ⟦ C ⟧ X} → ◇ C (P ∪ Q) xs ↔ (◇ C P xs ⊎ ◇ C Q xs)
  ◇⊎↔⊎◇ {xs} = inverse to from from∘to to∘from
    where
    to : ◇ C (λ x → P x ⊎ Q x) xs → ◇ C P xs ⊎ ◇ C Q xs
    to (any (pos , inj₁ p)) = inj₁ (any (pos , p))
    to (any (pos , inj₂ q)) = inj₂ (any (pos , q))

    from : ◇ C P xs ⊎ ◇ C Q xs → ◇ C (λ x → P x ⊎ Q x) xs
    from = [ Any.map₂ inj₁ , Any.map₂ inj₂ ]

    from∘to : from ∘ to ≗ id
    from∘to (any (pos , inj₁ p)) = P.refl
    from∘to (any (pos , inj₂ q)) = P.refl

    to∘from : to ∘ from ≗ id
    to∘from = [ (λ _ → P.refl) , (λ _ → P.refl) ]

-- Products "commute" with ◇.

module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s₂ p₂}
         {x y} {X : Set x} {Y : Set y} {ℓ ℓ′} {P : Pred X ℓ} {Q : Pred Y ℓ′} where

  ×◇↔◇◇× : ∀ {xs : ⟦ C₁ ⟧ X} {ys : ⟦ C₂ ⟧ Y} →
           ◇ C₁ (λ x → ◇ C₂ (λ y → P x × Q y) ys) xs ↔ (◇ C₁ P xs × ◇ C₂ Q ys)
  ×◇↔◇◇× {xs} {ys} = inverse to from (λ _ → P.refl) (λ _ → P.refl)
    where
    ◇₁ = ◇ C₁; ◇₂ = ◇ C₂

    to : ◇₁ (λ x → ◇₂ (λ y → P x × Q y) ys) xs → ◇₁ P xs × ◇₂ Q ys
    to (any (p₁ , any (p₂ , p , q))) = (any (p₁ , p) , any (p₂ , q))

    from : ◇₁ P xs × ◇₂ Q ys → ◇₁ (λ x → ◇₂ (λ y → P x × Q y) ys) xs
    from (any (p₁ , p) , any (p₂ , q)) = any (p₁ , any (p₂ , p , q))

-- map can be absorbed by the predicate.

module _ {s p} (C : Container s p) {x y} {X : Set x} {Y : Set y}
         {ℓ} (P : Pred Y ℓ) where

  map↔∘ : ∀ {xs : ⟦ C ⟧ X} (f : X → Y) → ◇ C P (map f xs) ↔ ◇ C (P ∘′ f) xs
  map↔∘ {xs} f =
   ◇ C P (map f xs)          ↔⟨ ↔Σ C ⟩
   ∃ (P ∘′ proj₂ (map f xs)) ↔⟨⟩
   ∃ (P ∘′ f ∘′ proj₂ xs)    ↔⟨ SK-sym (↔Σ C) ⟩
   ◇ C (P ∘′ f) xs           ∎

-- Membership in a mapped container can be expressed without reference
-- to map.

module _ {s p} (C : Container s p) {x y} {X : Set x} {Y : Set y}
         {ℓ} (P : Pred Y ℓ) where

  ∈map↔∈×≡ : ∀ {f : X → Y} {xs : ⟦ C ⟧ X} {y} →
             y ∈ map f xs ↔ (∃ λ x → x ∈ xs × y ≡ f x)
  ∈map↔∈×≡ {f = f} {xs} {y} =
    y ∈ map f xs               ↔⟨ map↔∘ C (y ≡_) f ⟩
    ◇ C (λ x → y ≡ f x) xs     ↔⟨ ↔∈ C ⟩
    ∃ (λ x → x ∈ xs × y ≡ f x) ∎

-- map is a congruence for bag and set equality and related preorders.

module _ {s p} (C : Container s p) {x y} {X : Set x} {Y : Set y}
         {ℓ} (P : Pred Y ℓ) where

  map-cong : ∀ {k} {f₁ f₂ : X → Y} {xs₁ xs₂ : ⟦ C ⟧ X} →
             f₁ ≗ f₂ → xs₁ ∼[ k ] xs₂ →
             map f₁ xs₁ ∼[ k ] map f₂ xs₂
  map-cong {f₁ = f₁} {f₂} {xs₁} {xs₂} f₁≗f₂ xs₁≈xs₂ {x} =
    x ∈ map f₁ xs₁           ↔⟨ map↔∘ C (_≡_ x) f₁ ⟩
    ◇ C (λ y → x ≡ f₁ y) xs₁ ∼⟨ cong (Related.↔⇒ ∘ helper) xs₁≈xs₂ ⟩
    ◇ C (λ y → x ≡ f₂ y) xs₂ ↔⟨ SK-sym (map↔∘ C (_≡_ x) f₂) ⟩
    x ∈ map f₂ xs₂           ∎
    where
    helper : ∀ y → (x ≡ f₁ y) ↔ (x ≡ f₂ y)
    helper y rewrite f₁≗f₂ y = Inv.id

-- Uses of linear morphisms can be removed.

module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s₂ p₂}
         {x} {X : Set x} {ℓ} (P : Pred X ℓ) where

  remove-linear : ∀ {xs : ⟦ C₁ ⟧ X} (m : C₁ ⊸ C₂) → ◇ C₂ P (⟪ m ⟫⊸ xs) ↔ ◇ C₁ P xs
  remove-linear {xs} m = Inv.inverse t f f∘t t∘f
    where
    open _≃_
    open P.≡-Reasoning renaming (_∎ to _∎′)

    position⊸m : ∀ {s} → Position C₂ (shape⊸ m s) ≃ Position C₁ s
    position⊸m = ↔→≃ (position⊸ m)

    ◇₁ = ◇ C₁; ◇₂ = ◇ C₂

    t : ◇₂ P (⟪ m ⟫⊸ xs) → ◇₁ P xs
    t = Any.map₁ (_⊸_.morphism m)

    f : ◇₁ P xs → ◇₂ P (⟪ m ⟫⊸ xs)
    f (any (x , p)) =
      any $ from position⊸m x
          , P.subst (P ∘′ proj₂ xs) (P.sym (right-inverse-of position⊸m _)) p

    f∘t : f ∘ t ≗ id
    f∘t (any (p₂ , p)) = P.cong any $ Inverse.to Σ-≡,≡↔≡ ⟨$⟩
      ( left-inverse-of position⊸m p₂
      , (P.subst (P ∘ proj₂ xs ∘ to position⊸m)
           (left-inverse-of position⊸m p₂)
           (P.subst (P ∘ proj₂ xs)
              (P.sym (right-inverse-of position⊸m
                        (to position⊸m p₂)))
              p)                                                ≡⟨ P.subst-∘ (left-inverse-of position⊸m _) ⟩

         P.subst (P ∘ proj₂ xs)
           (P.cong (to position⊸m)
              (left-inverse-of position⊸m p₂))
           (P.subst (P ∘ proj₂ xs)
              (P.sym (right-inverse-of position⊸m
                        (to position⊸m p₂)))
              p)                                                ≡⟨ P.cong (λ eq → P.subst (P ∘ proj₂ xs) eq
                                                                                (P.subst (P ∘ proj₂ xs)
                                                                                (P.sym (right-inverse-of position⊸m _)) _))
                                                                     (_≃_.left-right position⊸m _) ⟩
         P.subst (P ∘ proj₂ xs)
           (right-inverse-of position⊸m
              (to position⊸m p₂))
           (P.subst (P ∘ proj₂ xs)
              (P.sym (right-inverse-of position⊸m
                        (to position⊸m p₂)))
              p)                                                ≡⟨ P.subst-subst (P.sym (right-inverse-of position⊸m _)) ⟩

         P.subst (P ∘ proj₂ xs)
           (P.trans
              (P.sym (right-inverse-of position⊸m
                        (to position⊸m p₂)))
              (right-inverse-of position⊸m
                 (to position⊸m p₂)))
           p                                                    ≡⟨ P.cong (λ eq → P.subst (P ∘ proj₂ xs) eq p)
                                                                     (P.trans-symˡ (right-inverse-of position⊸m _)) ⟩

         P.subst (P ∘ proj₂ xs) P.refl p                        ≡⟨⟩

        p                                                       ∎′)
      )

    t∘f : t ∘ f ≗ id
    t∘f (any (p₁ , p)) = P.cong any $ Inverse.to Σ-≡,≡↔≡ ⟨$⟩
      ( right-inverse-of position⊸m p₁
      , (P.subst (P ∘ proj₂ xs)
           (right-inverse-of position⊸m p₁)
           (P.subst (P ∘ proj₂ xs)
              (P.sym (right-inverse-of position⊸m p₁))
              p)                                                ≡⟨ P.subst-subst (P.sym (right-inverse-of position⊸m _)) ⟩

         P.subst (P ∘ proj₂ xs)
           (P.trans
              (P.sym (right-inverse-of position⊸m p₁))
              (right-inverse-of position⊸m p₁))
           p                                                    ≡⟨ P.cong (λ eq → P.subst (P ∘ proj₂ xs) eq p)
                                                                     (P.trans-symˡ (right-inverse-of position⊸m _)) ⟩
         P.subst (P ∘ proj₂ xs) P.refl p                        ≡⟨⟩

        p                                                       ∎′)
      )

-- Linear endomorphisms are identity functions if bag equality is used.

module _ {s p} {C : Container s p} {x} {X : Set x} where

  linear-identity : ∀ {xs : ⟦ C ⟧ X} (m : C ⊸ C) → ⟪ m ⟫⊸ xs ∼[ bag ] xs
  linear-identity {xs} m {x} =
    x ∈ ⟪ m ⟫⊸ xs  ↔⟨ remove-linear (_≡_ x) m ⟩
    x ∈        xs  ∎

-- If join can be expressed using a linear morphism (in a certain
-- way), then it can be absorbed by the predicate.

module _ {s₁ s₂ s₃ p₁ p₂ p₃}
         {C₁ : Container s₁ p₁} {C₂ : Container s₂ p₂} {C₃ : Container s₃ p₃}
         {x} {X : Set x} {ℓ} (P : Pred X ℓ) where

  join↔◇ : (join′ : (C₁ C.∘ C₂) ⊸ C₃) (xss : ⟦ C₁ ⟧ (⟦ C₂ ⟧ X)) →
           let join : ∀ {X} → ⟦ C₁ ⟧ (⟦ C₂ ⟧ X) → ⟦ C₃ ⟧ X
               join = λ {_} → ⟪ join′ ⟫⊸ ∘
                      _⟨$⟩_ (Inverse.from (Composition.correct C₁ C₂)) in
           ◇ C₃ P (join xss) ↔ ◇ C₁ (◇ C₂ P) xss
  join↔◇ join xss =
    ◇ C₃ P (⟪ join ⟫⊸ xss′) ↔⟨ remove-linear P join ⟩
    ◇ (C₁ C.∘ C₂) P xss′    ↔⟨ SK-sym $ flatten P xss ⟩
    ◇ C₁ (◇ C₂ P) xss       ∎
    where xss′ = Inverse.from (Composition.correct C₁ C₂) ⟨$⟩ xss


text: module Highlighting.M where

ext: agda

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module Sized.CounterCell where

open import Data.Product
open import Data.Nat.Base
open import Data.Nat.Show
open import Data.String.Base using (String; _++_)

open import SizedIO.Object
open import SizedIO.IOObject

open import SizedIO.Base
open import SizedIO.Console hiding (main)
open import SizedIO.ConsoleObject

open import NativeIO

open import Sized.SimpleCell hiding (program; main)

open import Size

data CounterMethod A : Set where
  super : (m : CellMethod A) → CounterMethod A
  stats : CounterMethod A

pattern getᶜ   = super get
pattern putᶜ x = super (put x)

-- CounterResult : ∀{A} →

counterI : (A : Set) → Interface
Method (counterI A)           =  CounterMethod A
Result (counterI A) (super m) =  Result (cellJ A) m
Result (counterI A) stats     =  Unit

CounterC : (i : Size) → Set
CounterC i = ConsoleObject i (counterI String)

-- counterP is constructor for the consoleObject for interface counterI

counterP : ∀{i} (c : CellC i) (ngets nputs : ℕ) → CounterC i
method (counterP c ngets nputs) getᶜ =
  method c get                                >>= λ { (s , c') →
  return (s , counterP c' (1 + ngets) nputs)  }
method (counterP c ngets nputs) (putᶜ x) =
  method c (put x)                            >>= λ { (_ , c') →
  return (_ , counterP c' ngets (1 + nputs))  }
method (counterP c ngets nputs) stats =
  exec (putStrLn ("Counted "
    ++ show ngets ++ " calls to get and "
    ++ show nputs ++ " calls to put."))       λ _ →
  return (_ , counterP c ngets nputs)

program : String → IOConsole ∞ Unit
program arg =
  let c₀ = counterP (cellP "Start") 0 0 in
  method c₀ getᶜ               >>= λ{ (s   , c₁) →
  exec1 (putStrLn s)            >>
  method c₁ (putᶜ arg)         >>= λ{ (_        , c₂) →
  method c₂ getᶜ               >>= λ{ (s'  , c₃) →
  exec1 (putStrLn s')           >>
  method c₃ (putᶜ "Over!")     >>= λ{ (_ , c₄) →
  method c₄ stats              >>= λ{ (_ , c₅) →
  return _                     }}}}}

main : NativeIO Unit
main = translateIOConsole (program "Hello")

-- -}
-- -}
-- -}
-- -}
-- -}
-- -}
-- -}

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


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

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.Properties
open import Cubical.ZCohomology.MayerVietorisUnreduced
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Function
open import Cubical.HITs.Wedge
open import Cubical.HITs.SetTruncation renaming (rec to sRec ; rec2 to pRec2 ; elim to sElim ; elim2 to sElim2 ; map to sMap)
open import Cubical.HITs.PropositionalTruncation renaming (rec to pRec ; ∣_∣ to ∣_∣₁)
open import Cubical.HITs.Truncation renaming (elim to trElim ; rec to trRec ; elim2 to trElim2)
open import Cubical.Data.Nat
open import Cubical.Algebra.Group

open import Cubical.ZCohomology.Groups.Unit
open import Cubical.ZCohomology.Groups.Sn

open import Cubical.HITs.Pushout
open import Cubical.Data.Sigma

open import Cubical.Foundations.Isomorphism
open import Cubical.Homotopy.Connected
open import Cubical.HITs.Susp
open import Cubical.HITs.S1
open import Cubical.HITs.Sn
open import Cubical.Foundations.Equiv

module _ {ℓ ℓ'} (A : Pointed ℓ) (B : Pointed ℓ') where
  module I = MV (typ A) (typ B) Unit (λ _ → pt A) (λ _ → pt B)

  Hⁿ-⋁ : (n : ℕ) → GroupIso (coHomGr (suc n) (A ⋁ B)) (×coHomGr (suc n) (typ A) (typ B))
  Hⁿ-⋁ zero = BijectionIsoToGroupIso bijIso
    where
    surj-helper : (x : coHom 0 Unit) → isInIm _ _ (I.Δ 0) x
    surj-helper =
      sElim (λ _ → isOfHLevelSuc 1 propTruncIsProp)
            λ f → ∣ (∣ (λ _ → f tt) ∣₂ , 0ₕ 0) , cong ∣_∣₂ (funExt λ _ → -rUnitₖ 0 (f tt)) ∣₁

    helper : (x : coHom 1 (A ⋁ B)) → isInIm _ _ (I.d 0) x → x ≡ 0ₕ 1
    helper x inim =
      pRec (setTruncIsSet _ _)
           (λ p → sym (snd p) ∙
                       MV.Im-Δ⊂Ker-d _ _ Unit (λ _ → pt A) (λ _ → pt B) 0 (fst p) (surj-helper (fst p)))
             inim

    bijIso : BijectionIso (coHomGr 1 (A ⋁ B)) (×coHomGr 1 (typ A) (typ B))
    BijectionIso.map' bijIso = I.i 1
    BijectionIso.inj bijIso =
      sElim (λ _ → isSetΠ λ _ → isProp→isSet (setTruncIsSet _ _))
            λ f inker → helper ∣ f ∣₂ (I.Ker-i⊂Im-d 0 ∣ f ∣₂ inker)
    BijectionIso.surj bijIso p = I.Ker-Δ⊂Im-i 1 p (isContr→isProp (isContrHⁿ-Unit 0) _ _)

  Hⁿ-⋁ (suc n) = Iso+Hom→GrIso mainIso
                                (sElim2 (λ _ _ → isOfHLevelPath 2 (isOfHLevel× 2 setTruncIsSet setTruncIsSet) _ _)
                                         λ _ _ → refl)
    where
    helpIso : ∀ {ℓ'''} {C : Type ℓ'''} → Iso (A ⋁ B → C) (Σ[ f ∈ (typ A → C) × (typ B → C) ] (fst f) (pt A) ≡ (snd f) (pt B))
    Iso.fun helpIso f = ((λ x → f (inl x)) , λ x → f (inr x)) , cong f (push tt)
    Iso.inv helpIso ((f , g) , p) (inl x) = f x
    Iso.inv helpIso ((f , g) , p) (inr x) = g x
    Iso.inv helpIso ((f , g) , p) (push a i) = p i
    Iso.rightInv helpIso ((f , g) , p) = ΣPathP (ΣPathP (refl , refl) , refl)
    Iso.leftInv helpIso f = funExt λ {(inl a) → refl ; (inr a) → refl ; (push a i) → refl}

    mainIso : Iso (coHom (2 + n) (A ⋁ B))
                  (coHom (2 + n) (typ A) × coHom (2 + n) (typ B))
    mainIso = compIso (setTruncIso helpIso) (compIso theIso setTruncOfProdIso)
      where
      forget :  ∥ (Σ[ f ∈ (typ A → coHomK (2 + n)) × (typ B → coHomK (2 + n)) ] (fst f) (pt A) ≡ (snd f) (pt B)) ∥₂
                     → ∥ (typ A → coHomK (2 + n)) × (typ B → coHomK (2 + n)) ∥₂
      forget = sMap (λ {((f , g) , _) → f , g})

      isEq :  (f :  ∥ (typ A → coHomK (2 + n)) × (typ B → coHomK (2 + n)) ∥₂) → isContr (fiber forget f)
      isEq = sElim (λ _ → isOfHLevelSuc 1 isPropIsContr) (uncurry λ f g → helper f g (f (pt A)) (g (pt B)) refl refl)
        where
        helper : (f : (typ A → coHomK (2 +  n))) (g : (typ B → coHomK (2 + n))) (x y : coHomK (2 + n))
               → f (pt A) ≡ x
               → g (pt B) ≡ y
               → isContr (fiber forget ∣ f , g ∣₂)
        helper f g = trElim2 (λ _ _ → isProp→isOfHLevelSuc (3 + n)
                               (isPropΠ2 λ _ _ → isPropIsContr))
                             (suspToPropElim2 (ptSn (suc n))
                                              (λ _ _ → isPropΠ2 λ _ _ → isPropIsContr)
                                              λ p q → (∣ (f , g) , (p ∙ sym q) ∣₂
                         , refl)
                         , uncurry (sElim (λ _ → isSetΠ λ _ → isOfHLevelPath 2 (isOfHLevelΣ 2 setTruncIsSet λ _ → isOfHLevelPath 2 setTruncIsSet _ _) _ _)
                               λ { ((f' , g') , id1) y →
                                     Σ≡Prop (λ _ → setTruncIsSet _ _)
                                              (pRec (setTruncIsSet _ _)
                                                 (λ id2 → trRec (setTruncIsSet _ _)
                                                   (λ pathp → cong ∣_∣₂ (ΣPathP ((sym id2) , pathp)))
                                                   (isConnectedPathP 1
                                                     {A = λ i → (fst (id2 (~ i)) (pt A) ≡ snd (id2 (~ i)) (pt B))}
                                                       (isConnectedPath 2 (isConnectedSubtr 3 n
                                                                          (subst (λ m → isConnected m (coHomK (2 + n))) (+-comm 3 n)
                                                                                (isConnectedKn (suc n)))) _ _)
                                                       (p ∙ sym q) id1 .fst))
                                                       (Iso.fun PathIdTrunc₀Iso y))}))
      theIso : Iso ∥ (Σ[ f ∈ (typ A → coHomK (2 + n)) × (typ B → coHomK (2 + n)) ] (fst f) (pt A) ≡ (snd f) (pt B)) ∥₂
                   ∥ (typ A → coHomK (2 + n)) × (typ B → coHomK (2 + n)) ∥₂
      theIso = equivToIso (forget , record { equiv-proof = isEq })

   {- Alternative, less direct proof :
       vSES→GroupIso _ _
         (ses (isOfHLevelSuc 0 (isContrHⁿ-Unit n))
              (isOfHLevelSuc 0 (isContrHⁿ-Unit (suc n)))
              (I.d (suc n))
              (I.Δ (suc (suc n)))
              (I.i (suc (suc n)))
              (I.Ker-i⊂Im-d (suc n))
              (I.Ker-Δ⊂Im-i (suc (suc n))))
   -}

  wedgeConnected : ((x : typ A) → ∥ pt A ≡ x ∥) → ((x : typ B) → ∥ pt B ≡ x ∥) → (x : A ⋁ B) → ∥ inl (pt A) ≡ x ∥
  wedgeConnected conA conB =
    PushoutToProp (λ _ → propTruncIsProp)
                  (λ a → pRec propTruncIsProp (λ p → ∣ cong inl p ∣₁) (conA a))
                   λ b → pRec propTruncIsProp (λ p → ∣ push tt ∙ cong inr p ∣₁) (conB b)

max_stars_repo_name: ayberkt/cubical

max_issues_repo_name: ayberkt/cubical

max_forks_repo_name: ayberkt/cubical


text:
module Generic.Test.Data.W where

open import Generic.Main

data W′ {α β} (A : Set α) (B : A -> Set β) : Set (α ⊔ β) where
  sup′ : ∀ {x} -> (B x -> W′ A B) -> W′ A B

W : ∀ {α β} -> (A : Set α) -> (A -> Set β) -> Set (α ⊔ β)
W = readData W′

pattern sup x g = !#₀ (relv x , g , lrefl)

elimW : ∀ {α β π} {A : Set α} {B : A -> Set β}
      -> (P : W A B -> Set π)
      -> (∀ {x} {g : B x -> W A B} -> (∀ y -> P (g y)) -> P (sup x g))
      -> ∀ w
      -> P w
elimW {B = B} P h (sup x g) = h (λ y -> elimW {B = B} P h (g y))

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


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

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

module ExampleSheets.LogicAndSets.Sheet1 where

  q1i : {a : _} {A : Set a} → (p1 p2 p3 : Propositions A) → Tautology (implies (implies p1 (implies p2 p3)) (implies p2 (implies p1 p3)))
  Tautology.isTaut (q1i p1 p2 p3) {v} with inspect (Valuation.v v p3)
  Tautology.isTaut (q1i p1 p2 p3) {v} | BoolTrue with≡ p3T = Valuation.vImplicationT v (Valuation.vImplicationT v (Valuation.vImplicationT v p3T))
  Tautology.isTaut (q1i p1 p2 p3) {v} | BoolFalse with≡ p3F with inspect (Valuation.v v p2)
  Tautology.isTaut (q1i p1 p2 p3) {v} | BoolFalse with≡ p3F | BoolTrue with≡ p2T with inspect (Valuation.v v p1)
  Tautology.isTaut (q1i p1 p2 p3) {v} | BoolFalse with≡ p3F | BoolTrue with≡ p2T | BoolTrue with≡ p1T = Valuation.vImplicationVacuous v (Valuation.vImplicationF v p1T (Valuation.vImplicationF v p2T p3F))
  Tautology.isTaut (q1i p1 p2 p3) {v} | BoolFalse with≡ p3F | BoolTrue with≡ p2T | BoolFalse with≡ p1F = Valuation.vImplicationT v (Valuation.vImplicationT v (Valuation.vImplicationVacuous v p1F))
  Tautology.isTaut (q1i p1 p2 p3) {v} | BoolFalse with≡ p3F | BoolFalse with≡ p2F = Valuation.vImplicationT v (Valuation.vImplicationVacuous v p2F)


text:
module Numeral.Natural.Oper.Modulo.Proofs.Elim where

import Lvl
open import Data.Boolean.Stmt
open import Logic.Propositional
open import Numeral.Natural
open import Numeral.Natural.Inductions
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Comparisons
open import Numeral.Natural.Oper.DivMod.Proofs
open import Numeral.Natural.Oper.FlooredDivision
open import Numeral.Natural.Oper.Modulo
open import Numeral.Natural.Oper.Modulo.Proofs
open import Numeral.Natural.Oper.Proofs.Order
open import Numeral.Natural.Relation.Order
open import Numeral.Natural.Relation.Order.Proofs
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Relator
open import Structure.Relator.Ordering
open import Structure.Relator.Properties
open import Type

mod-elim : ∀{ℓ} → (P : {ℕ} → ℕ → Type{ℓ}) → ∀{b} ⦃ _ : IsTrue(positive?(b)) ⦄ → (∀{a n} → (a < b) → P{a + (n ⋅ b)}(a)) → (∀{a} → P{a}(a mod b))
mod-elim P {𝐒 b} proof {a} with [<][≥]-dichotomy {a}{𝐒 b}
... | [∨]-introₗ lt = substitute₂(\x y → P{x}(y))
  (reflexivity(_≡_))
  (symmetry(_≡_) (mod-lesser-than-modulus ⦃ [≤]-without-[𝐒] lt ⦄))
  (proof{a}{0} lt)
... | [∨]-introᵣ ge = substitute₂(\x y → P{x}(y))
  ([↔]-to-[→] ([−₀][+]-nullify2ᵣ {(a ⌊/⌋ 𝐒(b)) ⋅ 𝐒(b)}{a}) (subtransitivityᵣ(_≤_)(_≡_) ([≤]-of-[+]ₗ {(a ⌊/⌋ 𝐒(b)) ⋅ 𝐒(b)}{a mod 𝐒(b)}) ([⌊/⌋][mod]-is-division-with-remainder {a}{b})))
  (symmetry(_≡_) ([⌊/⌋][⋅]-inverseOperatorᵣ-error {a}{b}))
  (proof{a −₀ ((a ⌊/⌋ 𝐒(b)) ⋅ 𝐒(b))}{a ⌊/⌋ 𝐒(b)} (subtransitivityₗ(_<_)(_≡_) (symmetry(_≡_) ([⌊/⌋][⋅]-inverseOperatorᵣ-error {a}{b})) (mod-maxᵣ{a}{𝐒 b})))

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Structure.Container.Iterable where

import      Lvl
open import Data
open import Data.Boolean
open import Data.Option
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Functional
import      Structure.Container.IndexedIterable
open import Type

private variable ℓ ℓₑ ℓₑ₁ ℓₑ₂ : Lvl.Level
private variable T : Type{ℓ}
private variable Elem : Type{ℓₑ}

open Structure.Container.IndexedIterable{Index = Unit{Lvl.𝟎}} hiding (Iterable ; module Iterable)
module Iterable{ℓ}{Iter} = Structure.Container.IndexedIterable.Iterable{Index = Unit{Lvl.𝟎}}{ℓ}{Iter = const Iter}
Iterable : ∀{ℓ} → Type{ℓ} → ∀{ℓₑ} → Type
Iterable{ℓ} Iter {ℓₑ} = Structure.Container.IndexedIterable.Iterable{Index = Unit{Lvl.𝟎}}{ℓ}(const Iter){ℓₑ}

module _ {Iter : Type{ℓ}} (iterator : Iterable(Iter){ℓₑ}) where
  open Iterable(iterator)

  next : Iter → Option(Element ⨯ Iter)
  next(i) with isEmpty(i) | indexStep i | current i | step i
  ... | 𝑇 | <> | <> | <> = None
  ... | 𝐹 | _  | x  | is = Some(x , is)

  head : Iter → Option(Element)
  head(i) with isEmpty(i) | indexStep i | current i
  ... | 𝑇 | <>  | <> = None
  ... | 𝐹 | _   | x  = Some(x)

  tail : Iter → Option(Iter)
  tail(i) with isEmpty(i) | indexStep i | step i
  ... | 𝑇 | <>  | <> = None
  ... | 𝐹 | _   | is = Some(is)

  tail₀ : Iter → Iter
  tail₀(i) with isEmpty(i) | indexStep i | step i
  ... | 𝑇 | <>  | <> = i
  ... | 𝐹 | _   | is = is

  {-
  record Finite : Type{ℓ} where
    field
      length : I → ℕ
    field
      length-proof : LengthCriteria(length)
    --field
    --  length-when-empty    : ∀{i} → IsTrue (isEmpty(i)) → (length(i) ≡ 𝟎)
      -- length-when-nonempty : ∀{i} → IsFalse(isEmpty(i)) → ∃(n ↦ length(i) ≡ 𝐒(n))
      -- length-of-step : ∀{i} → IsFalse(isEmpty(i)) → (𝐒(length(step i)) ≡ length(i)))
      -- empty-on-length-step : ∀{i} → IsTrue(isEmpty₊(length(i)) i)
      -- length-minimal-empty-step : ∀{n}{i} → (n < length(i)) → IsFalse(isEmpty₊(n) i)
  open Finite ⦃ … ⦄ public
  -}

  -- TODO: It is possible for Finite and the constructions to be from different iterables
  module _
    ⦃ fin : Finite ⦄
    {prepend : (x : Element) → (iter : Iter) → Iter}
    ⦃ prepend-construction : PrependConstruction(prepend) ⦄
    where

    _++_ : Iter → Iter → Iter
    _++_ = swap(foldᵣ prepend)

  module _
    ⦃ fin : Finite ⦄
    {empty}
    ⦃ empty-construciton : EmptyConstruction(empty) ⦄
    {prepend : (x : Element) → (iter : Iter) → Iter}
    ⦃ prepend-construction : PrependConstruction(prepend) ⦄
    where

    map : (Element → Element) → (Iter → Iter)
    map f = foldᵣ (prepend ∘ f) empty

    filter : (Element → Bool) → Iter → Iter
    filter f = foldᵣ (x ↦ if f(x) then (prepend x) else id) empty

    reverse : Iter → Iter
    reverse = foldₗ (swap prepend) empty

    postpend : Element → Iter → Iter
    postpend = foldᵣ prepend ∘ singleton

    open import Numeral.Natural
    repeat : Element → ℕ → Iter
    repeat x 𝟎      = empty
    repeat x (𝐒(n)) = prepend x (repeat x n)


text:
-- Private signatures
module Issue476d where

module M where
  private
    record R : Set₁

  record R where
    field X : Set

Q : Set₁
Q = M.R

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- {-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v term:20 -v term.function:30 #-}

-- Andreas, 2015-05-31, issue reported by Bruno Bianchi

module Issue1530 {A : Set}(_<=_ : A -> A -> Set) where

open import Common.List
open import Issue1530.Bound _<=_

data OList : Bound -> Set where
  nil : {b : Bound} -> OList b
  cons : {b : Bound}{x : A} -> LeB b (val x) -> OList (val x) -> OList b

forget : {b : Bound} -> OList b -> List A
forget nil = []
forget (cons {x = x} _ xs) = x ∷ forget xs

data Sorted : List A -> Set where
  empty : Sorted []
  single : (x : A) -> Sorted (x ∷ [])
  step : {x y : A}{ys : List A} -> x <= y -> Sorted (y ∷ ys) -> Sorted (x ∷ y ∷ ys)

olist-sorted : {b : Bound}(xs : OList b) -> Sorted (forget xs)
olist-sorted nil = empty
olist-sorted (cons {x = x} _ nil) = single x
olist-sorted (cons b<=x (cons (lexy x<=y) ys)) = step x<=y (olist-sorted (cons (lexy x<=y) ys))

-- should termination check

-- problem WAS: TermCheck did not *deeply* resolve constructor names on rhs in last clause.
-- TermCheck.reduceCon did not reduce the lexy on the rhs, as it was deep inside.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Andreas, 2019-08-17, issue #1346

open import Issue1346

-- Repeating the definitions of Issue1346.agda

private
  test₁ : List⁺ Bool
  test₁ = true ∷ false ∷ []  -- mixing _∷_ of _×_ and List

  test₂ : ∀{A : Set} → A → List A × List⁺ A × List⁺ A
  test₂ a = [] , a ∷ [] , a ∷ a ∷ []  -- mixing _,_ and _∷_ of _×_


text:
firstTrue : (f : ℕ → Bool) → ∃ (λ n → f n ≡ true) → ℕ
firstTrue f prf = mp-ℕ

firstTrue-true : firstTrue f prf ≡ n → f n ≡ true
firstTrue-true = ?

firstTrue-false : firstTrue f prf ≡ n → ∀ m → m < n → f m ≡ false
firstTrue-false = ?


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

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.GroupStructure
open import Cubical.ZCohomology.Properties
open import Cubical.ZCohomology.Groups.KleinBottle
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.GroupoidLaws
open import Cubical.HITs.SetTruncation renaming (rec to sRec ; rec2 to pRec2 ; elim to sElim ; elim2 to sElim2 ; map to sMap)
open import Cubical.HITs.PropositionalTruncation renaming (rec to pRec ; elim to pElim) hiding (map)
open import Cubical.HITs.Truncation renaming (elim to trElim ; rec to trRec ; elim2 to trElim2)
open import Cubical.Algebra.Group

open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.Transport

open import Cubical.ZCohomology.Groups.Connected

open import Cubical.Data.Sigma

open import Cubical.Foundations.Isomorphism
open import Cubical.HITs.S1
open import Cubical.HITs.Sn
open import Cubical.Foundations.Equiv
open import Cubical.Homotopy.Connected
open import Cubical.HITs.RPn.Base

open GroupIso renaming (map to map')
open GroupHom

open import Cubical.Data.Empty renaming (rec to ⊥-rec)
open import Cubical.Data.Bool
open import Cubical.Data.Int

open import Cubical.Foundations.Path

private
  variable
    ℓ : Level
    A : Type ℓ

funSpaceIso-RP² : Iso (RP² → A) (Σ[ x ∈ A ] Σ[ p ∈ x ≡ x ] p ≡ sym p)
Iso.fun funSpaceIso-RP² f = f point , (cong f line , λ i j → f (square i j))
Iso.inv funSpaceIso-RP² (x , p , P) point = x
Iso.inv funSpaceIso-RP² (x , p , P) (line i) = p i
Iso.inv funSpaceIso-RP² (x , p , P) (square i j) = P i j
Iso.rightInv funSpaceIso-RP² (x , p , P) i = x , p , P
Iso.leftInv funSpaceIso-RP² f _ point = f point
Iso.leftInv funSpaceIso-RP² f _ (line i) = f (line i)
Iso.leftInv funSpaceIso-RP² f _ (square i j) = f (square i j)

private
  pathIso : {x : A} {p : x ≡ x} → Iso (p ≡ sym p) (p ∙ p ≡ refl)
  pathIso {p = p} = compIso (congIso (equivToIso (_ , compPathr-isEquiv p)))
                            (pathToIso (cong (p ∙ p ≡_) (lCancel p)))

--- H⁰(RP²) ≅ ℤ ----
H⁰-RP²≅ℤ : GroupIso (coHomGr 0 RP²) intGroup
H⁰-RP²≅ℤ = H⁰-connected point connectedRP¹
  where
  connectedRP¹ : (x : RP²) → ∥ point ≡ x ∥
  connectedRP¹ point = ∣ refl ∣
  connectedRP¹ (line i) =
    isOfHLevel→isOfHLevelDep 1 {B = λ x → ∥ point ≡ x ∥}
      (λ _ → propTruncIsProp) ∣ refl ∣ ∣ refl ∣ line i
  connectedRP¹ (square i j) = helper i j
    where
    helper : SquareP (λ i j → ∥ point ≡ square i j ∥)
                     (isOfHLevel→isOfHLevelDep 1 {B = λ x → ∥ point ≡ x ∥}
                       (λ _ → propTruncIsProp) ∣ refl ∣ ∣ refl ∣ line)
                     (symP (isOfHLevel→isOfHLevelDep 1 {B = λ x → ∥ point ≡ x ∥}
                             (λ _ → propTruncIsProp) ∣ refl ∣ ∣ refl ∣ line))
                     refl refl
    helper = toPathP (isOfHLevelPathP 1 propTruncIsProp _ _ _ _)

--- H¹(RP²) ≅ 0 ----
isContr-H¹-RP²-helper : isContr ∥ Σ[ x ∈ coHomK 1 ] Σ[ p ∈ x ≡ x ] p ∙ p ≡ refl ∥₂
fst isContr-H¹-RP²-helper = ∣ 0ₖ 1 , refl , sym (rUnit refl) ∣₂
snd isContr-H¹-RP²-helper =
  sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
    (uncurry
      (trElim (λ _ → isGroupoidΠ λ _ → isOfHLevelPlus {n = 1} 2 (setTruncIsSet _ _))
      (toPropElim (λ _ → isPropΠ (λ _ → setTruncIsSet _ _))
         λ {(p , nilp)
            → cong ∣_∣₂ (ΣPathP (refl , Σ≡Prop (λ _ → isOfHLevelTrunc 3 _ _ _ _)
                                         (rUnit refl
                                       ∙∙ cong (Kn→ΩKn+1 0) (sym (nilpotent→≡0 (ΩKn+1→Kn 0 p)
                                                                                (sym (ΩKn+1→Kn-hom 0 p p)
                                                                                ∙ cong (ΩKn+1→Kn 0) nilp)))
                                       ∙∙ Iso.rightInv (Iso-Kn-ΩKn+1 0) p)))})))

H¹-RP²≅0 : GroupIso (coHomGr 1 RP²) trivialGroup
H¹-RP²≅0 =
  IsoContrGroupTrivialGroup
    (isOfHLevelRetractFromIso 0
      (setTruncIso (compIso funSpaceIso-RP²
                            (Σ-cong-iso-snd (λ _ → Σ-cong-iso-snd λ _ → pathIso))))
      isContr-H¹-RP²-helper)

--- H²(RP²) ≅ ℤ/2ℤ ----

Iso-H²-RP²₁ : Iso ∥ Σ[ x ∈ coHomK 2 ] Σ[ p ∈ x ≡ x ] p ≡ sym p ∥₂
                  ∥ Σ[ p ∈ 0ₖ 2 ≡ 0ₖ 2 ] p ≡ sym p ∥₂
Iso.fun Iso-H²-RP²₁ =
  sRec setTruncIsSet
    (uncurry
      (trElim (λ _ → is2GroupoidΠ λ _ → isOfHLevelPlus {n = 2} 2 setTruncIsSet)
        (sphereElim _ (λ _ → isSetΠ (λ _ → setTruncIsSet))
          λ p → ∣ fst p , snd p ∣₂)))
Iso.inv Iso-H²-RP²₁ = sMap λ p → (0ₖ 2) , p
Iso.rightInv Iso-H²-RP²₁ = sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                           λ _ → refl
Iso.leftInv Iso-H²-RP²₁ =
  sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
    (uncurry (trElim (λ _ → is2GroupoidΠ λ _ → isOfHLevelPlus {n = 1} 3 (setTruncIsSet _ _))
      (sphereToPropElim _ (λ _ → isPropΠ (λ _ → setTruncIsSet _ _))
        λ p → refl)))

Iso-H²-RP²₂ : Iso ∥ Σ[ p ∈ 0ₖ 2 ≡ 0ₖ 2 ] p ≡ sym p ∥₂ Bool
Iso-H²-RP²₂ = compIso (setTruncIso (Σ-cong-iso-snd λ _ → pathIso))
                (compIso Iso-H²-𝕂²₂ testIso)

H²-RP²≅Bool : GroupIso (coHomGr 2 RP²) BoolGroup
H²-RP²≅Bool = invGroupIso (≅Bool (compIso
                                    (compIso (setTruncIso funSpaceIso-RP²)
                                             Iso-H²-RP²₁)
                                    Iso-H²-RP²₂))

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

module Definition.Typed.Consequences.Consistency where

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

open import Tools.Embedding
open import Tools.Empty
open import Tools.Product
import Tools.PropositionalEquality as PE

zero≢one′ : ∀ {Γ l} ([ℕ] : Γ ⊩⟨ l ⟩ℕ ℕ)
           → Γ ⊩⟨ l ⟩ zero ≡ suc zero ∷ ℕ / ℕ-intr [ℕ] → ⊥
zero≢one′ (noemb x) (ιx (ℕₜ₌ .(suc _) .(suc _) d d′ k≡k′ (sucᵣ x₁))) =
  zero≢suc (whnfRed*Term (redₜ d) zeroₙ)
zero≢one′ (noemb x) (ιx (ℕₜ₌ .zero .zero d d′ k≡k′ zeroᵣ)) =
  zero≢suc (PE.sym (whnfRed*Term (redₜ d′) sucₙ))
zero≢one′ (noemb x) (ιx (ℕₜ₌ k k′ d d′ k≡k′ (ne (neNfₜ₌ neK neM k≡m)))) =
  zero≢ne neK (whnfRed*Term (redₜ d) zeroₙ)
zero≢one′ (emb 0<1 [ℕ]) (ιx n) = zero≢one′ [ℕ] n

-- Zero cannot be judgmentally equal to one.
zero≢one : ∀ {Γ} → Γ ⊢ zero ≡ suc zero ∷ ℕ → ⊥
zero≢one 0≡1 =
  let [ℕ] , [0≡1] = reducibleEqTerm 0≡1
  in  zero≢one′ (ℕ-elim [ℕ]) (irrelevanceEqTerm [ℕ] (ℕ-intr (ℕ-elim [ℕ])) [0≡1])

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


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

open import Agda.Builtin.Nat
open import Agda.Builtin.Cubical.Path

postulate
  admit : ∀ {A : Set} → A

data Z : Set where
  pos      : Nat → Z
  neg      : Nat → Z
  sameZero : pos 0 ≡ neg 0

_+Z_ : Z → Z → Z
pos x      +Z pos y      = admit
pos x      +Z neg y      = admit
pos x      +Z sameZero y = admit
neg x      +Z z          = admit
sameZero x +Z z          = admit

max_stars_repo_name: zgrannan/agda

max_issues_repo_name: zgrannan/agda

max_forks_repo_name: zgrannan/agda


text:
module Stable where

open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)

open import Negation using (¬_; ¬¬¬-elim)

Stable : Set → Set
Stable A = ¬ ¬ A → A

¬-stable : ∀ {A : Set} → Stable (¬ A)
¬-stable = λ ¬¬¬a → (λ a → ¬¬¬a (λ ¬a → ¬a a))
-- ¬-stable = ¬¬¬-elim

×-stable : ∀ {A B : Set} → Stable A → Stable B → Stable (A × B)
×-stable sa sb = λ ¬¬a×b →
  ⟨ (sa λ{ ¬a → ¬¬a×b λ{ a×b → ¬a (proj₁ a×b) }})
  , (sb λ{ ¬b → ¬¬a×b λ{ a×b → ¬b (proj₂ a×b) }})
  ⟩

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
data Term (V : Set) : Set where
  App : Term V -> Term V -> Term V
  Abs : (V -> Term V) -> Term V -- ouch, posititity.

max_stars_repo_name: johnyob/agda-sigma

max_issues_repo_name: johnyob/agda-sigma

max_forks_repo_name: johnyob/agda-sigma


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

module Fragment.Examples.Semigroup.Arith.Atomic where

open import Fragment.Examples.Semigroup.Arith.Base

-- Fully dynamic associativity

dyn-assoc₁ : ∀ {m n o} → (m + n) + o ≡ m + (n + o)
dyn-assoc₁ = fragment SemigroupFrex +-semigroup

dyn-assoc₂ : ∀ {m n o p} → ((m + n) + o) + p ≡ m + (n + (o + p))
dyn-assoc₂ = fragment SemigroupFrex +-semigroup

dyn-assoc₃ : ∀ {m n o p q} → (m + n) + o + (p + q) ≡ m + (n + o + p) + q
dyn-assoc₃ = fragment SemigroupFrex +-semigroup

-- Partially static associativity

sta-assoc₁ : ∀ {m n} → (m + 2) + (3 + n) ≡ m + (5 + n)
sta-assoc₁ = fragment SemigroupFrex +-semigroup

sta-assoc₂ : ∀ {m n o p} → (((m + n) + 5) + o) + p ≡ m + (n + (2 + (3 + (o + p))))
sta-assoc₂ = fragment SemigroupFrex +-semigroup

sta-assoc₃ : ∀ {m n o p} → ((m + n) + 2) + (3 + (o + p)) ≡ m + ((n + 1) + (4 + o)) + p
sta-assoc₃ = fragment SemigroupFrex +-semigroup

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
-- Andreas, 2012-11-18 see issue 761
module AbstractMutual where

module MA where

  mutual
    abstract -- accepted

      S : Set₁
      S = T

      T : Set₁
      T = Set

module AM where

  abstract -- rejected before, should also be accepted
    mutual

      S : Set₁
      S = T

      T : Set₁
      T = Set

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import LogicalFormulae
open import Orders
open import Groups.Groups
open import Numbers.Naturals.Naturals
open import Numbers.Naturals.WithK
open import Numbers.Primes.PrimeNumbers
open import Rings.Definition
open import Setoids.Setoids
open import Numbers.Modulo.IntegersModN
open import Semirings.Definition

module IntegersModNRing where
  modNToℕ : {n : ℕ} {pr : 0 <N n} → (a : ℤn n pr) → ℕ
  modNToℕ record { x = x ; xLess = xLess } = x

  *nhelper : {n : ℕ} {pr : 0 <N n} → (max : ℕ) → (a : ℤn n pr) → ℤn n pr → (max ≡ modNToℕ a) → ℤn n pr
  *nhelper {zero} {()}
  *nhelper {succ n} zero a b pr2 = record { x = 0 ; xLess = succIsPositive n }
  *nhelper {succ n} (succ max) record { x = zero ; xLess = xLess } b ()
  *nhelper {succ n} (succ max) record { x = (succ x) ; xLess = xLess } b pr2 = (*nhelper max record { x = x ; xLess = xLess2 } b (succInjective pr2)) +n b
    where
      xLess2 : x <N succ n
      xLess2 = PartialOrder.transitive (TotalOrder.order ℕTotalOrder) (a<SuccA x) xLess

  _*n_ : {n : ℕ} {pr : 0 <N n} → ℤn n pr → ℤn n pr → ℤn n pr
  _*n_ {0} {()}
  _*n_ {succ n} {_} record { x = a ; xLess = aLess } b = *nhelper a record { x = a ; xLess = aLess } b refl

  ℤnIdent : (n : ℕ) → (pr : 0 <N n) → ℤn n pr
  ℤnIdent 0 ()
  ℤnIdent 1 pr = record { x = 0 ; xLess = pr }
  ℤnIdent (succ (succ n)) _ = record { x = 1 ; xLess = succPreservesInequality (succIsPositive n) }

  ℤnMult0Right : {n : ℕ} {pr : 0 <N n} → (max : ℕ) → (a : ℤn n pr) → (modNToℕ a ≡ max) → (a *n record { x = 0 ; xLess = pr }) ≡ record { x = 0 ; xLess = pr }
  ℤnMult0Right {0} {()}
  ℤnMult0Right {succ n} .zero record { x = zero ; xLess = xLess } refl = equalityZn _ _ refl
  ℤnMult0Right {succ n} {pr} (.succ x) record { x = (succ x) ; xLess = xLess } refl rewrite ℤnMult0Right {succ n} {pr} x record { x = x ; xLess = PartialOrder.transitive (TotalOrder.order ℕTotalOrder) (a<SuccA x) xLess } refl = equalityZn _ _ refl

  ℤnMultCommutative : {n : ℕ} {pr : 0 <N n} → (a b : ℤn n pr) → (a *n b) ≡ (b *n a)
  ℤnMultCommutative {0} {()}
  ℤnMultCommutative {succ n} {pr} record { x = zero ; xLess = xLess } b with <NRefl pr xLess
  ... | refl rewrite ℤnMult0Right (modNToℕ b) b refl = equalityZn _ _ refl
  ℤnMultCommutative {succ n} record { x = (succ x) ; xLess = xLess } b = {!!}

  ℤnMultIdent : {n : ℕ} {pr : 0 <N n} → (a : ℤn n pr) → (ℤnIdent n pr) *n a ≡ a
  ℤnMultIdent {zero} {()}
  ℤnMultIdent {succ zero} {pr} record { x = zero ; xLess = (le diff proof) } = equalityZn _ _ refl
  ℤnMultIdent {succ zero} {pr} record { x = (succ a) ; xLess = (le diff proof) } = exFalso f
    where
      f : False
      f rewrite Semiring.commutative ℕSemiring diff (succ a) = naughtE (succInjective (equalityCommutative proof))
  ℤnMultIdent {succ (succ n)} {pr} record { x = a ; xLess = aLess } with orderIsTotal a (succ (succ n))
  ℤnMultIdent {succ (succ n)} {pr} record { x = a ; xLess = aLess } | inl (inl a<ssn) = equalityZn _ _ refl
  ℤnMultIdent {succ (succ n)} {pr} record { x = a ; xLess = aLess } | inl (inr ssn<a) = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) (PartialOrder.transitive (TotalOrder.order ℕTotalOrder) aLess ssn<a))
  ℤnMultIdent {succ (succ n)} {pr} record { x = .(succ (succ n)) ; xLess = aLess } | inr refl = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) aLess)

  ℤnRing : (n : ℕ) → (pr : 0 <N n) → Ring (reflSetoid (ℤn n pr)) (_+n_) (_*n_)
  Ring.additiveGroup (ℤnRing n 0<n) = (ℤnGroup n 0<n)
  Ring.multWellDefined (ℤnRing n 0<n) = reflGroupWellDefined
  Ring.1R (ℤnRing n pr) = ℤnIdent n pr
  Ring.groupIsAbelian (ℤnRing n 0<n) = AbelianGroup.commutative (ℤnAbGroup n 0<n)
  Ring.multAssoc (ℤnRing n 0<n) = {!!}
  Ring.multCommutative (ℤnRing n 0<n) {a} {b} = ℤnMultCommutative a b
  Ring.multDistributes (ℤnRing n 0<n) = {!!}
  Ring.multIdentIsIdent (ℤnRing n 0<n) {a} = ℤnMultIdent a


text:
open import Type

module Graph.Properties where

open import Functional
open import Function.Equals
open import Lang.Instance
open import Logic
open import Logic.Propositional
import      Lvl
open import Graph
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv
open import Structure.Setoid.Uniqueness
open import Structure.Relator.Properties
open import Type.Properties.MereProposition

module _ {ℓ₁ ℓ₂} {V : Type{ℓ₁}} (_⟶_ : Graph{ℓ₁}{ℓ₂}(V)) where
  -- An undirected graph always have for every edge an edge in the other direction which is the same edge.
  record Undirected : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
    constructor intro
    field
      ⦃ reversable ⦄ : Symmetry(_⟶_)
    reverse = symmetry(_⟶_)

    field
      reverse-involution : ∀{a b} → (reverse ∘ reverse ⊜ (id {T = a ⟶ b}))
  undirected-reverse = inst-fn Undirected.reverse

  -- Construction of an undirected graph from any graph.
  undirect : Graph{ℓ₁}{ℓ₂}(V)
  undirect a b = (b ⟶ a) ∨ (a ⟶ b)

  -- A graph is singular when there is at most one edge between every pair of vertices.
  -- In other words, when it is not a multigraph.
  -- Note: Equality on edges must respect uniqueness. In other words, one edge must not have multiple constructions.
  record Singular : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
    constructor intro
    field proof : ∀{a b : V} → MereProposition(a ⟶ b)
  singular = inst-fn(\inst {a}{b}{x}{y} → MereProposition.uniqueness(Singular.proof inst {a}{b}) {x}{y})

  -- A complete graph have an edge for each pair of vertices from V. Loops are allowed.
  record Complete : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
    constructor intro
    field proof : ∀{x y : V} → (x ⟶ y) ↔ (x ≢ y)
  complete = inst-fn Complete.proof

  record CompleteWithLoops : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
    constructor intro
    field proof : ∀{x y : V} → (x ⟶ y)
  completeWithLoops = inst-fn CompleteWithLoops.proof

  -- A linear graph contains vertices with a maximum of one outgoing edge and a maximum of one ingoing edge.
  record Linear : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
    constructor intro
    field
      unique-start-vertex : ∀{y} → Unique(x ↦ (x ⟶ y))
      unique-end-vertex   : ∀{x} → Unique(y ↦ (x ⟶ y))

  module _ (v : V) where
    -- An initial vertex have no ingoing edges pointing towards it.
    record InitialVertex : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
      constructor intro
      field proof : ∀{x} → ¬(x ⟶ v)
    initialVertex = inst-fn InitialVertex.proof

    -- A final vertex have no outgoing edges pointing from it.
    record FinalVertex : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
      constructor intro
      field proof : ∀{x} → ¬(v ⟶ x)
    finalVertex = inst-fn FinalVertex.proof

  -- A graph is a list when it is linear and has an unique initial vertex and an unique final vertex.
  -- The linearity guarantees so that if there are preceding and succeding elements of the list, they are unique.
  -- The initial vertex represents the first element of the list.
  -- The final vertex represents the last element of the list.
  record IsList : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
    constructor intro
    field
      ⦃ linear ⦄ : Linear
      unique-initial-vertex : Unique(InitialVertex)
      unique-final-vertex   : Unique(FinalVertex)

  -- A graph is a cycle when it is linear and do not have initial or final vertices.
  -- The linearity guarantees so that if there are preceding and succeding elements of the list, they are unique.
  -- The non-existence of initial vertices and final vertices means no first and last elements.
  record IsCycle : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
    constructor intro
    field
      ⦃ linear ⦄ : Linear
      no-initial-vertex : ∀{v} → ¬(InitialVertex v)
      no-final-vertex   : ∀{v} → ¬(FinalVertex v)

  module _ where
    open import Graph.Walk
    open import Graph.Walk.Properties

    -- A graph is a tree when it has an unique path between every pair of vertices.
    -- The existence of a path means that it is always possible to traverse the tree from every vertex along the edges to every vertex.
    record IsTree : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
      constructor intro
      field proof : ∀{x y : V} → ∃!{Obj = Walk(_⟶_) x y}(Path)
    isTree = inst-fn IsTree.proof

    record IsForest : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
      constructor intro
      field proof : ∀{x y : V} → Unique{Obj = Walk(_⟶_) x y}(Path)
    isForest = inst-fn IsForest.proof

    record IsOutwardRootedTree : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
      constructor intro
      field
        ⦃ tree ⦄ : IsTree
        unique-initial-vertex : ∃!(InitialVertex)
        -- TODO: Should not this be defined as ∃!(root ↦ InitialVertex(root) ∧ (∀{x : V} → ∃!{T = Walk(_⟶_) root x}(Path))) ?

    record IsInwardRootedTree : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
      constructor intro
      field
        ⦃ tree ⦄ : IsTree
        unique-initial-vertex : ∃!(FinalVertex)

module _ {ℓ₁ ℓ₂} {V : Type{ℓ₁}} (_⟶_ : Graph{ℓ₁}{ℓ₂}(V)) where
  open import Graph.Walk

  -- A connected graph have walks from every vertex to any vertex.
  -- For undirected graphs, this can be visually interpreted as disconnected islands of vertices.
  -- Note: Equality on edges must respect uniqueness. In other words, one edge must not have multiple constructions.
  Connected = CompleteWithLoops(Walk(_⟶_))
  connected = completeWithLoops(Walk(_⟶_))


text:
open import Oscar.Prelude
open import Oscar.Class
open import Oscar.Class.Unit

module Oscar.Class.Surjection where

module Surjection
  {𝔬₁} (𝔒₁ : Ø 𝔬₁)
  {𝔬₂} (𝔒₂ : Ø 𝔬₂)
  = ℭLASS (𝔒₁ , 𝔒₂) (𝔒₁ → 𝔒₂)

module _
  {𝔬₁} {𝔒₁ : Ø 𝔬₁}
  {𝔬₂} {𝔒₂ : Ø 𝔬₂}
  where
  surjection = Surjection.method 𝔒₁ 𝔒₂
  instance
    Surjection-toUnit : ⦃ _ : Surjection.class 𝔒₁ 𝔒₂ ⦄ → Unit.class (Surjection.type 𝔒₁ 𝔒₂)
    Surjection-toUnit .⋆ = surjection


text:
-- 2014-09-19
-- Reported by Mateusz Kowalczyk.

good : Set₁
good = let -- F : _  -- worked if you added the type signature
           F X = X
       in F Set

-- Now works without the type signature.

max_stars_repo_name: masondesu/agda


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.CommRing.Instances.MultivariatePoly where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat renaming(_+_ to _+n_; _·_ to _·n_)
open import Cubical.Data.Vec

open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing

open import Cubical.Algebra.Polynomials.Multivariate.Base
open import Cubical.Algebra.Polynomials.Multivariate.Properties

private variable
  ℓ ℓ' : Level

module _ (A' : CommRing ℓ) (n : ℕ) where

  private
    A = fst A'
    Ar = CommRing→Ring A'

  open CommRingStr
  open RingTheory Ar
  open Nth-Poly-structure A' n

  PolyCommRing : CommRing ℓ
  fst PolyCommRing = Poly A' n
  0r (snd PolyCommRing) = 0P
  1r (snd PolyCommRing) = 1P
  _+_ (snd PolyCommRing) = _Poly+_
  _·_ (snd PolyCommRing) = _Poly*_
  - snd PolyCommRing = Poly-inv
  isCommRing (snd PolyCommRing) = makeIsCommRing
                                  trunc
                                  Poly+-assoc
                                  Poly+-Rid
                                  Poly+-rinv
                                  Poly+-comm
                                  Poly*-assoc
                                  Poly*-Rid
                                  Poly*-Rdist
                                  Poly*-comm

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text: test = forall _0_ → Set


text:
module Human.List where

open import Human.Nat

infixr 5 _,_
data List {a} (A : Set a) : Set a where
  end : List A
  _,_ : (x : A) (xs : List A) → List A

{-# BUILTIN LIST List #-}

{-# COMPILE JS  List = function(x,v) { if (x.length < 1) { return v["[]"](); } else { return v["_∷_"](x[0], x.slice(1)); } } #-}
{-# COMPILE JS end = Array() #-}
{-# COMPILE JS _,_ = function (x) { return function(y) { return Array(x).concat(y); }; } #-}

foldr : ∀ {A : Set} {B : Set} → (A → B → B) → B → List A → B
foldr c n end       = n
foldr c n (x , xs) = c x (foldr c n xs)

length : ∀ {A : Set} → List A → Nat
length = foldr (λ a n → suc n) zero

max_stars_repo_name: MaisaMilena/AgdaCalculator

max_issues_repo_name: MaisaMilena/AgdaCalculator

max_forks_repo_name: MaisaMilena/AgdaCalculator


text:
module Auxiliary where

open import Agda.Primitive
open import Data.List
open import Data.Nat renaming (_+_ to _+ᴺ_ ; _≤_ to _≤ᴺ_ ; _≥_ to _≥ᴺ_ ; _<_ to _<ᴺ_ ; _>_ to _>ᴺ_)
open import Data.Nat.Properties
open import Data.Integer renaming (_+_ to _+ᶻ_ ; _≤_ to _≤ᶻ_ ; _≥_ to _≥ᶻ_ ; _<_ to _<ᶻ_ ; _>_ to _>ᶻ_)
import Data.Integer.Properties
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Data.Product
open import Data.Sum

-- natural numbers

n≢m⇒sucn≢sucm : {n m : ℕ} → n ≢ m → ℕ.suc n ≢ ℕ.suc m
n≢m⇒sucn≢sucm {n} {m} neq = λ x → contradiction (cong Data.Nat.pred x) neq

sucn≢sucm⇒n≢m : {n m : ℕ} → ℕ.suc n ≢ ℕ.suc m → n ≢ m
sucn≢sucm⇒n≢m {n} {m} neq = λ x → contradiction (cong ℕ.suc x) neq

n+1≡sucn : {n : ℕ} → n +ᴺ 1 ≡ ℕ.suc n
n+1≡sucn {zero} = refl
n+1≡sucn {ℕ.suc n} = cong ℕ.suc (n+1≡sucn{n})

n≤sucn : {n : ℕ} → n ≤ᴺ ℕ.suc n
n≤sucn {zero} = z≤n
n≤sucn {ℕ.suc n} = s≤s n≤sucn

n<sucn : {n : ℕ} → n <ᴺ ℕ.suc n
n<sucn {zero} = s≤s z≤n
n<sucn {ℕ.suc n} = s≤s n<sucn

m<n⇒m+o<n+o : {m n o : ℕ} → m <ᴺ n → m +ᴺ o <ᴺ n +ᴺ o
m<n⇒m+o<n+o {zero} {n} {o} le = m<n+m o le
m<n⇒m+o<n+o {ℕ.suc m} {ℕ.suc n} {o} (s≤s le) = s≤s (m<n⇒m+o<n+o le)

m≤n⇒m+o≤n+o : {m n o : ℕ} → m ≤ᴺ n → m +ᴺ o ≤ᴺ n +ᴺ o
m≤n⇒m+o≤n+o {zero} {n} {o} le = m≤n+m o n
m≤n⇒m+o≤n+o {ℕ.suc m} {ℕ.suc n} {o} (s≤s le) = s≤s (m≤n⇒m+o≤n+o le)

≤-refl-+-comm : {m n : ℕ} → m +ᴺ n ≤ᴺ n +ᴺ m
≤-refl-+-comm {m} {n} rewrite (+-comm m n) = ≤-refl

a<b≤c⇒a<c : {a b c : ℕ} → a <ᴺ b → b ≤ᴺ c → a <ᴺ c
a<b≤c⇒a<c {a} {b} {c} lt le = ≤-trans lt le

a≤b<c⇒a<c : {a b c : ℕ} → a ≤ᴺ b → b <ᴺ c → a <ᴺ c
a≤b<c⇒a<c {.0} {zero} {c} z≤n lt = lt
a≤b<c⇒a<c {.0} {ℕ.suc b} {ℕ.suc c} z≤n (s≤s lt) = s≤s z≤n
a≤b<c⇒a<c {.(ℕ.suc _)} {.(ℕ.suc _)} {ℕ.suc c} (s≤s le) (s≤s lt) = s≤s (a≤b<c⇒a<c le lt)

m≤n∧m≡q⇒q≤n : {m n q : ℕ} → m ≤ᴺ n → m ≡ q → q ≤ᴺ n
m≤n∧m≡q⇒q≤n {m} {n} {q} le eq rewrite eq = le

m≤n∧n≡q⇒m≤q : {m n q : ℕ} → m ≤ᴺ n → n ≡ q → m ≤ᴺ q
m≤n∧n≡q⇒m≤q le eq rewrite eq = le

n≤m⇒n≤sucm : {n m : ℕ} → n ≤ᴺ m → n ≤ᴺ ℕ.suc m
n≤m⇒n≤sucm {.0} {m} z≤n = z≤n
n≤m⇒n≤sucm {.(ℕ.suc _)} {.(ℕ.suc _)} (s≤s le) = s≤s (n≤m⇒n≤sucm le)

n≤m⇒n<sucm : {n m : ℕ} → n ≤ᴺ m → n <ᴺ ℕ.suc m
n≤m⇒n<sucm {n} {m} le = s≤s le

sucn≤m⇒n≤m : {n m : ℕ} → ℕ.suc n ≤ᴺ m → n ≤ᴺ m
sucn≤m⇒n≤m {n} {.(ℕ.suc _)} (s≤s le) = ≤-trans le n≤sucn

[k<x]⇒[k<x+1] : {x : ℕ} {k : ℕ} → (k <ᴺ x) → (k <ᴺ x +ᴺ 1)
[k<x]⇒[k<x+1]{x} {k} le = <-trans le (m<m+n x (s≤s z≤n))

[k<x]⇒[k<sucx] : {x : ℕ} {k : ℕ} → (k <ᴺ x) → (k <ᴺ ℕ.suc (x))
[k<x]⇒[k<sucx] {x} {k} le = <-trans le (s≤s ≤-refl)

¬[x≤k]⇒¬[sucx≤k] : {x : ℕ} {k : ℕ} → ¬ (x ≤ᴺ k) → ¬ ((x +ᴺ 1) ≤ᴺ k)
¬[x≤k]⇒¬[sucx≤k] {x} {k} nle = <⇒≱ ([k<x]⇒[k<x+1] (≰⇒> nle))

n+m≤n+q+m : {n m q : ℕ} → n +ᴺ m ≤ᴺ n +ᴺ (q +ᴺ m)
n+m≤n+q+m {n} {m} {q} rewrite (+-comm q m) | (sym (+-assoc n m q)) = m≤m+n (n +ᴺ m) q

m>n⇒m∸n≥1 : {m n : ℕ} → n <ᴺ m → m ∸ n ≥ᴺ 1
m>n⇒m∸n≥1 {ℕ.suc m} {zero} le = s≤s z≤n
m>n⇒m∸n≥1 {ℕ.suc m} {ℕ.suc n} (s≤s le) = m>n⇒m∸n≥1 le

m∸n≥q⇒m≥q : {m n q : ℕ} → m ∸ n ≥ᴺ q → m ≥ᴺ q
m∸n≥q⇒m≥q {m} {n} {q} ge = ≤-trans ge (m∸n≤m m n)

-- lists & length

++-assoc : {a : Level} {s : Set a} {Δ ∇ Γ : List s} → ((Δ ++ ∇) ++ Γ) ≡ (Δ ++ (∇ ++ Γ))
++-assoc {a} {s} {[]} {∇} {Γ} = refl
++-assoc {a} {s} {x ∷ Δ} {∇} {Γ} = cong (_∷_ x) (++-assoc{a}{s}{Δ}{∇}{Γ})

length[A]≥0 : {a : Level} {s : Set a} {A : List s} → length A ≥ᴺ 0
length[A]≥0 {a} {s} {A} = z≤n

A++[]≡A : {a : Level} {s : Set a} {A : List s} → A ++ [] ≡ A
A++[]≡A {a} {s} {[]} = refl
A++[]≡A {a} {s} {x ∷ A} = cong (_∷_ x) (A++[]≡A {a} {s} {A})

n+length[]≡n : {a : Level} {A : Set a} {n : ℕ} → n +ᴺ length{a}{A} [] ≡ n
n+length[]≡n {a} {A} {zero} = refl
n+length[]≡n {a} {A} {ℕ.suc n} = cong ℕ.suc (n+length[]≡n{a}{A})

length[A∷B]≡suc[length[B]] : {a : Level} {s : Set a} {A : s} {B : List s} → length (A ∷ B) ≡ ℕ.suc (length B)
length[A∷B]≡suc[length[B]] {a} {s} {A} {B} = refl

length[A∷B]≥1 : {a : Level} {s : Set a} {A : s} {B : List s} → length (A ∷ B) ≥ᴺ 1
length[A∷B]≥1 {a} {s} {A} {B} = s≤s z≤n

length[A++B]≡length[A]+length[B] : {a : Level} {s : Set a} {A B : List s} → length (A ++ B) ≡ length A +ᴺ length B
length[A++B]≡length[A]+length[B] {a} {s} {[]} {B} = refl
length[A++B]≡length[A]+length[B] {a} {s} {x ∷ A} {B} rewrite length[A∷B]≡suc[length[B]]{a}{s}{x}{A ++ B} = cong ℕ.suc (length[A++B]≡length[A]+length[B]{a}{s}{A}{B})

length[A++B∷[]]≡suc[length[A]] : {a : Level} {s : Set a} {A : List s} {B : s} → length (A ++ B ∷ []) ≡ ℕ.suc (length A)
length[A++B∷[]]≡suc[length[A]] {a} {s} {A} {B} rewrite (length[A++B]≡length[A]+length[B]{a}{s}{A}{B ∷ []}) = n+1≡sucn

A++B∷[]++C≡A++B∷C : {a : Level} {s : Set a} {A C : List s} {B : s} → ((A ++ B ∷ []) ++ C) ≡ (A ++ B ∷ C)
A++B∷[]++C≡A++B∷C {a} {s} {[]} {C} {B} = refl
A++B∷[]++C≡A++B∷C {a} {s} {x ∷ A} {C} {B} = cong (_∷_ x) A++B∷[]++C≡A++B∷C

A++B++D∷[]++C≡A++B++D∷C : {a : Level} {s : Set a} { A B C : List s} {D : s} → (A ++ B ++ D ∷ []) ++ C ≡ (A ++ B ++ D ∷ C)
A++B++D∷[]++C≡A++B++D∷C {a} {s} {[]} {B} {C} {D} = A++B∷[]++C≡A++B∷C
A++B++D∷[]++C≡A++B++D∷C {a} {s} {x ∷ A} {B} {C} {D} = cong (_∷_ x) (A++B++D∷[]++C≡A++B++D∷C{a}{s}{A}{B}{C}{D})

-- integers

m≥0⇒n+m≥0 : {n : ℕ} {m : ℤ} → m ≥ᶻ +0 → + n +ᶻ m ≥ᶻ +0
m≥0⇒n+m≥0 {n} {+_ m} ge = +≤+ z≤n

n>0⇒n>∣n⊖1∣ : {n : ℕ} → n ≥ᴺ 1 → n >ᴺ ∣ n ⊖ 1 ∣
n>0⇒n>∣n⊖1∣ {.(ℕ.suc _)} (s≤s le) = n<sucn

∣nℕ+1⊖1∣≡n : {n : ℕ} → ∣ n +ᴺ 1 ⊖ 1 ∣ ≡ n
∣nℕ+1⊖1∣≡n {zero} = refl
∣nℕ+1⊖1∣≡n {ℕ.suc n} = n+1≡sucn

m≥0⇒∣n+m∣≥n : {n : ℕ} {m : ℤ} → m ≥ᶻ +0 → ∣ +_ n +ᶻ m ∣ ≥ᴺ n
m≥0⇒∣n+m∣≥n {n} {+_ m} ge = m≤m+n n m

m>0⇒∣n+m∣>n : {n : ℕ} {m : ℤ} → m >ᶻ +0 → ∣ +_ n +ᶻ m ∣ >ᴺ n
m>0⇒∣n+m∣>n {n} {(+ m)} (+<+ m<n) = m<m+n n m<n

∣n∣≥n : {n : ℤ} → + ∣ n ∣ ≥ᶻ n
∣n∣≥n {+_ n} = +≤+ ≤-refl
∣n∣≥n { -[1+_] n} = -≤+

+a≤b⇒a≤∣b∣ : {a : ℕ} {b : ℤ} → + a ≤ᶻ b → a ≤ᴺ ∣ b ∣
+a≤b⇒a≤∣b∣ {zero} {b} le = z≤n
+a≤b⇒a≤∣b∣ {ℕ.suc a} {(+ b)} (+≤+ m≤n) = m≤n

+[1+q]≡q+1 : {q : ℕ} → +[1+ q ] ≡ + q +ᶻ + 1
+[1+q]≡q+1 {zero} = refl
+[1+q]≡q+1 {ℕ.suc q} = cong +[1+_] (sym n+1≡sucn)

+q≤+c+l⇒+1q≤+1c+l : {q c : ℕ} {l : ℤ} → + q ≤ᶻ + c +ᶻ l → +[1+ q ] ≤ᶻ +[1+ c ] +ᶻ l
+q≤+c+l⇒+1q≤+1c+l {q} {c} {l} le
  rewrite (+[1+q]≡q+1{q})
        | (+[1+q]≡q+1{c})
        | (Data.Integer.Properties.+-assoc (+ c) (+ 1) l)
        | (Data.Integer.Properties.+-comm (+ 1) l)
        | (sym (Data.Integer.Properties.+-assoc (+ c) (l) (+ 1)))
        = Data.Integer.Properties.+-monoˡ-≤ (+ 1) le

ℤ-m≤n⇒m+o≤n+o : {m n o : ℤ} → m ≤ᶻ n → m +ᶻ o ≤ᶻ n +ᶻ o
ℤ-m≤n⇒m+o≤n+o {m} {n} {o} le = Data.Integer.Properties.+-monoˡ-≤ o le

minus-1 : {y x : ℕ} {lt : x <ᴺ y} → ∣ y ∸ x ⊖ 1 ∣ +ᴺ x ≡ ∣ y ⊖ 1 ∣
minus-1 {y} {x} {lt}
  rewrite (Data.Integer.Properties.⊖-≥{y ∸ x}{1} (m>n⇒m∸n≥1 lt))
        | (sym (+-∸-comm {y ∸ x} x {1} (m>n⇒m∸n≥1 lt)))
        | (m∸n+n≡m {y} {x} (sucn≤m⇒n≤m lt))
        | (Data.Integer.Properties.⊖-≥{y}{1} ((m∸n≥q⇒m≥q{y}{x} (m>n⇒m∸n≥1{y}{x} lt))))
        = refl

k≥0⇒∣+x+k∣≡x+k : {x k : ℕ} → ∣ + x +ᶻ + k ∣ ≡ x +ᴺ k
k≥0⇒∣+x+k∣≡x+k {x} {k} = refl

-- products & sums

-- deMorgan on products and sums
dm1 : {P Q : Set} → (¬ P × ¬ Q) → ¬ (P ⊎ Q)
dm1 {P} {Q} (fst , snd) (inj₁ x) = contradiction x fst
dm1 {P} {Q} (fst , snd) (inj₂ y) = contradiction y snd

dm2 : {P Q : Set} → ¬ (P ⊎ Q) → (¬ P × ¬ Q)
dm2 {P} {Q} d = (λ x → contradiction (inj₁ x) d) , λ x → contradiction (inj₂ x) d

max_stars_repo_name: kcaliban/ldlc

max_issues_repo_name: kcaliban/ldlc

max_forks_repo_name: kcaliban/ldlc


text:
{-# OPTIONS --experimental-irrelevance #-}
module ShapeIrrelevantParameterNoBecauseOfRecursion where

data ⊥ : Set where
record ⊤ : Set where

data Bool : Set where
  true false : Bool

True : Bool → Set
True false = ⊥
True true  = ⊤

data D ..(b : Bool) : Set where
  c : True b → D b  -- should fail

-- Jesper, 2017-09-14: I think the definition of D is fine, but the definition
-- of cast below should fail since `D a` and `D b` are different types.

fromD : {b : Bool} → D b → True b
fromD (c p) = p

cast : .(a b : Bool) → D a → D b
cast _ _ x = x

bot : ⊥
bot = fromD (cast true false (c _))

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


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

-- Definition of Monoidal Category

-- Big design decision that differs from the previous version:
-- Do not go through "Functor.Power" to encode variables and work
-- at the level of NaturalIsomorphisms, instead work at the object/morphism
-- level, via the more direct _⊗₀_ _⊗₁_ _⊗- -⊗_.
-- The original design needed quite a few contortions to get things working,
-- but these are simply not needed when working directly with the morphisms.
--
-- Smaller design decision: export some items with long names
-- (unitorˡ, unitorʳ and associator), but internally work with the more classical
-- short greek names (λ, ρ and α respectively).

module Categories.Category.Monoidal.Core {o ℓ e} (C : Category o ℓ e) where

open import Level
open import Function using (_$_)
open import Data.Product using (_×_; _,_; curry′)

open import Categories.Category.Product
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Bifunctor using (Bifunctor; appˡ; appʳ)
open import Categories.Functor.Properties using ([_]-resp-≅)
open import Categories.NaturalTransformation renaming (id to idN)
open import Categories.NaturalTransformation.NaturalIsomorphism
  hiding (unitorˡ; unitorʳ; associator; _≃_)
open import Categories.Morphism C using (_≅_; module ≅)
open import Categories.Morphism.IsoEquiv C using (_≃_; ⌞_⌟)
open import Categories.Morphism.Isomorphism C using (_∘ᵢ_; lift-triangle′; lift-pentagon′)
open import Categories.Morphism.Reasoning C

private
  module C = Category C

open C hiding (id; identityˡ; identityʳ; assoc)
open Commutation

private
  variable
    X Y Z W A B : Obj
    f g h i a b : X ⇒ Y

record Monoidal : Set (o ⊔ ℓ ⊔ e) where
  infixr 10 _⊗₀_ _⊗₁_

  field
    ⊗  : Bifunctor C C C
    unit : Obj

  open Functor ⊗

  _⊗₀_ : Obj → Obj → Obj
  _⊗₀_ = curry′ F₀

  -- this is also 'curry', but a very-dependent version
  _⊗₁_ : X ⇒ Y → Z ⇒ W → X ⊗₀ Z ⇒ Y ⊗₀ W
  f ⊗₁ g = F₁ (f , g)

  _⊗- : Obj → Functor C C
  X ⊗- = appˡ ⊗ X

  -⊗_ : Obj → Functor C C
  -⊗ X = appʳ ⊗ X

  field
    unitorˡ    : unit ⊗₀ X ≅ X
    unitorʳ    : X ⊗₀ unit ≅ X
    associator : (X ⊗₀ Y) ⊗₀ Z ≅ X ⊗₀ (Y ⊗₀ Z)

  module unitorˡ {X} = _≅_ (unitorˡ {X = X})
  module unitorʳ {X} = _≅_ (unitorʳ {X = X})
  module associator {X} {Y} {Z} = _≅_ (associator {X} {Y} {Z})

  -- for exporting, it makes sense to use the above long names, but for
  -- internal consumption, the traditional (short!) categorical names are more
  -- convenient. However, they are not symmetric, even though the concepts are, so
  -- we'll use ⇒ and ⇐ arrows to indicate that

  private
    λ⇒ = unitorˡ.from
    λ⇐ = unitorˡ.to
    ρ⇒ = unitorʳ.from
    ρ⇐ = unitorʳ.to
    -- eta expansion fixes a problem in 2.6.1, will be reported
    α⇒ = λ {X} {Y} {Z} → associator.from {X} {Y} {Z}
    α⇐ = λ {X} {Y} {Z} → associator.to {X} {Y} {Z}

  field
    unitorˡ-commute-from : CommutativeSquare (C.id ⊗₁ f) λ⇒ λ⇒ f
    unitorˡ-commute-to   : CommutativeSquare f λ⇐ λ⇐ (C.id ⊗₁ f)
    unitorʳ-commute-from : CommutativeSquare (f ⊗₁ C.id) ρ⇒ ρ⇒ f
    unitorʳ-commute-to   : CommutativeSquare f ρ⇐ ρ⇐ (f ⊗₁ C.id)
    assoc-commute-from   : CommutativeSquare ((f ⊗₁ g) ⊗₁ h) α⇒ α⇒ (f ⊗₁ (g ⊗₁ h))
    assoc-commute-to     : CommutativeSquare (f ⊗₁ (g ⊗₁ h)) α⇐ α⇐ ((f ⊗₁ g) ⊗₁ h)
    triangle             : [ (X ⊗₀ unit) ⊗₀ Y ⇒ X ⊗₀ Y ]⟨
                             α⇒           ⇒⟨ X ⊗₀ (unit ⊗₀ Y) ⟩
                             C.id ⊗₁ λ⇒
                           ≈ ρ⇒ ⊗₁ C.id
                           ⟩
    pentagon             : [ ((X ⊗₀ Y) ⊗₀ Z) ⊗₀ W ⇒ X ⊗₀ Y ⊗₀ Z ⊗₀ W ]⟨
                             α⇒ ⊗₁ C.id       ⇒⟨ (X ⊗₀ Y ⊗₀ Z) ⊗₀ W ⟩
                             α⇒               ⇒⟨ X ⊗₀ (Y ⊗₀ Z) ⊗₀ W ⟩
                             C.id ⊗₁ α⇒
                           ≈ α⇒               ⇒⟨ (X ⊗₀ Y) ⊗₀ Z ⊗₀ W ⟩
                             α⇒
                           ⟩

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
module Prelude.Show where

open import Prelude.Unit
open import Prelude.String
open import Prelude.Char
open import Prelude.Nat
open import Prelude.Int
open import Prelude.Word
open import Prelude.Function
open import Prelude.List
open import Prelude.Fin
open import Prelude.Vec
open import Prelude.Maybe
open import Prelude.Sum
open import Prelude.Product
open import Prelude.Bool
open import Prelude.Ord
open import Prelude.Semiring

--- Class ---

ShowS = String → String

showString : String → ShowS
showString s r = s & r

showParen : Bool → ShowS → ShowS
showParen false s = s
showParen true  s = showString "(" ∘ s ∘ showString ")"

record Show {a} (A : Set a) : Set a where
  field
    showsPrec : Nat → A → ShowS

  show : A → String
  show x = showsPrec 0 x ""

  shows : A → ShowS
  shows = showsPrec 0

open Show {{...}} public

simpleShowInstance : ∀ {a} {A : Set a} → (A → String) → Show A
showsPrec {{simpleShowInstance s}} _ x = showString (s x)

ShowBy : ∀ {a b} {A : Set a} {B : Set b} {{ShowB : Show B}} → (A → B) → Show A
showsPrec {{ShowBy f}} p = showsPrec p ∘ f

--- Instances ---

-- Bool --

instance
  ShowBool : Show Bool
  ShowBool = simpleShowInstance λ b → if b then "true" else "false"

-- Int --

instance
  ShowInt : Show Int
  ShowInt = simpleShowInstance primShowInteger

-- Nat --

instance
  ShowNat : Show Nat
  ShowNat = simpleShowInstance (primShowInteger ∘ pos)

-- Word64 --

instance
  ShowWord64 : Show Word64
  ShowWord64 = simpleShowInstance (show ∘ word64ToNat)

-- Char --

instance
  ShowChar : Show Char
  ShowChar = simpleShowInstance primShowChar

-- String --

instance
  ShowString : Show String
  ShowString = simpleShowInstance primShowString

-- List --

instance
  ShowList : ∀ {a} {A : Set a} {{ShowA : Show A}} → Show (List A)
  showsPrec {{ShowList}} _ []       = showString "[]"
  showsPrec {{ShowList}} _ (x ∷ xs) =
    showString "["
    ∘ foldl (λ r x → r ∘ showString ", " ∘ showsPrec 2 x) (showsPrec 2 x) xs
    ∘ showString "]"

-- Fin --

instance
  ShowFin : ∀ {n} → Show (Fin n)
  ShowFin = simpleShowInstance (show ∘ finToNat)

-- Vec --

instance
  ShowVec : ∀ {a} {A : Set a} {n} {{ShowA : Show A}} → Show (Vec A n)
  ShowVec = ShowBy vecToList

-- Maybe --

instance
  ShowMaybe : ∀ {a} {A : Set a} {{ShowA : Show A}} → Show (Maybe A)
  showsPrec {{ShowMaybe}} p nothing  = showString "nothing"
  showsPrec {{ShowMaybe}} p (just x) = showParen (p >? 9) (showString "just " ∘ showsPrec 10 x)

-- Either --

instance
  ShowEither : ∀ {a b} {A : Set a} {B : Set b} {{ShowA : Show A}} {{ShowB : Show B}} → Show (Either A B)
  showsPrec {{ShowEither}} p (left  x) = showParen (p >? 9) $ showString "left " ∘ showsPrec 10 x
  showsPrec {{ShowEither}} p (right x) = showParen (p >? 9) $ showString "right " ∘ showsPrec 10 x

-- Sigma --

instance
  ShowSigma : ∀ {a b} {A : Set a} {B : A → Set b} {{ShowA : Show A}} {{ShowB : ∀ {x} → Show (B x)}} →
                Show (Σ A B)
  showsPrec {{ShowSigma}} p (x , y) = showParen (p >? 1) $ showsPrec 2 x ∘ showString ", " ∘ showsPrec 1 y

max_stars_repo_name: t-more/agda-prelude

max_issues_repo_name: t-more/agda-prelude

max_forks_repo_name: t-more/agda-prelude


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

open import Agda.Builtin.Reflection
open import Agda.Builtin.List
open import Agda.Builtin.Unit
_>>=_ = bindTC
return = returnTC

postulate
  X : Prop
  x₀ : X

f : X
f = x₀

macro
  getValue : Name → Term → TC ⊤
  getValue s _ = do
    function (clause _ _ t ∷ []) ← getDefinition s
      where _ → typeError (strErr "Not a defined name" ∷ [])
    typeError (strErr "The value of " ∷ nameErr s ∷ strErr " is " ∷ termErr t ∷ [])

test = getValue f

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
------------------------------------------------------------------------------
-- Equality on Conat
------------------------------------------------------------------------------

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

module FOTC.Data.Conat.Equality.Type where

open import FOTC.Base

infix 4 _≈_

------------------------------------------------------------------------------
-- Functional for the relation _≈_ (adapted from (Sander 1992,
-- p. 58)).
--
-- ≈-F : (D → D → Set) → D → D → Set
-- ≈-F R m n =
-- (m ≡ zero ∧ n ≡ zero) ∨ (∃[ m' ] ∃[ n' ] m ≡ succ m' ∧ n ≡ succ n' ∧ R m' n')

-- The relation _≈_ is the greatest post-fixed point of the functional
-- ≈-F (by ≈-out and ≈-coind).

-- The equality on Conat.
postulate _≈_ : D → D → Set

-- The relation _≈_ is a post-fixed point of the functional ≈-F,
-- i.e.
--
-- _≈_ ≤ ≈-F _≈_.
postulate ≈-out : ∀ {m n} → m ≈ n →
                  m ≡ zero ∧ n ≡ zero
                  ∨ (∃[ m' ] ∃[ n' ] m ≡ succ₁ m' ∧ n ≡ succ₁ n' ∧ m' ≈ n')
{-# ATP axiom ≈-out #-}

-- The relation _N≈_ is the greatest post-fixed point of _N≈_, i.e.
--
-- ∀ R. R ≤ ≈-F R ⇒ R ≤ _N≈_.
--
-- N.B. This is an axiom schema. Because in the automatic proofs we
-- *must* use an instance, we do not add this postulate as an ATP
-- axiom.
postulate
  ≈-coind :
    (R : D → D → Set) →
    -- R is a post-fixed point of the functional ≈-F.
    (∀ {m n} → R m n → m ≡ zero ∧ n ≡ zero
      ∨ (∃[ m' ] ∃[ n' ] m ≡ succ₁ m' ∧ n ≡ succ₁ n' ∧ R m' n')) →
    -- _≈_ is greater than R.
    ∀ {m n} → R m n → m ≈ n

------------------------------------------------------------------------------
-- References
--
-- Sander, Herbert P. (1992). A Logic of Functional Programs with an
-- Application to Concurrency. PhD thesis. Department of Computer
-- Sciences: Chalmers University of Technology and University of
-- Gothenburg.

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 lib.Basics
open import lib.NType2
open import lib.Equivalence2
open import lib.path-seq.Rotations
open import lib.types.Unit
open import lib.types.Nat
open import lib.types.Pi
open import lib.types.Pointed
open import lib.types.Sigma
open import lib.types.Paths
open import lib.types.TLevel
open import lib.types.Truncation

module lib.NConnected where

is-connected : ∀ {i} → ℕ₋₂ → Type i → Type i
is-connected n A = is-contr (Trunc n A)

has-conn-fibers : ∀ {i j} {A : Type i} {B : Type j} → ℕ₋₂ → (A → B) → Type (lmax i j)
has-conn-fibers {A = A} {B = B} n f =
  Π B (λ b → is-connected n (hfiber f b))

{- all types are -2-connected -}
-2-conn : ∀ {i} (A : Type i) → is-connected -2 A
-2-conn A = Trunc-level

{- all inhabited types are -1-connected -}
inhab-conn : ∀ {i} {A : Type i} (a : A) → is-connected -1 A
inhab-conn a = has-level-in ([ a ] , prop-has-all-paths [ a ])

{- connectedness is a prop -}
is-connected-is-prop : ∀ {i} {n : ℕ₋₂} {A : Type i}
  → is-prop (is-connected n A)
is-connected-is-prop = is-contr-is-prop

{- "induction principle" for n-connected maps (where codomain is n-type) -}
module ConnExtend {i j k} {A : Type i} {B : Type j} {n : ℕ₋₂}
                  {h : A → B} (c : has-conn-fibers n h)
                  (P : B → n -Type k) where

  private
    helper : Π A (fst ∘ P ∘ h)
      → (b : B) → Trunc n (Σ A (λ a → h a == b)) → (fst (P b))
    helper t b r =
      Trunc-rec {{snd (P b)}}
        (λ x → transport (λ y → fst (P y)) (snd x) (t (fst x)))
        r

  restr : Π B (fst ∘ P) → Π A (fst ∘ P ∘ h)
  restr t = t ∘ h

  abstract
    ext : Π A (fst ∘ P ∘ h) → Π B (fst ∘ P)
    ext f b = helper f b (contr-center (c b))

  private
    abstract
      ext-β' : (f : Π A (fst ∘ P ∘ h)) (a : A) → restr (ext f) a == f a
      ext-β' f a =
        transport
          (λ r →  Trunc-rec {{snd (P (h a))}} _ r == f a)
          (! (contr-path(c (h a)) [ (a , idp) ]))
          idp

  abstract
    restr-β : (t : Π B (fst ∘ P)) (b : B) → ext (restr t) b == t b
    restr-β t b =
      Trunc-elim
        {{λ r → =-preserves-level {x = helper (t ∘ h) b r} (snd (P b))}}
        (λ x → lemma (fst x) b (snd x))
        (contr-center (c b))
      where
      lemma : ∀ xl → ∀ b → (p : h xl == b) →
        helper (t ∘ h) b [ (xl , p) ] == t b
      lemma xl ._ idp = idp

  restr-is-equiv : is-equiv restr
  restr-is-equiv = is-eq restr ext (λ= ∘ ext-β') (λ= ∘ restr-β)

  restr-equiv : Π B (fst ∘ P) ≃ Π A (fst ∘ P ∘ h)
  restr-equiv = restr , restr-is-equiv

  ext-β : (f : Π A (fst ∘ P ∘ h)) (a : A) → restr (ext f) a == f a
  ext-β f = app= (is-equiv.f-g restr-is-equiv f)

  abstract
    restr-β-ext-β-adj : (t : Π B (fst ∘ P)) (a : A)
      → ext-β (restr t) a == restr-β t (h a)
    restr-β-ext-β-adj t a =
      ext-β (restr t) a
        =⟨ ! (ap (λ s → app= s a) (is-equiv.adj restr-is-equiv t)) ⟩
      app= (ap restr (λ= (restr-β t))) a
        =⟨ ∘-ap (_$ a) restr (λ= (restr-β t)) ⟩
      app= (λ= (restr-β t)) (h a)
        =⟨ app=-β (restr-β t) (h a) ⟩
      restr-β t (h a) =∎

open ConnExtend using () renaming
  (ext to conn-extend;
   ext-β to conn-extend-β;
   restr-is-equiv to pre∘-conn-is-equiv) public

module ⊙ConnExtend {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k} {n : ℕ₋₂}
                   (h : X ⊙→ Y) (c : has-conn-fibers n (fst h))
                   (Z-level : has-level n (de⊙ Z)) where

  open ConnExtend c (λ _ → de⊙ Z , Z-level) public

  ⊙restr : Y ⊙→ Z → X ⊙→ Z
  ⊙restr = _⊙∘ h

  ext-pt-seq : (f : X ⊙→ Z) → ext (fst f) (pt Y) =-= pt Z
  ext-pt-seq f =
    ext (fst f) (pt Y)
      =⟪ ! (ap (ext (fst f)) (snd h)) ⟫
    ext (fst f) (fst h (pt X))
      =⟪ ext-β (fst f) (pt X) ⟫
    fst f (pt X)
      =⟪ snd f ⟫
    pt Z ∎∎

  ext-pt : (f : X ⊙→ Z) → ext (fst f) (pt Y) == pt Z
  ext-pt f = ↯ (ext-pt-seq f)

  ⊙ext : X ⊙→ Z → Y ⊙→ Z
  ⊙ext f = ext (fst f) , ext-pt f

  abstract
    ⊙ext-β : (f : X ⊙→ Z) → ⊙restr (⊙ext f) == f
    ⊙ext-β f =
      ⊙λ=' (ext-β (fst f)) $
      ↓-idf=cst-in $ =ₛ-out $
      ap (fst (⊙ext f)) (snd h) ◃∙ ext-pt-seq f
        =ₛ⟨ 0 & 2 & seq-!-inv-r (ap (fst (⊙ext f)) (snd h) ◃∎) ⟩
      ext-β (fst f) (pt X) ◃∙ snd f ◃∎ ∎ₛ

    ⊙restr-β : (t : Y ⊙→ Z) → ⊙ext (⊙restr t) == t
    ⊙restr-β t =
      ⊙λ=' (restr-β (fst t)) $
      ↓-idf=cst-in $ =ₛ-out $
      ext-pt-seq (⊙restr t)
        =ₛ₁⟨ 1 & 1 & restr-β-ext-β-adj (fst t) (pt X) ⟩
      ! (ap (ext (fst (⊙restr t))) (snd h)) ◃∙
      restr-β (fst t) (fst h (pt X)) ◃∙
      snd (⊙restr t) ◃∎
        =ₛ⟨ 2 & 1 & expand (ap (fst t) (snd h) ◃∙ snd t ◃∎) ⟩
      ! (ap (ext (fst (⊙restr t))) (snd h)) ◃∙
      restr-β (fst t) (fst h (pt X)) ◃∙
      ap (fst t) (snd h) ◃∙
      snd t ◃∎
        =ₛ⟨ 0 & 3 & !ₛ $ pre-rotate-in $
            homotopy-naturality
              (ext (fst (⊙restr t)))
              (fst t)
              (restr-β (fst t))
              (snd h) ⟩
      restr-β (fst t) (pt Y) ◃∙ snd t ◃∎ ∎ₛ

  ⊙restr-is-equiv : is-equiv ⊙restr
  ⊙restr-is-equiv = is-eq ⊙restr ⊙ext ⊙ext-β ⊙restr-β

  ⊙restr-equiv : (Y ⊙→ Z) ≃ (X ⊙→ Z)
  ⊙restr-equiv = ⊙restr , ⊙restr-is-equiv

open ⊙ConnExtend using () renaming
  (⊙ext to ⊙conn-extend;
   ⊙restr-is-equiv to pre⊙∘-conn-is-equiv) public

{- generalized "almost induction principle" for maps into ≥n-types
   TODO: rearrange this to use ≤T?                                 -}
conn-extend-general : ∀ {i j} {A : Type i} {B : Type j} {n k : ℕ₋₂}
  → {f : A → B} → has-conn-fibers n f
  → ∀ {l} (P : B → (k +2+ n) -Type l)
  → ∀ t → has-level k (Σ (Π B (fst ∘ P)) (λ s → (s ∘ f) == t))
conn-extend-general {k = ⟨-2⟩} c P t =
  equiv-is-contr-map (pre∘-conn-is-equiv c P) t
conn-extend-general {B = B} {n = n} {k = S k'} {f = f} c P t = has-level-in
  λ {(g , p) (h , q) →
    equiv-preserves-level (e g h p q)
      {{conn-extend-general {k = k'} c (Q g h) (app= (p ∙ ! q))}} }
  where
    Q : (g h : Π B (fst ∘ P)) → B → (k' +2+ n) -Type _
    Q g h b = ((g b == h b) , has-level-apply (snd (P b)) _ _)

    app=-pre∘ : ∀ {i j k} {A : Type i} {B : Type j} {C : B → Type k}
      (f : A → B) {g h : Π B C} (p : g == h)
      → app= (ap (λ k → k ∘ f) p) == app= p ∘ f
    app=-pre∘ f idp = idp

    move-right-on-right-econv : ∀ {i} {A : Type i} {x y z : A}
      (p : x == y) (q : x == z) (r : y == z)
      → (p == q ∙ ! r) ≃ (p ∙ r == q)
    move-right-on-right-econv {x = x} p idp idp =
      (_ , pre∙-is-equiv (∙-unit-r p))

    lemma : ∀ g h p q → (H : g ∼ h)
      → ((H ∘ f) == app= (p ∙ ! q))
         ≃ (ap (λ v → v ∘ f) (λ= H) ∙ q == p)
    lemma g h p q H =
      move-right-on-right-econv (ap (λ v → v ∘ f) (λ= H)) p q
      ∘e transport (λ w → (w == app= (p ∙ ! q))
                      ≃ (ap (λ v → v ∘ f) (λ= H) == p ∙ ! q))
                   (app=-pre∘ f (λ= H) ∙ ap (λ k → k ∘ f) (λ= $ app=-β H))
                   (ap-equiv app=-equiv _ _ ⁻¹)

    e : ∀ g h p q  →
      (Σ (g ∼ h) (λ r → (r ∘ f) == app= (p ∙ ! q)))
      ≃ ((g , p) == (h , q))
    e g h p q =
      ((=Σ-econv _ _ ∘e Σ-emap-r (λ u → ↓-app=cst-econv ∘e !-equiv))
      ∘e (Σ-emap-l _ λ=-equiv)) ∘e Σ-emap-r (lemma g h p q)

conn-in : ∀ {i j} {A : Type i} {B : Type j} {n : ℕ₋₂} {h : A → B}
  → (∀ (P : B → n -Type (lmax i j))
     → Σ (Π A (fst ∘ P ∘ h) → Π B (fst ∘ P))
         (λ u → ∀ (t : Π A (fst ∘ P ∘ h)) → u t ∘ h ∼ t))
  → has-conn-fibers n h
conn-in {A = A} {B = B} {h = h} sec b =
  let s = sec (λ b → (Trunc _ (hfiber h b) , Trunc-level))
  in has-level-in (fst s (λ a → [ a , idp ]) b ,
      Trunc-elim (λ k → transport
                   (λ v → fst s (λ a → [ a , idp ]) (fst v) == [ fst k , snd v ])
                   (contr-path (pathfrom-is-contr (h (fst k))) (b , snd k))
                   (snd s (λ a → [ a , idp ]) (fst k))))

abstract
  pointed-conn-in : ∀ {i} {n : ℕ₋₂} (A : Type i) (a₀ : A)
    → has-conn-fibers {A = ⊤} n (cst a₀) → is-connected (S n) A
  pointed-conn-in {n = n} A a₀ c = has-level-in
    ([ a₀ ] ,
     Trunc-elim
       (λ a → Trunc-rec
             (λ x → ap [_] (snd x)) (contr-center $ c a)))

abstract
  pointed-conn-out : ∀ {i} {n : ℕ₋₂} (A : Type i) (a₀ : A)
    {{_ : is-connected (S n) A}} → has-conn-fibers {A = ⊤} n (cst a₀)
  pointed-conn-out {n = n} A a₀ {{c}} a = has-level-in
    (point ,
     λ y → ! (cancel point)
           ∙ (ap out $ contr-has-all-paths (into point) (into y))
           ∙ cancel y)
    where
      into-aux : Trunc n (Σ ⊤ (λ _ → a₀ == a)) → Trunc n (a₀ == a)
      into-aux = Trunc-fmap snd

      into : Trunc n (Σ ⊤ (λ _ → a₀ == a))
        → [_] {n = S n} a₀ == [ a ]
      into = <– (=ₜ-equiv [ a₀ ] [ a ]) ∘ into-aux

      out-aux : Trunc n (a₀ == a) → Trunc n (Σ ⊤ (λ _ → a₀ == a))
      out-aux = Trunc-fmap (λ p → (tt , p))

      out : [_] {n = S n} a₀ == [ a ] → Trunc n (Σ ⊤ (λ _ → a₀ == a))
      out = out-aux ∘ –> (=ₜ-equiv [ a₀ ] [ a ])

      cancel : (x : Trunc n (Σ ⊤ (λ _ → a₀ == a))) → out (into x) == x
      cancel x =
        out (into x)
          =⟨ ap out-aux (<–-inv-r (=ₜ-equiv [ a₀ ] [ a ]) (into-aux x)) ⟩
        out-aux (into-aux x)
          =⟨ Trunc-fmap-∘ _ _ x ⟩
        Trunc-fmap (λ q → (tt , (snd q))) x
          =⟨ Trunc-elim {P = λ x → Trunc-fmap (λ q → (tt , snd q)) x == x}
               (λ _ → idp) x ⟩
        x =∎

      point : Trunc n (Σ ⊤ (λ _ → a₀ == a))
      point = out $ contr-has-all-paths [ a₀ ] [ a ]

prop-over-connected :  ∀ {i j} {A : Type i} {a : A} {{p : is-connected 0 A}}
  → (P : A → hProp j)
  → fst (P a) → Π A (fst ∘ P)
prop-over-connected P x = conn-extend (pointed-conn-out _ _) P (λ _ → x)

{- Connectedness of a truncated type -}
instance
  Trunc-preserves-conn : ∀ {i} {A : Type i} {n : ℕ₋₂} {m : ℕ₋₂}
    → is-connected n A → is-connected n (Trunc m A)
  Trunc-preserves-conn {n = ⟨-2⟩} _ = Trunc-level
  Trunc-preserves-conn {A = A} {n = S n} {m} c = lemma (contr-center c) (contr-path c)
    where
    lemma : (x₀ : Trunc (S n) A) → (∀ x → x₀ == x) → is-connected (S n) (Trunc m A)
    lemma = Trunc-elim
      (λ a → λ p → has-level-in ([ [ a ] ] ,
        Trunc-elim
          (Trunc-elim
            {{λ _ → =-preserves-level
                      (Trunc-preserves-level (S n) Trunc-level)}}
            (λ x → <– (=ₜ-equiv [ [ a ] ] [ [ x ] ])
               (Trunc-fmap (ap [_])
                 (–> (=ₜ-equiv [ a ] [ x ]) (p [ x ])))))))

{- Connectedness of a Σ-type -}
abstract
 instance
  Σ-conn : ∀ {i} {j} {A : Type i} {B : A → Type j} {n : ℕ₋₂}
    → is-connected n A → (∀ a → is-connected n (B a))
    → is-connected n (Σ A B)
  Σ-conn {A = A} {B = B} {n = ⟨-2⟩} cA cB = -2-conn (Σ A B)
  Σ-conn {A = A} {B = B} {n = S m} cA cB =
    Trunc-elim
      {P = λ ta → (∀ tx → ta == tx) → is-connected (S m) (Σ A B)}
      (λ a₀ pA →
        Trunc-elim
          {P = λ tb → (∀ ty → tb == ty) → is-connected (S m) (Σ A B)}
          (λ b₀ pB → has-level-in
            ([ a₀ , b₀ ] ,
              Trunc-elim
                {P = λ tp → [ a₀ , b₀ ] == tp}
                (λ {(r , s) →
                  Trunc-rec
                    (λ pa → Trunc-rec
                      (λ pb → ap [_] (pair= pa (from-transp! B pa pb)))
                      (–> (=ₜ-equiv [ b₀ ] [ transport! B pa s ])
                          (pB [ transport! B pa s ])))
                    (–> (=ₜ-equiv [ a₀ ] [ r ]) (pA [ r ]))})))
          (contr-center (cB a₀)) (contr-path (cB a₀)))
      (contr-center cA) (contr-path cA)

  ×-conn : ∀ {i} {j} {A : Type i} {B : Type j} {n : ℕ₋₂}
    → is-connected n A → is-connected n B
    → is-connected n (A × B)
  ×-conn cA cB = Σ-conn cA (λ _ → cB)

{- connectedness of a path space -}
abstract
 instance
  path-conn : ∀ {i} {A : Type i} {x y : A} {n : ℕ₋₂}
    → is-connected (S n) A → is-connected n (x == y)
  path-conn {x = x} {y = y} cA =
    equiv-preserves-level (=ₜ-equiv [ x ] [ y ])
      {{has-level-apply (contr-is-prop cA) [ x ] [ y ]}}

{- an n-Type which is n-connected is contractible -}
connected-at-level-is-contr : ∀ {i} {A : Type i} {n : ℕ₋₂}
  {{pA : has-level n A}} {{cA : is-connected n A}} → is-contr A
connected-at-level-is-contr {{pA}} {{cA}} =
  equiv-preserves-level (unTrunc-equiv _) {{cA}}

{- if A is n-connected and m ≤ n, then A is m-connected -}
connected-≤T : ∀ {i} {m n : ℕ₋₂} {A : Type i}
  → m ≤T n → {{_ : is-connected n A}} → is-connected m A
connected-≤T {m = m} {n = n} {A = A} leq =
  transport is-contr (ua (Trunc-fuse-≤ A leq)) (Trunc-preserves-level m ⟨⟩)

{- Equivalent types have the same connectedness -}
equiv-preserves-conn : ∀ {i j} {A : Type i} {B : Type j} {n : ℕ₋₂} (e : A ≃ B)
  {{_ : is-connected n A}} → is-connected n B
equiv-preserves-conn {n = n} e = equiv-preserves-level (Trunc-emap e)

trunc-proj-conn : ∀ {i} (A : Type i) (n : ℕ₋₂)
  → has-conn-fibers n ([_] {n = n} {A = A})
trunc-proj-conn A n =
  conn-in $ λ P →
  Trunc-elim {P = fst ∘ P} {{snd ∘ P}} , λ t a → idp

{- Composite of two connected functions is connected -}
∘-conn : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k}
  → {n : ℕ₋₂} → (f : A → B) → (g : B → C)
  → has-conn-fibers n f
  → has-conn-fibers n g
  → has-conn-fibers n (g ∘ f)
∘-conn {n = n} f g cf cg =
  conn-in (λ P → conn-extend cg P ∘ conn-extend cf (P ∘ g) , lemma P)
    where
      lemma : ∀ P h x → conn-extend cg P (conn-extend cf (P ∘ g) h) (g (f x)) == h x
      lemma P h x =
        conn-extend cg P (conn-extend cf (P ∘ g) h) (g (f x))
          =⟨ conn-extend-β cg P (conn-extend cf (P ∘ g) h) (f x) ⟩
        conn-extend cf (P ∘ g) h (f x)
          =⟨ conn-extend-β cf (P ∘ g) h x ⟩
        h x
          =∎

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


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

module FiniteType where

open import Equiv using (_≃_)
open import Data.Product using (Σ; _,_)
open import Data.Nat using (ℕ)
open import Data.Fin using (Fin)

--------------------------------------------------------------------------
--
-- A finite type is a type which is equivalent to Fin n
--

FiniteType : ∀ {ℓ} → (A : Set ℓ) → (n : ℕ) →  Set ℓ
FiniteType A n = A ≃ Fin n

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
{-# OPTIONS --copatterns #-}

module IOExampleGraphicsDrawingProgramWhenJust where

open import Data.Bool.Base
open import Data.Char.Base renaming (primCharEquality to charEquality)
open import Data.Nat.Base hiding (_≟_;_⊓_; _+_; _*_)
open import Data.List.Base hiding (_++_)
open import Data.Integer.Base hiding (suc)
open import Data.String.Base
open import Data.Maybe.Base

open import Function

open import SizedIO.Base
open import SizedIO.IOGraphicsLib

open import NativeInt --PrimTypeHelpers
open import NativeIO

integerLess     :  ℤ →  ℤ → Bool
integerLess x y with ∣(y - (x ⊓ y))∣
... | zero = true
... | z = false

line : Point → Point → Graphic
line p  newpoint = withColor red (polygon
                       (point x y
                        ∷ point a b
                        ∷ point (a + xAddition) (b + yAddition)
                        ∷ point (x + xAddition) (y + yAddition)
                        ∷ [] ) )
  where
  x = proj1Point p
  y = proj2Point p
  a = proj1Point newpoint
  b = proj2Point newpoint

  diffx = + ∣ (a - x) ∣
  diffy = + ∣ (b - y) ∣

  diffx*3 = diffx * (+ 3)
  diffy*3 = diffy * (+ 3)

  condition = (integerLess diffx diffy*3) ∧ (integerLess diffy diffx*3)

  xAddition = if condition then + 2 else + 1
  yAddition = if condition then + 2 else + 1

State = Maybe Point

loop                 :  ∀{i} → Window → State → IOGraphics i Unit
force (loop w s)     =  exec'  (getWindowEvent w)
  λ{  (Key c t)      →  if charEquality c 'x' then return _ else loop w s
   ;  (MouseMove p₂) →  whenJust s (λ p₁ → exec1 (drawInWindow w (line p₁ p₂))) >>= λ _ →
                        loop w (just p₂)
   ; _               →  loop w  s
   }

myProgram : ∀{i} → IOGraphics i Unit
myProgram =
  exec (openWindow "Drawing Program" nothing
       (just (size (+ 1000) (+ 1000))) nativeDrawGraphic nothing) λ window →
  loop window nothing

main : NativeIO Unit
main = nativeRunGraphics (translateIOGraphics myProgram)

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
module Miscellaneous.associative-side where

private variable T : Set
private variable _▫_ : T → T → T
private variable id : T

data _≡_ {ℓ}{T : Set(ℓ)} : T → T → Set(ℓ) where
  [≡]-intro : ∀{x : T} → (x ≡ x)

Associativity : (T → T → T) → Set
Associativity(_▫_) = ∀{a b c} → ((a ▫ (b ▫ c)) ≡ ((a ▫ b) ▫ c))

Identityₗ : (T → T → T) → T → Set
Identityₗ(_▫_)(id) = ∀{a} → ((id ▫ a) ≡ a)

Identityᵣ : (T → T → T) → T → Set
Identityᵣ(_▫_)(id) = ∀{a} → ((a ▫ id) ≡ a)

right-op₂-associativity : Associativity{T}(\x y → y)
right-op₂-associativity = [≡]-intro

right-op₂-identityₗ : Identityₗ{T}(\x y → y)(id)
right-op₂-identityₗ {a = a} = [≡]-intro

right-op₂-when-identityᵣₗ : (∀{a} → (id ≡ a)) → Identityᵣ{T}(\x y → y)(id)
right-op₂-when-identityᵣₗ p = p

right-op₂-when-identityᵣᵣ : Identityᵣ{T}(\x y → y)(id) → (∀{a} → (id ≡ a))
right-op₂-when-identityᵣᵣ p = p

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
open import Common.Level

postulate
  ℓ : Level

data D : Set (lsuc ℓ) where
  c : (ℓ : Level) → Set ℓ → D

-- Bad error:
-- The type of the constructor does not fit in the sort of the
-- datatype, since Set (lsuc ℓ) is not less or equal than Set (lsuc ℓ)
-- when checking the constructor c in the declaration of D