text:
{-

Maybe structure: X ↦ Maybe (S X)

-}
{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}
module Cubical.Structures.Relational.Maybe where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Structure
open import Cubical.Foundations.RelationalStructure
open import Cubical.Data.Unit
open import Cubical.Data.Empty
open import Cubical.Data.Maybe
open import Cubical.Data.Sigma
open import Cubical.HITs.PropositionalTruncation as Trunc
open import Cubical.HITs.SetQuotients

open import Cubical.Structures.Maybe

private
  variable
    ℓ ℓ₁ ℓ₁' ℓ₁'' : Level

-- Structured relations

MaybeRelStr : {S : Type ℓ → Type ℓ₁} {ℓ₁' : Level}
  → StrRel S ℓ₁' → StrRel (λ X → Maybe (S X)) ℓ₁'
MaybeRelStr ρ R = MaybeRel (ρ R)

maybeSuitableRel : {S : Type ℓ → Type ℓ₁} {ρ : StrRel S ℓ₁'}
  → SuitableStrRel S ρ
  → SuitableStrRel (MaybeStructure S) (MaybeRelStr ρ)
maybeSuitableRel θ .quo (X , nothing) R _ .fst = nothing , _
maybeSuitableRel θ .quo (X , nothing) R _ .snd (nothing , _) = refl
maybeSuitableRel θ .quo (X , just s) R c .fst =
  just (θ .quo (X , s) R c .fst .fst) , θ .quo (X , s) R c .fst .snd
maybeSuitableRel θ .quo (X , just s) R c .snd (just s' , r) =
  cong (λ {(t , r') → just t , r'}) (θ .quo (X , s) R c .snd (s' , r))
maybeSuitableRel θ .symmetric R {nothing} {nothing} r = _
maybeSuitableRel θ .symmetric R {just s} {just t} r = θ .symmetric R r
maybeSuitableRel θ .transitive R R' {nothing} {nothing} {nothing} r r' = _
maybeSuitableRel θ .transitive R R' {just s} {just t} {just u} r r' = θ .transitive R R' r r'
maybeSuitableRel θ .set setX = isOfHLevelMaybe 0 (θ .set setX)
maybeSuitableRel θ .prop propR nothing nothing = isOfHLevelLift 1 isPropUnit
maybeSuitableRel θ .prop propR nothing (just y) = isOfHLevelLift 1 isProp⊥
maybeSuitableRel θ .prop propR (just x) nothing = isOfHLevelLift 1 isProp⊥
maybeSuitableRel θ .prop propR (just x) (just y) = θ .prop propR x y

maybeRelMatchesEquiv : {S : Type ℓ → Type ℓ₁} (ρ : StrRel S ℓ₁') {ι : StrEquiv S ℓ₁''}
  → StrRelMatchesEquiv ρ ι
  → StrRelMatchesEquiv (MaybeRelStr ρ) (MaybeEquivStr ι)
maybeRelMatchesEquiv ρ μ (X , nothing) (Y , nothing) _ = Lift≃Lift (idEquiv _)
maybeRelMatchesEquiv ρ μ (X , nothing) (Y , just y) _ = Lift≃Lift (idEquiv _)
maybeRelMatchesEquiv ρ μ (X , just x) (Y , nothing) _ = Lift≃Lift (idEquiv _)
maybeRelMatchesEquiv ρ μ (X , just x) (Y , just y) = μ (X , x) (Y , y)

maybeRelAction :
  {S : Type ℓ → Type ℓ₁} {ρ : StrRel S ℓ₁'}
  → StrRelAction ρ
  → StrRelAction (MaybeRelStr ρ)
maybeRelAction α .actStr f = map-Maybe (α .actStr f)
maybeRelAction α .actStrId s =
  funExt⁻ (cong map-Maybe (funExt (α .actStrId))) s ∙ map-Maybe-id s
maybeRelAction α .actRel h nothing nothing = _
maybeRelAction α .actRel h (just s) (just t) r = α .actRel h s t r

maybePositiveRel :
  {S : Type ℓ → Type ℓ₁} {ρ : StrRel S ℓ₁'} {θ : SuitableStrRel S ρ}
  → PositiveStrRel θ
  → PositiveStrRel (maybeSuitableRel θ)
maybePositiveRel σ .act = maybeRelAction (σ .act)
maybePositiveRel σ .reflexive nothing = _
maybePositiveRel σ .reflexive (just s) = σ .reflexive s
maybePositiveRel σ .detransitive R R' {nothing} {nothing} r = ∣ nothing , _ , _ ∣
maybePositiveRel σ .detransitive R R' {just s} {just u} rr' =
  Trunc.map (λ {(t , r , r') → just t , r , r'}) (σ .detransitive R R' rr')
maybePositiveRel {S = S} {ρ = ρ} {θ = θ} σ .quo {X} R =
  subst isEquiv
    (funExt
      (elimProp (λ _ → maybeSuitableRel θ .set squash/ _ _)
        (λ {nothing → refl; (just _) → refl})))
    (compEquiv (isoToEquiv isom) (congMaybeEquiv (_ , σ .quo R)) .snd)
  where
  fwd : Maybe (S X) / MaybeRel (ρ (R .fst .fst)) → Maybe (S X / ρ (R .fst .fst))
  fwd [ nothing ] = nothing
  fwd [ just s ] = just [ s ]
  fwd (eq/ nothing nothing r i) = nothing
  fwd (eq/ (just s) (just t) r i) = just (eq/ s t r i)
  fwd (squash/ _ _ p q i j) =
    isOfHLevelMaybe 0 squash/ _ _ (cong fwd p) (cong fwd q) i j

  bwd : Maybe (S X / ρ (R .fst .fst)) → Maybe (S X) / MaybeRel (ρ (R .fst .fst))
  bwd nothing = [ nothing ]
  bwd (just [ s ]) = [ just s ]
  bwd (just (eq/ s t r i)) = eq/ (just s) (just t) r i
  bwd (just (squash/ _ _ p q i j)) =
    squash/ _ _ (cong (bwd ∘ just) p) (cong (bwd ∘ just) q) i j

  open Iso
  isom : Iso (Maybe (S X) / MaybeRel (ρ (R .fst .fst))) (Maybe (S X / ρ (R .fst .fst)))
  isom .fun = fwd
  isom .inv = bwd
  isom .rightInv nothing = refl
  isom .rightInv (just x) =
    elimProp {B = λ x → fwd (bwd (just x)) ≡ just x}
      (λ _ → isOfHLevelMaybe 0 squash/ _ _)
      (λ _ → refl)
      x
  isom .leftInv = elimProp (λ _ → squash/ _ _) (λ {nothing → refl; (just _) → refl})

maybeRelMatchesTransp : {S : Type ℓ → Type ℓ₁}
  (ρ : StrRel S ℓ₁') (α : EquivAction S)
  → StrRelMatchesEquiv ρ (EquivAction→StrEquiv α)
  → StrRelMatchesEquiv (MaybeRelStr ρ) (EquivAction→StrEquiv (maybeEquivAction α))
maybeRelMatchesTransp _ _ μ (X , nothing) (Y , nothing) _ =
  isContr→Equiv (isOfHLevelLift 0 isContrUnit) isContr-nothing≡nothing
maybeRelMatchesTransp _ _ μ (X , nothing) (Y , just y) _ =
  uninhabEquiv lower ¬nothing≡just
maybeRelMatchesTransp _ _ μ (X , just x) (Y , nothing) _ =
  uninhabEquiv lower ¬just≡nothing
maybeRelMatchesTransp _ _ μ (X , just x) (Y , just y) e =
  compEquiv (μ (X , x) (Y , y) e) (_ , isEmbedding-just _ _)

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 --cubical --no-import-sorts --safe #-}

{-

This file defines integers as equivalence classes of pairs of natural numbers
using a direct & untruncated HIT definition (cf. HITs.Ints.DiffInt)

and some basic operations, and the zero value:

succ : DeltaInt → DeltaInt
pred : DeltaInt → DeltaInt
zero : {a : ℕ} → DeltaInt

and conversion function for ℕ and Int:

fromℕ : ℕ → DeltaInt
fromInt : Int → DeltaInt
toInt : DeltaInt → Int

and a generalized version of cancel:

cancelN : ∀ a b n → a ⊖ b ≡ (n + a) ⊖ n + b

-}

module Cubical.HITs.Ints.DeltaInt.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Nat hiding (zero)
open import Cubical.Data.Int hiding (abs; sgn; _+_)

infixl 5 _⊖_
data DeltaInt : Type₀ where
  _⊖_    : ℕ → ℕ → DeltaInt
  cancel : ∀ a b → a ⊖ b ≡ suc a ⊖ suc b

succ : DeltaInt → DeltaInt
succ (x ⊖ y) = suc x ⊖ y
succ (cancel a b i) = cancel (suc a) b i

pred : DeltaInt → DeltaInt
pred (x ⊖ y) = x ⊖ suc y
pred (cancel a b i) = cancel a (suc b) i

zero : {a : ℕ} → DeltaInt
zero {a} = a ⊖ a

fromℕ : ℕ → DeltaInt
fromℕ n = n ⊖ 0

fromInt : Int → DeltaInt
fromInt (pos n) = fromℕ n
fromInt (negsuc n) = 0 ⊖ suc n

toInt : DeltaInt → Int
toInt (x ⊖ y) = x ℕ- y
toInt (cancel a b i) = a ℕ- b

cancelN : ∀ a b n → a ⊖ b ≡ (n + a) ⊖ n + b
cancelN a b 0 = refl
cancelN a b (suc n) = cancelN a b n ∙ cancel (n + a) (n + b)

ext: agda

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
-- Andreas, 2014-11-01, reported by Andrea Vezzosi

-- Non-printable characters in line comments

-- Soft hyphen in comment creates lexical error:
--  (SOFT HYPHEN \- 0xAD)

-- Or parse error:
-- A

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

-- The category of Cats is Monoidal

module Categories.Category.Monoidal.Instance.Cats where

open import Level
open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂; uncurry)

open import Categories.Category
open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
open import Categories.Category.Instance.Cats
open import Categories.Category.Monoidal
open import Categories.Functor.Bifunctor
open import Categories.Category.Instance.One
open import Categories.Category.Product
open import Categories.Category.Product.Properties
import Categories.Category.Cartesian as Cartesian
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism)

-- Cats is a Monoidal Category with Product as Bifunctor
module Product {o ℓ e : Level} where
  private
    C = Cats o ℓ e
    open Cartesian C

  Cats-has-all : BinaryProducts
  Cats-has-all = record { product = λ {A} {B} → record
    { A×B = Product A B
    ; π₁ = πˡ
    ; π₂ = πʳ
    ; ⟨_,_⟩ = _※_
    ; project₁ = λ {_} {h} {i} → project₁ {i = h} {j = i}
    ; project₂ = λ {_} {h} {i} → project₂ {i = h} {j = i}
    ; unique = unique
    } }

  Cats-is : Cartesian
  Cats-is = record { terminal = One-⊤ ; products = Cats-has-all }

  private
    module Cart = Cartesian.Cartesian Cats-is

  Cats-Monoidal : Monoidal C
  Cats-Monoidal = Cart.monoidal

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
module VecReplicate where

open import Prelude

replicate : forall {A} -> (n : Nat) -> A -> Vec A n
replicate count x = {!!}

max_stars_repo_name: carlostome/martin

max_issues_repo_name: carlostome/martin

max_forks_repo_name: carlostome/martin


text:
module Function where

import      Lvl
open import Type

-- The domain type of a function.
domain : ∀{ℓ₁ ℓ₂} {A : Type{ℓ₁}}{B : Type{ℓ₂}} → (A → B) → Type{ℓ₁}
domain{A = A} _ = A

-- The codomain type of a function.
codomain : ∀{ℓ₁ ℓ₂} {A : Type{ℓ₁}}{B : Type{ℓ₂}} → (A → B) → Type{ℓ₂}
codomain{B = B} _ = 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:
{-# OPTIONS --without-K #-}

open import HoTT

module homotopy.HSpace where

-- This is just an approximation because
-- not all higher cells are killed.
record HSpaceStructure {i} (A : Type i) : Type i where
  constructor hSpaceStructure
  field
    e : A
    μ : A → A → A
    μ-e-l : (a : A) → μ e a == a
    μ-e-r : (a : A) → μ a e == a
    μ-coh : μ-e-l e == μ-e-r e

module ConnectedHSpace {i} (A : Type i) (c : is-connected 0 A)
  (hA : HSpaceStructure A) where

  open HSpaceStructure hA

  {-
  Given that [A] is 0-connected, to prove that each [μ a] is an equivalence we
  only need to prove that one of them is. But for [a] = [e], [μ a] is the
  identity so we’re done.
  -}

  μ-e-l-is-equiv : (a : A) → is-equiv (λ a' → μ a' a)
  μ-e-l-is-equiv = prop-over-connected {a = e} c
    (λ a → (is-equiv (λ a' → μ a' a) , is-equiv-is-prop (λ a' → μ a' a)))
    (transport! is-equiv (λ= μ-e-r) (idf-is-equiv A))

  μ-e-r-is-equiv : (a : A) → is-equiv (μ a)
  μ-e-r-is-equiv = prop-over-connected {a = e} c
    (λ a → (is-equiv (μ a) , is-equiv-is-prop (μ a)))
    (transport! is-equiv (λ= μ-e-l) (idf-is-equiv A))

  μ-e-l-equiv : A → A ≃ A
  μ-e-l-equiv a = _ , μ-e-l-is-equiv a

  μ-e-r-equiv : A → A ≃ A
  μ-e-r-equiv a = _ , μ-e-r-is-equiv a

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness #-}

module Agda.Builtin.Float where

open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Agda.Builtin.Int
open import Agda.Builtin.String

postulate Float : Set
{-# BUILTIN FLOAT Float #-}

primitive
  primFloatEquality : Float → Float → Bool
  primFloatLess     : Float → Float → Bool
  primFloatNumericalEquality : Float → Float → Bool
  primFloatNumericalLess     : Float → Float → Bool
  primNatToFloat    : Nat → Float
  primFloatPlus     : Float → Float → Float
  primFloatMinus    : Float → Float → Float
  primFloatTimes    : Float → Float → Float
  primFloatNegate   : Float → Float
  primFloatDiv      : Float → Float → Float
  primFloatSqrt     : Float → Float
  primRound         : Float → Int
  primFloor         : Float → Int
  primCeiling       : Float → Int
  primExp           : Float → Float
  primLog           : Float → Float
  primSin           : Float → Float
  primCos           : Float → Float
  primTan           : Float → Float
  primASin          : Float → Float
  primACos          : Float → Float
  primATan          : Float → Float
  primATan2         : Float → Float → Float
  primShowFloat     : Float → String

max_stars_repo_name: phadej/agda

max_issues_repo_name: phadej/agda

max_forks_repo_name: phadej/agda


text:
module Human.Unit where

-- Do I need a record and the built-in ⊤? Why?
data Unit : Set where
  unit : Unit

max_stars_repo_name: MaisaMilena/JuiceMaker

max_issues_repo_name: MaisaMilena/JuiceMaker

max_forks_repo_name: MaisaMilena/JuiceMaker


text:
module Data.Word.Primitive where

postulate
  Word : Set
  Word8 : Set
  Word16 : Set
  Word32 : Set
  Word64 : Set

{-# IMPORT Data.Word #-}
{-# COMPILED_TYPE Word Data.Word.Word #-}
{-# COMPILED_TYPE Word8 Data.Word.Word8 #-}
{-# COMPILED_TYPE Word16 Data.Word.Word16 #-}
{-# COMPILED_TYPE Word32 Data.Word.Word32 #-}
{-# COMPILED_TYPE Word64 Data.Word.Word64 #-}

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io


text:
open import Mockingbird.Forest.Base using (Forest)

module Mockingbird.Forest.Birds {b ℓ} (forest : Forest {b} {ℓ}) where

open import Level using (_⊔_)
open import Data.Product using (_×_; ∃-syntax)
open import Relation.Unary using (Pred)
open import Relation.Binary using (Rel)

open Forest forest

-- TODO: consider using implicit arguments in the predicates, e.g.
--   IsMockingbird M = ∀ {x} → M ∙ x ≈ x ∙ x.

IsComposition : (A B C : Bird) → Set (b ⊔ ℓ)
IsComposition A B C = ∀ x → C ∙ x ≈ A ∙ (B ∙ x)

-- A forest ‘has composition’ if for every two birds A and B there exists a bird
-- C = A ∘ B such that C is the composition of A and B.
record HasComposition : Set (b ⊔ ℓ) where
  infixr 6 _∘_

  field
    _∘_ : (A B : Bird) → Bird
    isComposition : ∀ A B → IsComposition A B (A ∘ B)

open HasComposition ⦃ ... ⦄ public

IsMockingbird : Pred Bird (b ⊔ ℓ)
IsMockingbird M = ∀ x → M ∙ x ≈ x ∙ x

record HasMockingbird : Set (b ⊔ ℓ) where
  field
    M : Bird
    isMockingbird : IsMockingbird M

open HasMockingbird ⦃ ... ⦄ public

infix 4 _IsFondOf_
_IsFondOf_ : Rel Bird ℓ
A IsFondOf B = A ∙ B ≈ B

IsEgocentric : Pred Bird ℓ
IsEgocentric A = A IsFondOf A

Agree : (A B x : Bird) → Set ℓ
Agree A B x = A ∙ x ≈ B ∙ x

IsAgreeable : Pred Bird (b ⊔ ℓ)
IsAgreeable A = ∀ B → ∃[ x ] Agree A B x

Compatible : Rel Bird (b ⊔ ℓ)
Compatible A B = ∃[ x ] ∃[ y ] (A ∙ x ≈ y) × (B ∙ y ≈ x)

IsHappy : Pred Bird (b ⊔ ℓ)
IsHappy A = Compatible A A

IsNormal : Pred Bird (b ⊔ ℓ)
IsNormal A = ∃[ x ] A IsFondOf x

infix 4 _IsFixatedOn_
_IsFixatedOn_ : Rel Bird (b ⊔ ℓ)
A IsFixatedOn B = ∀ x → A ∙ x ≈ B

IsHopelesslyEgocentric : Pred Bird (b ⊔ ℓ)
IsHopelesslyEgocentric A = A IsFixatedOn A

IsKestrel : Pred Bird (b ⊔ ℓ)
IsKestrel K = ∀ x y → (K ∙ x) ∙ y ≈ x
-- Alternative definition:
-- IsKestrel K = ∀ x → K ∙ x IsFixatedOn x

record HasKestrel : Set (b ⊔ ℓ) where
  field
    K : Bird
    isKestrel : IsKestrel K

open HasKestrel ⦃ ... ⦄ public

IsIdentity : Pred Bird (b ⊔ ℓ)
IsIdentity I = ∀ x → I ∙ x ≈ x

record HasIdentity : Set (b ⊔ ℓ) where
  field
    I : Bird
    isIdentity : IsIdentity I

open HasIdentity ⦃ ... ⦄ public

IsLark : Pred Bird (b ⊔ ℓ)
IsLark L = ∀ x y → (L ∙ x) ∙ y ≈ x ∙ (y ∙ y)

record HasLark : Set (b ⊔ ℓ) where
  field
    L : Bird
    isLark : IsLark L

IsSageBird : Pred Bird (b ⊔ ℓ)
IsSageBird Θ = ∀ x → x IsFondOf (Θ ∙ x)

open HasLark ⦃ ... ⦄ public

record HasSageBird : Set (b ⊔ ℓ) where
  field
    Θ : Bird
    isSageBird : IsSageBird Θ

IsBluebird : Pred Bird (b ⊔ ℓ)
IsBluebird B = ∀ x y z → B ∙ x ∙ y ∙ z ≈ x ∙ (y ∙ z)

open HasSageBird ⦃ ... ⦄ public

record HasBluebird : Set (b ⊔ ℓ) where
  field
    B : Bird
    isBluebird : IsBluebird B

open HasBluebird ⦃ ... ⦄ public

IsDove : Pred Bird (b ⊔ ℓ)
IsDove D = ∀ x y z w → D ∙ x ∙ y ∙ z ∙ w ≈ x ∙ y ∙ (z ∙ w)

record HasDove : Set (b ⊔ ℓ) where
  field
    D : Bird
    isDove : IsDove D

open HasDove ⦃ ... ⦄ public

IsBlackbird : Pred Bird (b ⊔ ℓ)
IsBlackbird B₁ = ∀ x y z w → B₁ ∙ x ∙ y ∙ z ∙ w ≈ x ∙ (y ∙ z ∙ w)

record HasBlackbird : Set (b ⊔ ℓ) where
  field
    B₁ : Bird
    isBlackbird : IsBlackbird B₁

open HasBlackbird ⦃ ... ⦄ public

IsEagle : Pred Bird (b ⊔ ℓ)
IsEagle E = ∀ x y z w v → E ∙ x ∙ y ∙ z ∙ w ∙ v ≈ x ∙ y ∙ (z ∙ w ∙ v)

record HasEagle : Set (b ⊔ ℓ) where
  field
    E : Bird
    isEagle : IsEagle E

open HasEagle ⦃ ... ⦄ public

IsBunting : Pred Bird (b ⊔ ℓ)
IsBunting B₂ = ∀ x y z w v → B₂ ∙ x ∙ y ∙ z ∙ w ∙ v ≈ x ∙ (y ∙ z ∙ w ∙ v)

record HasBunting : Set (b ⊔ ℓ) where
  field
    B₂ : Bird
    isBunting : IsBunting B₂

open HasBunting ⦃ ... ⦄ public

IsDickcissel : Pred Bird (b ⊔ ℓ)
IsDickcissel D₁ = ∀ x y z w v → D₁ ∙ x ∙ y ∙ z ∙ w ∙ v ≈ x ∙ y ∙ z ∙ (w ∙ v)

record HasDickcissel : Set (b ⊔ ℓ) where
  field
    D₁ : Bird
    isDickcissel : IsDickcissel D₁

open HasDickcissel ⦃ ... ⦄ public

IsBecard : Pred Bird (b ⊔ ℓ)
IsBecard B₃ = ∀ x y z w → B₃ ∙ x ∙ y ∙ z ∙ w ≈ x ∙ (y ∙ (z ∙ w))

record HasBecard : Set (b ⊔ ℓ) where
  field
    B₃ : Bird
    isBecard : IsBecard B₃

open HasBecard ⦃ ... ⦄ public

IsDovekie : Pred Bird (b ⊔ ℓ)
IsDovekie D₂ = ∀ x y z w v → D₂ ∙ x ∙ y ∙ z ∙ w ∙ v ≈ x ∙ (y ∙ z) ∙ (w ∙ v)

record HasDovekie : Set (b ⊔ ℓ) where
  field
    D₂ : Bird
    isDovekie : IsDovekie D₂

open HasDovekie ⦃ ... ⦄ public

IsBaldEagle : Pred Bird (b ⊔ ℓ)
IsBaldEagle Ê = ∀ x y₁ y₂ y₃ z₁ z₂ z₃ → Ê ∙ x ∙ y₁ ∙ y₂ ∙ y₃ ∙ z₁ ∙ z₂ ∙ z₃ ≈ x ∙ (y₁ ∙ y₂ ∙ y₃) ∙ (z₁ ∙ z₂ ∙ z₃)

record HasBaldEagle : Set (b ⊔ ℓ) where
  field
    Ê : Bird
    isBaldEagle : IsBaldEagle Ê

open HasBaldEagle ⦃ ... ⦄ public

IsWarbler : Pred Bird (b ⊔ ℓ)
IsWarbler W = ∀ x y → W ∙ x ∙ y ≈ x ∙ y ∙ y

record HasWarbler : Set (b ⊔ ℓ) where
  field
    W : Bird
    isWarbler : IsWarbler W

open HasWarbler ⦃ ... ⦄ public

IsCardinal : Pred Bird (b ⊔ ℓ)
IsCardinal C = ∀ x y z → C ∙ x ∙ y ∙ z ≈ x ∙ z ∙ y

record HasCardinal : Set (b ⊔ ℓ) where
  field
    C : Bird
    isCardinal : IsCardinal C

open HasCardinal ⦃ ... ⦄ public

IsThrush : Pred Bird (b ⊔ ℓ)
IsThrush T = ∀ x y → T ∙ x ∙ y ≈ y ∙ x

record HasThrush : Set (b ⊔ ℓ) where
  field
    T : Bird
    isThrush : IsThrush T

open HasThrush ⦃ ... ⦄ public

Commute : (x y : Bird) → Set ℓ
Commute x y = x ∙ y ≈ y ∙ x

IsRobin : Pred Bird (b ⊔ ℓ)
IsRobin R = ∀ x y z → R ∙ x ∙ y ∙ z ≈ y ∙ z ∙ x

record HasRobin : Set (b ⊔ ℓ) where
  field
    R : Bird
    isRobin : IsRobin R

open HasRobin ⦃ ... ⦄ public

IsFinch : Pred Bird (b ⊔ ℓ)
IsFinch F = ∀ x y z → F ∙ x ∙ y ∙ z ≈ z ∙ y ∙ x

record HasFinch : Set (b ⊔ ℓ) where
  field
    F : Bird
    isFinch : IsFinch F

open HasFinch ⦃ ... ⦄ public

IsVireo : Pred Bird (b ⊔ ℓ)
IsVireo V = ∀ x y z → V ∙ x ∙ y ∙ z ≈ z ∙ x ∙ y

record HasVireo : Set (b ⊔ ℓ) where
  field
    V : Bird
    isVireo : IsVireo V

open HasVireo ⦃ ... ⦄ public

IsCardinalOnceRemoved : Pred Bird (b ⊔ ℓ)
IsCardinalOnceRemoved C* = ∀ x y z w → C* ∙ x ∙ y ∙ z ∙ w ≈ x ∙ y ∙ w ∙ z

record HasCardinalOnceRemoved : Set (b ⊔ ℓ) where
  field
    C* : Bird
    isCardinalOnceRemoved : IsCardinalOnceRemoved C*

open HasCardinalOnceRemoved ⦃ ... ⦄ public

IsRobinOnceRemoved : Pred Bird (b ⊔ ℓ)
IsRobinOnceRemoved R* = ∀ x y z w → R* ∙ x ∙ y ∙ z ∙ w ≈ x ∙ z ∙ w ∙ y

record HasRobinOnceRemoved : Set (b ⊔ ℓ) where
  field
    R* : Bird
    isRobinOnceRemoved : IsRobinOnceRemoved R*

open HasRobinOnceRemoved ⦃ ... ⦄ public

IsFinchOnceRemoved : Pred Bird (b ⊔ ℓ)
IsFinchOnceRemoved F* = ∀ x y z w → F* ∙ x ∙ y ∙ z ∙ w ≈ x ∙ w ∙ z ∙ y

record HasFinchOnceRemoved : Set (b ⊔ ℓ) where
  field
    F* : Bird
    isFinchOnceRemoved : IsFinchOnceRemoved F*

open HasFinchOnceRemoved ⦃ ... ⦄ public

IsVireoOnceRemoved : Pred Bird (b ⊔ ℓ)
IsVireoOnceRemoved V* = ∀ x y z w → V* ∙ x ∙ y ∙ z ∙ w ≈ x ∙ w ∙ y ∙ z

record HasVireoOnceRemoved : Set (b ⊔ ℓ) where
  field
    V* : Bird
    isVireoOnceRemoved : IsVireoOnceRemoved V*

open HasVireoOnceRemoved ⦃ ... ⦄ public

IsCardinalTwiceRemoved : Pred Bird (b ⊔ ℓ)
IsCardinalTwiceRemoved C** = ∀ x y z₁ z₂ z₃ → C** ∙ x ∙ y ∙ z₁ ∙ z₂ ∙ z₃ ≈ x ∙ y ∙ z₁ ∙ z₃ ∙ z₂

record HasCardinalTwiceRemoved : Set (b ⊔ ℓ) where
  field
    C** : Bird
    isCardinalTwiceRemoved : IsCardinalTwiceRemoved C**

open HasCardinalTwiceRemoved ⦃ ... ⦄ public

IsRobinTwiceRemoved : Pred Bird (b ⊔ ℓ)
IsRobinTwiceRemoved R** = ∀ x y z₁ z₂ z₃ → R** ∙ x ∙ y ∙ z₁ ∙ z₂ ∙ z₃ ≈ x ∙ y ∙ z₂ ∙ z₃ ∙ z₁

record HasRobinTwiceRemoved : Set (b ⊔ ℓ) where
  field
    R** : Bird
    isRobinTwiceRemoved : IsRobinTwiceRemoved R**

open HasRobinTwiceRemoved ⦃ ... ⦄ public

IsFinchTwiceRemoved : Pred Bird (b ⊔ ℓ)
IsFinchTwiceRemoved F** = ∀ x y z₁ z₂ z₃ → F** ∙ x ∙ y ∙ z₁ ∙ z₂ ∙ z₃ ≈ x ∙ y ∙ z₃ ∙ z₂ ∙ z₁

record HasFinchTwiceRemoved : Set (b ⊔ ℓ) where
  field
    F** : Bird
    isFinchTwiceRemoved : IsFinchTwiceRemoved F**

open HasFinchTwiceRemoved ⦃ ... ⦄ public

IsVireoTwiceRemoved : Pred Bird (b ⊔ ℓ)
IsVireoTwiceRemoved V** = ∀ x y z₁ z₂ z₃ → V** ∙ x ∙ y ∙ z₁ ∙ z₂ ∙ z₃ ≈ x ∙ y ∙ z₃ ∙ z₁ ∙ z₂

record HasVireoTwiceRemoved : Set (b ⊔ ℓ) where
  field
    V** : Bird
    isVireoTwiceRemoved : IsVireoTwiceRemoved V**

open HasVireoTwiceRemoved ⦃ ... ⦄ public

IsQueerBird : Pred Bird (b ⊔ ℓ)
IsQueerBird Q = ∀ x y z → Q ∙ x ∙ y ∙ z ≈ y ∙ (x ∙ z)

record HasQueerBird : Set (b ⊔ ℓ) where
  field
    Q : Bird
    isQueerBird : IsQueerBird Q

open HasQueerBird ⦃ ... ⦄ public

IsQuixoticBird : Pred Bird (b ⊔ ℓ)
IsQuixoticBird Q₁ = ∀ x y z → Q₁ ∙ x ∙ y ∙ z ≈ x ∙ (z ∙ y)

record HasQuixoticBird : Set (b ⊔ ℓ) where
  field
    Q₁ : Bird
    isQuixoticBird : IsQuixoticBird Q₁

open HasQuixoticBird ⦃ ... ⦄ public

IsQuizzicalBird : Pred Bird (b ⊔ ℓ)
IsQuizzicalBird Q₂ = ∀ x y z → Q₂ ∙ x ∙ y ∙ z ≈ y ∙ (z ∙ x)

record HasQuizzicalBird : Set (b ⊔ ℓ) where
  field
    Q₂ : Bird
    isQuizzicalBird : IsQuizzicalBird Q₂

open HasQuizzicalBird ⦃ ... ⦄ public

IsQuirkyBird : Pred Bird (b ⊔ ℓ)
IsQuirkyBird Q₃ = ∀ x y z → Q₃ ∙ x ∙ y ∙ z ≈ z ∙ (x ∙ y)

record HasQuirkyBird : Set (b ⊔ ℓ) where
  field
    Q₃ : Bird
    isQuirkyBird : IsQuirkyBird Q₃

open HasQuirkyBird ⦃ ... ⦄ public

IsQuackyBird : Pred Bird (b ⊔ ℓ)
IsQuackyBird Q₄ = ∀ x y z → Q₄ ∙ x ∙ y ∙ z ≈ z ∙ (y ∙ x)

record HasQuackyBird : Set (b ⊔ ℓ) where
  field
    Q₄ : Bird
    isQuackyBird : IsQuackyBird Q₄

open HasQuackyBird ⦃ ... ⦄ public

IsGoldfinch : Pred Bird (b ⊔ ℓ)
IsGoldfinch G = ∀ x y z w → G ∙ x ∙ y ∙ z ∙ w ≈ x ∙ w ∙ (y ∙ z)

record HasGoldfinch : Set (b ⊔ ℓ) where
  field
    G : Bird
    isGoldfinch : IsGoldfinch G

open HasGoldfinch ⦃ ... ⦄ public

IsDoubleMockingbird : Pred Bird (b ⊔ ℓ)
IsDoubleMockingbird M₂ = ∀ x y → M₂ ∙ x ∙ y ≈ x ∙ y ∙ (x ∙ y)

record HasDoubleMockingbird : Set (b ⊔ ℓ) where
  field
    M₂ : Bird
    isDoubleMockingbird : IsDoubleMockingbird M₂

open HasDoubleMockingbird ⦃ ... ⦄ public

IsConverseWarbler : Pred Bird (b ⊔ ℓ)
IsConverseWarbler W′ = ∀ x y → W′ ∙ x ∙ y ≈ y ∙ x ∙ x

record HasConverseWarbler : Set (b ⊔ ℓ) where
  field
    W′ : Bird
    isConverseWarbler : IsConverseWarbler W′

open HasConverseWarbler ⦃ ... ⦄ public

IsWarblerOnceRemoved : Pred Bird (b ⊔ ℓ)
IsWarblerOnceRemoved W* = ∀ x y z → W* ∙ x ∙ y ∙ z ≈ x ∙ y ∙ z ∙ z

record HasWarblerOnceRemoved : Set (b ⊔ ℓ) where
  field
    W* : Bird
    isWarblerOnceRemoved : IsWarblerOnceRemoved W*

open HasWarblerOnceRemoved ⦃ ... ⦄ public

IsWarblerTwiceRemoved : Pred Bird (b ⊔ ℓ)
IsWarblerTwiceRemoved W** = ∀ x y z w → W** ∙ x ∙ y ∙ z ∙ w ≈ x ∙ y ∙ z ∙ w ∙ w

record HasWarblerTwiceRemoved : Set (b ⊔ ℓ) where
  field
    W** : Bird
    isWarblerTwiceRemoved : IsWarblerTwiceRemoved W**

open HasWarblerTwiceRemoved ⦃ ... ⦄ public

IsHummingbird : Pred Bird (b ⊔ ℓ)
IsHummingbird H = ∀ x y z → H ∙ x ∙ y ∙ z ≈ x ∙ y ∙ z ∙ y

record HasHummingbird : Set (b ⊔ ℓ) where
  field
    H : Bird
    isHummingbird : IsHummingbird H

open HasHummingbird ⦃ ... ⦄ public

IsStarling : Pred Bird (b ⊔ ℓ)
IsStarling S = ∀ x y z → S ∙ x ∙ y ∙ z ≈ x ∙ z ∙ (y ∙ z)

record HasStarling : Set (b ⊔ ℓ) where
  field
    S : Bird
    isStarling : IsStarling S

open HasStarling ⦃ ... ⦄ public

IsPhoenix : Pred Bird (b ⊔ ℓ)
IsPhoenix Φ = ∀ x y z w → Φ ∙ x ∙ y ∙ z ∙ w ≈ x ∙ (y ∙ w) ∙ (z ∙ w)

record HasPhoenix : Set (b ⊔ ℓ) where
  field
    Φ : Bird
    isPhoenix : IsPhoenix Φ

open HasPhoenix ⦃ ... ⦄ public

IsPsiBird : Pred Bird (b ⊔ ℓ)
IsPsiBird Ψ = ∀ x y z w → Ψ ∙ x ∙ y ∙ z ∙ w ≈ x ∙ (y ∙ z) ∙ (y ∙ w)

record HasPsiBird : Set (b ⊔ ℓ) where
  field
    Ψ : Bird
    isPsiBird : IsPsiBird Ψ

open HasPsiBird ⦃ ... ⦄ public

IsTuringBird : Pred Bird (b ⊔ ℓ)
IsTuringBird U = ∀ x y → U ∙ x ∙ y ≈ y ∙ (x ∙ x ∙ y)

record HasTuringBird : Set (b ⊔ ℓ) where
  field
    U : Bird
    isTuringBird : IsTuringBird U

open HasTuringBird ⦃ ... ⦄ public

IsOwl : Pred Bird (b ⊔ ℓ)
IsOwl O = ∀ x y → O ∙ x ∙ y ≈ y ∙ (x ∙ y)

record HasOwl : Set (b ⊔ ℓ) where
  field
    O : Bird
    isOwl : IsOwl O

open HasOwl ⦃ ... ⦄ public

IsChoosy : Pred Bird (b ⊔ ℓ)
IsChoosy A = ∀ x → A IsFondOf x → IsSageBird x

IsJaybird : Pred Bird (b ⊔ ℓ)
IsJaybird J = ∀ x y z w → J ∙ x ∙ y ∙ z ∙ w ≈ x ∙ y ∙ (x ∙ w ∙ z)

record HasJaybird : Set (b ⊔ ℓ) where
  field
    J : Bird
    isJaybird : IsJaybird J

open HasJaybird ⦃ ... ⦄ public

max_stars_repo_name: splintah/combinatory-logic

max_issues_repo_name: splintah/combinatory-logic

max_forks_repo_name: splintah/combinatory-logic


text:
-- WARNING: This file was generated automatically by Vehicle
-- and should not be modified manually!
-- Metadata
--  - Agda version: 2.6.2
--  - AISEC version: 0.1.0.1
--  - Time generated: ???

{-# OPTIONS --allow-exec #-}

open import Vehicle
open import Vehicle.Data.Tensor
open import Data.Nat as ℕ using (ℕ)
open import Data.Fin as Fin using (Fin; #_)
open import Data.List

module simple-tensor-temp-output where

zeroD : Tensor ℕ []
zeroD = 2

oneD : Tensor ℕ (2 ∷ [])
oneD = zeroD ∷ (1 ∷ [])

twoD : Tensor ℕ (2 ∷ (2 ∷ []))
twoD = oneD ∷ ((2 ∷ (3 ∷ [])) ∷ [])

lookup2D : ℕ
lookup2D = twoD (# 0) (# 1)

max_stars_repo_name: vehicle-lang/vehicle

max_issues_repo_name: vehicle-lang/vehicle

max_forks_repo_name: vehicle-lang/vehicle


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

open import Categories.Category

-- The core of a category.
-- See https://ncatlab.org/nlab/show/core

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

open import Level using (_⊔_)
open import Function using (flip)

open import Categories.Category.Groupoid using (Groupoid; IsGroupoid)
open import Categories.Morphism 𝒞 as Morphism
open import Categories.Morphism.IsoEquiv 𝒞 as IsoEquiv

open Category 𝒞
open _≃_

Core : Category o (ℓ ⊔ e) e
Core = record
  { Obj       = Obj
  ; _⇒_       = _≅_
  ; _≈_       = _≃_
  ; id        = ≅.refl
  ; _∘_       = flip ≅.trans
  ; assoc     = ⌞ assoc     ⌟
  ; sym-assoc = ⌞ sym-assoc ⌟
  ; identityˡ = ⌞ identityˡ ⌟
  ; identityʳ = ⌞ identityʳ ⌟
  ; identity² = ⌞ identity² ⌟
  ; equiv     = ≃-isEquivalence
  ; ∘-resp-≈  = λ where ⌞ eq₁ ⌟ ⌞ eq₂ ⌟ → ⌞ ∘-resp-≈ eq₁ eq₂ ⌟
  }

Core-isGroupoid : IsGroupoid Core
Core-isGroupoid = record
  { _⁻¹ = ≅.sym
  ; iso = λ {_ _ f} → record { isoˡ = ⌞ isoˡ f ⌟ ; isoʳ = ⌞ isoʳ f ⌟ }
  }
  where open _≅_

CoreGroupoid : Groupoid o (ℓ ⊔ e) e
CoreGroupoid = record { category = Core; isGroupoid = Core-isGroupoid }

module CoreGroupoid = Groupoid CoreGroupoid

-- Useful shorthands for reasoning about isomorphisms and morphisms of
-- 𝒞 in the same module.

module Shorthands where
  module Commutationᵢ where
    open Commutation Core public using () renaming ([_⇒_]⟨_≈_⟩ to [_≅_]⟨_≈_⟩)

    infixl 2 connectᵢ
    connectᵢ : ∀ {A C : Obj} (B : Obj) → A ≅ B → B ≅ C → A ≅ C
    connectᵢ B f g = ≅.trans f g

    syntax connectᵢ B f g = f ≅⟨ B ⟩ g

  open _≅_ public
  open _≃_ public
  open Morphism public using (module _≅_)
  open IsoEquiv public using (⌞_⌟) renaming (module _≃_ to _≈ᵢ_)
  open CoreGroupoid public using (_⁻¹) renaming
    ( _⇒_                 to _≅_
    ; _≈_                 to _≈ᵢ_
    ; id                  to idᵢ
    ; _∘_                 to _∘ᵢ_
    ; iso                 to ⁻¹-iso
    ; module Equiv        to Equivᵢ
    ; module HomReasoning to HomReasoningᵢ
    ; module iso          to ⁻¹-iso
    )

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some derivable properties
------------------------------------------------------------------------

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

open import Algebra

module Algebra.Properties.AbelianGroup
  {a ℓ} (G : AbelianGroup a ℓ) where

open AbelianGroup G
open import Function
open import Relation.Binary.Reasoning.Setoid setoid

------------------------------------------------------------------------
-- Publicly re-export group properties

open import Algebra.Properties.Group group public

------------------------------------------------------------------------
-- Properties of abelian groups

xyx⁻¹≈y : ∀ x y → x ∙ y ∙ x ⁻¹ ≈ y
xyx⁻¹≈y x y = begin
  x ∙ y ∙ x ⁻¹    ≈⟨ ∙-congʳ $ comm _ _ ⟩
  y ∙ x ∙ x ⁻¹    ≈⟨ assoc _ _ _ ⟩
  y ∙ (x ∙ x ⁻¹)  ≈⟨ ∙-congˡ $ inverseʳ _ ⟩
  y ∙ ε           ≈⟨ identityʳ _ ⟩
  y               ∎

⁻¹-∙-comm : ∀ x y → x ⁻¹ ∙ y ⁻¹ ≈ (x ∙ y) ⁻¹
⁻¹-∙-comm x y = begin
  x ⁻¹ ∙ y ⁻¹ ≈˘⟨ ⁻¹-anti-homo-∙ y x ⟩
  (y ∙ x) ⁻¹  ≈⟨ ⁻¹-cong $ comm y x ⟩
  (x ∙ y) ⁻¹  ∎


text:
------------------------------------------------------------------------
-- By indexing the program and WHNF types on a universe one can handle
-- several types at the same time
------------------------------------------------------------------------

module UniverseIndex where

open import Codata.Musical.Notation
open import Codata.Musical.Stream
open import Data.Product

infixr 5 _∷_
infixr 4 _,_

data U : Set₁ where
  lift    : Set → U
  stream  : U → U
  product : U → U → U

El : U → Set
El (lift A)      = A
El (stream a)    = Stream (El a)
El (product a b) = El a × El b

data ElP : U → Set₁ where
  interleave : ∀ {a} → ElP (stream a) → ElP (stream a) → ElP (stream a)
  fst        : ∀ {a b} → ElP (product a b) → ElP a
  snd        : ∀ {a b} → ElP (product a b) → ElP b

data ElW : U → Set₁ where
  _∷_  : ∀ {a} → ElW a → ElP (stream a) → ElW (stream a)
  _,_  : ∀ {a b} → ElW a → ElW b → ElW (product a b)
  ⌈_⌉  : ∀ {A} → A → ElW (lift A)

interleaveW : ∀ {a} → ElW (stream a) → ElP (stream a) → ElW (stream a)
interleaveW (x ∷ xs) ys = x ∷ interleave ys xs

fstW : ∀ {a b} → ElW (product a b) → ElW a
fstW (x , y) = x

sndW : ∀ {a b} → ElW (product a b) → ElW b
sndW (x , y) = y

whnf : ∀ {a} → ElP a → ElW a
whnf (interleave xs ys) = interleaveW (whnf xs) ys
whnf (fst p)            = fstW (whnf p)
whnf (snd p)            = sndW (whnf p)

mutual

  ⟦_⟧W : ∀ {a} → ElW a → El a
  ⟦ x ∷ xs ⟧W = ⟦ x ⟧W ∷ ♯ ⟦ xs ⟧P
  ⟦ x , y  ⟧W = (⟦ x ⟧W , ⟦ y ⟧W)
  ⟦ ⌈ x ⌉  ⟧W = x

  ⟦_⟧P : ∀ {a} → ElP a → El a
  ⟦ p ⟧P = ⟦ whnf p ⟧W

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


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

module hott where

open import hott.level public
open import hott.equivalence public
open import hott.loop public
open import hott.univalence public
open import hott.truncation public

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
module NamedImplicit where

postulate
  T    : Set -> Set
  map' : (A B : Set) -> (A -> B) -> T A -> T B

map : {A B : Set} -> (A -> B) -> T A -> T B
map = map' _ _

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

data Bool : Set where
  true  : Bool
  false : Bool

id : {A : Set} -> A -> A
id x = x

const : {A B : Set} -> A -> B -> A
const x y = x

postulate
  unsafeCoerce : {A B : Set} -> A -> B

test1 = map {B = Nat} id
test2 = map {A = Nat} (const zero)
test3 = map {B = Bool} (unsafeCoerce {A = Nat})
test4 = map {B = Nat -> Nat} (const {B = Bool} id)

f : {A B C D : Set} -> D -> D
f {D = X} = \(x : X) -> x


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.ZCohomology.CohomologyRings.Sn where

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

open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Unit
open import Cubical.Data.Nat renaming (_+_ to _+n_ ; +-comm to +n-comm ; _·_ to _·n_ ; snotz to nsnotz)
open import Cubical.Data.Nat.Order
open import Cubical.Data.Int hiding (_+'_)
open import Cubical.Data.Sigma
open import Cubical.Data.Vec
open import Cubical.Data.FinData

open import Cubical.Relation.Nullary

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.Instances.Int renaming (ℤGroup to ℤG)
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.DirectSum.Base
open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.FGIdeal
open import Cubical.Algebra.CommRing.QuotientRing
open import Cubical.Algebra.Polynomials.Multivariate.Base renaming (base to baseP)
open import Cubical.Algebra.CommRing.Instances.Int renaming (ℤCommRing to ℤCR)
open import Cubical.Algebra.CommRing.Instances.MultivariatePoly
open import Cubical.Algebra.CommRing.Instances.MultivariatePoly-Quotient
open import Cubical.Algebra.CommRing.Instances.MultivariatePoly-notationZ

open import Cubical.HITs.SetQuotients as SQ renaming (_/_ to _/sq_)
open import Cubical.HITs.PropositionalTruncation as PT
open import Cubical.HITs.SetTruncation as ST
open import Cubical.HITs.Truncation
open import Cubical.HITs.Sn

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.GroupStructure
open import Cubical.ZCohomology.RingStructure.CupProduct
open import Cubical.ZCohomology.RingStructure.RingLaws
open import Cubical.ZCohomology.RingStructure.CohomologyRing
open import Cubical.ZCohomology.Groups.Sn

open Iso

-----------------------------------------------------------------------------
-- Somme properties over H⁰-Sⁿ≅ℤ
module Properties-H⁰-Sⁿ≅ℤ where

  open RingStr

  T0m : (m : ℕ) → (z : ℤ) → coHom 0 (S₊ (suc m))
  T0m m = inv (fst (H⁰-Sⁿ≅ℤ m))

  T0mg : (m : ℕ) → IsGroupHom (snd ℤG) (T0m m) (coHomGr 0 (S₊ (suc m)) .snd)
  T0mg m = snd (invGroupIso (H⁰-Sⁿ≅ℤ m))

  T0m-pres1 : (m : ℕ) → base 0 ((T0m m) 1) ≡ 1r (snd (H*R (S₊ (suc m))))
  T0m-pres1 zero = refl
  T0m-pres1 (suc m) = refl

  T0m-pos0 : (m : ℕ) → {l : ℕ} → (x : coHom l (S₊ (suc m))) → (T0m m) (pos zero) ⌣ x ≡ 0ₕ l
  T0m-pos0 zero = ST.elim (λ x  → isProp→isSet (squash₂ _ _)) λ x → refl
  T0m-pos0 (suc m) = ST.elim (λ x  → isProp→isSet (squash₂ _ _)) λ x → refl

  T0m-posS : (m : ℕ) → {l : ℕ} → (k : ℕ) → (x : coHom l (S₊ (suc m)))
            → T0m m (pos (suc k)) ⌣ x ≡ x +ₕ (T0m m (pos k) ⌣ x)
  T0m-posS zero k = ST.elim (λ x → isProp→isSet (squash₂ _ _)) (λ x → refl)
  T0m-posS (suc m) k = ST.elim (λ x → isProp→isSet (squash₂ _ _)) (λ x → refl)

  T0m-neg0 : (m : ℕ) → {l : ℕ} → (x : coHom l (S₊ (suc m))) → T0m m (negsuc zero) ⌣ x ≡ -ₕ x
  T0m-neg0 zero = ST.elim (λ x → isProp→isSet (squash₂ _ _)) (λ x → refl)
  T0m-neg0 (suc m) = ST.elim (λ x → isProp→isSet (squash₂ _ _)) (λ x → refl)

  T0m-negS : (m : ℕ) → {l : ℕ} → (k : ℕ) → (x : coHom l (S₊ (suc m)))
            → T0m m (negsuc (suc k)) ⌣ x ≡ (T0m m (negsuc k) ⌣ x) +ₕ (-ₕ x)
  T0m-negS zero k = ST.elim (λ x → isProp→isSet (squash₂ _ _)) (λ x → refl)
  T0m-negS (suc m) k = ST.elim (λ x → isProp→isSet (squash₂ _ _)) (λ x → refl)

-----------------------------------------------------------------------------
-- Definitions

module Equiv-Sn-Properties (n : ℕ) where

  open IsGroupHom
  open Properties-H⁰-Sⁿ≅ℤ

  open CommRingStr (snd ℤCR) using ()
    renaming
    ( 0r        to 0ℤ
    ; 1r        to 1ℤ
    ; _+_       to _+ℤ_
    ; -_        to -ℤ_
    ; _·_       to _·ℤ_
    ; +Assoc    to +ℤAssoc
    ; +Identity to +ℤIdentity
    ; +Lid      to +ℤLid
    ; +Rid      to +ℤRid
    ; +Inv      to +ℤInv
    ; +Linv     to +ℤLinv
    ; +Rinv     to +ℤRinv
    ; +Comm     to +ℤComm
    ; ·Assoc    to ·ℤAssoc
    ; ·Identity to ·ℤIdentity
    ; ·Lid      to ·ℤLid
    ; ·Rid      to ·ℤRid
    ; ·Rdist+   to ·ℤRdist+
    ; ·Ldist+   to ·ℤLdist+
    ; is-set    to isSetℤ     )

  open RingStr (snd (H*R (S₊ (suc n)))) using ()
    renaming
    ( 0r        to 0H*
    ; 1r        to 1H*
    ; _+_       to _+H*_
    ; -_        to -H*_
    ; _·_       to _cup_
    ; +Assoc    to +H*Assoc
    ; +Identity to +H*Identity
    ; +Lid      to +H*Lid
    ; +Rid      to +H*Rid
    ; +Inv      to +H*Inv
    ; +Linv     to +H*Linv
    ; +Rinv     to +H*Rinv
    ; +Comm     to +H*Comm
    ; ·Assoc    to ·H*Assoc
    ; ·Identity to ·H*Identity
    ; ·Lid      to ·H*Lid
    ; ·Rid      to ·H*Rid
    ; ·Rdist+   to ·H*Rdist+
    ; ·Ldist+   to ·H*Ldist+
    ; is-set    to isSetH*     )

  open CommRingStr (snd ℤ[X]) using ()
    renaming
    ( 0r        to 0Pℤ
    ; 1r        to 1Pℤ
    ; _+_       to _+Pℤ_
    ; -_        to -Pℤ_
    ; _·_       to _·Pℤ_
    ; +Assoc    to +PℤAssoc
    ; +Identity to +PℤIdentity
    ; +Lid      to +PℤLid
    ; +Rid      to +PℤRid
    ; +Inv      to +PℤInv
    ; +Linv     to +PℤLinv
    ; +Rinv     to +PℤRinv
    ; +Comm     to +PℤComm
    ; ·Assoc    to ·PℤAssoc
    ; ·Identity to ·PℤIdentity
    ; ·Lid      to ·PℤLid
    ; ·Rid      to ·PℤRid
    ; ·Comm     to ·PℤComm
    ; ·Rdist+   to ·PℤRdist+
    ; ·Ldist+   to ·PℤLdist+
    ; is-set    to isSetPℤ     )

  open CommRingStr (snd ℤ[X]/X²) using ()
    renaming
    ( 0r        to 0PℤI
    ; 1r        to 1PℤI
    ; _+_       to _+PℤI_
    ; -_        to -PℤI_
    ; _·_       to _·PℤI_
    ; +Assoc    to +PℤIAssoc
    ; +Identity to +PℤIIdentity
    ; +Lid      to +PℤILid
    ; +Rid      to +PℤIRid
    ; +Inv      to +PℤIInv
    ; +Linv     to +PℤILinv
    ; +Rinv     to +PℤIRinv
    ; +Comm     to +PℤIComm
    ; ·Assoc    to ·PℤIAssoc
    ; ·Identity to ·PℤIIdentity
    ; ·Lid      to ·PℤILid
    ; ·Rid      to ·PℤIRid
    ; ·Rdist+   to ·PℤIRdist+
    ; ·Ldist+   to ·PℤILdist+
    ; is-set    to isSetPℤI     )

-----------------------------------------------------------------------------
-- Partition of ℕ

  data partℕ (k : ℕ) : Type ℓ-zero where
    is0  : (k ≡ 0)                          → partℕ k
    isSn : (k ≡ suc n)                      → partℕ k
    else : (k ≡ 0 → ⊥) × (k ≡ suc n → ⊥) → partℕ k

  part : (k : ℕ) → partℕ k
  part k with (discreteℕ k 0)
  ... | yes p = is0 p
  ... | no ¬p with (discreteℕ k (suc n))
  ... |            yes q = isSn q
  ... |            no ¬q = else (¬p , ¬q)

  part0 : part 0 ≡ is0 refl
  part0 = refl

  partSn : (x : partℕ (suc n)) → x ≡ isSn refl
  partSn (is0 x)  = ⊥.rec (nsnotz x)
  partSn (isSn x) = cong isSn (isSetℕ _ _ _ _)
  partSn (else x) = ⊥.rec (snd x refl)

-----------------------------------------------------------------------------
-- As we are in the general case, the definition are now up to a path and not definitional
-- Hence when need to add transport to go from coHom 0 X to coHom 0 X
-- This some notation and usefull lemma

  substCoHom : {k l : ℕ} → (x : k ≡ l) → (a : coHom k (S₊ (suc n))) → coHom l (S₊ (suc n))
  substCoHom x a = subst (λ X → coHom X (S₊ (suc n))) x a

  -- solve a pbl of project with the notation
  substReflCoHom : {k : ℕ} → (a : coHom k (S₊ (suc n))) → subst (λ X → coHom X (S₊ (suc n))) refl a ≡ a
  substReflCoHom a = substRefl a

  subst-0 : (k l : ℕ) → (x : k ≡ l) → substCoHom x (0ₕ k) ≡ 0ₕ l
  subst-0 k l x = J (λ l x → substCoHom x (0ₕ k) ≡ 0ₕ l) (substReflCoHom (0ₕ k)) x

  subst-+ : (k : ℕ) → (a b : coHom k (S₊ (suc n))) → (l : ℕ) → (x : k ≡ l)
            → substCoHom x (a +ₕ b) ≡ substCoHom x a +ₕ substCoHom x b
  subst-+ k a b l x = J (λ l x → substCoHom x (a +ₕ b) ≡ substCoHom x a +ₕ substCoHom x b)
                        (substReflCoHom (a +ₕ b) ∙ sym (cong₂ _+ₕ_ (substReflCoHom a) (substReflCoHom b)))
                        x

  subst-⌣ : (k : ℕ) → (a b : coHom k (S₊ (suc n))) → (l : ℕ) → (x : k ≡ l)
            → substCoHom (cong₂ _+'_ x x) (a ⌣ b) ≡ substCoHom x a ⌣ substCoHom x b
  subst-⌣ k a b l x = J (λ l x → substCoHom (cong₂ _+'_ x x) (a ⌣ b) ≡ substCoHom x a ⌣ substCoHom x b)
                        (substReflCoHom (a ⌣ b) ∙ sym (cong₂ _⌣_ (substReflCoHom a) (substReflCoHom b)))
                        x

-----------------------------------------------------------------------------
-- Direct Sens on ℤ[x]

  ℤ[x]→H*-Sⁿ : ℤ[x] → H* (S₊ (suc n))
  ℤ[x]→H*-Sⁿ = Poly-Rec-Set.f _ _ _ isSetH*
       0H*
       base-trad
       _+H*_
       +H*Assoc
       +H*Rid
       +H*Comm
       base-neutral-eq
       base-add-eq
    where

    base-trad : _
    base-trad (zero ∷ []) a = base 0 (inv (fst (H⁰-Sⁿ≅ℤ n)) a)
    base-trad (one ∷ []) a = base (suc n) (inv (fst (Hⁿ-Sⁿ≅ℤ n)) a)
    base-trad (suc (suc k) ∷ []) a = 0H*

    base-neutral-eq : _
    base-neutral-eq (zero ∷ []) = cong (base 0) (pres1 (snd (invGroupIso (H⁰-Sⁿ≅ℤ n)))) ∙ base-neutral _
    base-neutral-eq (one ∷ []) = cong (base (suc n)) (pres1 (snd (invGroupIso (Hⁿ-Sⁿ≅ℤ n)))) ∙ base-neutral _
    base-neutral-eq (suc (suc k) ∷ []) = refl

    base-add-eq : _
    base-add-eq (zero ∷ []) a b = base-add _ _ _ ∙ cong (base 0) (sym (pres· (snd (invGroupIso (H⁰-Sⁿ≅ℤ n))) a b))
    base-add-eq (one ∷ []) a b = base-add _ _ _ ∙ cong (base (suc n)) (sym (pres· (snd (invGroupIso (Hⁿ-Sⁿ≅ℤ n))) a b))
    base-add-eq (suc (suc k) ∷ []) a b = +H*Rid _

-----------------------------------------------------------------------------
-- Morphism on ℤ[x]

  -- doesn't compute without an abstract value !
  ℤ[x]→H*-Sⁿ-pres1 : ℤ[x]→H*-Sⁿ (1Pℤ) ≡ 1H*
  ℤ[x]→H*-Sⁿ-pres1 = T0m-pres1 n

  ℤ[x]→H*-Sⁿ-pres+ : (x y : ℤ[x]) → ℤ[x]→H*-Sⁿ (x +Pℤ y) ≡ ℤ[x]→H*-Sⁿ x +H* ℤ[x]→H*-Sⁿ y
  ℤ[x]→H*-Sⁿ-pres+ x y = refl

  T0 = T0m n
  T0g = T0mg n
  T0-pos0 = T0m-pos0 n
  T0-posS = T0m-posS n
  T0-neg0 = T0m-neg0 n
  T0-negS = T0m-negS n

-- cup product on H⁰ → Hⁿ → Hⁿ
  module _
    (l : ℕ)
    (Tl : (z : ℤ) → coHom l (S₊ (suc n)))
    (Tlg : IsGroupHom (ℤG .snd) Tl (coHomGr l (S₊ (suc n)) .snd))
    where

      pres·-base-case-0l : (a : ℤ) → (b : ℤ) →
                            Tl (a ·ℤ b) ≡ (T0 a) ⌣ (Tl b)
      pres·-base-case-0l (pos zero)       b = pres1 Tlg
                                               ∙ sym (T0-pos0 (Tl b))
      pres·-base-case-0l (pos (suc k))    b = pres· Tlg b (pos k ·ℤ b)
                                               ∙ cong (λ X → (Tl b) +ₕ X) (pres·-base-case-0l (pos k) b)
                                               ∙ sym (T0-posS k (Tl b))
      pres·-base-case-0l (negsuc zero)    b =  presinv Tlg b
                                               ∙ sym (T0-neg0 (Tl b))
      pres·-base-case-0l (negsuc (suc k)) b = cong Tl (+ℤComm (-ℤ b) (negsuc k ·ℤ b))
                                               ∙ pres· Tlg (negsuc k ·ℤ b) (-ℤ b)
                                               ∙ cong₂ _+ₕ_ (pres·-base-case-0l (negsuc k) b)
                                                            (presinv Tlg b)
                                               ∙ sym (T0-negS k (Tl b))

-- Nice packging of the proof
  pres·-base-case-int : (k : ℕ) → (a : ℤ) → (l : ℕ) → (b : ℤ) →
                         ℤ[x]→H*-Sⁿ (baseP (k ∷ []) a ·Pℤ baseP (l ∷ []) b)
                         ≡ ℤ[x]→H*-Sⁿ (baseP (k ∷ []) a) cup ℤ[x]→H*-Sⁿ (baseP (l ∷ []) b)
  pres·-base-case-int zero          a zero          b = cong (base 0) (pres·-base-case-0l 0 (inv (fst (H⁰-Sⁿ≅ℤ n)))
                                                                                (snd (invGroupIso (H⁰-Sⁿ≅ℤ n))) a b)
  pres·-base-case-int zero          a one           b = cong (base (suc n)) (pres·-base-case-0l (suc n) (inv (fst (Hⁿ-Sⁿ≅ℤ n)))
                                                                                (snd (invGroupIso (Hⁿ-Sⁿ≅ℤ n))) a b)
  pres·-base-case-int zero          a (suc (suc l)) b = refl
  pres·-base-case-int one           a zero          b = cong ℤ[x]→H*-Sⁿ (·PℤComm (baseP (one ∷ []) a) (baseP (zero ∷ []) b))
                                                         ∙ pres·-base-case-int zero b one a
                                                         ∙ gradCommRing (S₊ (suc n)) 0 (suc n) (inv (fst (H⁰-Sⁿ≅ℤ n)) b) (inv (fst (Hⁿ-Sⁿ≅ℤ n)) a)
  pres·-base-case-int one           a one           b = sym (base-neutral (suc n +' suc n))
                                                         ∙ cong (base (suc n +' suc n))
                                                           (isOfHLevelRetractFromIso
                                                                1
                                                                (fst (Hⁿ-Sᵐ≅0 (suc (n +n n)) n (λ p → <→≢ (n , (+n-comm n (suc n))) (sym p))))
                                                                isPropUnit _ _)
  pres·-base-case-int one           a (suc (suc l)) b = refl
  pres·-base-case-int (suc (suc k)) a             l b = refl

  pres·-base-case-vec : (v : Vec ℕ 1) → (a : ℤ) → (v' : Vec ℕ 1) → (b : ℤ) →
                ℤ[x]→H*-Sⁿ (baseP v a ·Pℤ baseP v' b)
              ≡ ℤ[x]→H*-Sⁿ (baseP v a) cup ℤ[x]→H*-Sⁿ (baseP v' b)
  pres·-base-case-vec (k ∷ []) a (l ∷ []) b = pres·-base-case-int k a l b

  -- proof of the morphism
  ℤ[x]→H*-Sⁿ-pres· : (x y : ℤ[x]) → ℤ[x]→H*-Sⁿ (x ·Pℤ y) ≡ ℤ[x]→H*-Sⁿ x cup ℤ[x]→H*-Sⁿ y
  ℤ[x]→H*-Sⁿ-pres· = Poly-Ind-Prop.f _ _ _
                         (λ x p q i y j → isSetH* _ _ (p y) (q y) i j)
                         (λ y → refl)
                         base-case
                         λ {U V} ind-U ind-V y → cong₂ _+H*_ (ind-U y) (ind-V y)
    where
    base-case : _
    base-case (k ∷ []) a = Poly-Ind-Prop.f _ _ _ (λ _ → isSetH* _ _)
                           (sym (RingTheory.0RightAnnihilates (H*R (S₊ (suc n))) _))
                           (λ v' b → pres·-base-case-vec (k ∷ []) a v' b)
                           λ {U V} ind-U ind-V → (cong₂ _+H*_ ind-U ind-V) ∙ sym (·H*Rdist+ _ _ _)

-----------------------------------------------------------------------------
-- Function on ℤ[x]/x + morphism

  ℤ[x]→H*-Sⁿ-cancelX : (k : Fin 1) → ℤ[x]→H*-Sⁿ (<X²> k) ≡ 0H*
  ℤ[x]→H*-Sⁿ-cancelX zero = refl

  ℤ[X]→H*-Sⁿ : RingHom (CommRing→Ring ℤ[X]) (H*R (S₊ (suc n)))
  fst ℤ[X]→H*-Sⁿ = ℤ[x]→H*-Sⁿ
  snd ℤ[X]→H*-Sⁿ = makeIsRingHom ℤ[x]→H*-Sⁿ-pres1 ℤ[x]→H*-Sⁿ-pres+ ℤ[x]→H*-Sⁿ-pres·

  ℤ[X]/X²→H*R-Sⁿ : RingHom (CommRing→Ring ℤ[X]/X²) (H*R (S₊ (suc n)))
  ℤ[X]/X²→H*R-Sⁿ = Quotient-FGideal-CommRing-Ring.f ℤ[X] (H*R (S₊ (suc n))) ℤ[X]→H*-Sⁿ <X²> ℤ[x]→H*-Sⁿ-cancelX

  ℤ[x]/x²→H*-Sⁿ : ℤ[x]/x² → H* (S₊ (suc n))
  ℤ[x]/x²→H*-Sⁿ = fst ℤ[X]/X²→H*R-Sⁿ

-----------------------------------------------------------------------------
-- Converse Sens on ℤ[X] + ℤ[x]/x

  base-trad-H* : (k : ℕ) → (a : coHom k (S₊ (suc n))) → (x : partℕ k) → ℤ[x]
  base-trad-H* k a (is0 x) = baseP (0 ∷ []) (fun (fst (H⁰-Sⁿ≅ℤ n)) (substCoHom x a))
  base-trad-H* k a (isSn x) = baseP (1 ∷ []) (fun (fst (Hⁿ-Sⁿ≅ℤ n)) (substCoHom x a))
  base-trad-H* k a (else x) = 0Pℤ

  H*-Sⁿ→ℤ[x] : H* (S₊ (suc n)) → ℤ[x]
  H*-Sⁿ→ℤ[x] = DS-Rec-Set.f _ _ _ _ isSetPℤ
       0Pℤ
       (λ k a → base-trad-H* k a (part k))
       _+Pℤ_
       +PℤAssoc
       +PℤRid
       +PℤComm
       (λ k → base-neutral-eq k (part k))
       λ k a b → base-add-eq k a b (part k)
    where

    base-neutral-eq : (k : ℕ) → (x : partℕ k) → base-trad-H* k (0ₕ k) x ≡ 0Pℤ
    base-neutral-eq k (is0 x)  = cong (baseP (0 ∷ [])) (cong (fun (fst (H⁰-Sⁿ≅ℤ n))) (subst-0 k 0 x))
                                 ∙ cong (baseP (0 ∷ [])) (pres1 (snd (H⁰-Sⁿ≅ℤ n)))
                                 ∙ base-0P (0 ∷ [])
    base-neutral-eq k (isSn x) = cong (baseP (1 ∷ [])) (cong (fun (fst (Hⁿ-Sⁿ≅ℤ n))) (subst-0 k (suc n) x))
                                 ∙ cong (baseP (1 ∷ [])) (pres1 (snd (Hⁿ-Sⁿ≅ℤ n)))
                                 ∙ base-0P (1 ∷ [])
    base-neutral-eq k (else x) = refl

    base-add-eq : (k : ℕ) → (a b : coHom k (S₊ (suc n))) → (x : partℕ k)
                  → base-trad-H* k a x +Pℤ base-trad-H* k b x ≡ base-trad-H* k (a +ₕ b) x
    base-add-eq k a b (is0 x) = base-poly+ _ _ _
                                ∙ cong (baseP (0 ∷ [])) (sym (pres· (snd (H⁰-Sⁿ≅ℤ n)) _ _))
                                ∙ cong (baseP (0 ∷ [])) (cong (fun (fst (H⁰-Sⁿ≅ℤ n))) (sym (subst-+ k a b 0 x)))
    base-add-eq k a b (isSn x) =  base-poly+ _ _ _
                                  ∙ cong (baseP (1 ∷ [])) (sym (pres· (snd (Hⁿ-Sⁿ≅ℤ n)) _ _))
                                  ∙ cong (baseP (1 ∷ [])) (cong (fun (fst (Hⁿ-Sⁿ≅ℤ n))) (sym (subst-+ k a b (suc n) x)))
    base-add-eq k a b (else x) = +PℤRid _

  H*-Sⁿ→ℤ[x]-pres+ : (x y : H* (S₊ (suc n))) → H*-Sⁿ→ℤ[x] ( x +H* y) ≡ H*-Sⁿ→ℤ[x] x +Pℤ H*-Sⁿ→ℤ[x] y
  H*-Sⁿ→ℤ[x]-pres+ x y = refl

  H*-Sⁿ→ℤ[x]/x² : H* (S₊ (suc n)) → ℤ[x]/x²
  H*-Sⁿ→ℤ[x]/x² = [_] ∘ H*-Sⁿ→ℤ[x]

  H*-Sⁿ→ℤ[x]/x²-pres+ : (x y : H* (S₊ (suc n))) → H*-Sⁿ→ℤ[x]/x² (x +H* y) ≡ (H*-Sⁿ→ℤ[x]/x² x) +PℤI (H*-Sⁿ→ℤ[x]/x² y)
  H*-Sⁿ→ℤ[x]/x²-pres+ x y = refl

-----------------------------------------------------------------------------
-- Section

  e-sect-base : (k : ℕ) → (a : coHom k (S₊ (suc n))) → (x : partℕ k) →
                ℤ[x]/x²→H*-Sⁿ [ (base-trad-H* k a x) ] ≡ base k a
  e-sect-base k a (is0 x)  = cong (base 0) (leftInv (fst (H⁰-Sⁿ≅ℤ n)) (substCoHom x a))
                             ∙ sym (constSubstCommSlice (λ x → coHom x (S₊ (suc n))) (H* (S₊ (suc n))) base x a)

  e-sect-base k a (isSn x) = cong (base (suc n)) (leftInv (fst (Hⁿ-Sⁿ≅ℤ n)) (substCoHom x a))
                             ∙ sym (constSubstCommSlice (λ x → coHom x (S₊ (suc n))) (H* (S₊ (suc n))) base x a)
  e-sect-base k a (else x) = sym (base-neutral k)
                             ∙ constSubstCommSlice ((λ x → coHom x (S₊ (suc n)))) ((H* (S₊ (suc n)))) base (suc-predℕ k (fst x)) (0ₕ k)
                             ∙ cong (base (suc (predℕ k)))
                               ((isOfHLevelRetractFromIso 1
                                       (fst (Hⁿ-Sᵐ≅0 (predℕ k) n λ p → snd x (suc-predℕ k (fst x) ∙ cong suc p)))
                                       isPropUnit _ _))
                             ∙ sym (constSubstCommSlice ((λ x → coHom x (S₊ (suc n)))) ((H* (S₊ (suc n)))) base (suc-predℕ k (fst x)) a)

  e-sect : (x : H* (S₊ (suc n))) → ℤ[x]/x²→H*-Sⁿ (H*-Sⁿ→ℤ[x]/x² x) ≡ x
  e-sect = DS-Ind-Prop.f _ _ _ _ (λ _ → isSetH* _ _)
           refl
           (λ k a → e-sect-base k a (part k))
           λ {U V} ind-U ind-V → cong₂ _+H*_ ind-U ind-V

-----------------------------------------------------------------------------
-- Retraction

  e-retr : (x : ℤ[x]/x²) → H*-Sⁿ→ℤ[x]/x² (ℤ[x]/x²→H*-Sⁿ x) ≡ x
  e-retr = SQ.elimProp (λ _ → isSetPℤI _ _)
           (Poly-Ind-Prop.f _ _ _ (λ _ → isSetPℤI _ _)
           refl
           base-case
           λ {U V} ind-U ind-V → cong₂ _+PℤI_ ind-U ind-V)
           where
           base-case : _
           base-case (zero ∷ []) a = cong [_] (cong (base-trad-H* 0 (inv (fst (H⁰-Sⁿ≅ℤ n)) a)) part0)
                                     ∙ cong [_] (cong (baseP (0 ∷ [])) (cong (fun (fst (H⁰-Sⁿ≅ℤ n)))
                                                                             (substReflCoHom (inv (fst (H⁰-Sⁿ≅ℤ n)) a))))
                                     ∙ cong [_] (cong (baseP (0 ∷ [])) (rightInv (fst (H⁰-Sⁿ≅ℤ n)) a))
           base-case (one ∷ []) a  = cong [_] (cong (base-trad-H* (suc n) (inv (fst (Hⁿ-Sⁿ≅ℤ n)) a)) (partSn (part (suc n))))
                                     ∙ cong [_] (cong (baseP (1 ∷ [])) (cong (fun (fst (Hⁿ-Sⁿ≅ℤ n)))
                                                                             (substReflCoHom (inv (fst (Hⁿ-Sⁿ≅ℤ n)) a))))
                                     ∙ cong [_] (cong (baseP (1 ∷ [])) (rightInv (fst (Hⁿ-Sⁿ≅ℤ n)) a))
           base-case (suc (suc k) ∷ []) a = eq/ 0Pℤ (baseP (suc (suc k) ∷ []) a)  ∣ ((λ x → baseP (k ∷ []) (-ℤ a)) , helper) ∣₁
             where
             helper : _
             helper = (+PℤLid _) ∙ cong₂ baseP (cong (λ X → X ∷ []) (sym (+n-comm k 2))) (sym (·ℤRid _)) ∙ (sym (+PℤRid _))

-----------------------------------------------------------------------------
-- Computation of the Cohomology Ring

module _ (n : ℕ) where

  open Equiv-Sn-Properties n

  Sⁿ-CohomologyRing : RingEquiv (CommRing→Ring ℤ[X]/X²) (H*R (S₊ (suc n)))
  fst Sⁿ-CohomologyRing = isoToEquiv is
    where
    is : Iso ℤ[x]/x² (H* (S₊ (suc n)))
    fun is = ℤ[x]/x²→H*-Sⁿ
    inv is = H*-Sⁿ→ℤ[x]/x²
    rightInv is = e-sect
    leftInv is = e-retr
  snd Sⁿ-CohomologyRing = snd ℤ[X]/X²→H*R-Sⁿ

  CohomologyRing-Sⁿ : RingEquiv (H*R (S₊ (suc n))) (CommRing→Ring ℤ[X]/X²)
  CohomologyRing-Sⁿ = RingEquivs.invEquivRing Sⁿ-CohomologyRing

max_stars_repo_name: xekoukou/cubical

max_issues_repo_name: xekoukou/cubical

max_forks_repo_name: xekoukou/cubical


text:
{-# OPTIONS --type-in-type #-}

data ⊥ : Set where

℘ : ∀ {ℓ} → Set ℓ → Set _
℘ {ℓ} S = S → Set

U : Set
U = ∀ (X : Set) → (℘ (℘ X) → X) → ℘ (℘ X)

{- If using two impredicative universe layers instead of type-in-type:
U : Set₁
U = ∀ (X : Set₁) → (℘ (℘ X) → X) → ℘ (℘ X)
-}

τ : ℘ (℘ U) → U
τ t = λ X f p → t (λ x → p (f (x X f)))

σ : U → ℘ (℘ U)
σ s = s U τ

Δ : ℘ U
Δ y = (∀ p → σ y p → p (τ (σ y))) → ⊥

Ω : U
Ω = τ (λ p → (∀ x → σ x p → p x))

R : ∀ p → (∀ x → σ x p → p x) → p Ω
R _ 𝟙 = 𝟙 Ω (λ x → 𝟙 (τ (σ x)))

M : ∀ x → σ x Δ → Δ x
M _ 𝟚 𝟛 = 𝟛 Δ 𝟚 (λ p → 𝟛 (λ y → p (τ (σ y))))

L : (∀ p → (∀ x → σ x p → p x) → p Ω) → ⊥
L 𝟘 = 𝟘 Δ M (λ p → 𝟘 (λ y → p (τ (σ y))))

false : ⊥
false = L R


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.Group where

open import Cubical.Algebra.Group.Base public
open import Cubical.Algebra.Group.Properties public
open import Cubical.Algebra.Group.Morphism public
open import Cubical.Algebra.Group.MorphismProperties public
open import Cubical.Algebra.Group.Algebra public


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Signs
------------------------------------------------------------------------

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

module Data.Sign where

open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Nullary using (yes; no)

-- Signs.

data Sign : Set where
  - : Sign
  + : Sign

-- Decidable equality.

infix 4 _≟_

_≟_ : Decidable {A = Sign} _≡_
- ≟ - = yes refl
- ≟ + = no λ()
+ ≟ - = no λ()
+ ≟ + = yes refl

-- The opposite sign.

opposite : Sign → Sign
opposite - = +
opposite + = -

-- "Multiplication".

infixl 7 _*_

_*_ : Sign → Sign → Sign
+ * s₂ = s₂
- * s₂ = opposite s₂


text:
module RAdjunctions.RAdj2RMon where

open import Function
open import Relation.Binary.HeterogeneousEquality
open import Categories
open import Functors
open import RMonads
open import RAdjunctions

open Cat
open Fun
open RAdj

Adj2Mon : ∀{a b c d e f}{C : Cat {a}{b}}{D : Cat {c}{d}}{E : Cat {e}{f}}
          {J : Fun C D} → RAdj J E → RMonad J
Adj2Mon {C = C}{D}{E}{J} A = record{
  T    = OMap (R A) ∘ OMap (L A);
  η    = left A (iden E);
  bind = HMap (R A) ∘ right A;
  law1 = trans (cong (HMap (R A)) (lawa A (iden E))) (fid (R A));
  law2 = λ {_ _ f} →
    trans (cong (comp D (HMap (R A) (right A f)))
                (trans (sym (idr D))
                       (cong (comp D (left A (iden E))) (sym (fid J)))))
          (trans (natleft A (iden C) (right A f) (iden E))
                 (trans (cong (left A)
                              (trans (cong (comp E (right A f))
                                           (trans (idl E) (fid (L A))))
                                     (idr E)))
                        (lawb A f)));
  law3 = λ{_ _ _ f g} →
    trans (cong (HMap (R A))
                (trans (trans (cong (right A)
                                    (cong (comp D (HMap (R A) (right A g)))
                                          (trans (sym (idr D))
                                                 (cong (comp D f)
                                                       (sym (fid J))))))
                              (trans (natright A (iden C) (right A g) f)
                                     (trans (sym (ass E))
                                            (cong (comp E (comp E (right A g)
                                                                  (right A f)))
                                                  (fid (L A))))))
                       (idr E)))
          (fcomp (R A))}

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
{-# OPTIONS --safe --postfix-projections #-}
module Cubical.Algebra.OrderedCommMonoid.PropCompletion where
{-
  The completion of an ordered monoid, viewed as monoidal prop-enriched category.
  This is used in the construction of the upper naturals, which is an idea of David
  Jaz Myers presented here

  https://felix-cherubini.de/myers-slides-II.pdf

  It should be straight forward, but tedious,
  to generalize this to enriched monoidal categories.
-}

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

open import Cubical.Functions.Logic
open import Cubical.Functions.Embedding

open import Cubical.Data.Sigma

open import Cubical.HITs.PropositionalTruncation renaming (rec to propTruncRec; rec2 to propTruncRec2)

open import Cubical.Algebra.CommMonoid.Base
open import Cubical.Algebra.OrderedCommMonoid

open import Cubical.Relation.Binary.Poset

private
  variable
    ℓ : Level

module PropCompletion (ℓ : Level) (M : OrderedCommMonoid ℓ ℓ) where
  open OrderedCommMonoidStr (snd M)
  _≤p_ : fst M → fst M → hProp ℓ
  n ≤p m = (n ≤ m) , (is-prop-valued _ _)

  isUpwardClosed : (s : fst M → hProp ℓ) → Type _
  isUpwardClosed s = (n m : fst M) → n ≤ m → fst (s n) → fst (s m)

  isPropUpwardClosed : (N : fst M → hProp ℓ) → isProp (isUpwardClosed N)
  isPropUpwardClosed N =
    isPropΠ4 (λ _ m _ _ → snd (N m))

  isSetM→Prop : isSet (fst M → hProp ℓ)
  isSetM→Prop = isOfHLevelΠ 2 λ _ → isSetHProp

  M↑ : Type _
  M↑ = Σ[ s ∈ (fst M → hProp ℓ)] isUpwardClosed s

  isSetM↑ : isSet M↑
  isSetM↑ = isOfHLevelΣ 2 isSetM→Prop λ s → isOfHLevelSuc 1 (isPropUpwardClosed s)

  _isUpperBoundOf_ : fst M → M↑ → Type ℓ
  n isUpperBoundOf s = fst (fst s n)

  isBounded : (s : M↑) → Type _
  isBounded s = ∃[ m ∈ (fst M) ] (m isUpperBoundOf s)

  isPropIsBounded : (s : M↑) → isProp (isBounded s)
  isPropIsBounded s = isPropPropTrunc

  _^↑ : fst M → M↑
  n ^↑ = n ≤p_ , isUpwardClosed≤
    where
      isUpwardClosed≤ : {m : fst M} → isUpwardClosed (m ≤p_)
      isUpwardClosed≤ = λ {_ _ n≤k m≤n → is-trans _ _ _ m≤n n≤k}

  isBounded^ : (m : fst M) → isBounded (m ^↑)
  isBounded^ m = ∣ (m , (is-refl m)) ∣₁

  1↑ : M↑
  1↑ = ε ^↑

  _·↑_ : M↑ → M↑ → M↑
  s ·↑ l = seq , seqIsUpwardClosed
         where
           seq : fst M → hProp ℓ
           seq n = (∃[ (a , b) ∈ (fst M) × (fst M) ] fst ((fst s a) ⊓ (fst l b) ⊓ ((a · b) ≤p n) )) ,
                   isPropPropTrunc
           seqIsUpwardClosed : isUpwardClosed seq
           seqIsUpwardClosed n m n≤m =
             propTruncRec
               isPropPropTrunc
               λ {((a , b) , wa , (wb , a·b≤n)) → ∣ (a , b) , wa , (wb , is-trans _ _ _ a·b≤n n≤m) ∣₁}

  ·presBounded : (s l : M↑) (bs : isBounded s) (bl : isBounded l) → isBounded (s ·↑ l)
  ·presBounded s l =
    propTruncRec2
      isPropPropTrunc
      λ {(m , s≤m) (k , l≤k)
          → ∣ (m · k) , ∣ (m , k) , (s≤m , (l≤k , (is-refl (m · k)))) ∣₁ ∣₁
        }

  {- convenience functions for the proof that ·↑ is the multiplication of a monoid -}
  typeAt : fst M → M↑ → Type _
  typeAt n s = fst (fst s n)

  M↑Path : {s l : M↑} → ((n : fst M) → typeAt n s ≡ typeAt n l) → s ≡ l
  M↑Path {s = s} {l = l} pwPath = path
     where
       seqPath : fst s ≡ fst l
       seqPath i n = subtypePathReflection (λ A → isProp A , isPropIsProp)
                                           (fst s n)
                                           (fst l n)
                                           (pwPath n) i
       path : s ≡ l
       path = subtypePathReflection (λ s → isUpwardClosed s , isPropUpwardClosed s) s l seqPath

  pathFromImplications : (s l : M↑)
           → ((n : fst M) → typeAt n s → typeAt n l)
           → ((n : fst M) → typeAt n l → typeAt n s)
           → s ≡ l
  pathFromImplications s l s→l l→s =
      M↑Path λ n → cong fst (propPath n)
            where propPath : (n : fst M) → fst s n ≡ fst l n
                  propPath n = ⇒∶ s→l n
                               ⇐∶ l→s n

  ^↑Pres· : (x y : fst M) → (x · y) ^↑ ≡ (x ^↑) ·↑ (y ^↑)
  ^↑Pres· x y = pathFromImplications ((x · y) ^↑) ((x ^↑) ·↑ (y ^↑)) (⇐) ⇒
    where
      ⇐ : (n : fst M) → typeAt n ((x · y) ^↑) → typeAt n ((x ^↑) ·↑ (y ^↑))
      ⇐ n x·y≤n = ∣ (x , y) , ((is-refl _) , ((is-refl _) , x·y≤n)) ∣₁

      ⇒ : (n : fst M) → typeAt n ((x ^↑) ·↑ (y ^↑)) → typeAt n ((x · y) ^↑)
      ⇒ n = propTruncRec
              (snd (fst ((x · y) ^↑) n))
              λ {((m , l) , x≤m , (y≤l , m·l≤n))
                  → is-trans _ _ _
                             (is-trans _ _ _ (MonotoneR x≤m)
                                             (MonotoneL y≤l))
                             m·l≤n
                }

  ·↑Comm : (s l : M↑) → s ·↑ l ≡ l ·↑ s
  ·↑Comm s l = M↑Path λ n → cong fst (propPath n)
    where implication : (s l : M↑) (n : fst M) → fst (fst (s ·↑ l) n) → fst (fst (l ·↑ s) n)
          implication s l n = propTruncRec
                             isPropPropTrunc
                             (λ {((a , b) , wa , (wb , a·b≤n))
                               → ∣ (b , a) , wb , (wa , subst (λ k → fst (k ≤p n)) (·Comm a b) a·b≤n) ∣₁ })
          propPath : (n : fst M) → fst (s ·↑ l) n ≡ fst (l ·↑ s) n
          propPath n = ⇒∶ implication s l n
                       ⇐∶ implication l s n

  ·↑Rid : (s : M↑) → s ·↑ 1↑ ≡ s
  ·↑Rid s = pathFromImplications (s ·↑ 1↑) s (⇒) ⇐
    where ⇒ : (n : fst M) → typeAt n (s ·↑ 1↑) → typeAt n s
          ⇒ n = propTruncRec
                  (snd (fst s n))
                  (λ {((a , b) , sa , (1b , a·b≤n))
                     → (snd s) a n ( subst (_≤ n) (·IdR a) (is-trans _ _ _ (MonotoneL 1b) a·b≤n)) sa })
          ⇐ : (n : fst M) → typeAt n s → typeAt n (s ·↑ 1↑)
          ⇐ n = λ sn → ∣ (n , ε) , (sn , (is-refl _ , subst (_≤ n) (sym (·IdR n)) (is-refl _))) ∣₁

  ·↑Assoc : (s l k : M↑) → s ·↑ (l ·↑ k) ≡ (s ·↑ l) ·↑ k
  ·↑Assoc s l k = pathFromImplications (s ·↑ (l ·↑ k)) ((s ·↑ l) ·↑ k) (⇒) ⇐
    where ⇒ : (n : fst M) → typeAt n (s ·↑ (l ·↑ k)) → typeAt n ((s ·↑ l) ·↑ k)
          ⇒ n = propTruncRec
                isPropPropTrunc
                λ {((a , b) , sa , (l·kb , a·b≤n))
                     → propTruncRec
                         isPropPropTrunc
                         (λ {((a' , b') , la' , (kb' , a'·b'≤b))
                         → ∣ ((a · a') , b') , ∣ (a , a') , (sa , (la' , is-refl _)) ∣₁ , kb' ,
                             (let a·⟨a'·b'⟩≤n = (is-trans _ _ _ (MonotoneL a'·b'≤b) a·b≤n)
                              in subst (_≤ n) (·Assoc a a' b') a·⟨a'·b'⟩≤n) ∣₁
                            }) l·kb
                   }
          ⇐ : _
          ⇐ n = propTruncRec
                isPropPropTrunc
                λ {((a , b) , s·l≤a , (k≤b , a·b≤n))
                     → propTruncRec
                         isPropPropTrunc
                         (λ {((a' , b') , s≤a' , (l≤b' , a'·b'≤a))
                         → ∣ (a' , b' · b) , s≤a' , ( ∣ (b' , b) , l≤b' , (k≤b , is-refl _) ∣₁ ,
                             (let ⟨a'·b'⟩·b≤n = (is-trans _ _ _ (MonotoneR a'·b'≤a) a·b≤n)
                              in subst (_≤ n) (sym (·Assoc a' b' b)) ⟨a'·b'⟩·b≤n) ) ∣₁
                            }) s·l≤a
                   }

  asCommMonoid : CommMonoid (ℓ-suc ℓ)
  asCommMonoid = makeCommMonoid 1↑ _·↑_ isSetM↑ ·↑Assoc ·↑Rid ·↑Comm

  {-
    Poset structure on M↑
  -}
  _≤↑_ : (s l : M↑) → Type _
  s ≤↑ l = (m : fst M) → fst ((fst l) m) → fst ((fst s) m)

  isBounded→≤↑ : (s : M↑) → isBounded s → ∃[ m ∈ fst M ] (s ≤↑ (m ^↑))
  isBounded→≤↑ s =
    propTruncRec
      isPropPropTrunc
      λ {(m , mIsBound)
           → ∣ m , (λ n m≤n → snd s m n m≤n mIsBound) ∣₁
        }

  ≤↑IsProp : (s l : M↑) → isProp (s ≤↑ l)
  ≤↑IsProp s l = isPropΠ2 (λ x p → snd (fst s x))

  ≤↑IsRefl : (s : M↑) → s ≤↑ s
  ≤↑IsRefl s = λ m x → x

  ≤↑IsTrans : (s l t : M↑) → s ≤↑ l → l ≤↑ t → s ≤↑ t
  ≤↑IsTrans s l t p q x = (p x) ∘ (q x)

  ≤↑IsAntisym : (s l : M↑) → s ≤↑ l → l ≤↑ s → s ≡ l
  ≤↑IsAntisym s l p q = pathFromImplications _ _ q p

  {-
    Compatability with the monoid structure
  -}
  ·↑IsRMonotone : (l t s : M↑) → l ≤↑ t → (l ·↑ s) ≤↑ (t ·↑ s)
  ·↑IsRMonotone l t s p x =
    propTruncRec
      isPropPropTrunc
      λ { ((a , b) , l≤a , (s≤b , a·b≤x)) → ∣ (a , b) , p a l≤a , s≤b , a·b≤x ∣₁}

  ·↑IsLMonotone : (l t s : M↑) → l ≤↑ t → (s ·↑ l) ≤↑ (s ·↑ t)
  ·↑IsLMonotone l t s p x =
    propTruncRec
      isPropPropTrunc
      λ {((a , b) , s≤a , (l≤b , a·b≤x)) → ∣ (a , b) , s≤a , p b l≤b , a·b≤x ∣₁}

  asOrderedCommMonoid : OrderedCommMonoid (ℓ-suc ℓ) ℓ
  asOrderedCommMonoid .fst = _
  asOrderedCommMonoid .snd .OrderedCommMonoidStr._≤_ = _≤↑_
  asOrderedCommMonoid .snd .OrderedCommMonoidStr._·_ = _·↑_
  asOrderedCommMonoid .snd .OrderedCommMonoidStr.ε = 1↑
  asOrderedCommMonoid .snd .OrderedCommMonoidStr.isOrderedCommMonoid =
    IsOrderedCommMonoidFromIsCommMonoid
          (CommMonoidStr.isCommMonoid (snd asCommMonoid))
          ≤↑IsProp ≤↑IsRefl ≤↑IsTrans ≤↑IsAntisym ·↑IsRMonotone ·↑IsLMonotone

  boundedSubstructure : OrderedCommMonoid (ℓ-suc ℓ) ℓ
  boundedSubstructure =
    makeOrderedSubmonoid
      asOrderedCommMonoid
      (λ s → (isBounded s , isPropIsBounded s))
      ·presBounded
      (isBounded^ ε)

PropCompletion :
    OrderedCommMonoid ℓ ℓ
  → OrderedCommMonoid (ℓ-suc ℓ) ℓ
PropCompletion M = PropCompletion.asOrderedCommMonoid _ M

BoundedPropCompletion :
     OrderedCommMonoid ℓ ℓ
  → OrderedCommMonoid (ℓ-suc ℓ) ℓ
BoundedPropCompletion M = PropCompletion.boundedSubstructure _ M

isSetBoundedPropCompletion :
     (M : OrderedCommMonoid ℓ ℓ)
   → isSet (⟨ BoundedPropCompletion M ⟩)
isSetBoundedPropCompletion M =
  isSetΣSndProp (isSetOrderedCommMonoid (PropCompletion M))
                λ x → PropCompletion.isPropIsBounded _ M x

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- Andreas, 2018-10-18, re issue #2757
--
-- Extracted this snippet from the standard library
-- as it caused problems during work in #2757
-- (runtime erasue using 0-quantity).

-- {-# OPTIONS -v tc.lhs.unify:65 -v tc.irr:50 #-}

open import Agda.Builtin.Size

data ⊥ : Set where

mutual
  data Conat (i : Size) : Set where
    zero : Conat i
    suc : ∞Conat i → Conat i

  record ∞Conat (i : Size) : Set where
    coinductive
    field force : ∀{j : Size< i} → Conat j
open ∞Conat

infinity : ∀ {i} → Conat i
infinity = suc λ where .force → infinity

data Finite : Conat ∞ → Set where
  zero : Finite zero
  suc  : ∀ {n} → Finite (n .force) → Finite (suc n)

¬Finite∞ : Finite infinity → ⊥
¬Finite∞ (suc p) = ¬Finite∞ p

-- The problem was that the usableMod check in the
-- unifier (LHS.Unify) refuted this pattern match
-- because a runtime-erased argument ∞ (via meta-variable)
-- the the extended lambda.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import MJ.Types
open import MJ.Classtable

import MJ.Syntax as Syntax
import MJ.Semantics.Values as Values

--
-- Substitution-free interpretation of welltyped MJ
--

module MJ.Semantics.Functional {c} (Σ : CT c) (ℂ : Syntax.Impl Σ) where

open import Prelude

open import Data.Vec hiding (init)
open import Data.Vec.All.Properties.Extra as Vec∀++
open import Data.Sum
open import Data.List as List
open import Data.List.All as List∀ hiding (lookup)
open import Data.List.All.Properties.Extra
open import Data.List.Any
open import Data.List.Prefix
open import Data.List.Properties.Extra as List+
open import Data.Maybe as Maybe using (Maybe; just; nothing)
open import Relation.Binary.PropositionalEquality
open import Data.Star.Indexed

import Data.Vec.All as Vec∀

open Membership-≡
open Values Σ
open CT Σ
open Syntax Σ

-- open import MJ.Semantics.Objects.Hierarchical Σ ℂ using (encoding)
open import MJ.Semantics.Objects.Flat Σ ℂ using (encoding)
open ObjEncoding encoding
open Heap encoding

⊒-res : ∀ {a}{I : World c → Set a}{W W'} → W' ⊒ W → Res I W' → Res I W
⊒-res {W = W} p (W' , ext' , μ' , v) = W' , ⊑-trans p ext' , μ' , v

mutual

  --
  -- object initialization
  --

  init : ∀ {W} cid → Cont (fromList (Class.constr (clookup cid))) (λ W → Obj W cid) W
  init cid E μ with Impl.bodies ℂ cid
  init cid E μ | impl super-args defs with evalₙ (defs FLD) E μ
  ... | W₁ , ext₁ , μ₁ , vs with clookup cid | inspect clookup cid

  -- case *without* super initialization
  init cid E μ | impl nothing defs | (W₁ , ext₁ , μ₁ , vs) | (class nothing constr decls) | [ eq ] =
    W₁ , ext₁ , μ₁ , vs

  -- case *with* super initialization
  init cid E μ | impl (just sc) defs | (W₁ , ext₁ , μ₁ , vs) |
    (class (just x) constr decls) | [ eq ] with evalₑ-all sc (Vec∀.map (coerce ext₁) E) μ₁
  ... | W₂ , ext₂ , μ₂ , svs with init x (all-fromList svs) μ₂
  ... | W₃ , ext₃ , μ₃ , inherited = W₃ , ⊑-trans (⊑-trans ext₁ ext₂) ext₃ , μ₃ ,
    (List∀.map (coerce (⊑-trans ext₂ ext₃)) vs ++-all inherited)

  {-}
  init cid E μ with Impl.bodies ℂ cid
  init cid E μ | impl super-args defs with evalₙ (defs FLD) E μ
  ... | W₁ , ext₁ , μ₁ , vs with clookup cid | inspect clookup cid

  -- case *without* super initialization
  init cid E μ | impl nothing defs | (W₁ , ext₁ , μ₁ , vs) |
    (class nothing constr decls) | [ eq ] =
    , ext₁
    , μ₁
    , record {
      own = λ{
        MTH → List∀.tabulate (λ _ → tt) ;
        FLD → subst (λ C → All _ (Class.decls C FLD)) (sym eq) vs
      };
      inherited = subst (λ C → Maybe.All _ (Class.parent C)) (sym eq) nothing
    }

  -- case *with* super initialization
  init cid E μ | impl (just sc) defs | (W₁ , ext₁ , μ₁ , vs) |
    (class (just x) constr decls) | [ eq ] with evalₑ-all sc (Vec∀.map (coerce ext₁) E) μ₁
  ... | W₂ , ext₂ , μ₂ , svs with init x (all-fromList svs) μ₂
  ... | W₃ , ext₃ , μ₃ , sO =
    , ⊑-trans (⊑-trans ext₁ ext₂) ext₃
    , μ₃
    , record {
      own = λ{
        MTH → List∀.tabulate (λ _ → tt) ;
        FLD → subst
          (λ C → All _ (Class.decls C FLD))
          (sym eq)
          (List∀.map (coerce (⊑-trans ext₂ ext₃)) vs)
      };
      inherited = subst (λ C → Maybe.All _ (Class.parent C)) (sym eq) (just sO)
    }
  -}

  evalₑ-all : ∀ {n}{Γ : Ctx c n}{as} →
              All (Expr Γ) as → ∀ {W} → Cont Γ (λ W' → All (Val W') as) W
  evalₑ-all [] E μ = , ⊑-refl , μ , []
  evalₑ-all (px ∷ exps) E μ with evalₑ px E μ
  ... | W' , ext' , μ' , v with evalₑ-all exps (Vec∀.map (coerce ext') E) μ'
  ... | W'' , ext'' , μ'' , vs = W'' , ⊑-trans ext' ext'' , μ'' , coerce ext'' v ∷ vs

  --
  -- evaluation of expressions
  --

  {-# TERMINATING #-}
  evalₑ : ∀ {n}{Γ : Ctx c n}{a} → Expr Γ a → ∀ {W} → Cont Γ (flip Val a) W
  evalₑ (upcast sub e) E μ with evalₑ e E μ
  ... | W' , ext' , μ' , (ref r s) = W' , ext' , μ' , ref r (<:-trans s sub)

  -- primitive values
  evalₑ unit = pure (const unit)
  evalₑ (num n) = pure (const (num n))

  -- variable lookup
  evalₑ (var i) = pure (λ E → Vec∀.lookup i E)

  -- object allocation
  evalₑ (new C args) {W} E μ with evalₑ-all args E μ
  -- create the object, typed under the current heap shape
  ... | W₁ , ext₁ , μ₁ , vs with init C (all-fromList vs) μ₁
  ... | W₂ , ext₂ , μ₂ , O =
    let
      -- extension fact for the heap extended with the new object allocation
      ext = ∷ʳ-⊒ (obj C) W₂
    in
      , ⊑-trans (⊑-trans ext₁ ext₂) ext
      , all-∷ʳ (List∀.map (coerce ext) μ₂) (coerce ext (obj C O))
      , ref (∈-∷ʳ W₂ (obj C)) refl -- value typed under the extended heap

  -- binary interger operations
  evalₑ (iop f l r) E μ with evalₑ l E μ
  ... | W₁ , ext₁ , μ₁ , (num i) with evalₑ r (Vec∀.map (coerce ext₁) E) μ₁
  ... | W₂ , ext₂ , μ₂ , (num j) = W₂ , ⊑-trans ext₁ ext₂ , μ₂ , num (f i j)

  -- method calls
  evalₑ (call {C} e mtd args) E μ with evalₑ e E μ              -- eval obj expression
  ... | W₁ , ext₁ , μ₁ , r@(ref o sub) with ∈-all o μ₁         -- lookup obj on the heap
  ... | val ()
  ... | obj cid O with evalₑ-all args (Vec∀.map (coerce ext₁) E) μ₁ -- eval arguments
  ... | W₂ , ext₂ , μ₂ , vs =
    -- and finally eval the body of the method under the environment
    -- generated from the call arguments and the object's "this"
    ⊒-res
      (⊑-trans ext₁ ext₂)
      (eval-body cmd (ref (∈-⊒ o ext₂) <:-fact Vec∀.∷ all-fromList vs) μ₂)
    where
      -- get the method definition
      cmd = getDef C mtd ℂ
      -- get a subtyping fact
      <:-fact = <:-trans sub (proj₁ (proj₂ mtd))

  -- field lookup in the heap
  evalₑ (get e fld) E μ with evalₑ e E μ
  ... | W' , ext' , μ' , ref o C<:C₁ with ∈-all o μ'
  ... | (val ())
  -- apply the runtime subtyping fact to weaken the member fact
  ... | obj cid O = W' , ext' , μ' , getter O (mem-inherit Σ C<:C₁ fld)

  --
  -- command evaluation
  --

  evalc : ∀ {n m}{I : Ctx c n}{O : Ctx c m}{W : World c}{a} →
          -- we use a sum for abrupt returns
          Cmd I a O → Cont I (λ W → (Val W a) ⊎ (Env O W)) W

  -- new locals variable
  evalc (loc x e) E μ with evalₑ e E μ
  ... | W₁ , ext₁ , μ₁ , v = W₁ , ext₁ , μ₁ , inj₂ (v Vec∀.∷ (Vec∀.map (coerce ext₁) E))

  -- assigning to a local
  evalc (asgn i x) E μ with evalₑ x E μ
  ... | W₁ , ext₁ , μ₁ , v = W₁ , ext₁ , μ₁ , inj₂ (Vec∀.map (coerce ext₁) E Vec∀++.[ i ]≔ v)

  -- setting a field
  -- start by lookuping up the referenced object on the heap & eval the expression to assign it
  evalc (set rf fld e) E μ with evalₑ rf E μ
  ... | W₁ , ext₁ , μ₁ , ref p s with List∀.lookup μ₁ p | evalₑ e (Vec∀.map (coerce ext₁) E) μ₁
  ... | (val ()) | _
  ... | (obj cid O) | (W₂ , ext₂ , μ₂ , v) = let ext = ⊑-trans ext₁ ext₂ in
    , ext
    , (μ₂ All[ ∈-⊒ p ext₂ ]≔' -- update the store at the reference location
        -- update the object at the member location
        obj cid (
          setter (coerce ext₂ O) (mem-inherit Σ s fld) v
        )
      )
    , (inj₂ $ Vec∀.map (coerce ext) E)

  -- side-effectful expressions
  evalc (do x) E μ with evalₑ x E μ
  ... | W₁ , ext₁ , μ₁ , _ = W₁ , ext₁ , μ₁ , inj₂ (Vec∀.map (coerce ext₁) E)

  -- early returns
  evalc (ret x) E μ with evalₑ x E μ
  ... | W₁ , ext₁ , μ₁ , v = W₁ , ext₁ , μ₁ , inj₁ v

  eval-body : ∀ {n}{I : Ctx c n}{W : World c}{a} → Body I a → Cont I (λ W → Val W a) W
  eval-body (body ε re) E μ = evalₑ re E μ
  eval-body (body (x ◅ xs) re) E μ with evalc x E μ
  ... | W₁ , ext₁ , μ₁ , inj₂ E₁ = ⊒-res ext₁ (eval-body (body xs re) E₁ μ₁)
  ... | W₁ , ext₁ , μ₁ , inj₁ v = _ , ext₁ , μ₁ , v

  evalₙ : ∀ {n}{I : Ctx c n}{W : World c}{as} → All (Body I) as →
          Cont I (λ W → All (Val W) as) W
  evalₙ [] E μ = , ⊑-refl , μ , []
  evalₙ (px ∷ bs) E μ with eval-body px E μ
  ... | W₁ , ext₁ , μ₁ , v with evalₙ bs (Vec∀.map (coerce ext₁) E) μ₁
  ... | W₂ , ext₂ , μ₂ , vs = W₂ , ⊑-trans ext₁ ext₂ , μ₂ , coerce ext₂ v ∷ vs

  eval : ∀ {a} → Prog a → ∃ λ W → Store W × Val W a
  eval (lib , main) with eval-body main Vec∀.[] []
  ... | W , ext , μ , v = W , μ , v


text:
{-# OPTIONS --allow-unsolved-metas #-}
module LiteralFormula where

open import OscarPrelude

open import IsLiteralFormula
open import HasNegation
open import Formula

record LiteralFormula : Set
 where
  constructor ⟨_⟩
  field
    {formula} : Formula
    isLiteralFormula : IsLiteralFormula formula

open LiteralFormula public

instance EqLiteralFormula : Eq LiteralFormula
Eq._==_ EqLiteralFormula (⟨_⟩ {φ₁} lf₁) (⟨_⟩ {φ₂} lf₂)
 with φ₁ ≟ φ₂
… | no φ₁≢φ₂ = no (λ {refl → φ₁≢φ₂ refl})
Eq._==_ EqLiteralFormula (⟨_⟩ {φ₁} lf₁) (⟨_⟩ {φ₂} lf₂) | yes refl = case (eqIsLiteralFormula lf₁ lf₂) of λ {refl → yes refl}

instance HasNegationLiteralFormula : HasNegation LiteralFormula
HasNegation.~ HasNegationLiteralFormula ⟨ atomic 𝑃 τs ⟩ = ⟨ logical 𝑃 τs ⟩
HasNegation.~ HasNegationLiteralFormula ⟨ logical 𝑃 τs ⟩ = ⟨ atomic 𝑃 τs ⟩

open import Interpretation
open import Vector
open import Term
open import Elements
open import TruthValue

module _ where

  open import HasSatisfaction

  instance HasSatisfactionLiteralFormula : HasSatisfaction LiteralFormula
  HasSatisfaction._⊨_ HasSatisfactionLiteralFormula I ⟨ atomic 𝑃 τs ⟩ = 𝑃⟦ I ⟧ 𝑃 ⟨ ⟨ τ⟦ I ⟧ <$> vector (terms τs) ⟩ ⟩ ≡ ⟨ true ⟩
  HasSatisfaction._⊨_ HasSatisfactionLiteralFormula I ⟨ logical 𝑃 τs ⟩ = 𝑃⟦ I ⟧ 𝑃 ⟨ ⟨ τ⟦ I ⟧ <$> vector (terms τs) ⟩ ⟩ ≡ ⟨ false ⟩

  instance HasDecidableSatisfactionLiteralFormula : HasDecidableSatisfaction LiteralFormula
  HasDecidableSatisfaction._⊨?_ HasDecidableSatisfactionLiteralFormula
    I ⟨ atomic 𝑃 τs ⟩
   with 𝑃⟦ I ⟧ 𝑃 ⟨ ⟨ τ⟦ I ⟧ <$> vector (terms τs) ⟩ ⟩
  … | ⟨ true ⟩ = yes refl
  … | ⟨ false ⟩ = no λ ()
  HasDecidableSatisfaction._⊨?_ HasDecidableSatisfactionLiteralFormula
    I ⟨ logical 𝑃 τs ⟩
    with 𝑃⟦ I ⟧ 𝑃 ⟨ ⟨ τ⟦ I ⟧ <$> vector (terms τs) ⟩ ⟩
  … | ⟨ true ⟩ = no λ ()
  … | ⟨ false ⟩ = yes refl

  instance HasDecidableValidationLiteralFormula : HasDecidableValidation LiteralFormula
  HasDecidableValidation.⊨? HasDecidableValidationLiteralFormula = {!!}

module _ where

  open import HasSubstantiveDischarge

  postulate
    instance cs' : CanonicalSubstitution LiteralFormula
    instance hpu' : HasPairUnification LiteralFormula (CanonicalSubstitution.S cs')

  instance HasSubstantiveDischargeLiteralFormula : HasSubstantiveDischarge LiteralFormula
  --HasSubstantiveDischarge._o≽o_ HasSubstantiveDischargeLiteralFormula φ₁ φ₂ = φ₁ ≡ φ₂
  HasSubstantiveDischarge.hasNegation HasSubstantiveDischargeLiteralFormula = it
  HasSubstantiveDischarge.≽-reflexive HasSubstantiveDischargeLiteralFormula = {!!}
  HasSubstantiveDischarge.≽-consistent HasSubstantiveDischargeLiteralFormula = {!!}
  HasSubstantiveDischarge.≽-contrapositive HasSubstantiveDischargeLiteralFormula = {!!}

  instance HasDecidableSubstantiveDischargeLiteralFormula : HasDecidableSubstantiveDischarge LiteralFormula
  HasDecidableSubstantiveDischarge.hasSubstantiveDischarge HasDecidableSubstantiveDischargeLiteralFormula = it
  HasDecidableSubstantiveDischarge._≽?_ HasDecidableSubstantiveDischargeLiteralFormula φ+ φ- = {!!} -- φ+ ≟ φ-


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Foundations.Bundle where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Fibration

open import Cubical.Foundations.Structure
open import Cubical.Structures.TypeEqvTo

open import Cubical.Data.Sigma.Properties
open import Cubical.HITs.PropositionalTruncation

module _ {ℓb ℓf} {B : Type ℓb} {F : Type ℓf} {ℓ} where

{-
    A fiber bundle with base space B and fibers F is a map `p⁻¹ : B → TypeEqvTo F`
     taking points in the base space to their respective fibers.

    e.g. a double cover is a map `B → TypeEqvTo Bool`
-}

  Total : (p⁻¹ : B → TypeEqvTo ℓ F) → Type (ℓ-max ℓb ℓ)
  Total p⁻¹ = Σ[ x ∈ B ] p⁻¹ x .fst

  pr : (p⁻¹ : B → TypeEqvTo ℓ F) → Total p⁻¹ → B
  pr p⁻¹ = fst

  inc : (p⁻¹ : B → TypeEqvTo ℓ F) (x : B) → p⁻¹ x .fst → Total p⁻¹
  inc p⁻¹ x = (x ,_)

  fibPrEquiv : (p⁻¹ : B → TypeEqvTo ℓ F) (x : B) → fiber (pr p⁻¹) x ≃ p⁻¹ x .fst
  fibPrEquiv p⁻¹ x = fiberEquiv (λ x → typ (p⁻¹ x)) x

module _ {ℓb ℓf} (B : Type ℓb) (ℓ : Level) (F : Type ℓf) where
  private
    ℓ' = ℓ-max ℓb ℓ

{-
    Equivalently, a fiber bundle with base space B and fibers F is a type E and
     a map `p : E → B` with fibers merely equivalent to F.
-}

  bundleEquiv : (B → TypeEqvTo ℓ' F) ≃ (Σ[ E ∈ Type ℓ' ] Σ[ p ∈ (E → B) ] ∀ x → ∥ fiber p x ≃ F ∥)
  bundleEquiv = compEquiv (compEquiv PiΣ (pathToEquiv p)) assocΣ
    where e = fibrationEquiv B ℓ
          p :   (Σ[ p⁻¹ ∈ (B → Type ℓ') ]            ∀ x → ∥ p⁻¹ x ≃ F ∥)
              ≡ (Σ[ p ∈ (Σ[ E ∈ Type ℓ' ] (E → B)) ] ∀ x → ∥ fiber (snd p) x ≃ F ∥ )
          p i = Σ[ q ∈ ua e (~ i) ] ∀ x → ∥ ua-unglue e (~ i) q x ≃ F ∥

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


text:
module Generic.Property.Reify where

open import Generic.Core

data ExplView : Visibility -> Set where
  yes-expl : ExplView expl
  no-expl  : ∀ {v} -> ExplView v

explView : ∀ v -> ExplView v
explView expl = yes-expl
explView v    = no-expl

ExplMaybe : ∀ {α} -> Visibility -> Set α -> Set α
ExplMaybe v A with explView v
... | yes-expl = A
... | no-expl  = ⊤

caseExplMaybe : ∀ {α π} {A : Set α} (P : Visibility -> Set π)
              -> (A -> P expl) -> (∀ {v} -> P v) -> ∀ v -> ExplMaybe v A -> P v
caseExplMaybe P f y v x with explView v
... | yes-expl = f x
... | no-expl  = y

Prod : ∀ {α} β -> Visibility -> Set α -> Set (α ⊔ β) -> Set (α ⊔ β)
Prod β v A B with explView v
... | yes-expl = A × B
... | no-expl  = B

uncurryProd : ∀ {α β γ} {A : Set α} {B : Set (α ⊔ β)} {C : Set γ} v
            -> Prod β v A B -> (ExplMaybe v A -> B -> C) -> C
uncurryProd v p g with explView v | p
... | yes-expl | (x , y) = g x  y
... | no-expl  |  y      = g tt y

SemReify : ∀ {i β} {I : Set i} -> Desc I β -> Set
SemReify (var i)   = ⊤
SemReify (π i q C) = ⊥
SemReify (D ⊛ E)   = SemReify D × SemReify E

mutual
  ExtendReify : ∀ {i β} {I : Set i} -> Desc I β -> Set β
  ExtendReify (var i)   = ⊤
  ExtendReify (π i q C) = ExtendReifyᵇ i C q
  ExtendReify (D ⊛ E)   = SemReify D × ExtendReify E

  ExtendReifyᵇ : ∀ {ι α β γ q} {I : Set ι} i -> Binder α β γ i q I -> α ≤ℓ β -> Set β
  ExtendReifyᵇ {β = β} i (coerce (A , D)) q = Coerce′ q $
    Prod β (visibility i) (Reify A) (∀ {x} -> ExtendReify (D x))

-- Can't reify an irrelevant thing into its relevant representation.
postulate
  reifyᵢ : ∀ {α} {A : Set α} {{aReify : Reify A}} -> .A -> Term

instance
  {-# TERMINATING #-}
  DataReify : ∀ {i β} {I : Set i} {D : Data (Desc I β)} {j}
                {{reD : All ExtendReify (consTypes D)}} -> Reify (μ D j)
  DataReify {ι} {β} {I} {D₀} = record { reify = reifyMu } where
    mutual
      reifySem : ∀ D {{reD : SemReify D}} -> ⟦ D ⟧ (μ D₀) -> Term
      reifySem (var i)                  d      = reifyMu d
      reifySem (π i q C) {{()}}
      reifySem (D ⊛ E)   {{reD , reE}} (x , y) =
        sate _,_ (reifySem D {{reD}} x) (reifySem E {{reE}} y)

      reifyExtend : ∀ {j} D {{reD : ExtendReify D}} -> Extend D (μ D₀) j -> List Term
      reifyExtend (var i)                  lrefl  = []
      reifyExtend (π i q C)                p      = reifyExtendᵇ i C q p
      reifyExtend (D ⊛ E)   {{reD , reE}} (x , e) =
        reifySem D {{reD}} x ∷ reifyExtend E {{reE}} e

      reifyExtendᵇ : ∀ {α γ q j} i (C : Binder α β γ i q I) q′ {{reC : ExtendReifyᵇ i C q′}}
                   -> Extendᵇ i C q′ (μ D₀) j -> List Term
      reifyExtendᵇ i (coerce (A , D)) q {{reC}} p =
        uncurryProd (visibility i) (uncoerce′ q reC) λ mreA reD -> split q p λ x e ->
          let es = reifyExtend (D x) {{reD}} e in
            caseExplMaybe _ (λ reA -> elimRelValue _ (reify {{reA}}) (reifyᵢ {{reA}}) x ∷ es)
                             es
                            (visibility i)
                             mreA

      reifyDesc : ∀ {j} D {{reD : ExtendReify D}} -> Name -> Extend D (μ D₀) j -> Term
      reifyDesc D n e = vis appCon n (reifyExtend D e)

      reifyAny : ∀ {j} (Ds : List (Desc I β)) {{reD : All ExtendReify Ds}}
               -> ∀ d a b ns -> Node D₀ (packData d a b Ds ns) j -> Term
      reifyAny  []                         d a b  tt       ()
      reifyAny (D ∷ [])     {{reD , _}}    d a b (n , ns)  e       = reifyDesc D {{reD}} n e
      reifyAny (D ∷ E ∷ Ds) {{reD , reDs}} d a b (n , ns) (inj₁ e) = reifyDesc D {{reD}} n e
      reifyAny (D ∷ E ∷ Ds) {{reD , reDs}} d a b (n , ns) (inj₂ r) =
        reifyAny (E ∷ Ds) {{reDs}} d a b ns r

      reifyMu : ∀ {j} -> μ D₀ j -> Term
      reifyMu (node e) = reifyAny (consTypes D₀)
                                  (dataName  D₀)
                                  (parsTele  D₀)
                                  (indsTele  D₀)
                                  (consNames D₀)
                                   e

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
module Issue1760g where

data ⊥ : Set where

{-# NO_POSITIVITY_CHECK #-}
{-# NON_TERMINATING     #-}
mutual
  record U : Set where
    constructor roll
    field ap : U → U

  lemma : U → ⊥
  lemma (roll u) = lemma (u (roll u))

  bottom : ⊥
  bottom = lemma (roll λ x → x)

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


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

open import Algebra.Structures.Bundles.Field

module Algebra.Linear.Morphism.VectorSpace
  {k ℓᵏ} (K : Field k ℓᵏ)
  where

open import Level
open import Algebra.FunctionProperties as FP
import Algebra.Linear.Morphism.Definitions as LinearMorphismDefinitions
import Algebra.Morphism as Morphism
open import Relation.Binary using (Rel; Setoid)
open import Relation.Binary.Morphism.Structures
open import Algebra.Morphism

open import Algebra.Linear.Core
open import Algebra.Linear.Structures.VectorSpace K
open import Algebra.Linear.Structures.Bundles

module LinearDefinitions {a₁ a₂ ℓ₂} (A : Set a₁) (B : Set a₂) (_≈_ : Rel B ℓ₂) where
  open Morphism.Definitions A B _≈_ public
  open LinearMorphismDefinitions K A B _≈_ public

module _
  {a₁ ℓ₁} (From : VectorSpace K a₁ ℓ₁)
  {a₂ ℓ₂} (To   : VectorSpace K a₂ ℓ₂)
  where

  private
    module F = VectorSpace From
    module T = VectorSpace To

    K' : Set k
    K' = Field.Carrier K

  open F using () renaming (Carrier to A; _≈_ to _≈₁_; _+_ to _+₁_; _∙_ to _∙₁_)
  open T using () renaming (Carrier to B; _≈_ to _≈₂_; _+_ to _+₂_; _∙_ to _∙₂_)

  open import Function

  open LinearDefinitions (VectorSpace.Carrier From) (VectorSpace.Carrier To) _≈₂_

  record IsLinearMap (⟦_⟧ : Morphism) : Set (k ⊔ a₁ ⊔ a₂ ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      isAbelianGroupMorphism : IsAbelianGroupMorphism F.abelianGroup T.abelianGroup ⟦_⟧
      ∙-homo : ScalarHomomorphism ⟦_⟧ _∙₁_ _∙₂_

    open IsAbelianGroupMorphism isAbelianGroupMorphism public
      renaming (∙-homo to +-homo; ε-homo to 0#-homo)

    distrib-linear : ∀ (a b : K') (u v : A) -> ⟦ a ∙₁ u +₁ b ∙₁ v ⟧ ≈₂ a ∙₂ ⟦ u ⟧ +₂ b ∙₂ ⟦ v ⟧
    distrib-linear a b u v = T.trans (+-homo (a ∙₁ u) (b ∙₁ v)) (T.+-cong (∙-homo a u) (∙-homo b v))

  record IsLinearMonomorphism (⟦_⟧ : Morphism) : Set (k ⊔ a₁ ⊔ a₂ ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      isLinearMap : IsLinearMap ⟦_⟧
      injective   : Injective _≈₁_ _≈₂_ ⟦_⟧

    open IsLinearMap isLinearMap public

  record IsLinearIsomorphism (⟦_⟧ : Morphism) : Set (k ⊔ a₁ ⊔ a₂ ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      isLinearMonomorphism : IsLinearMonomorphism ⟦_⟧
      surjective           : Surjective _≈₁_ _≈₂_ ⟦_⟧

    open IsLinearMonomorphism isLinearMonomorphism public

module _
  {a ℓ} (V : VectorSpace K a ℓ)
  where

  open VectorSpace V

  open LinearDefinitions Carrier Carrier _≈_

  IsLinearEndomorphism : Morphism -> Set (k ⊔ a ⊔ ℓ)
  IsLinearEndomorphism ⟦_⟧ = IsLinearMap V V ⟦_⟧

  IsLinearAutomorphism : Morphism -> Set (k ⊔ a ⊔ ℓ)
  IsLinearAutomorphism ⟦_⟧ = IsLinearIsomorphism V V ⟦_⟧

max_stars_repo_name: felko/linear-algebra

max_issues_repo_name: felko/linear-algebra

max_forks_repo_name: felko/linear-algebra


text:
module helloworld where
open import IO

main = run (putStrLn "Hello World")


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

module hott.types where

open import hott.types.nat public
open import hott.types.coproduct public

max_stars_repo_name: piyush-kurur/hott

max_issues_repo_name: piyush-kurur/hott

max_forks_repo_name: piyush-kurur/hott


text:
module README where

----------------------------------------------------------------------
-- The Agda smallib library, version 0.1
----------------------------------------------------------------------
--
-- This library implements a type theory which is described in the
-- Appendix of the HoTT book. It also contains some properties derived
-- from the rules of this theory.
----------------------------------------------------------------------
--
-- This project is meant to be a practice for the author but as a
-- secondary goal it would be nice to create a small library which is
-- less intimidating than the standard one.
--
-- This version was tested using Agda 2.6.1.
----------------------------------------------------------------------

----------------------------------------------------------------------
-- High-level overview of contents
----------------------------------------------------------------------
--
-- The top-level module L is not implemented (yet), it's sole purpose
-- is to prepend all of the module names with something to avoid
-- possible name clashes with the standard library.
--
-- The structure of the library is the following:
--
-- • Base
--    The derivation rules of the implemented type theory and some
--    useful properties which can be derived from these. To make a
--    clear distinction between these every type has a Core and a
--    Properties submodule. In some cases the latter might be empty.
--
-- • Data
--  ◦ Bool
--     A specialized form of the Coproduct type. It implements if as
--     an elimination rule. The following operations are defined on
--     them: not, ∧, ∨, xor.
----------------------------------------------------------------------

----------------------------------------------------------------------
-- Some useful modules
----------------------------------------------------------------------
--
-- • To use several things at once
import L.Base      -- Type theory with it's properties.
import L.Base.Core -- Derivation rules.
--
-- • To use only one base type
import L.Base.Sigma     -- Products (universe polymorphic).
import L.Base.Coproduct -- Disjoint sums (universe polymorphic).
import L.Base.Empty     -- Empty type.
import L.Base.Unit      -- Unit type.
import L.Base.Nat       -- Natural numbers.
import L.Base.Id        -- Propositional equality (universe poly.).
--
-- • To use the properties of the above
import L.Base.Sigma.Properties
import L.Base.Coproduct.Properties
import L.Base.Empty.Properties
import L.Base.Unit.Properties
import L.Base.Nat.Properties
import L.Base.Id.Properties
--
-- • Some datatypes
import L.Data.Bool -- Booleans.
----------------------------------------------------------------------

----------------------------------------------------------------------
-- Notes
----------------------------------------------------------------------
--
-- • L.Base exports L.Coproduct.Core._+_ as _⊎_ to avoid multiple
--   definitions of _+_, as L.Base.Nat declares it as well.
----------------------------------------------------------------------

max_stars_repo_name: borszag/smallib

max_issues_repo_name: borszag/smallib

max_forks_repo_name: borszag/smallib


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

open import HoTT
open import cohomology.SuspAdjointLoopIso
open import cohomology.WithCoefficients
open import cohomology.Theory
open import cohomology.Exactness
open import cohomology.Choice

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

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

module SpectrumModel where

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

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

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

  {- Cⁿ(X) is an abelian group -}
  C-abelian : (n : ℤ) (X : Ptd i) → is-abelian (C n X)
  C-abelian n X =
    transport (is-abelian ∘ →Ω-group X) (spectrum (succ n)) $
      Trunc-group-abelian (→Ω-group-structure _ _) $ λ {(f , fpt) (g , gpt) →
        ⊙λ= (λ x → conc^2-comm (f x) (g x)) (pt-lemma fpt gpt)}
    where
    pt-lemma : ∀ {i} {A : Type i} {x : A} {p q : idp {a = x} == idp {a = x}}
      (α : p == idp) (β : q == idp)
      → ap (uncurry _∙_) (ap2 _,_ α β) ∙ idp
        == conc^2-comm p q ∙ ap (uncurry _∙_) (ap2 _,_ β α) ∙ idp
    pt-lemma idp idp = idp

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

    CF-hom : fst (X ⊙→ Y) → (C n Y →ᴳ C n X)
    CF-hom f = →Ω-group-dom-act f (E (succ n))

    CF : fst (X ⊙→ Y) → fst (⊙CEl n Y ⊙→ ⊙CEl n X)
    CF F = GroupHom.⊙f (CF-hom F)

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

    CF-ident : CF-hom n {X} {X} (⊙idf X) == idhom (C n X)
    CF-ident = →Ω-group-dom-idf (E (succ n))

    CF-comp : {Y Z : Ptd i} (g : fst (Y ⊙→ Z)) (f : fst (X ⊙→ Y))
      → CF-hom n (g ⊙∘ f) == CF-hom n f ∘ᴳ CF-hom n g
    CF-comp g f = →Ω-group-dom-∘ g f (E (succ n))

  -- Eilenberg-Steenrod Axioms

  {- Suspension Axiom -}
  private
    C-Susp' : {E₁ E₀ : Ptd i} (p : ⊙Ω E₁ == E₀) (X : Ptd i)
      → →Ω-group (⊙Susp X) E₁ ≃ᴳ →Ω-group X E₀
    C-Susp' {E₁ = E₁} idp X = SuspAdjointLoopIso.iso X E₁

    C-SuspF' : {E₁ E₀ : Ptd i} (p : ⊙Ω E₁ == E₀)
      {X Y : Ptd i} (f : fst (X ⊙→ Y))
      → fst (C-Susp' p X) ∘ᴳ →Ω-group-dom-act (⊙susp-fmap f) E₁
        == →Ω-group-dom-act f E₀ ∘ᴳ fst (C-Susp' p Y)
    C-SuspF' {E₁ = E₁} idp f = SuspAdjointLoopIso.nat-dom f E₁

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

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

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

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

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

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

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

    {- in image of (CF n (⊙cfcod' f)) ⇒ in kernel of (CF n f) -}
    abstract
      C-exact-itok : (f : fst (X ⊙→ Y))
        → is-exact-itok (CF-hom n (⊙cfcod' f)) (CF-hom n f)
      C-exact-itok f =
        itok-alt-in (CF-hom n (⊙cfcod' f)) (CF-hom n f) $
          Trunc-elim (λ _ → =-preserves-level _ (Trunc-level {n = 0}))
            (ap [_] ∘ exact-itok-lemma n f)

    {- in kernel of (CF n f) ⇒ in image of (CF n (⊙cfcod' f)) -}
    abstract
      C-exact-ktoi : (f : fst (X ⊙→ Y))
        → is-exact-ktoi (CF-hom n (⊙cfcod' f)) (CF-hom n f)
      C-exact-ktoi f =
        Trunc-elim
          (λ _ → Π-level (λ _ → raise-level _ Trunc-level))
          (λ h tp → Trunc-rec Trunc-level (lemma h) (–> (Trunc=-equiv _ _) tp))
        where
        lemma : (h : uCEl n Y) → h ⊙∘ f == ⊙cst
          → Trunc -1 (Σ (CEl n (⊙Cof f))
                          (λ tk → fst (CF n (⊙cfcod' f)) tk == [ h ]))
        lemma h p = [ [ fst wit ] , ap [_] (snd wit) ]
          where
          wit : Σ (uCEl n (⊙Cof f)) (λ k → k ⊙∘ ⊙cfcod' f == h)
          wit = exact-ktoi-lemma n f h p

    C-exact : (f : fst (X ⊙→ Y)) → is-exact (CF-hom n (⊙cfcod' f)) (CF-hom n f)
    C-exact f = record {itok = C-exact-itok f; ktoi = C-exact-ktoi f}

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

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

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

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

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

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

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

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

open SpectrumModel

spectrum-cohomology : CohomologyTheory i
spectrum-cohomology = record {
  C = C;
  CF-hom = CF-hom;
  CF-ident = CF-ident;
  CF-comp = CF-comp;
  C-abelian = C-abelian;
  C-Susp = C-Susp;
  C-SuspF = C-SuspF;
  C-exact = C-exact;
  C-additive = C-additive}

spectrum-C-S⁰ : (n : ℤ) → C n (⊙Lift ⊙S⁰) == πS 0 (E (succ n))
spectrum-C-S⁰ n = Bool⊙→Ω-is-π₁ (E (succ n))

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda