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

module rings where

import abelian-groups
open abelian-groups public

has-mul-Ab :
  { l1 : Level} (A : Ab l1) → UU l1
has-mul-Ab A =
  Σ ( has-associative-bin-op (set-Ab A))
    ( λ μ →
      ( is-unital (pair (set-Ab A) μ)) ×
      ( ( (a b c : type-Ab A) →
          Id (pr1 μ a (add-Ab A b c)) (add-Ab A (pr1 μ a b) (pr1 μ a c))) ×
        ( (a b c : type-Ab A) →
          Id (pr1 μ (add-Ab A a b) c) (add-Ab A (pr1 μ a c) (pr1 μ b c)))))

Ring : (l1 : Level) → UU (lsuc l1)
Ring l1 = Σ (Ab l1) has-mul-Ab

{- Basic infrastructure of rings -}

ab-Ring : {l1 : Level} → Ring l1 → Ab l1
ab-Ring R = pr1 R

group-Ring :
  {l : Level} (R : Ring l) → Group l
group-Ring R = group-Ab (ab-Ring R)

set-Ring :
  {l : Level} (R : Ring l) → UU-Set l
set-Ring R = set-Ab (ab-Ring R)

type-Ring :
  {l : Level} (R : Ring l) → UU l
type-Ring R = type-Ab (ab-Ring R)

is-set-type-Ring :
  {l : Level} (R : Ring l) → is-set (type-Ring R)
is-set-type-Ring R = is-set-type-Ab (ab-Ring R)

associative-add-Ring :
  {l : Level} (R : Ring l) → has-associative-bin-op (set-Ring R)
associative-add-Ring R = associative-add-Ab (ab-Ring R)

add-Ring :
  {l : Level} (R : Ring l) → type-Ring R → type-Ring R → type-Ring R
add-Ring R = add-Ab (ab-Ring R)

is-associative-add-Ring :
  {l : Level} (R : Ring l) (x y z : type-Ring R) →
  Id (add-Ring R (add-Ring R x y) z) (add-Ring R x (add-Ring R y z))
is-associative-add-Ring R = is-associative-add-Ab (ab-Ring R)

additive-semi-group-Ring :
  {l : Level} (R : Ring l) → Semi-Group l
additive-semi-group-Ring R = semi-group-Ab (ab-Ring R)

is-group-additive-semi-group-Ring :
  {l : Level} (R : Ring l) → is-group (additive-semi-group-Ring R)
is-group-additive-semi-group-Ring R = is-group-Ab (ab-Ring R)

has-zero-Ring :
  {l : Level} (R : Ring l) → is-unital (additive-semi-group-Ring R)
has-zero-Ring R = has-zero-Ab (ab-Ring R)

zero-Ring :
  {l : Level} (R : Ring l) → type-Ring R
zero-Ring R = zero-Ab (ab-Ring R)

left-zero-law-add-Ring :
  {l : Level} (R : Ring l) (x : type-Ring R) →
  Id (add-Ring R (zero-Ring R) x) x
left-zero-law-add-Ring R = left-zero-law-Ab (ab-Ring R)

right-zero-law-add-Ring :
  {l : Level} (R : Ring l) (x : type-Ring R) →
  Id (add-Ring R x (zero-Ring R)) x
right-zero-law-add-Ring R = right-zero-law-Ab (ab-Ring R)

has-negatives-Ring :
  {l : Level} (R : Ring l) →
  is-group' (additive-semi-group-Ring R) (has-zero-Ring R)
has-negatives-Ring R = has-negatives-Ab (ab-Ring R)

neg-Ring :
  {l : Level} (R : Ring l) → type-Ring R → type-Ring R
neg-Ring R = neg-Ab (ab-Ring R)

left-negative-law-Ring :
  {l : Level} (R : Ring l) (x : type-Ring R) →
  Id (add-Ring R (neg-Ring R x) x) (zero-Ring R)
left-negative-law-Ring R = left-negative-law-Ab (ab-Ring R)

right-negative-law-Ring :
  {l : Level} (R : Ring l) (x : type-Ring R) →
  Id (add-Ring R x (neg-Ring R x)) (zero-Ring R)
right-negative-law-Ring R = right-negative-law-Ab (ab-Ring R)

is-commutative-add-Ring :
  {l : Level} (R : Ring l) (x y : type-Ring R) →
  Id (add-Ring R x y) (add-Ring R y x)
is-commutative-add-Ring R = is-commutative-add-Ab (ab-Ring R)

has-associative-mul-Ring :
  {l : Level} (R : Ring l) → has-associative-bin-op (set-Ring R)
has-associative-mul-Ring R = pr1 (pr2 R)

mul-Ring :
  {l : Level} (R : Ring l) → type-Ring R → type-Ring R → type-Ring R
mul-Ring R = pr1 (has-associative-mul-Ring R)

is-associative-mul-Ring :
  {l : Level} (R : Ring l) (x y z : type-Ring R) →
  Id (mul-Ring R (mul-Ring R x y) z) (mul-Ring R x (mul-Ring R y z))
is-associative-mul-Ring R = pr2 (has-associative-mul-Ring R)

multiplicative-semi-group-Ring :
  {l : Level} (R : Ring l) → Semi-Group l
multiplicative-semi-group-Ring R =
  pair (set-Ring R) (has-associative-mul-Ring R)

is-unital-Ring :
  {l : Level} (R : Ring l) → is-unital (multiplicative-semi-group-Ring R)
is-unital-Ring R = pr1 (pr2 (pr2 R))

multiplicative-monoid-Ring :
  {l : Level} (R : Ring l) → Monoid l
multiplicative-monoid-Ring R =
  pair (multiplicative-semi-group-Ring R) (is-unital-Ring R)

unit-Ring :
  {l : Level} (R : Ring l) → type-Ring R
unit-Ring R = unit-Monoid (multiplicative-monoid-Ring R)

left-unit-law-mul-Ring :
  {l : Level} (R : Ring l) (x : type-Ring R) →
  Id (mul-Ring R (unit-Ring R) x) x
left-unit-law-mul-Ring R = left-unit-law-Monoid (multiplicative-monoid-Ring R)

right-unit-law-mul-Ring :
  {l : Level} (R : Ring l) (x : type-Ring R) →
  Id (mul-Ring R x (unit-Ring R)) x
right-unit-law-mul-Ring R = right-unit-law-Monoid (multiplicative-monoid-Ring R)

left-distributive-law-mul-add-Ring :
  {l : Level} (R : Ring l) (x y z : type-Ring R) →
  Id ( mul-Ring R x (add-Ring R y z))
     ( add-Ring R (mul-Ring R x y) (mul-Ring R x z))
left-distributive-law-mul-add-Ring R =
  pr1 (pr2 (pr2 (pr2 R)))

right-distributive-law-mul-add-Ring :
  {l : Level} (R : Ring l) (x y z : type-Ring R) →
  Id ( mul-Ring R (add-Ring R x y) z)
     ( add-Ring R (mul-Ring R x z) (mul-Ring R y z))
right-distributive-law-mul-add-Ring R =
  pr2 (pr2 (pr2 (pr2 R)))

{- Ring homomorphisms -}

preserves-mul-hom-Ab :
  {l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) →
  hom-Ab (ab-Ring R1) (ab-Ring R2) → UU (l1 ⊔ l2)
preserves-mul-hom-Ab R1 R2 f =
  (x y : type-Ring R1) →
  Id ( map-hom-Ab (ab-Ring R1) (ab-Ring R2) f (mul-Ring R1 x y))
     ( mul-Ring R2
       ( map-hom-Ab (ab-Ring R1) (ab-Ring R2) f x)
       ( map-hom-Ab (ab-Ring R1) (ab-Ring R2) f y))

is-prop-preserves-mul-hom-Ab :
  {l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) →
  ( f : hom-Ab (ab-Ring R1) (ab-Ring R2)) →
  is-prop (preserves-mul-hom-Ab R1 R2 f)
is-prop-preserves-mul-hom-Ab R1 R2 f =
  is-prop-Π
    ( λ x →
      is-prop-Π
        ( λ y →
          is-set-type-Ring R2
            ( map-hom-Ab (ab-Ring R1) (ab-Ring R2) f (mul-Ring R1 x y))
            ( mul-Ring R2
              ( map-hom-Ab (ab-Ring R1) (ab-Ring R2) f x)
              ( map-hom-Ab (ab-Ring R1) (ab-Ring R2) f y))))

preserves-unit-hom-Ab :
  {l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) →
  hom-Ab (ab-Ring R1) (ab-Ring R2) → UU l2
preserves-unit-hom-Ab R1 R2 f =
  Id (map-hom-Ab (ab-Ring R1) (ab-Ring R2) f (unit-Ring R1)) (unit-Ring R2)

is-prop-preserves-unit-hom-Ab :
  {l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) →
  ( f : hom-Ab (ab-Ring R1) (ab-Ring R2)) →
  is-prop (preserves-unit-hom-Ab R1 R2 f)
is-prop-preserves-unit-hom-Ab R1 R2 f =
  is-set-type-Ring R2
    ( map-hom-Ab (ab-Ring R1) (ab-Ring R2) f (unit-Ring R1))
    ( unit-Ring R2)

is-ring-homomorphism-hom-Ab :
  {l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) →
  ( f : hom-Ab (ab-Ring R1) (ab-Ring R2)) → UU (l1 ⊔ l2)
is-ring-homomorphism-hom-Ab R1 R2 f =
  preserves-mul-hom-Ab R1 R2 f × preserves-unit-hom-Ab R1 R2 f

is-prop-is-ring-homomorphism-hom-Ab :
  {l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) →
  ( f : hom-Ab (ab-Ring R1) (ab-Ring R2)) →
  is-prop (is-ring-homomorphism-hom-Ab R1 R2 f)
is-prop-is-ring-homomorphism-hom-Ab R1 R2 f =
  is-prop-prod
    ( is-prop-preserves-mul-hom-Ab R1 R2 f)
    ( is-prop-preserves-unit-hom-Ab R1 R2 f)

hom-Ring :
  {l1 l2 : Level} (R1 : Ring l1) (R : Ring l2) → UU (l1 ⊔ l2)
hom-Ring R1 R2 =
  Σ (hom-Ab (ab-Ring R1) (ab-Ring R2)) (is-ring-homomorphism-hom-Ab R1 R2)

{- Basic infrastructure for ring homomorphisms. -}

hom-Ab-hom-Ring :
  {l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) →
  hom-Ring R1 R2 → hom-Ab (ab-Ring R1) (ab-Ring R2)
hom-Ab-hom-Ring R1 R2 = pr1

map-hom-Ring :
  {l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) →
  hom-Ring R1 R2 → type-Ring R1 → type-Ring R2
map-hom-Ring R1 R2 f =
  map-hom-Ab (ab-Ring R1) (ab-Ring R2) (hom-Ab-hom-Ring R1 R2 f)

preserves-add-hom-Ring :
  {l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) →
  (f : hom-Ring R1 R2) →
  preserves-add (ab-Ring R1) (ab-Ring R2) (map-hom-Ring R1 R2 f)
preserves-add-hom-Ring R1 R2 f =
  preserves-add-Ab (ab-Ring R1) (ab-Ring R2) (hom-Ab-hom-Ring R1 R2 f)

preserves-mul-hom-Ring :
  {l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) →
  (f : hom-Ring R1 R2) → preserves-mul-hom-Ab R1 R2 (hom-Ab-hom-Ring R1 R2 f)
preserves-mul-hom-Ring R1 R2 f = pr1 (pr2 f)

preserves-unit-hom-Ring :
  {l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) →
  (f : hom-Ring R1 R2) → preserves-unit-hom-Ab R1 R2 (hom-Ab-hom-Ring R1 R2 f)
preserves-unit-hom-Ring R1 R2 f = pr2 (pr2 f)

is-ring-homomorphism-hom-Ring :
  {l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) →
  (f : hom-Ring R1 R2) →
  prod ( preserves-mul-hom-Ab R1 R2 (hom-Ab-hom-Ring R1 R2 f))
       ( preserves-unit-hom-Ab R1 R2 (hom-Ab-hom-Ring R1 R2 f))
is-ring-homomorphism-hom-Ring R1 R2 f =
  pair ( preserves-mul-hom-Ring R1 R2 f)
       ( preserves-unit-hom-Ring R1 R2 f)

{- We characterize the identity type of ring homomorphisms -}

htpy-hom-Ring :
  {l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) →
  hom-Ring R1 R2 → hom-Ring R1 R2 → UU (l1 ⊔ l2)
htpy-hom-Ring R1 R2 f g = map-hom-Ring R1 R2 f ~ map-hom-Ring R1 R2 g

reflexive-htpy-hom-Ring :
  {l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) →
  (f : hom-Ring R1 R2) → htpy-hom-Ring R1 R2 f f
reflexive-htpy-hom-Ring R1 R2 f = refl-htpy

htpy-hom-Ring-eq :
  {l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) →
  (f g : hom-Ring R1 R2) → Id f g → htpy-hom-Ring R1 R2 f g
htpy-hom-Ring-eq R1 R2 f .f refl = reflexive-htpy-hom-Ring R1 R2 f

is-contr-total-htpy-hom-Ring :
  {l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) (f : hom-Ring R1 R2) →
  is-contr (Σ (hom-Ring R1 R2) (htpy-hom-Ring R1 R2 f))
is-contr-total-htpy-hom-Ring R1 R2 f =
  is-contr-total-Eq-substructure
    ( is-contr-total-htpy-hom-Ab
      ( ab-Ring R1)
      ( ab-Ring R2)
      ( hom-Ab-hom-Ring R1 R2 f))
    ( is-prop-is-ring-homomorphism-hom-Ab R1 R2)
    ( hom-Ab-hom-Ring R1 R2 f)
    ( reflexive-htpy-hom-Ring R1 R2 f)
    ( is-ring-homomorphism-hom-Ring R1 R2 f)

is-equiv-htpy-hom-Ring-eq :
  {l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) (f g : hom-Ring R1 R2) →
  is-equiv (htpy-hom-Ring-eq R1 R2 f g)
is-equiv-htpy-hom-Ring-eq R1 R2 f =
  fundamental-theorem-id f
    ( reflexive-htpy-hom-Ring R1 R2 f)
    ( is-contr-total-htpy-hom-Ring R1 R2 f)
    ( htpy-hom-Ring-eq R1 R2 f)

equiv-htpy-hom-Ring-eq :
  {l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) (f g : hom-Ring R1 R2) →
  Id f g ≃ htpy-hom-Ring R1 R2 f g
equiv-htpy-hom-Ring-eq R1 R2 f g =
  pair
    ( htpy-hom-Ring-eq R1 R2 f g)
    ( is-equiv-htpy-hom-Ring-eq R1 R2 f g)

eq-htpy-hom-Ring :
  {l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) (f g : hom-Ring R1 R2) →
  htpy-hom-Ring R1 R2 f g → Id f g
eq-htpy-hom-Ring R1 R2 f g =
  inv-is-equiv (is-equiv-htpy-hom-Ring-eq R1 R2 f g)

is-set-hom-Ring :
  {l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) → is-set (hom-Ring R1 R2)
is-set-hom-Ring R1 R2 =
  is-trunc-succ-subtype
    ( neg-one-𝕋)
    ( is-prop-is-ring-homomorphism-hom-Ab R1 R2)
    ( is-set-hom-Ab (ab-Ring R1) (ab-Ring R2))

{- We define the categorical structure of rings -}

preserves-mul-id-hom-Ring :
  {l : Level} (R : Ring l) → preserves-mul-hom-Ab R R (id-hom-Ab (ab-Ring R))
preserves-mul-id-hom-Ring R x y = refl

preserves-unit-id-hom-Ring :
  {l : Level} (R : Ring l) → preserves-unit-hom-Ab R R (id-hom-Ab (ab-Ring R))
preserves-unit-id-hom-Ring R = refl

is-ring-homomorphism-id-hom-Ring :
  {l : Level} (R : Ring l) → is-ring-homomorphism-hom-Ab R R (id-hom-Ab (ab-Ring R))
is-ring-homomorphism-id-hom-Ring R =
  pair (preserves-mul-id-hom-Ring R) (preserves-unit-id-hom-Ring R)

id-hom-Ring :
  {l : Level} (R : Ring l) → hom-Ring R R
id-hom-Ring R = pair (id-hom-Ab (ab-Ring R)) (is-ring-homomorphism-id-hom-Ring R)

hom-Ab-comp-hom-Ring :
  { l1 l2 l3 : Level} (R1 : Ring l1) (R2 : Ring l2) (R3 : Ring l3) →
  ( g : hom-Ring R2 R3) (f : hom-Ring R1 R2) →
  hom-Ab (ab-Ring R1) (ab-Ring R3)
hom-Ab-comp-hom-Ring R1 R2 R3 g f =
  comp-hom-Ab
    ( ab-Ring R1)
    ( ab-Ring R2)
    ( ab-Ring R3)
    ( hom-Ab-hom-Ring R2 R3 g)
    ( hom-Ab-hom-Ring R1 R2 f)

preserves-mul-comp-hom-Ring :
  { l1 l2 l3 : Level} (R1 : Ring l1) (R2 : Ring l2) (R3 : Ring l3) →
  ( g : hom-Ring R2 R3) (f : hom-Ring R1 R2) →
  preserves-mul-hom-Ab R1 R3 (hom-Ab-comp-hom-Ring R1 R2 R3 g f)
preserves-mul-comp-hom-Ring R1 R2 R3 g f x y =
  ( ap (map-hom-Ring R2 R3 g) (preserves-mul-hom-Ring R1 R2 f x y)) ∙
  ( preserves-mul-hom-Ring R2 R3 g
    ( map-hom-Ring R1 R2 f x)
    ( map-hom-Ring R1 R2 f y))

preserves-unit-comp-hom-Ring :
  { l1 l2 l3 : Level} (R1 : Ring l1) (R2 : Ring l2) (R3 : Ring l3) →
  ( g : hom-Ring R2 R3) (f : hom-Ring R1 R2) →
  preserves-unit-hom-Ab R1 R3 (hom-Ab-comp-hom-Ring R1 R2 R3 g f)
preserves-unit-comp-hom-Ring R1 R2 R3 g f =
  ( ap (map-hom-Ring R2 R3 g) (preserves-unit-hom-Ring R1 R2 f)) ∙
  ( preserves-unit-hom-Ring R2 R3 g)

is-ring-homomorphism-comp-hom-Ring :
  { l1 l2 l3 : Level} (R1 : Ring l1) (R2 : Ring l2) (R3 : Ring l3) →
  ( g : hom-Ring R2 R3) (f : hom-Ring R1 R2) →
  is-ring-homomorphism-hom-Ab R1 R3 (hom-Ab-comp-hom-Ring R1 R2 R3 g f)
is-ring-homomorphism-comp-hom-Ring R1 R2 R3 g f =
  pair ( preserves-mul-comp-hom-Ring R1 R2 R3 g f)
       ( preserves-unit-comp-hom-Ring R1 R2 R3 g f)

comp-hom-Ring :
  { l1 l2 l3 : Level} (R1 : Ring l1) (R2 : Ring l2) (R3 : Ring l3) →
  hom-Ring R2 R3 → hom-Ring R1 R2 → hom-Ring R1 R3
comp-hom-Ring R1 R2 R3 g f =
  pair ( hom-Ab-comp-hom-Ring R1 R2 R3 g f)
       ( is-ring-homomorphism-comp-hom-Ring R1 R2 R3 g f)

{- We prove the laws of a category for Rings -}

is-associative-comp-hom-Ring :
  { l1 l2 l3 l4 : Level}
  ( R1 : Ring l1) (R2 : Ring l2) (R3 : Ring l3) (R4 : Ring l4) →
  ( h : hom-Ring R3 R4) (g : hom-Ring R2 R3) (f : hom-Ring R1 R2) →
  Id (comp-hom-Ring R1 R2 R4 (comp-hom-Ring R2 R3 R4 h g) f)
     (comp-hom-Ring R1 R3 R4 h (comp-hom-Ring R1 R2 R3 g f))
is-associative-comp-hom-Ring R1 R2 R3 R4 h g f =
  eq-htpy-hom-Ring R1 R4
    ( comp-hom-Ring R1 R2 R4 (comp-hom-Ring R2 R3 R4 h g) f)
    ( comp-hom-Ring R1 R3 R4 h (comp-hom-Ring R1 R2 R3 g f))
    ( refl-htpy)

left-unit-law-comp-hom-Ring :
  { l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) (f : hom-Ring R1 R2) →
  Id (comp-hom-Ring R1 R2 R2 (id-hom-Ring R2) f) f
left-unit-law-comp-hom-Ring R1 R2 f =
  eq-htpy-hom-Ring R1 R2
    ( comp-hom-Ring R1 R2 R2 (id-hom-Ring R2) f)
    ( f)
    ( refl-htpy)

right-unit-law-comp-hom-Ring :
  { l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) (f : hom-Ring R1 R2) →
  Id (comp-hom-Ring R1 R1 R2 f (id-hom-Ring R1)) f
right-unit-law-comp-hom-Ring R1 R2 f =
  eq-htpy-hom-Ring R1 R2
    ( comp-hom-Ring R1 R1 R2 f (id-hom-Ring R1))
    ( f)
    ( refl-htpy)

{- We show that the forgetful map ab-Ring is a functor -}

id-law-ab-Ring :
  { l1 : Level} (R1 : Ring l1) →
  Id (hom-Ab-hom-Ring R1 R1 (id-hom-Ring R1)) (id-hom-Ab (ab-Ring R1))
id-law-ab-Ring R1 =
  eq-htpy-hom-Ab
    ( ab-Ring R1)
    ( ab-Ring R1)
    ( refl-htpy)

comp-law-ab-Ring :
  { l1 l2 l3 : Level} (R1 : Ring l1) (R2 : Ring l2) (R3 : Ring l3) →
  ( g : hom-Ring R2 R3) (f : hom-Ring R1 R2) →
  Id ( hom-Ab-hom-Ring R1 R3 (comp-hom-Ring R1 R2 R3 g f))
     ( comp-hom-Ab
       ( ab-Ring R1)
       ( ab-Ring R2)
       ( ab-Ring R3)
       ( hom-Ab-hom-Ring R2 R3 g)
       ( hom-Ab-hom-Ring R1 R2 f))
comp-law-ab-Ring R1 R2 R3 g f =
  eq-htpy-hom-Ab
    ( ab-Ring R1)
    ( ab-Ring R3)
    ( refl-htpy)

{- We introduce ring isomorphisms -}

is-iso-hom-Ring :
  { l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) →
  hom-Ring R1 R2 → UU (l1 ⊔ l2)
is-iso-hom-Ring R1 R2 f =
  Σ ( hom-Ring R2 R1)
    ( λ g →
      ( Id (comp-hom-Ring R2 R1 R2 f g) (id-hom-Ring R2)) ×
      ( Id (comp-hom-Ring R1 R2 R1 g f) (id-hom-Ring R1)))

{- Infrastructure for invertible ring homomorphisms -}

inv-is-iso-hom-Ring :
  { l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) (f : hom-Ring R1 R2) →
  is-iso-hom-Ring R1 R2 f → hom-Ring R2 R1
inv-is-iso-hom-Ring R1 R2 f = pr1

is-sec-inv-is-iso-hom-Ring :
  { l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) (f : hom-Ring R1 R2) →
  ( is-iso-f : is-iso-hom-Ring R1 R2 f) →
  Id (comp-hom-Ring R2 R1 R2 f (inv-is-iso-hom-Ring R1 R2 f is-iso-f))
     (id-hom-Ring R2)
is-sec-inv-is-iso-hom-Ring R1 R2 f is-iso-f = pr1 (pr2 is-iso-f)

is-retr-inv-is-iso-hom-Ring :
  { l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) (f : hom-Ring R1 R2) →
  ( is-iso-f : is-iso-hom-Ring R1 R2 f) →
  Id (comp-hom-Ring R1 R2 R1 (inv-is-iso-hom-Ring R1 R2 f is-iso-f) f)
     (id-hom-Ring R1)
is-retr-inv-is-iso-hom-Ring R1 R2 f is-iso-f = pr2 (pr2 is-iso-f)

inv-map-is-iso-hom-Ring :
  { l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) (f : hom-Ring R1 R2) →
  is-iso-hom-Ring R1 R2 f → type-Ring R2 → type-Ring R1
inv-map-is-iso-hom-Ring R1 R2 f is-iso-f =
  map-hom-Ring R2 R1 (inv-is-iso-hom-Ring R1 R2 f is-iso-f)

is-sec-inv-map-is-iso-hom-Ring :
  { l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) (f : hom-Ring R1 R2) →
  ( is-iso-f : is-iso-hom-Ring R1 R2 f) →
  ( (map-hom-Ring R1 R2 f) ∘ (inv-map-is-iso-hom-Ring R1 R2 f is-iso-f)) ~ id
is-sec-inv-map-is-iso-hom-Ring R1 R2 f is-iso-f =
  htpy-hom-Ring-eq R2 R2
    ( comp-hom-Ring R2 R1 R2 f (inv-is-iso-hom-Ring R1 R2 f is-iso-f))
    ( id-hom-Ring R2)
    ( is-sec-inv-is-iso-hom-Ring R1 R2 f is-iso-f)

is-retr-inv-map-is-iso-hom-Ring :
  { l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) (f : hom-Ring R1 R2) →
  ( is-iso-f : is-iso-hom-Ring R1 R2 f) →
  ( (inv-map-is-iso-hom-Ring R1 R2 f is-iso-f) ∘ (map-hom-Ring R1 R2 f)) ~ id
is-retr-inv-map-is-iso-hom-Ring R1 R2 f is-iso-f =
  htpy-hom-Ring-eq R1 R1
    ( comp-hom-Ring R1 R2 R1 (inv-is-iso-hom-Ring R1 R2 f is-iso-f) f)
    ( id-hom-Ring R1)
    ( is-retr-inv-is-iso-hom-Ring R1 R2 f is-iso-f)

{- Being invertible is a property -}

is-prop-is-iso-hom-Ring' :
  { l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) (f : hom-Ring R1 R2) →
  is-prop' (is-iso-hom-Ring R1 R2 f)
is-prop-is-iso-hom-Ring' R1 R2 f inv-f inv-f' =
  eq-subtype
    ( λ g →
      is-prop-prod
        ( is-set-hom-Ring R2 R2 (comp-hom-Ring R2 R1 R2 f g) (id-hom-Ring R2))
        ( is-set-hom-Ring R1 R1 (comp-hom-Ring R1 R2 R1 g f) (id-hom-Ring R1)))
    ( eq-htpy-hom-Ring R2 R1
      ( inv-is-iso-hom-Ring R1 R2 f inv-f)
      ( inv-is-iso-hom-Ring R1 R2 f inv-f')
      ( λ x →
        ( inv
          ( ap ( map-hom-Ring R2 R1 (pr1 inv-f))
               ( is-sec-inv-map-is-iso-hom-Ring R1 R2 f inv-f' x))) ∙
        ( is-retr-inv-map-is-iso-hom-Ring R1 R2 f inv-f
          ( map-hom-Ring R2 R1 (pr1 inv-f') x))))

is-prop-is-iso-hom-Ring :
  { l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) (f : hom-Ring R1 R2) →
  is-prop (is-iso-hom-Ring R1 R2 f)
is-prop-is-iso-hom-Ring R1 R2 f =
  is-prop-is-prop' (is-prop-is-iso-hom-Ring' R1 R2 f)

iso-Ring :
  { l1 l2 : Level} → Ring l1 → Ring l2 → UU (l1 ⊔ l2)
iso-Ring R1 R2 = Σ (hom-Ring R1 R2) (is-iso-hom-Ring R1 R2)

hom-iso-Ring :
  { l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) →
  iso-Ring R1 R2 → hom-Ring R1 R2
hom-iso-Ring R1 R2 = pr1

is-iso-hom-iso-Ring :
  { l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) →
  ( f : iso-Ring R1 R2) → is-iso-hom-Ring R1 R2 (hom-iso-Ring R1 R2 f)
is-iso-hom-iso-Ring R1 R2 = pr2

inv-hom-iso-Ring :
  { l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) →
  iso-Ring R1 R2 → hom-Ring R2 R1
inv-hom-iso-Ring R1 R2 f =
  inv-is-iso-hom-Ring R1 R2
    ( hom-iso-Ring R1 R2 f)
    ( is-iso-hom-iso-Ring R1 R2 f)

is-iso-id-hom-Ring :
  { l1 : Level} (R1 : Ring l1) → is-iso-hom-Ring R1 R1 (id-hom-Ring R1)
is-iso-id-hom-Ring R1 =
  pair ( id-hom-Ring R1)
       ( pair
         ( left-unit-law-comp-hom-Ring R1 R1 (id-hom-Ring R1))
         ( left-unit-law-comp-hom-Ring R1 R1 (id-hom-Ring R1)))

id-iso-Ring :
  { l1 : Level} (R1 : Ring l1) → iso-Ring R1 R1
id-iso-Ring R1 = pair (id-hom-Ring R1) (is-iso-id-hom-Ring R1)

iso-eq-Ring :
  { l : Level} (R1 R2 : Ring l) → Id R1 R2 → iso-Ring R1 R2
iso-eq-Ring R1 .R1 refl = id-iso-Ring R1

{- We first show that a ring homomorphism is an isomorphism if and only if
   the underlying homomorphism of abelian groups is an isomorphism. -}

is-iso-hom-Ab-hom-Ring :
  { l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) →
  hom-Ring R1 R2 → UU (l1 ⊔ l2)
is-iso-hom-Ab-hom-Ring R1 R2 f =
  is-iso-hom-Ab (ab-Ring R1) (ab-Ring R2) (hom-Ab-hom-Ring R1 R2 f)

is-iso-hom-Ab-is-iso-hom-Ring :
  { l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) (f : hom-Ring R1 R2) →
  is-iso-hom-Ring R1 R2 f →
  is-iso-hom-Ab-hom-Ring R1 R2 f
is-iso-hom-Ab-is-iso-hom-Ring R1 R2 f is-iso-f =
  pair ( hom-Ab-hom-Ring R2 R1 (inv-is-iso-hom-Ring R1 R2 f is-iso-f))
       ( pair
         ( ap ( hom-Ab-hom-Ring R2 R2)
              ( is-sec-inv-is-iso-hom-Ring R1 R2 f is-iso-f))
         ( ap ( hom-Ab-hom-Ring R1 R1)
              ( is-retr-inv-is-iso-hom-Ring R1 R2 f is-iso-f)))

abstract
  preserves-mul-inv-is-iso-hom-Ab :
    { l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) →
    ( f : hom-Ab (ab-Ring R1) (ab-Ring R2)) →
    ( is-iso-f : is-iso-hom-Ab (ab-Ring R1) (ab-Ring R2) f) →
    ( pres-mul-f : preserves-mul-hom-Ab R1 R2 f) →
    preserves-mul-hom-Ab R2 R1
      ( inv-is-iso-hom-Ab (ab-Ring R1) (ab-Ring R2) f is-iso-f)
  preserves-mul-inv-is-iso-hom-Ab R1 R2 f is-iso-f pres-mul-f x y =
    ( inv
      ( ap
        ( map-inv-is-iso-hom-Ab (ab-Ring R1) (ab-Ring R2) f is-iso-f)
        ( ( pres-mul-f
            ( map-inv-is-iso-hom-Ab (ab-Ring R1) (ab-Ring R2) f is-iso-f x)
            ( map-inv-is-iso-hom-Ab (ab-Ring R1) (ab-Ring R2) f is-iso-f y)) ∙
          ( ( ap ( mul-Ring R2
                   ( map-hom-Ab (ab-Ring R1) (ab-Ring R2) f
                     ( map-inv-is-iso-hom-Ab
                       ( ab-Ring R1)
                       ( ab-Ring R2)
                       f is-iso-f x)))
                 ( is-sec-map-inv-is-iso-hom-Ab
                   ( ab-Ring R1)
                   ( ab-Ring R2)
                   ( f)
                   ( is-iso-f)
                   ( y))) ∙
            ( ap ( λ z → mul-Ring R2 z y)
                 ( is-sec-map-inv-is-iso-hom-Ab
                   ( ab-Ring R1)
                   ( ab-Ring R2)
                   ( f)
                   ( is-iso-f)
                   ( x))))))) ∙
    ( is-retr-map-inv-is-iso-hom-Ab (ab-Ring R1) (ab-Ring R2) f is-iso-f
      ( mul-Ring R1
        ( map-inv-is-iso-hom-Ab (ab-Ring R1) (ab-Ring R2) f is-iso-f x)
        ( map-inv-is-iso-hom-Ab (ab-Ring R1) (ab-Ring R2) f is-iso-f y)))

preserves-unit-inv-is-iso-hom-Ab :
  { l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2)
  ( f : hom-Ab (ab-Ring R1) (ab-Ring R2)) →
  ( is-iso-f : is-iso-hom-Ab (ab-Ring R1) (ab-Ring R2) f)
  ( pres-unit-f : preserves-unit-hom-Ab R1 R2 f) →
  preserves-unit-hom-Ab R2 R1
    ( inv-is-iso-hom-Ab (ab-Ring R1) (ab-Ring R2) f is-iso-f)
preserves-unit-inv-is-iso-hom-Ab R1 R2 f is-iso-f pres-unit-f =
  ( inv
    ( ap
      ( map-inv-is-iso-hom-Ab (ab-Ring R1) (ab-Ring R2) f is-iso-f)
      ( pres-unit-f))) ∙
  ( is-retr-map-inv-is-iso-hom-Ab (ab-Ring R1) (ab-Ring R2) f is-iso-f
    ( unit-Ring R1))

is-ring-homomorphism-inv-is-iso-hom-Ab :
  { l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2)
  ( f : hom-Ab (ab-Ring R1) (ab-Ring R2)) →
  ( is-iso-f : is-iso-hom-Ab (ab-Ring R1) (ab-Ring R2) f) →
  ( is-ring-hom-f : is-ring-homomorphism-hom-Ab R1 R2 f) →
  is-ring-homomorphism-hom-Ab R2 R1
    ( inv-is-iso-hom-Ab (ab-Ring R1) (ab-Ring R2) f is-iso-f)
is-ring-homomorphism-inv-is-iso-hom-Ab
  R1 R2 f is-iso-f (pair pres-mul-f pres-unit-f) =
  pair
    ( preserves-mul-inv-is-iso-hom-Ab R1 R2 f is-iso-f pres-mul-f)
    ( preserves-unit-inv-is-iso-hom-Ab R1 R2 f is-iso-f pres-unit-f)

inv-hom-Ring-is-iso-hom-Ab :
  { l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) (f : hom-Ring R1 R2) →
  ( is-iso-f : is-iso-hom-Ab
                 ( ab-Ring R1)
                 ( ab-Ring R2)
                 ( hom-Ab-hom-Ring R1 R2 f)) →
  hom-Ring R2 R1
inv-hom-Ring-is-iso-hom-Ab R1 R2 f is-iso-f =
  pair
    ( inv-is-iso-hom-Ab
      ( ab-Ring R1)
      ( ab-Ring R2)
      ( hom-Ab-hom-Ring R1 R2 f)
      ( is-iso-f))
    ( is-ring-homomorphism-inv-is-iso-hom-Ab R1 R2
      ( hom-Ab-hom-Ring R1 R2 f)
      ( is-iso-f)
      ( is-ring-homomorphism-hom-Ring R1 R2 f))

abstract
  is-iso-hom-Ring-is-iso-hom-Ab :
    { l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2)
    ( f : hom-Ring R1 R2) →
    is-iso-hom-Ab (ab-Ring R1) (ab-Ring R2) (hom-Ab-hom-Ring R1 R2 f) →
    is-iso-hom-Ring R1 R2 f
  is-iso-hom-Ring-is-iso-hom-Ab R1 R2 f is-iso-f =
    pair
      ( inv-hom-Ring-is-iso-hom-Ab R1 R2 f is-iso-f)
      ( pair
        ( eq-htpy-hom-Ring R2 R2
          ( comp-hom-Ring R2 R1 R2 f
            ( inv-hom-Ring-is-iso-hom-Ab R1 R2 f is-iso-f))
          ( id-hom-Ring R2)
          ( htpy-hom-Ab-eq (ab-Ring R2) (ab-Ring R2)
            ( hom-Ab-hom-Ring R2 R2
              ( comp-hom-Ring R2 R1 R2 f
                ( inv-hom-Ring-is-iso-hom-Ab R1 R2 f is-iso-f)))
            ( id-hom-Ab (ab-Ring R2))
            ( is-sec-inv-is-iso-hom-Ab
              ( ab-Ring R1)
              ( ab-Ring R2)
              ( hom-Ab-hom-Ring R1 R2 f)
              ( is-iso-f))))
        ( eq-htpy-hom-Ring R1 R1
          ( comp-hom-Ring R1 R2 R1
            ( inv-hom-Ring-is-iso-hom-Ab R1 R2 f is-iso-f)
            ( f))
          ( id-hom-Ring R1)
          ( htpy-hom-Ab-eq (ab-Ring R1) (ab-Ring R1)
            ( hom-Ab-hom-Ring R1 R1
              ( comp-hom-Ring R1 R2 R1
                ( inv-hom-Ring-is-iso-hom-Ab R1 R2 f is-iso-f)
                ( f)))
            ( id-hom-Ab (ab-Ring R1))
            ( is-retr-inv-is-iso-hom-Ab
              ( ab-Ring R1)
              ( ab-Ring R2)
              ( hom-Ab-hom-Ring R1 R2 f)
              ( is-iso-f)))))

iso-Ab-Ring :
  { l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) → UU (l1 ⊔ l2)
iso-Ab-Ring R1 R2 =
  Σ ( iso-Ab (ab-Ring R1) (ab-Ring R2))
    ( λ f →
      is-ring-homomorphism-hom-Ab R1 R2
        ( hom-iso-Ab (ab-Ring R1) (ab-Ring R2) f))

iso-Ab-iso-Ab-Ring :
  { l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) →
  iso-Ab-Ring R1 R2 → iso-Ab (ab-Ring R1) (ab-Ring R2)
iso-Ab-iso-Ab-Ring R1 R2 = pr1

iso-Ab-iso-Ring :
  { l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) →
  iso-Ring R1 R2 → iso-Ab (ab-Ring R1) (ab-Ring R2)
iso-Ab-iso-Ring R1 R2 f =
  pair ( hom-Ab-hom-Ring R1 R2 (hom-iso-Ring R1 R2 f))
       ( is-iso-hom-Ab-is-iso-hom-Ring R1 R2
         ( hom-iso-Ring R1 R2 f)
         ( is-iso-hom-iso-Ring R1 R2 f))

equiv-iso-Ab-iso-Ring :
  { l1 : Level} (R1 : Ring l1) (R2 : Ring l1) →
  (iso-Ring R1 R2) ≃ (iso-Ab-Ring R1 R2)
equiv-iso-Ab-iso-Ring R1 R2 =
  ( ( ( inv-equiv
        ( equiv-Σ-assoc
          ( hom-Ab (ab-Ring R1) (ab-Ring R2))
          ( is-iso-hom-Ab (ab-Ring R1) (ab-Ring R2))
          ( λ f → is-ring-homomorphism-hom-Ab R1 R2 (pr1 f)))) ∘e
      ( equiv-tot
        ( λ f →
          equiv-swap-prod
            ( is-ring-homomorphism-hom-Ab R1 R2 f)
            ( is-iso-hom-Ab (ab-Ring R1) (ab-Ring R2) f)))) ∘e
    ( equiv-Σ-assoc
      ( hom-Ab (ab-Ring R1) (ab-Ring R2))
      ( is-ring-homomorphism-hom-Ab R1 R2)
      ( λ f → is-iso-hom-Ab (ab-Ring R1) (ab-Ring R2) (pr1 f)))) ∘e
  ( equiv-total-subtype
    ( is-prop-is-iso-hom-Ring R1 R2)
    ( λ f →
      is-prop-is-iso-hom-Ab
        ( ab-Ring R1)
        ( ab-Ring R2)
        ( hom-Ab-hom-Ring R1 R2 f))
    ( is-iso-hom-Ab-is-iso-hom-Ring R1 R2)
    ( is-iso-hom-Ring-is-iso-hom-Ab R1 R2))

abstract
  is-contr-total-iso-Ring :
    { l : Level} (R : Ring l) → is-contr (Σ (Ring l) (iso-Ring R))
  is-contr-total-iso-Ring {l} R =
    is-contr-equiv
      ( Σ (Ring l) (iso-Ab-Ring R))
      ( equiv-tot (equiv-iso-Ab-iso-Ring R))
      ( is-contr-total-Eq-structure
        ( λ A μ f →
          is-ring-homomorphism-hom-Ab R (pair A μ) (hom-iso-Ab (ab-Ring R) A f))
        ( is-contr-total-iso-Ab (ab-Ring R))
        ( pair (ab-Ring R) (id-iso-Ab (ab-Ring R)))
        ( is-contr-total-Eq-structure
          ( λ μ H pres-mul → Id (unit-Ring R) (pr1 (pr1 H)))
          ( is-contr-total-Eq-substructure
            ( is-contr-total-Eq-Π
              ( λ x m → (y : type-Ring R) → Id (mul-Ring R x y) (m y))
              ( λ x → is-contr-total-htpy (mul-Ring R x))
              ( mul-Ring R))
            ( λ μ → is-prop-Π (λ x → is-prop-Π (λ y → is-prop-Π (λ z →
              is-set-type-Ring R (μ (μ x y) z) (μ x (μ y z))))))
            ( mul-Ring R)
            ( λ x y → refl)
            ( is-associative-mul-Ring R))
          ( pair (pair (mul-Ring R) (is-associative-mul-Ring R)) (λ x y → refl))
          ( is-contr-total-Eq-substructure
            ( is-contr-total-Eq-substructure
              ( is-contr-total-path (unit-Ring R))
              ( λ x →
                is-prop-prod
                  ( is-prop-Π (λ y → is-set-type-Ring R (mul-Ring R x y) y))
                  ( is-prop-Π (λ y → is-set-type-Ring R (mul-Ring R y x) y)))
              ( unit-Ring R)
              ( refl)
              ( pair (left-unit-law-mul-Ring R) (right-unit-law-mul-Ring R)))
            ( λ u →
              is-prop-prod
                ( is-prop-Π (λ x → is-prop-Π (λ y → is-prop-Π (λ z →
                  is-set-type-Ring R
                    ( mul-Ring R x (add-Ring R y z))
                    ( add-Ring R (mul-Ring R x y) (mul-Ring R x z))))))
                ( is-prop-Π (λ x → is-prop-Π (λ y → is-prop-Π (λ z →
                  is-set-type-Ring R
                    ( mul-Ring R (add-Ring R x y) z)
                    ( add-Ring R (mul-Ring R x z) (mul-Ring R y z)))))))
            ( is-unital-Ring R)
            ( refl)
            ( pair
              ( left-distributive-law-mul-add-Ring R)
              ( right-distributive-law-mul-add-Ring R)))))

is-equiv-iso-eq-Ring :
  { l : Level} (R S : Ring l) → is-equiv (iso-eq-Ring R S)
is-equiv-iso-eq-Ring R =
  fundamental-theorem-id R
    ( id-iso-Ring R)
    ( is-contr-total-iso-Ring R)
    ( iso-eq-Ring R)

eq-iso-Ring :
  { l : Level} (R S : Ring l) → iso-Ring R S → Id R S
eq-iso-Ring R S = inv-is-equiv (is-equiv-iso-eq-Ring R S)

max_stars_repo_name: UlrikBuchholtz/HoTT-Intro

max_issues_repo_name: UlrikBuchholtz/HoTT-Intro

max_forks_repo_name: UlrikBuchholtz/HoTT-Intro


text:
module Everything where

import Tuple
import Inductive

import Inductive.Examples.Empty
import Inductive.Examples.Unit
import Inductive.Examples.Sum
import Inductive.Examples.Product
import Inductive.Examples.Nat
import Inductive.Examples.Ord
import Inductive.Examples.List
import Inductive.Examples.BinTree

ext: agda

max_stars_repo_name: mr-ohman/general-induction

max_issues_repo_name: mr-ohman/general-induction

max_forks_repo_name: mr-ohman/general-induction


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

open import HoTT
open import cohomology.Theory
open import groups.ExactSequence
open import groups.HomSequence

module cw.cohomology.GridLongExactSequence {i} (CT : CohomologyTheory i)
  {X Y Z : Ptd i} (n : ℤ) (f : X ⊙→ Y) (g : Y ⊙→ Z) where

open CohomologyTheory CT
open import cohomology.PtdMapSequence CT
open import cw.cohomology.CofiberGrid (fst f) (fst g)
open import cw.cohomology.GridPtdMap f g

{-
  X --> Y ----> Z
        |       |
        v       v
       Y/X --> Z/X
        | this  |
        v   one v
        1 ---> Z/Y
-}

private
  ⊙D-span : ⊙Span
  ⊙D-span = ⊙span Y/X Z Y (⊙cfcod' f) g

  ⊙D : Ptd i
  ⊙D = ⊙Pushout ⊙D-span

  Y/X-to-D : Y/X ⊙→ ⊙D
  Y/X-to-D = B/A-to-D , idp

  open import cohomology.LongExactSequence CT n Y/X-to-D

  ⊙E : Ptd i
  ⊙E = ⊙Cofiber (⊙left ⊙D-span)

  Z/Y-to-E : Z/Y ⊙→ ⊙E
  Z/Y-to-E = C/B-to-E , idp

  Z/X-to-D : Z/X ⊙→ ⊙D
  Z/X-to-D = C/A-to-D , idp

grid-co∂ : C n Y/X →ᴳ C (succ n) Z/Y
grid-co∂ = record {f = CEl-fmap (succ n) Z/Y-to-E ∘ GroupHom.f co∂ ; pres-comp = lemma} where
  abstract lemma = ∘-pres-comp (C-fmap (succ n) Z/Y-to-E) co∂

C-grid-cofiber-seq : HomSequence (C n Z/X) (C (succ n) Y/X)
C-grid-cofiber-seq =
  C n Z/X         →⟨ C-fmap n Y/X-to-Z/X        ⟩ᴳ
  C n Y/X         →⟨ grid-co∂                   ⟩ᴳ
  C (succ n) Z/Y  →⟨ C-fmap (succ n) Z/X-to-Z/Y ⟩ᴳ
  C (succ n) Z/X  →⟨ C-fmap (succ n) Y/X-to-Z/X ⟩ᴳ
  C (succ n) Y/X  ⊣|ᴳ

private
  C-cofiber-seq-to-C-grid-cofiber-seq :
    HomSeqMap C-cofiber-seq C-grid-cofiber-seq
      (C-fmap n Z/X-to-D) (idhom _)
  C-cofiber-seq-to-C-grid-cofiber-seq =
    C-fmap n Z/X-to-D         ↓⟨ comm-sqrᴳ (λ d → ! (C-fmap-idf n _)
                                                ∙ (C-comm-square n B/A-to-C/A-comm-square □$ᴳ d)) ⟩ᴳ
    idhom _                   ↓⟨ comm-sqrᴳ (λ _ → idp) ⟩ᴳ
    C-fmap (succ n) Z/Y-to-E  ↓⟨ C-comm-square (succ n) C/A-to-C/B-comm-square ⟩ᴳ
    C-fmap (succ n) Z/X-to-D  ↓⟨ comm-sqrᴳ (λ d → ! (C-fmap-idf (succ n) _)
                                                ∙ (C-comm-square (succ n) B/A-to-C/A-comm-square □$ᴳ d)) ⟩ᴳ
    idhom _                   ↓|ᴳ

  C-cofiber-seq-equiv-C-grid-cofiber-seq :
    HomSeqEquiv C-cofiber-seq C-grid-cofiber-seq
      (C-fmap n Z/X-to-D) (idhom _)
  C-cofiber-seq-equiv-C-grid-cofiber-seq =
    C-cofiber-seq-to-C-grid-cofiber-seq ,
      CEl-isemap n Z/X-to-D C/A-to-D-is-equiv ,
      idf-is-equiv _ ,
      CEl-isemap (succ n) Z/Y-to-E C/B-to-E-is-equiv ,
      CEl-isemap (succ n) Z/X-to-D C/A-to-D-is-equiv ,
      idf-is-equiv _

abstract
  C-grid-cofiber-seq-is-exact : is-exact-seq C-grid-cofiber-seq
  C-grid-cofiber-seq-is-exact = seq-equiv-preserves-exact
    C-cofiber-seq-equiv-C-grid-cofiber-seq C-cofiber-seq-is-exact

C-grid-cofiber-exact-seq : ExactSequence (C n Z/X) (C (succ n) Y/X)
C-grid-cofiber-exact-seq = C-grid-cofiber-seq , C-grid-cofiber-seq-is-exact

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
------------------------------------------------------------------------
-- A compiler
------------------------------------------------------------------------

open import Prelude

import Lambda.Syntax

module Lambda.Compiler
  {Name : Type}
  (open Lambda.Syntax Name)
  (def : Name → Tm 1)
  where

open import Equality.Propositional
open import Tactic.By.Propositional

open import List equality-with-J using (_++_)
open import Vec.Data equality-with-J

open import Lambda.Virtual-machine.Instructions Name

private
  module C = Closure Code
  module T = Closure Tm

-- The compiler takes an argument of type In-tail-context. The value
-- "true" means that the term is in a tail context. (I have based the
-- definition of tail context on the one in Section 4.5 of "Revised⁵
-- Report on the Algorithmic Language Scheme" by Abelson et al.) The
-- value "false" means that no such information is present.
--
-- The compiler compiles calls claimed to be in a tail context in a
-- special way.

In-tail-context : Type
In-tail-context = Bool

-- The compiler (which takes a code continuation).

mutual

  comp : ∀ {n} → In-tail-context → Tm n → Code n → Code n
  comp _     (var x)       c = var x ∷ c
  comp _     (lam t)       c = clo (comp-body t) ∷ c
  comp _     (t₁ · t₂)     c = comp false t₁ (comp false t₂ (app ∷ c))
  comp true  (call f t)    c = comp false t (tcl f ∷ c)
  comp false (call f t)    c = comp false t (cal f ∷ c)
  comp _     (con b)       c = con b ∷ c
  comp tc    (if t₁ t₂ t₃) c =
    comp false t₁ (bra (comp tc t₂ []) (comp tc t₃ []) ∷ c)

  comp-body : ∀ {n} → Tm (suc n) → Code (suc n)
  comp-body t = comp true t (ret ∷ [])

-- Compiler for named definitions.

comp-name : Name → Code 1
comp-name f = comp-body (def f)

-- Top-level compiler.
--
-- Note that the top-level expression is not assumed to be in a tail
-- context. Tail calls do not push a return frame on the stack. The
-- idea is to reuse an existing return frame, and the virtual machine
-- starts with an empty stack (which does not contain any return
-- frames).

comp₀ : Tm 0 → Code 0
comp₀ t = comp false t []

-- Environments and values can also be compiled.

mutual

  comp-env : ∀ {n} → T.Env n → C.Env n
  comp-env []      = []
  comp-env (v ∷ ρ) = comp-val v ∷ comp-env ρ

  comp-val : T.Value → C.Value
  comp-val (T.lam t ρ) = C.lam (comp-body t) (comp-env ρ)
  comp-val (T.con b)   = C.con b

-- Indexing commutes with compilation.

comp-index : ∀ {n} (ρ : T.Env n) (x : Fin n) →
             index (comp-env ρ) x ≡ comp-val (index ρ x)
comp-index (v ∷ ρ) fzero    = refl
comp-index (v ∷ ρ) (fsuc i) = comp-index ρ i

-- The function comp tc t commutes with _++ c₂.

comp-++ :
  ∀ {n} tc (t : Tm n) {c₁ c₂ : Code n} →
  comp tc t c₁ ++ c₂ ≡ comp tc t (c₁ ++ c₂)
comp-++ _     (var x)             = refl
comp-++ _     (lam t)             = refl
comp-++ true  (call f t)          = comp-++ _ t
comp-++ false (call f t)          = comp-++ _ t
comp-++ _     (con b)             = refl
comp-++ _     (if t₁ t₂ t₃)       = comp-++ _ t₁
comp-++ _     (t₁ · t₂) {c₁} {c₂} =
  comp false t₁ (comp false t₂ (app ∷ c₁)) ++ c₂  ≡⟨ comp-++ _ t₁ ⟩
  comp false t₁ (comp false t₂ (app ∷ c₁) ++ c₂)  ≡⟨ by (comp-++ _ t₂) ⟩∎
  comp false t₁ (comp false t₂ (app ∷ c₁ ++ c₂))  ∎

max_stars_repo_name: nad/definitional-interpreters

max_issues_repo_name: nad/definitional-interpreters

max_forks_repo_name: nad/definitional-interpreters


text:
module Bin-laws where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; sym; cong)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)

open import Induction′ using (+-suc; +-identityʳ; +-comm; +-assoc)

-- 2進数の表現
data Bin : Set where
  ⟨⟩ : Bin
  _O : Bin → Bin
  _I : Bin → Bin

-- 2進数のインクリメント
inc : Bin → Bin
inc ⟨⟩    = ⟨⟩ I
inc (b O) = b I
inc (b I) = inc b O

-- 自然数から2進数への変換
to : ℕ → Bin
to zero    = ⟨⟩ O
to (suc n) = inc (to n)

-- 2進数から自然数への変換
from : Bin → ℕ
from ⟨⟩    = zero
from (b O) = 2 * (from b)
from (b I) = 2 * (from b) + 1

2*n≡n+n : ∀ (n : ℕ) → 2 * n ≡ n + n
2*n≡n+n n =
  begin
    2 * n
  ≡⟨⟩
    n + (1 * n)
  ≡⟨⟩
    n + (n + (0 * n))
  ≡⟨⟩
    n + (n + 0)
  ≡⟨ cong (n +_) (+-identityʳ n) ⟩
    n + n
  ∎

+-suc-suc : ∀ (m n : ℕ) → (suc m) + (suc n) ≡ suc (suc (m + n))
+-suc-suc m n =
  begin
    (suc m) + (suc n)
  ≡⟨ +-suc (suc m) n ⟩
    suc ((suc m) + n)
  ≡⟨ cong suc (sym (+-assoc 1 m n)) ⟩
    suc (suc (m + n))
  ∎

-- 変換の前後どちらでインクリメントしても結果は等しい
from∘inc≡suc∘from : ∀ (b : Bin) → from (inc b) ≡ suc (from b)
from∘inc≡suc∘from ⟨⟩ =
  begin
    from (inc ⟨⟩)
  ≡⟨⟩
    from (⟨⟩ I)
  ≡⟨⟩
    suc zero
  ≡⟨⟩
    suc (from ⟨⟩)
  ∎
from∘inc≡suc∘from (b O) =
  begin
    from (inc (b O))
  ≡⟨⟩
    from (b I)
  ≡⟨⟩
    2 * (from b) + 1
  ≡⟨⟩
    from (b O) + 1
  ≡⟨ +-suc (from (b O)) zero ⟩
    suc (from (b O) + zero)
  ≡⟨ cong suc (+-identityʳ (from (b O))) ⟩
    suc (from (b O))
  ∎
from∘inc≡suc∘from (b I) =
  begin
    from (inc (b I))
  ≡⟨⟩
    from ((inc b) O)
  ≡⟨⟩
    2 * (from (inc b))
  ≡⟨ cong (2 *_) (from∘inc≡suc∘from b) ⟩
    2 * (suc (from b))
  ≡⟨ 2*n≡n+n (suc (from b)) ⟩
    (suc (from b)) + (suc (from b))
  ≡⟨ +-suc-suc (from b) (from b) ⟩
    suc (suc ((from b) + (from b)))
  ≡⟨ cong (λ 2*fromb → suc (suc 2*fromb)) (sym (2*n≡n+n (from b))) ⟩
    suc (suc (2 * (from b)))
  ≡⟨ cong suc (+-comm 1 (2 * (from b))) ⟩
    suc (2 * (from b) + 1)
  ≡⟨⟩
    suc (from (b I))
  ∎

-- to∘from : ∀ (b : Bin) → to (from b) ≡ b
-- to∘from ⟨⟩ = {!!} -- (to zero) が (⟨⟩ O) にエンコードされるため成り立たない
-- to∘from (b O) = {!!}
-- to∘from (b I) = {!!}

from∘to : ∀ (n : ℕ) → from (to n) ≡ n
from∘to zero =
  begin
    from (to zero)
  ≡⟨⟩
    from (⟨⟩ O)
  ≡⟨⟩
    2 * (from ⟨⟩)
  ≡⟨⟩
    2 * zero
  ≡⟨⟩
    zero
  ∎
from∘to (suc n) =
  begin
    from (to (suc n))
  ≡⟨⟩
    from (inc (to n))
  ≡⟨ from∘inc≡suc∘from (to n) ⟩
    suc (from (to n))
  ≡⟨ cong suc (from∘to n) ⟩
    suc n
  ∎

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
-- Previously Agda accepted invalid module names when no module header
-- was given.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module RandomAccessList.General.Redundant where

open import RandomAccessList.General.Core

open import Data.Nat

Redundant : Set → ℕ → Set
Redundant A = General A 0 2

cons : ∀ {n A} → A → Redundant A n → Redundant A n
cons a [] = ?
cons a (∺ x x₁ x₂ xs) = ?

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
module RMonads.RMonadMorphs where

open import Library
open import Functors
open import Categories
open import RMonads

open Fun
open RMonad

record RMonadMorph {a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}{J : Fun C D}
                   (M M' : RMonad J) : Set (a ⊔ b ⊔ c ⊔ d) where
  constructor rmonadmorph
  open Cat D
  field morph    : ∀ {X} → Hom (T M X) (T M' X)
        lawη     : ∀ {X} → comp morph (η M {X}) ≅ η M' {X}
        lawbind : ∀ {X Y}{k : Hom (OMap J X) (T M Y)} →
                  comp (morph {Y}) (bind M k)
                  ≅
                  comp (bind M' (comp (morph {Y}) k)) (morph {X})

RMonadMorphEq : ∀{a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}{J : Fun C D}
  {M M' : RMonad J}(α α' : RMonadMorph M M') ->
  (λ {X} -> RMonadMorph.morph α {X}) ≅ (λ {X} -> RMonadMorph.morph α' {X}) →
  α ≅ α'
RMonadMorphEq (rmonadmorph m lη lbind) (rmonadmorph .m lη' lbind') refl =
  cong₂ (rmonadmorph m)
        (iext λ _ → hir refl)
        (iext λ _ → iext λ _ → iext λ _ → hir refl)

IdRMonadMorph : ∀{a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}{J : Fun C D}
  (M  : RMonad J) → RMonadMorph M M
IdRMonadMorph {D = D} M = rmonadmorph
  iden
  idl
  (trans idl (trans (cong (bind M) (sym idl)) (sym idr)))
  where open Cat D

CompRMonadMorph : ∀{a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}{J : Fun C D}
  {M  M' M'' : RMonad J} →
  RMonadMorph M' M'' → RMonadMorph M M' → RMonadMorph M M''
CompRMonadMorph {D = D}{M'' = M''}
  (rmonadmorph f lawηf lawbindf)
  (rmonadmorph g lawηg lawbindg) =
  rmonadmorph
    (comp f g)
    (trans ass (trans (cong (comp f) lawηg) lawηf))
    \ {_ _ k} -> trans
      ass
      (trans (cong (comp f) lawbindg)
             (trans (trans (sym ass)
                           (cong (λ f → comp f g)
                                 (trans (lawbindf {k = comp g k})
                                        (cong (λ g → comp (bind M'' g) f)
                                              (sym ass)))))
                     ass))
  where open Cat D

idr : ∀{a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}{J : Fun C D}{M M' : RMonad J}
  (f : RMonadMorph M M') → CompRMonadMorph f (IdRMonadMorph _) ≅ f
idr {D = D} f = RMonadMorphEq _ _ (iext λ _ → Cat.idr D)

idl : ∀{a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}{J : Fun C D}{M M' : RMonad J}
  (f : RMonadMorph M M') → CompRMonadMorph (IdRMonadMorph _) f ≅ f
idl {D = D} f = RMonadMorphEq _ _ (iext λ _ → Cat.idl D)

ass : ∀{a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}
  {J : Fun C D}{M M' M'' M''' : RMonad J}
  (f : RMonadMorph M'' M''')(g : RMonadMorph M' M'')(h : RMonadMorph M M')  →
  CompRMonadMorph (CompRMonadMorph f g) h
  ≅
  CompRMonadMorph f (CompRMonadMorph g h)
ass {D = D} f g h = RMonadMorphEq _ _ (iext λ _ → Cat.ass D)

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
---------------------------------------------------------------------------
-- The gcd is greatest that any common divisor
---------------------------------------------------------------------------

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

open import LTC-PCF.Base
open import LTC-PCF.Data.Nat.Divisibility.NotBy0
open import LTC-PCF.Data.Nat.Inequalities
open import LTC-PCF.Data.Nat.Type

module LTC-PCF.Program.GCD.Partial.GreatestAnyCommonDivisor
  (x∣Sy→x≤Sy : ∀ {m n} → N m → N n → m ∣ (succ₁ n) → m ≤ succ₁ n)
  (0∤x       : ∀ {n} → ¬ (zero ∣ n))
  where

open import LTC-PCF.Program.GCD.Partial.Definitions

---------------------------------------------------------------------------
-- Knowing that gcd is a common divisor of m and n and that any other
-- common divisor of m and n divides it, we can prove that gcd is the
-- largest common divisor.

-- It requires the totality of gcd, ie. N gcd.
gcdGACD : ∀ {m n gcd} → N gcd → CD m n gcd → Divisible m n gcd → GACD m n gcd
gcdGACD nzero              (0∣m , _) = ⊥-elim (0∤x 0∣m)
gcdGACD (nsucc {gcd} Ngcd) _         =
  λ Divisible-mnSgcd c Nc CDmnc → x∣Sy→x≤Sy Nc Ngcd
                     (Divisible-mnSgcd c Nc CDmnc)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

module Algebra.Linear where

open import Algebra.Linear.Core       public
open import Algebra.Linear.Construct  public
open import Algebra.Linear.Morphism   public
open import Algebra.Linear.Structures public

max_stars_repo_name: felko/linear-algebra

max_issues_repo_name: felko/linear-algebra

max_forks_repo_name: felko/linear-algebra


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

module SymmetricMonoidalCategory where

open import Level

open import Categories.Category using (Category)
open import Categories.Monoidal using (Monoidal)
open import Categories.Monoidal.Braided using (Braided; module Braided)
open import Categories.NaturalIsomorphism using (module NaturalIsomorphism)
open import Categories.NaturalTransformation using (id; _∘₁_; _≡_)

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

record SymmetricMonoidalCategory {o ℓ e} {ℂ  : Category o ℓ e} {Mℂ : Monoidal ℂ}
  (BMℂ : Braided Mℂ) : Set (suc (o ⊔ ℓ ⊔ e)) where
  open Braided BMℂ using (braid)
  open NaturalIsomorphism braid using () renaming (F⇒G to x⊗y⇒y⊗x; F⇐G to y⊗x⇒x⊗y)
  field
    symmetry : y⊗x⇒x⊗y ∘₁ x⊗y⇒y⊗x ≡ id

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module Generic.Lib.Data.Sum where

open import Data.Sum hiding (swap) renaming (map to smap) hiding (map₁; map₂) public

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
-- Display whether or not the timeout was hit when using auto -l.
module Issue945 where

data ⊥ : Set where

¬_ : Set → Set
¬ A = A → ⊥

record ∃ {A : Set} (P : A → Set) : Set where
  constructor _,_
  field witness : A
        proof   : P witness

-- Exhaustive
lem₁ : ∀ {A : Set} (P : A → Set) (x : A) → (∀ x → ¬ P x) → (∀ x → P x) → ⊥
lem₁ A = {!-l -t 1!}

-- Timeout
lem₂ : ∀ {A} (P : A → Set) (x : A) → (∀ x → ¬ P x) → (∀ x → P x) → ∃ P → ⊥
lem₂ P a e = {!-l -t 1!}


text:
open import Everything

module Test.Class where

record ℭlass
  {ℓ}
  {𝔢}
  {CONSTRAINTS : Ø 𝔢}
  (constraints : CONSTRAINTS)
  : Ø ↑̂ ℓ
  where
  constructor ∁
  field
    type : Ø ℓ
  private
    record SET-CLASS
      ⦃ _ : Constraint constraints ⦄
      : Ø ℓ
      where
      constructor ∁
      field ⋆ : type
  open SET-CLASS public
  class : Ø _
  class = SET-CLASS
  method : ⦃ _ : class ⦄ → type
  method ⦃ ⌶ ⦄ = SET-CLASS.⋆ ⌶

mkClass : ∀
  {ℓ}
  {𝔢}
  {CONSTRAINTS : Ø 𝔢}
  (constraints : CONSTRAINTS)
  → Ø ℓ
  → ℭlass constraints
mkClass constraints set-method = ∁ set-method

module Unit-Unit/Unit/Unit
  {𝔬} (𝔒 : Ø 𝔬)
  = ℭlass (mkClass 𝔒 𝔒)

module PropSingle-Unit/Unit/Unit
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔭} (𝔓 : 𝔒 → Ø 𝔭)
  (x : 𝔒)
  = Unit-Unit/Unit/Unit (𝔓 x)

module Prop-Unit/Unit/Unit
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔭} (𝔓 : 𝔒 → Ø 𝔭)
  where
  private module M = PropSingle-Unit/Unit/Unit 𝔓
  class = ∀ {x} → M.class x
  type = ∀ x → M.type x
  method = λ ⦃ _ : class ⦄ x → M.method x

module RelSingle-Unit/Unit/Unit
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} (ℜ : 𝔒 → 𝔒 → Ø 𝔯)
  (x : 𝔒)
  = Unit-Unit/Unit/Unit (ℜ x x)

module Rel-Unit/Unit/Unit
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} (ℜ : 𝔒 → 𝔒 → Ø 𝔯)
  where
  private module M = RelSingle-Unit/Unit/Unit ℜ
  class = ∀ {x} → M.class x
  type = ∀ x → M.type x
  method = λ ⦃ _ : class ⦄ x → M.method x

module Prop-Rel-Unit/Unit/Unit
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔭} (𝔓 : 𝔒 → Ø 𝔭)
  = Rel-Unit/Unit/Unit (Extension 𝔓)

module UnitLevel-Unit/Unit/Unit
  {𝔬} (𝔒 : Ø 𝔬) (𝔯 : Ł)
  where
  private module M = Rel-Unit/Unit/Unit {𝔒 = 𝔒} {𝔯 = 𝔯}
  class = ∀ {ℜ} → M.class ℜ
  type = ∀ {ℜ} → M.type ℜ
  method : ⦃ _ : class ⦄ → type
  method ⦃ ⌶ ⦄ {ℜ = ℜ} = M.method ℜ ⦃ ⌶ {ℜ} ⦄ -- FIXME

module RelSingle-RelSingle/Rel/RelSingle
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} (ℜ : 𝔒 → 𝔒 → Ø 𝔯)
  (x : 𝔒)
  = ℭlass (mkClass ℜ (ℜ x x))

module Rel-RelSingle/Rel/RelSingle
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} (ℜ : 𝔒 → 𝔒 → Ø 𝔯)
  where
  private module M = RelSingle-RelSingle/Rel/RelSingle ℜ
  class = ∀ {x} → M.class x
  type = ∀ {x} → M.type x
  method = λ ⦃ _ : class ⦄ {x} → M.method x

module Prop-Rel-RelSingle/Rel/RelSingle
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔭} (𝔓 : 𝔒 → Ø 𝔭)
  = Rel-RelSingle/Rel/RelSingle (Extension 𝔓)

module All-Prop-Rel-RelSingle/Rel/RelSingle (𝔬 𝔭 : Ł) where
  private module M = Prop-Rel-RelSingle/Rel/RelSingle
  class = ∀ {𝔒 : Ø 𝔬} {𝔓 : 𝔒 → Ø 𝔭} → M.class 𝔓
  type = ∀ {𝔒 : Ø 𝔬} {𝔓 : 𝔒 → Ø 𝔭} → M.type 𝔓
  method : ⦃ _ : class ⦄ → type
  method {𝔓 = 𝔓} = M.method 𝔓

module UnitLevel-RelSingle/Rel/RelSingle
  {𝔬} (𝔒 : Ø 𝔬) (𝔯 : Ł)
  where
  private module M = Rel-RelSingle/Rel/RelSingle {𝔒 = 𝔒} {𝔯 = 𝔯}
  class = ∀ {ℜ} → M.class ℜ
  type = ∀ {ℜ} → M.type ℜ
  method : ⦃ _ : class ⦄ → type
  method {ℜ = ℜ} = M.method ℜ

module PropSingle-PropSingle/Prop/PropSingle
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔭} (𝔓 : 𝔒 → Ø 𝔭)
  (x : 𝔒)
  where
  open ℭlass (mkClass 𝔓 (𝔓 x)) public

module Prop-PropSingle/Prop/PropSingle
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔭} (𝔓 : 𝔒 → Ø 𝔭)
  where
  private module M = PropSingle-PropSingle/Prop/PropSingle 𝔓
  class = ∀ {x} → M.class x
  type = ∀ x → M.type x
  method = λ ⦃ _ : class ⦄ x → M.method x

module Asymmetric
  ℓ
  (𝔓' : ∀ {𝔬} {𝔒 : Ø 𝔬} {𝔭} (𝔓 : 𝔒 → Ø 𝔭) (x : 𝔒) → 𝔓 x → Ø ℓ)
  where
  module U = Unit-Unit/Unit/Unit
  test-class' : ⦃ _ : ∀ {𝔬} {𝔒 : Ø 𝔬} {𝔭} {𝔓 : 𝔒 → Ø 𝔭} {x : 𝔒} {y : 𝔓 x} → U.class (𝔓' 𝔓 x y) ⦄ → ∀ {𝔬} {𝔒 : Ø 𝔬} {𝔭} {𝔓 : 𝔒 → Ø 𝔭} {x : 𝔒} {y : 𝔓 x} → U.class (𝔓' 𝔓 x y)
  test-class' = !

module Symmetric
  ℓ
  (𝔓' : ∀ {𝔬} {𝔒 : Ø 𝔬} {𝔭} (𝔓 : 𝔒 → Ø 𝔭) (x : 𝔒) → 𝔓 x → 𝔓 x → Ø ℓ)
  where
  module U = Unit-Unit/Unit/Unit
  test-class' : ⦃ _ : ∀ {𝔬} {𝔒 : Ø 𝔬} {𝔭} {𝔓 : 𝔒 → Ø 𝔭} {x : 𝔒} {y z : 𝔓 x} → U.class (𝔓' 𝔓 x y z → 𝔓' 𝔓 x y z) ⦄ → ∀ {𝔬} {𝔒 : Ø 𝔬} {𝔭} {𝔓 : 𝔒 → Ø 𝔭} {x : 𝔒} {y z : 𝔓 x} → U.class (𝔓' 𝔓 x y z → 𝔓' 𝔓 x y z)
  test-class' ⦃ ⌶ ⦄ = !
  module V {𝔬} (𝔒 : Ø 𝔬) = ℭlass (mkClass 𝔒 (𝔒 → 𝔒))
  test-classV : ⦃ _ : ∀ {𝔬} {𝔒 : Ø 𝔬} {𝔭} {𝔓 : 𝔒 → Ø 𝔭} {x : 𝔒} {y z : 𝔓 x} → V.class (𝔓' 𝔓 x y z) ⦄ → ∀ {𝔬} {𝔒 : Ø 𝔬} {𝔭} {𝔓 : 𝔒 → Ø 𝔭} {x : 𝔒} {y z : 𝔓 x} → V.class (𝔓' 𝔓 x y z)
  test-classV ⦃ ⌶ ⦄ = !
  test-methodV : ⦃ _ : ∀ {𝔬} {𝔒 : Ø 𝔬} {𝔭} {𝔓 : 𝔒 → Ø 𝔭} {x : 𝔒} {y z : 𝔓 x} → V.class (𝔓' 𝔓 x y z) ⦄ → ∀ {𝔬} {𝔒 : Ø 𝔬} {𝔭} {𝔓 : 𝔒 → Ø 𝔭} {x : 𝔒} {y z : 𝔓 x} → V.type (𝔓' 𝔓 x y z)
  test-methodV ⦃ ⌶ ⦄ = V.method _
  module W {𝔬} {𝔒 : Ø 𝔬} (p : 𝔒) = ℭlass (mkClass p 𝔒)
  test-classW : ⦃ _ : ∀ {𝔬} {𝔒 : Ø 𝔬} {𝔭} {𝔓 : 𝔒 → Ø 𝔭} {x : 𝔒} {y z : 𝔓 x} {p : 𝔓' 𝔓 x y z} → W.class p ⦄ → ∀ {𝔬} {𝔒 : Ø 𝔬} {𝔭} {𝔓 : 𝔒 → Ø 𝔭} {x : 𝔒} {y z : 𝔓 x} {p : 𝔓' 𝔓 x y z} → W.class p
  test-classW ⦃ ⌶ ⦄ = magic
  test-methodW : ⦃ _ : ∀ {𝔬} {𝔒 : Ø 𝔬} {𝔭} {𝔓 : 𝔒 → Ø 𝔭} {x : 𝔒} {y z : 𝔓 x} {p : 𝔓' 𝔓 x y z} → W.class p ⦄ → ∀ {𝔬} {𝔒 : Ø 𝔬} {𝔭} {𝔓 : 𝔒 → Ø 𝔭} {x : 𝔒} {y z : 𝔓 x} {p : 𝔓' 𝔓 x y z} → W.type p
  test-methodW {p = p} = W.method p

module Prop-
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔭} (𝔓 : 𝔒 → Ø 𝔭)
  where
  module -Unit/Unit/Unit where
    module V = Prop-Unit/Unit/Unit 𝔓
    module H = Prop-Unit/Unit/Unit
    module X = Unit-Unit/Unit/Unit
    test-class' : ⦃ _ : {𝔓 : 𝔒 → Ø 𝔭} → H.class 𝔓 ⦄ → {𝔓 : 𝔒 → Ø 𝔭} → H.class 𝔓
    test-class' ⦃ ⌶ ⦄ {𝔓 = 𝔓} = magic -- ⌶ {𝔓 = 𝔓} -- FIXME
    test-class : ⦃ _ : V.class ⦄ → V.class
    test-class = !
    test-method-V : ⦃ _ : V.class ⦄ → V.type
    test-method-V = V.method
    test-method-H : ⦃ _ : V.class ⦄ → V.type
    test-method-H = H.method _
    test-method-X : ⦃ _ : V.class ⦄ → V.type
    test-method-X _ = X.method _ -- FIXME
  module -PropSingle/Prop/PropSingle where
    module V = Prop-PropSingle/Prop/PropSingle 𝔓
    module H = Prop-PropSingle/Prop/PropSingle
    module X = PropSingle-PropSingle/Prop/PropSingle
    test-class' : ⦃ _ : {𝔓 : 𝔒 → Ø 𝔭} → H.class 𝔓 ⦄ → {𝔓 : 𝔒 → Ø 𝔭} → H.class 𝔓
    test-class' ⦃ ⌶ ⦄ = magic
    test-class : ⦃ _ : V.class ⦄ → V.class
    test-class = !
    test-method-V : ⦃ _ : V.class ⦄ → V.type
    test-method-V = V.method
    test-method-H : ⦃ _ : V.class ⦄ → V.type
    test-method-H = H.method _
    test-method-X : ⦃ _ : V.class ⦄ → V.type
    test-method-X _ = X.method _ _ -- FIXME

module Rel-
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} (ℜ : 𝔒 → 𝔒 → Ø 𝔯)
  where
  module -Unit/Unit/Unit where
    module V = Rel-Unit/Unit/Unit ℜ
    module H = Rel-Unit/Unit/Unit
    module X = Unit-Unit/Unit/Unit
    test-class : ⦃ _ : V.class ⦄ → V.class
    test-class = !
    test-method-V : ⦃ _ : V.class ⦄ → V.type
    test-method-V = V.method
    test-method-H : ⦃ _ : V.class ⦄ → V.type
    test-method-H = H.method ℜ -- FIXME
    test-method-X : ⦃ _ : V.class ⦄ → V.type
    test-method-X _ = X.method _ -- FIXME
  module -RelSingle/Rel/RelSingle where
    module V = Rel-RelSingle/Rel/RelSingle ℜ
    module H = Rel-RelSingle/Rel/RelSingle
    module X = RelSingle-RelSingle/Rel/RelSingle
    test-class : ⦃ _ : V.class ⦄ → V.class
    test-class = !
    test-method-V : ⦃ _ : V.class ⦄ → V.type
    test-method-V = V.method
    test-method-H : ⦃ _ : V.class ⦄ → V.type
    test-method-H = H.method _
    test-method-X : ⦃ _ : V.class ⦄ → V.type
    test-method-X = X.method _ _

module Prop-Rel-
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔭} (𝔓 : 𝔒 → Ø 𝔭)
  where
  module -Unit/Unit/Unit where
    module V = Prop-Rel-Unit/Unit/Unit 𝔓
    module H = Prop-Rel-Unit/Unit/Unit
    module X = RelSingle-Unit/Unit/Unit
    test-class' : ⦃ _ : ∀ {𝔬} {𝔒 : Ø 𝔬} {𝔭} {𝔓 : 𝔒 → Ø 𝔭} → H.class 𝔓 ⦄ → ∀ {𝔬} {𝔒 : Ø 𝔬} {𝔭} {𝔓 : 𝔒 → Ø 𝔭} → H.class 𝔓
    test-class' ⦃ ⌶ ⦄ {ℜ} = magic -- ! -- FIXME
    test-class : ⦃ _ : V.class ⦄ → V.class
    test-class = !
    test-method-V : ⦃ _ : V.class ⦄ → V.type
    test-method-V ⦃ ⌶ ⦄ = magic
    test-method-H : ⦃ _ : V.class ⦄ → V.type
    test-method-H ⦃ ⌶ ⦄ = magic -- H.method _
    test-method-X : ⦃ _ : V.class ⦄ → V.type
    test-method-X ⦃ ⌶ ⦄ = magic -- X.method _ _
  module -RelSingle/Rel/RelSingle where
    module V = Prop-Rel-RelSingle/Rel/RelSingle 𝔓
    module H = Prop-Rel-RelSingle/Rel/RelSingle
    module X = RelSingle-RelSingle/Rel/RelSingle
    test-class' : ⦃ _ : ∀ {𝔬} {𝔒 : Ø 𝔬} {𝔭} {𝔓 : 𝔒 → Ø 𝔭} → H.class 𝔓 ⦄ → ∀ {𝔬} {𝔒 : Ø 𝔬} {𝔭} (𝔓 : 𝔒 → Ø 𝔭) → H.class 𝔓
    test-class' ⦃ ⌶ ⦄ = !
    test-class : ⦃ _ : V.class ⦄ → V.class
    test-class = !
    test-method-V : ⦃ _ : V.class ⦄ → V.type
    test-method-V ⦃ ⌶ ⦄ = magic -- V.method
    test-method-H : ⦃ _ : V.class ⦄ → V.type
    test-method-H ⦃ ⌶ ⦄ = magic -- H.method _
    test-method-X : ⦃ _ : V.class ⦄ → V.type
    test-method-X ⦃ ⌶ ⦄ = magic -- FIXME

module UnitLevel-
  {𝔬} (𝔒 : Ø 𝔬) ℓ
  where
  module -Unit/Unit/Unit where
    module V = UnitLevel-Unit/Unit/Unit 𝔒 ℓ
    module H = UnitLevel-Unit/Unit/Unit
    module X = RelSingle-Unit/Unit/Unit
    test-class : ⦃ _ : V.class ⦄ → V.class
    test-class ⦃ ⌶ ⦄ {ℜ} = ⌶ {ℜ} -- FIXME
    test-method-V : ⦃ _ : V.class ⦄ → V.type
    test-method-V ⦃ ⌶ ⦄ {ℜ} = magic
    test-method-H : ⦃ _ : V.class ⦄ → V.type
    test-method-H ⦃ ⌶ ⦄ {ℜ} = magic -- H.method _
    test-method-X : ⦃ _ : V.class ⦄ → V.type
    test-method-X ⦃ ⌶ ⦄ {ℜ} x = magic -- X.method _ _
  module -RelSingle/Rel/RelSingle where
    module V = UnitLevel-RelSingle/Rel/RelSingle 𝔒 ℓ
    module H = UnitLevel-RelSingle/Rel/RelSingle
    module X = RelSingle-RelSingle/Rel/RelSingle
    test-class : ⦃ _ : V.class ⦄ → V.class
    test-class = !
    test-method-V : ⦃ _ : V.class ⦄ → V.type
    test-method-V ⦃ ⌶ ⦄ {ℜ} = magic -- V.method
    test-method-H : ⦃ _ : V.class ⦄ → V.type
    test-method-H ⦃ ⌶ ⦄ {ℜ} = magic -- H.method _
    test-method-X : ⦃ _ : V.class ⦄ → V.type
    test-method-X ⦃ ⌶ ⦄ {ℜ} = X.method ℜ _ -- FIXME

module Rel-Extension
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔭} (𝔓 : 𝔒 → Ø 𝔭)
  (let ℜ = Extension 𝔓)
  where
  module -Unit/Unit/Unit where
    module V = Rel-Unit/Unit/Unit ℜ
    module H = Rel-Unit/Unit/Unit
    module X = Unit-Unit/Unit/Unit
    test-class' : ⦃ _ : ∀ {𝔬} {𝔒 : Ø 𝔬} {𝔭} {𝔓 : 𝔒 → Ø 𝔭} (let ℜ = Extension 𝔓) → H.class ℜ ⦄ → ∀ {𝔬} {𝔒 : Ø 𝔬} {𝔭} {𝔓 : 𝔒 → Ø 𝔭} (let ℜ = Extension 𝔓) → H.class ℜ
    test-class' ⦃ ⌶ ⦄ {𝔓 = 𝔓} = magic -- ⌶ {𝔓 = 𝔓} -- FIXME
    test-class : ⦃ _ : V.class ⦄ → V.class
    test-class = !
    test-method-V : ⦃ _ : V.class ⦄ → V.type
    test-method-V = V.method
    test-method-H : ⦃ _ : V.class ⦄ → V.type
    test-method-H = H.method ℜ -- FIXME
    test-method-X : ⦃ _ : V.class ⦄ → V.type
    test-method-X _ = X.method _ -- FIXME
  module -RelSingle/Rel/RelSingle where
    module V = Rel-RelSingle/Rel/RelSingle ℜ
    module H = Rel-RelSingle/Rel/RelSingle
    module X = RelSingle-RelSingle/Rel/RelSingle
    test-class' : ⦃ _ : ∀ {𝔬} {𝔒 : Ø 𝔬} {𝔭} {𝔓 : 𝔒 → Ø 𝔭} (let ℜ = Extension 𝔓) → H.class ℜ ⦄ → ∀ {𝔬} {𝔒 : Ø 𝔬} {𝔭} {𝔓 : 𝔒 → Ø 𝔭} (let ℜ = Extension 𝔓) → H.class ℜ
    test-class' ⦃ ⌶ ⦄ = ! -- !
    test-class'' : ⦃ _ : ∀ {𝔬} {𝔒 : Ø 𝔬} {𝔭} {𝔓 : 𝔒 → Ø 𝔭} (let ℜ = λ x _ → 𝔓 x) → H.class ℜ ⦄ → ∀ {𝔬} {𝔒 : Ø 𝔬} {𝔭} {𝔓 : 𝔒 → Ø 𝔭} (let ℜ = λ x _ → 𝔓 x) → H.class ℜ
    test-class'' ⦃ ⌶ ⦄ = ! -- !
    test-class : ⦃ _ : V.class ⦄ → V.class
    test-class = !
    test-method-V : ⦃ _ : V.class ⦄ → V.type
    test-method-V = V.method
    test-method-H : ⦃ _ : V.class ⦄ → V.type
    test-method-H = H.method _
    test-method-X : ⦃ _ : V.class ⦄ → V.type
    test-method-X = X.method _ _

module AllUnitTest where
  test : ⦃ I : ∀ {𝔬} {𝔒 : Ø 𝔬} → Unit-Unit/Unit/Unit.class 𝔒 ⦄ → ∀ {𝔬} {𝔒 : Ø 𝔬} → Unit-Unit/Unit/Unit.class 𝔒
  test = !

module AllTest
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔭}
  where

  testProp : ⦃ I : {𝔓 : 𝔒 → Ø 𝔭} → Prop-PropSingle/Prop/PropSingle.class 𝔓 ⦄ → {𝔓 : 𝔒 → Ø 𝔭} → Prop-PropSingle/Prop/PropSingle.class 𝔓
  testProp = !

  testUnitProp : ⦃ I : {𝔓 : 𝔒 → Ø 𝔭} → Prop-Unit/Unit/Unit.class 𝔓 ⦄ → {𝔓 : 𝔒 → Ø 𝔭} → Prop-Unit/Unit/Unit.class 𝔓
  testUnitProp ⦃ I ⦄ {𝔓} = I {𝔓}

module SinglePropTest
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔭} (𝔓 : 𝔒 → Ø 𝔭)
  where

  testProp : ⦃ _ : Prop-PropSingle/Prop/PropSingle.class 𝔓 ⦄ → Prop-PropSingle/Prop/PropSingle.class 𝔓
  testProp = !

  testUnitProp : ⦃ _ : Prop-Unit/Unit/Unit.class 𝔓 ⦄ → Prop-Unit/Unit/Unit.class 𝔓
  testUnitProp = !

module SingleRelTest
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} (ℜ : 𝔒 → 𝔒 → Ø 𝔯)
  where
  testProp : ⦃ _ : Rel-RelSingle/Rel/RelSingle.class ℜ ⦄ → Rel-RelSingle/Rel/RelSingle.class ℜ
  testProp = !
  testUnit : ⦃ _ : Rel-Unit/Unit/Unit.class ℜ ⦄ → Rel-Unit/Unit/Unit.class ℜ
  testUnit = !


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

-- The category of Sets is Monoidal

module Categories.Category.Monoidal.Instance.Sets where

open import Level
open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂; uncurry; map; <_,_>)
open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]′)
open import Data.Unit using (⊤)
open import Relation.Binary.PropositionalEquality
open import Function.Inverse using (module Inverse; _↔_)
open import Function.Related.TypeIsomorphisms
open import Function.Equality using () renaming (_⟨$⟩_ to fun)
open import Function using (_$_)

open import Categories.Category.Instance.Sets
open import Categories.Category.Monoidal
open import Categories.Functor.Bifunctor
open import Categories.Category.Instance.SingletonSet
open import Categories.Category.Instance.EmptySet
import Categories.Morphism as Morphism
import Categories.Category.Cartesian as Cartesian
import Categories.Category.Cocartesian as Cocartesian

open import Data.Sum.Properties

-- Sets is a Monoidal Category with × as Bifunctor
module Product {o : Level} where
  private
    S = Sets o
    open Cartesian S

  Sets-has-all : BinaryProducts
  Sets-has-all = record { product = λ {A} {B} → record
    { A×B = A × B
    ; π₁ = proj₁
    ; π₂ = proj₂
    ; ⟨_,_⟩ = <_,_>
    ; project₁ = refl
    ; project₂ = refl
    ; unique = λ p₁ p₂ {x} → sym (cong₂ _,_ (p₁ {x}) (p₂ {x}))
    } }

  Sets-is : Cartesian
  Sets-is = record { terminal = SingletonSet-⊤ ; products = Sets-has-all }

  private
    module Cart = Cartesian.Cartesian Sets-is

  Sets-Monoidal : Monoidal S
  Sets-Monoidal = Cart.monoidal

module Coproduct {o : Level} where
  private
    S = Sets o
    open Cocartesian S

  Sets-has-all : BinaryCoproducts
  Sets-has-all = record { coproduct = λ {A} {B} → record
    { A+B = A ⊎ B
    ; i₁ = inj₁
    ; i₂ = inj₂
    ; [_,_] = [_,_]′
    ; inject₁ = refl
    ; inject₂ = refl
    ; unique = λ { i₁ i₂ {inj₁ x} → sym (i₁ {x}) ; i₁ i₂ {inj₂ y} → sym (i₂ {y})} -- stdlib?
    } }

  Sets-is : Cocartesian
  Sets-is = record { initial = EmptySet-⊥ ; coproducts = Sets-has-all }

  private
    module Cocart = Cocartesian.Cocartesian Sets-is

  Sets-Monoidal : Monoidal S
  Sets-Monoidal =  Cocart.+-monoidal

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
-- Andreas, 2016-12-15, issue #2341
-- `with` needs to abstract also in sort of target type.

-- {-# OPTIONS -v tc.with:100 #-}

open import Agda.Primitive

test : ∀ a → Set (lsuc a)
test a with a
... | w = Set w

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Propositional equality
------------------------------------------------------------------------

-- This file contains some core definitions which are reexported by
-- Relation.Binary.PropositionalEquality.

module Relation.Binary.PropositionalEquality.Core where

open import Level
open import Relation.Binary.Core
open import Relation.Binary.Consequences.Core

------------------------------------------------------------------------
-- Some properties

sym : ∀ {a} {A : Set a} → Symmetric (_≡_ {A = A})
sym refl = refl

trans : ∀ {a} {A : Set a} → Transitive (_≡_ {A = A})
trans refl eq = eq

subst : ∀ {a p} {A : Set a} → Substitutive (_≡_ {A = A}) p
subst P refl p = p

resp₂ : ∀ {a ℓ} {A : Set a} (∼ : Rel A ℓ) → ∼ Respects₂ _≡_
resp₂ _∼_ = subst⟶resp₂ _∼_ subst

isEquivalence : ∀ {a} {A : Set a} → IsEquivalence (_≡_ {A = A})
isEquivalence = record
  { refl  = refl
  ; sym   = sym
  ; trans = trans
  }


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

open import lib.Basics
open import lib.types.Bool
open import lib.types.Lift
open import lib.types.Paths
open import lib.types.Pointed
open import lib.types.Wedge
open import lib.cubical.Square

module lib.types.BigWedge where

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

  private
    data #BigWedge-aux (X : A → Ptd j) : Type (lmax i j) where
      #bwbase : #BigWedge-aux X
      #bwin : (a : A) → fst (X a) → #BigWedge-aux X

    data #BigWedge (X : A → Ptd j) : Type (lmax i j) where
      #bigwedge : #BigWedge-aux X → (Unit → Unit) → #BigWedge X

  BigWedge : (A → Ptd j) → Type (lmax i j)
  BigWedge X = #BigWedge X

  bwbase : {X : A → Ptd j} → BigWedge X
  bwbase = #bigwedge #bwbase _

  bwin : {X : A → Ptd j} → (a : A) → fst (X a) → BigWedge X
  bwin a x = #bigwedge (#bwin a x) _

  ⊙BigWedge : (A → Ptd j) → Ptd (lmax i j)
  ⊙BigWedge X = ⊙[ BigWedge X , bwbase ]

  postulate  -- HIT
    bwglue : {X : A → Ptd j} → (a : A) → bwbase {X} == bwin a (snd (X a))

  ⊙bwin : {X : A → Ptd j} → (a : A) → fst (X a ⊙→ ⊙BigWedge X)
  ⊙bwin a = (bwin a , ! (bwglue a))

  module BigWedgeElim {X : A → Ptd j} {k} {P : BigWedge X → Type k}
    (base* : P bwbase)
    (in* : (a : A) (x : fst (X a)) → P (bwin a x))
    (glue* : (a : A) → base* == in* a (snd (X a)) [ P ↓ bwglue a ]) where

    f : Π (BigWedge X) P
    f = f-aux phantom where

      f-aux : Phantom glue* → Π (BigWedge X) P
      f-aux phantom (#bigwedge #bwbase _) = base*
      f-aux phantom (#bigwedge (#bwin a x) _) = in* a x

    postulate  -- HIT
      glue-β : (a : A) → apd f (bwglue a) == glue* a

  open BigWedgeElim public using () renaming (f to BigWedge-elim)

  module BigWedgeRec {X : A → Ptd j} {k} {C : Type k}
    (base* : C)
    (in* : (a : A) → fst (X a) → C)
    (glue* : (a : A) → base* == in* a (snd (X a))) where

    private
      module M = BigWedgeElim base* in* (λ c → ↓-cst-in (glue* c))

    f : BigWedge X → C
    f = M.f

    glue-β : (a : A) → ap f (bwglue a) == glue* a
    glue-β a = apd=cst-in {f = f} (M.glue-β a)

{- A BigWedge indexed by Bool is just a binary Wedge -}
module _ {i} (Pick : Lift {j = i} Bool → Ptd i) where

  BigWedge-Bool-equiv :
    BigWedge Pick ≃ Wedge (Pick (lift true)) (Pick (lift false))
  BigWedge-Bool-equiv = equiv f g f-g g-f
    where
    module F = BigWedgeRec {X = Pick}
      {C = Wedge (Pick (lift true)) (Pick (lift false))}
      (winl (snd (Pick (lift true))))
      (λ {(lift true) → winl; (lift false) → winr})
      (λ {(lift true) → idp; (lift false) → wglue})

    module G = WedgeRec {X = Pick (lift true)} {Y = Pick (lift false)}
      {C = BigWedge Pick}
      (bwin (lift true))
      (bwin (lift false))
      (! (bwglue (lift true)) ∙ bwglue (lift false))

    f = F.f
    g = G.f

    f-g : ∀ w → f (g w) == w
    f-g = Wedge-elim
      (λ _ → idp)
      (λ _ → idp)
      (↓-∘=idf-in f g $
        ap f (ap g wglue)
          =⟨ ap (ap f) G.glue-β ⟩
        ap f (! (bwglue (lift true)) ∙ bwglue (lift false))
          =⟨ ap-∙ f (! (bwglue (lift true))) (bwglue (lift false)) ⟩
        ap f (! (bwglue (lift true))) ∙ ap f (bwglue (lift false))
          =⟨ ap-! f (bwglue (lift true))
             |in-ctx (λ w → w ∙ ap f (bwglue (lift false))) ⟩
        ! (ap f (bwglue (lift true))) ∙ ap f (bwglue (lift false))
          =⟨ F.glue-β (lift true)
             |in-ctx (λ w → ! w ∙ ap f (bwglue (lift false))) ⟩
        ap f (bwglue (lift false))
          =⟨ F.glue-β (lift false) ⟩
        wglue ∎)

    g-f : ∀ bw → g (f bw) == bw
    g-f = BigWedge-elim
      (! (bwglue (lift true)))
      (λ {(lift true) → λ _ → idp; (lift false) → λ _ → idp})
      (λ {(lift true) → ↓-∘=idf-from-square g f $
            ap (ap g) (F.glue-β (lift true)) ∙v⊡
            bl-square (bwglue (lift true));
          (lift false) → ↓-∘=idf-from-square g f $
            (ap (ap g) (F.glue-β (lift false)) ∙ G.glue-β) ∙v⊡
            lt-square (! (bwglue (lift true))) ⊡h vid-square})

  BigWedge-Bool-⊙path :
    ⊙BigWedge Pick == ⊙Wedge (Pick (lift true)) (Pick (lift false))
  BigWedge-Bool-⊙path = ⊙ua (⊙≃-in BigWedge-Bool-equiv idp)

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
{-# OPTIONS --allow-incomplete-matches #-}

module Issue3295.Incomplete where

open import Agda.Builtin.Nat

f : Nat → Nat
f zero = zero


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

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat using (ℕ)
open import Cubical.Data.FinData
open import Cubical.Data.Vec

open import Cubical.Algebra.RingSolver.RawRing
open import Cubical.Algebra.RingSolver.AlmostRing renaming (⟨_⟩ to ⟨_⟩ᵣ)
open import Cubical.Algebra.RingSolver.HornerForms

private
  variable
    ℓ : Level

module HomomorphismProperties (R : AlmostRing {ℓ}) where
  private
    νR = AlmostRing→RawRing R
  open AlmostRing R
  open Theory R
  open IteratedHornerOperations νR

  evalHom+0 : (n : ℕ) (P : IteratedHornerForms νR n) (xs : Vec ⟨ νR ⟩ n)
      → eval n (0ₕ +ₕ P) xs ≡ eval n P xs
  evalHom+0 ℕ.zero (const x) [] = +Lid _
  evalHom+0 (ℕ.suc n) P xs = refl

  eval0H : (n : ℕ) (xs : Vec ⟨ νR ⟩ n)
         → eval {R = νR} n 0ₕ xs ≡ 0r
  eval0H .ℕ.zero [] = refl
  eval0H .(ℕ.suc _) (x ∷ xs) = refl

  eval1ₕ : (n : ℕ) (xs : Vec ⟨ νR ⟩ n)
         → eval {R = νR} n 1ₕ xs ≡ 1r
  eval1ₕ .ℕ.zero [] = refl
  eval1ₕ (ℕ.suc n) (x ∷ xs) =
    eval (ℕ.suc n) 1ₕ (x ∷ xs)                             ≡⟨ refl ⟩
    eval (ℕ.suc n) (0H ·X+ 1ₕ) (x ∷ xs)                    ≡⟨ refl ⟩
    eval {R = νR} (ℕ.suc n) 0H (x ∷ xs) · x + eval n 1ₕ xs ≡⟨ cong (λ u → u · x + eval n 1ₕ xs)
                                                                   (eval0H _ (x ∷ xs)) ⟩
    0r · x + eval n 1ₕ xs                                   ≡⟨ cong (λ u → 0r · x + u)
                                                                    (eval1ₕ _ xs) ⟩
    0r · x + 1r                                            ≡⟨ cong (λ u → u + 1r)
                                                                   (0LeftAnnihilates _) ⟩
    0r + 1r                                                ≡⟨ +Lid _ ⟩
    1r ∎

  -evalDist :
    (n : ℕ) (P : IteratedHornerForms νR n) (xs : Vec ⟨ νR ⟩ n)
    → eval n (-ₕ P) xs ≡ - eval n P xs
  -evalDist .ℕ.zero (const x) []   = refl
  -evalDist          n       0H  xs =
    eval n (-ₕ 0H) xs  ≡⟨ eval0H n xs ⟩
    0r                        ≡⟨ sym 0IsSelfinverse ⟩
    - 0r                      ≡⟨ cong -_ (sym (eval0H n xs)) ⟩
    - eval n 0H xs     ∎
  -evalDist .(ℕ.suc _) (P ·X+ Q) (x ∷ xs) =
      eval (ℕ.suc _) (-ₕ (P ·X+ Q)) (x ∷ xs)
    ≡⟨ refl ⟩
      eval (ℕ.suc _) ((-ₕ P) ·X+ (-ₕ Q)) (x ∷ xs)
    ≡⟨ refl ⟩
      (eval (ℕ.suc _) (-ₕ P) (x ∷ xs)) · x + eval _ (-ₕ Q) xs
    ≡⟨ cong (λ u → u · x + eval _ (-ₕ Q) xs) (-evalDist _ P _) ⟩
      (- eval (ℕ.suc _) P (x ∷ xs)) · x + eval _ (-ₕ Q) xs
    ≡⟨ cong (λ u → (- eval (ℕ.suc _) P (x ∷ xs)) · x + u) (-evalDist _ Q _) ⟩
      (- eval (ℕ.suc _) P (x ∷ xs)) · x + - eval _ Q xs
    ≡⟨ cong (λ u → u + - eval _ Q xs) (sym (-Comm· _ _)) ⟩
      - (eval (ℕ.suc _) P (x ∷ xs)) · x + - eval _ Q xs
    ≡⟨ sym (-Dist+ _ _) ⟩
      - ((eval (ℕ.suc _) P (x ∷ xs)) · x + eval _ Q xs)
    ≡⟨ refl ⟩
      - eval (ℕ.suc _) (P ·X+ Q) (x ∷ xs) ∎

  +Homeval :
    (n : ℕ) (P Q : IteratedHornerForms νR n) (xs : Vec ⟨ νR ⟩ n)
    → eval n (P +ₕ Q) xs ≡ (eval n P xs) + (eval n Q xs)
  +Homeval .ℕ.zero (const x) (const y) [] = refl
  +Homeval n 0H Q xs =
    eval n (0H +ₕ Q) xs            ≡⟨ refl ⟩
    eval n Q xs                    ≡⟨ sym (+Lid _) ⟩
    0r + eval n Q xs               ≡⟨ cong (λ u → u + eval n Q xs) (sym (eval0H n xs)) ⟩
    eval n 0H xs + eval n Q xs ∎
  +Homeval .(ℕ.suc _) (P ·X+ Q) 0H xs =
    eval (ℕ.suc _) ((P ·X+ Q) +ₕ 0H) xs                    ≡⟨ refl ⟩
    eval (ℕ.suc _) (P ·X+ Q) xs                            ≡⟨ sym (+Rid _) ⟩
    eval (ℕ.suc _) (P ·X+ Q) xs + 0r
   ≡⟨ cong (λ u → eval (ℕ.suc _) (P ·X+ Q) xs + u) (sym (eval0H _ xs)) ⟩
    eval (ℕ.suc _) (P ·X+ Q) xs + eval (ℕ.suc _) 0H xs ∎
  +Homeval .(ℕ.suc _) (P ·X+ Q) (S ·X+ T) (x ∷ xs) =
    eval (ℕ.suc _) ((P ·X+ Q) +ₕ (S ·X+ T)) (x ∷ xs)
   ≡⟨ refl ⟩
    eval (ℕ.suc _) ((P +ₕ S) ·X+ (Q +ₕ T)) (x ∷ xs)
   ≡⟨ refl ⟩
    (eval (ℕ.suc _) (P +ₕ S) (x ∷ xs)) · x + eval _ (Q +ₕ T) xs
   ≡⟨ cong (λ u → (eval (ℕ.suc _) (P +ₕ S) (x ∷ xs)) · x + u) (+Homeval _ Q T xs) ⟩
    (eval (ℕ.suc _) (P +ₕ S) (x ∷ xs)) · x + (eval _ Q xs + eval _ T xs)
   ≡⟨ cong (λ u → u · x + (eval _ Q xs + eval _ T xs)) (+Homeval (ℕ.suc _) P S (x ∷ xs)) ⟩
    (eval (ℕ.suc _) P (x ∷ xs) + eval (ℕ.suc _) S (x ∷ xs)) · x
    + (eval _ Q xs + eval _ T xs)
   ≡⟨ cong (λ u → u + (eval _ Q xs + eval _ T xs)) (·DistL+ _ _ _) ⟩
    (eval (ℕ.suc _) P (x ∷ xs)) · x + (eval (ℕ.suc _) S (x ∷ xs)) · x
    + (eval _ Q xs + eval _ T xs)
   ≡⟨ +ShufflePairs _ _ _ _ ⟩
    ((eval (ℕ.suc _) P (x ∷ xs)) · x + eval _ Q xs)
    + ((eval (ℕ.suc _) S (x ∷ xs)) · x + eval _ T xs)
   ≡⟨ refl ⟩
    eval (ℕ.suc _) (P ·X+ Q) (x ∷ xs)
    + eval (ℕ.suc _) (S ·X+ T) (x ∷ xs) ∎

  ⋆Homeval : (n : ℕ)
             (r : IteratedHornerForms νR n)
             (P : IteratedHornerForms νR (ℕ.suc n)) (x : ⟨ νR ⟩) (xs : Vec ⟨ νR ⟩ n)
           → eval (ℕ.suc n) (r ⋆ P) (x ∷ xs) ≡ eval n r xs · eval (ℕ.suc n) P (x ∷ xs)

  ⋆0LeftAnnihilates :
    (n : ℕ) (P : IteratedHornerForms νR (ℕ.suc n)) (xs : Vec ⟨ νR ⟩ (ℕ.suc n))
    → eval (ℕ.suc n) (0ₕ ⋆ P) xs ≡ 0r

  ·Homeval : (n : ℕ) (P Q : IteratedHornerForms νR n) (xs : Vec ⟨ νR ⟩ n)
    → eval n (P ·ₕ Q) xs ≡ (eval n P xs) · (eval n Q xs)

  ⋆0LeftAnnihilates n 0H xs = eval0H (ℕ.suc n) xs
  ⋆0LeftAnnihilates n (P ·X+ Q) (x ∷ xs) =
      eval (ℕ.suc n) (0ₕ ⋆ (P ·X+ Q)) (x ∷ xs)                    ≡⟨ refl ⟩
      eval (ℕ.suc n) ((0ₕ ⋆ P) ·X+ (0ₕ ·ₕ Q)) (x ∷ xs)             ≡⟨ refl ⟩
      (eval (ℕ.suc n) (0ₕ ⋆ P) (x ∷ xs)) · x + eval n (0ₕ ·ₕ Q) xs
    ≡⟨ cong (λ u → (u · x) + eval _ (0ₕ ·ₕ Q) _) (⋆0LeftAnnihilates n P (x ∷ xs)) ⟩
      0r · x + eval n (0ₕ ·ₕ Q) xs
    ≡⟨ cong (λ u → u + eval _ (0ₕ ·ₕ Q) _) (0LeftAnnihilates _) ⟩
      0r + eval n (0ₕ ·ₕ Q) xs
    ≡⟨ +Lid _ ⟩
      eval n (0ₕ ·ₕ Q) xs
    ≡⟨ ·Homeval n 0ₕ Q _ ⟩
      eval n 0ₕ xs · eval n Q xs
    ≡⟨ cong (λ u → u · eval n Q xs) (eval0H _ xs) ⟩
      0r · eval n Q xs
    ≡⟨ 0LeftAnnihilates _ ⟩
      0r ∎

  ⋆Homeval n r 0H x xs =
    eval (ℕ.suc n) (r ⋆ 0H) (x ∷ xs)         ≡⟨ refl ⟩
    0r                                       ≡⟨ sym (0RightAnnihilates _) ⟩
    eval n r xs · 0r                         ≡⟨ refl ⟩
    eval n r xs · eval {R = νR} (ℕ.suc n) 0H (x ∷ xs) ∎
  ⋆Homeval n r (P ·X+ Q) x xs =
      eval (ℕ.suc n) (r ⋆ (P ·X+ Q)) (x ∷ xs)                    ≡⟨ refl ⟩
      eval (ℕ.suc n) ((r ⋆ P) ·X+ (r ·ₕ Q)) (x ∷ xs)              ≡⟨ refl ⟩
      (eval (ℕ.suc n) (r ⋆ P) (x ∷ xs)) · x + eval n (r ·ₕ Q) xs
    ≡⟨ cong (λ u → u · x + eval n (r ·ₕ Q) xs) (⋆Homeval n r P x xs) ⟩
      (eval n r xs · eval (ℕ.suc n) P (x ∷ xs)) · x + eval n (r ·ₕ Q) xs
    ≡⟨ cong (λ u → (eval n r xs · eval (ℕ.suc n) P (x ∷ xs)) · x + u) (·Homeval n r Q xs) ⟩
      (eval n r xs · eval (ℕ.suc n) P (x ∷ xs)) · x + eval n r xs · eval n Q xs
    ≡⟨ cong (λ u → u  + eval n r xs · eval n Q xs) (sym (·Assoc _ _ _)) ⟩
      eval n r xs · (eval (ℕ.suc n) P (x ∷ xs) · x) + eval n r xs · eval n Q xs
    ≡⟨ sym (·DistR+ _ _ _) ⟩
      eval n r xs · ((eval (ℕ.suc n) P (x ∷ xs) · x) + eval n Q xs)
    ≡⟨ refl ⟩
      eval n r xs · eval (ℕ.suc n) (P ·X+ Q) (x ∷ xs) ∎

  combineCases :
    (n : ℕ) (Q : IteratedHornerForms νR n) (P S : IteratedHornerForms νR (ℕ.suc n))
    (xs : Vec ⟨ νR ⟩ (ℕ.suc n))
    → eval (ℕ.suc n) ((P ·X+ Q) ·ₕ S) xs ≡ eval (ℕ.suc n) (((P ·ₕ S) ·X+ 0ₕ) +ₕ (Q ⋆ S)) xs
  combineCases n Q P S (x ∷ xs) with (P ·ₕ S)
  ... | 0H =
    eval (ℕ.suc n) (Q ⋆ S) (x ∷ xs)                ≡⟨ sym (+Lid _) ⟩
    0r + eval (ℕ.suc n) (Q ⋆ S) (x ∷ xs)           ≡⟨ cong (λ u → u + eval _ (Q ⋆ S) (x ∷ xs)) lemma ⟩
    eval (ℕ.suc n) (0H ·X+ 0ₕ) (x ∷ xs)
    + eval (ℕ.suc n) (Q ⋆ S) (x ∷ xs)              ≡⟨ sym (+Homeval (ℕ.suc n)
                                                      (0H ·X+ 0ₕ) (Q ⋆ S) (x ∷ xs)) ⟩
    eval (ℕ.suc n) ((0H ·X+ 0ₕ) +ₕ (Q ⋆ S)) (x ∷ xs) ∎
    where lemma : 0r ≡ eval (ℕ.suc n) (0H ·X+ 0ₕ) (x ∷ xs)
          lemma = 0r
                ≡⟨ sym (+Rid _) ⟩
                  0r + 0r
                ≡⟨ cong (λ u → u + 0r) (sym (0LeftAnnihilates _)) ⟩
                  0r · x + 0r
                ≡⟨ cong (λ u → 0r · x + u) (sym (eval0H _ xs)) ⟩
                  0r · x + eval n 0ₕ xs
                ≡⟨ cong (λ u → u · x + eval n 0ₕ xs) (sym (eval0H _ (x ∷ xs))) ⟩
                  eval {R = νR} (ℕ.suc n) 0H (x ∷ xs) · x + eval n 0ₕ xs
                ≡⟨ refl ⟩
                  eval (ℕ.suc n) (0H ·X+ 0ₕ) (x ∷ xs) ∎
  ... | (_ ·X+ _) = refl

  ·Homeval .ℕ.zero (const x) (const y) [] = refl
  ·Homeval (ℕ.suc n) 0H Q xs =
    eval (ℕ.suc n) (0H ·ₕ Q) xs        ≡⟨ eval0H _ xs ⟩
    0r                                 ≡⟨ sym (0LeftAnnihilates _) ⟩
    0r · eval (ℕ.suc n) Q xs          ≡⟨ cong (λ u → u · eval _ Q xs) (sym (eval0H _ xs)) ⟩
    eval (ℕ.suc n) 0H xs · eval (ℕ.suc n) Q xs ∎
  ·Homeval (ℕ.suc n) (P ·X+ Q) S (x ∷ xs) =
      eval (ℕ.suc n) ((P ·X+ Q) ·ₕ S) (x ∷ xs)
    ≡⟨ combineCases n Q P S (x ∷ xs) ⟩
      eval (ℕ.suc n) (((P ·ₕ S) ·X+ 0ₕ) +ₕ (Q ⋆ S)) (x ∷ xs)
    ≡⟨ +Homeval (ℕ.suc n) ((P ·ₕ S) ·X+ 0ₕ) (Q ⋆ S) (x ∷ xs) ⟩
      eval (ℕ.suc n) ((P ·ₕ S) ·X+ 0ₕ) (x ∷ xs) + eval (ℕ.suc n) (Q ⋆ S) (x ∷ xs)
    ≡⟨ refl ⟩
      (eval (ℕ.suc n) (P ·ₕ S) (x ∷ xs) · x + eval n 0ₕ xs)
      + eval (ℕ.suc n) (Q ⋆ S) (x ∷ xs)
    ≡⟨ cong (λ u → u + eval (ℕ.suc n) (Q ⋆ S) (x ∷ xs))
          ((eval (ℕ.suc n) (P ·ₕ S) (x ∷ xs) · x + eval n 0ₕ xs)
         ≡⟨ cong (λ u → eval (ℕ.suc n) (P ·ₕ S) (x ∷ xs) · x + u) (eval0H _ xs) ⟩
           (eval (ℕ.suc n) (P ·ₕ S) (x ∷ xs) · x + 0r)
         ≡⟨ +Rid _ ⟩
           (eval (ℕ.suc n) (P ·ₕ S) (x ∷ xs) · x)
         ≡⟨ cong (λ u → u · x) (·Homeval (ℕ.suc n) P S (x ∷ xs)) ⟩
           ((eval (ℕ.suc n) P (x ∷ xs) · eval (ℕ.suc n) S (x ∷ xs)) · x)
         ≡⟨ sym (·Assoc _ _ _) ⟩
           (eval (ℕ.suc n) P (x ∷ xs) · (eval (ℕ.suc n) S (x ∷ xs) · x))
         ≡⟨ cong (λ u → eval (ℕ.suc n) P (x ∷ xs) · u) (·Comm _ _) ⟩
           (eval (ℕ.suc n) P (x ∷ xs) · (x · eval (ℕ.suc n) S (x ∷ xs)))
         ≡⟨ ·Assoc _ _ _ ⟩
           (eval (ℕ.suc n) P (x ∷ xs) · x) · eval (ℕ.suc n) S (x ∷ xs)
          ∎) ⟩
      (eval (ℕ.suc n) P (x ∷ xs) · x) · eval (ℕ.suc n) S (x ∷ xs)
      + eval (ℕ.suc n) (Q ⋆ S) (x ∷ xs)
    ≡⟨ cong (λ u → (eval (ℕ.suc n) P (x ∷ xs) · x) · eval (ℕ.suc n) S (x ∷ xs) + u)
            (⋆Homeval n Q S x xs) ⟩
      (eval (ℕ.suc n) P (x ∷ xs) · x) · eval (ℕ.suc n) S (x ∷ xs)
      + eval n Q xs · eval (ℕ.suc n) S (x ∷ xs)
    ≡⟨ sym (·DistL+ _ _ _) ⟩
      ((eval (ℕ.suc n) P (x ∷ xs) · x) + eval n Q xs) · eval (ℕ.suc n) S (x ∷ xs)
    ≡⟨ refl ⟩
      eval (ℕ.suc n) (P ·X+ Q) (x ∷ xs) · eval (ℕ.suc n) S (x ∷ xs) ∎

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical