text:
{-# OPTIONS --without-K --allow-unsolved-metas --exact-split #-}

module 17-cubical-diagrams where

import 16-pushouts
open 16-pushouts public

-- Section 15.1 Commuting cubes

-- Cubes

  {-
    We specify the type of the homotopy witnessing that a cube commutes.
    Imagine that the cube is presented as a lattice

            *
          / | \
         /  |  \
        /   |   \
       *    *    *
       |\ /   \ /|
       | \     / |
       |/ \   / \|
       *    *    *
        \   |   /
         \  |  /
          \ | /
            *

    with all maps pointing in the downwards direction. Presented in this way, a
    cube of maps has a top face, a back-left face, a back-right face, a
    front-left face, a front-right face, and a bottom face, all of which are
    homotopies.

    A term of type coherence-cube is a homotopy filling the cube.
  -}

coherence-cube :
  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
  (f : A → B) (g : A → C) (h : B → D) (k : C → D)
  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
  (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
  (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
  (top : (h' ∘ f') ~ (k' ∘ g'))
  (back-left : (f ∘ hA) ~ (hB ∘ f'))
  (back-right : (g ∘ hA) ~ (hC ∘ g'))
  (front-left : (h ∘ hB) ~ (hD ∘ h'))
  (front-right : (k ∘ hC) ~ (hD ∘ k'))
  (bottom : (h ∘ f) ~ (k ∘ g)) →
  UU _
coherence-cube
  f g h k f' g' h' k' hA hB hC hD
  top back-left back-right front-left front-right bottom =
  (((h ·l back-left) ∙h (front-left ·r f')) ∙h (hD ·l top)) ~
  ((bottom ·r hA) ∙h ((k ·l back-right) ∙h (front-right ·r g')))

coherence-hexagon :
  {l : Level} {A : UU l} {x u u' v v' y : A}
  (α : Id x u) (β : Id u u') (γ : Id u' y)
  (δ : Id x v) (ε : Id v v') (ζ : Id v' y) → UU l
coherence-hexagon α β γ δ ε ζ = Id ((α ∙ β) ∙ γ) (δ ∙ (ε ∙ ζ))

hexagon-rotate-120 :
  {l : Level} {A : UU l} {x u u' v v' y : A}
  (α : Id x u) (β : Id u u') (γ : Id u' y)
  (δ : Id x v) (ε : Id v v') (ζ : Id v' y) →
  coherence-hexagon α β γ δ ε ζ →
  coherence-hexagon (inv ε) (inv δ) α ζ (inv γ) (inv β)
hexagon-rotate-120 refl refl refl refl refl .refl refl = refl

hexagon-rotate-240 :
  {l : Level} {A : UU l} {x u u' v v' y : A}
  (α : Id x u) (β : Id u u') (γ : Id u' y)
  (δ : Id x v) (ε : Id v v') (ζ : Id v' y) →
  coherence-hexagon α β γ δ ε ζ →
  coherence-hexagon γ (inv ζ) (inv ε) (inv β) (inv α) δ
hexagon-rotate-240 refl refl refl refl refl .refl refl = refl

hexagon-mirror-A :
  {l : Level} {A : UU l} {x u u' v v' y : A}
  (α : Id x u) (β : Id u u') (γ : Id u' y)
  (δ : Id x v) (ε : Id v v') (ζ : Id v' y) →
  coherence-hexagon α β γ δ ε ζ →
  coherence-hexagon ε ζ (inv γ) (inv δ) α β
hexagon-mirror-A refl refl refl refl refl .refl refl = refl

hexagon-mirror-B :
  {l : Level} {A : UU l} {x u u' v v' y : A}
  (α : Id x u) (β : Id u u') (γ : Id u' y)
  (δ : Id x v) (ε : Id v v') (ζ : Id v' y) →
  coherence-hexagon α β γ δ ε ζ →
  coherence-hexagon (inv α) δ ε β γ (inv ζ)
hexagon-mirror-B refl refl refl refl refl .refl refl = refl

hexagon-mirror-C :
  {l : Level} {A : UU l} {x u u' v v' y : A}
  (α : Id x u) (β : Id u u') (γ : Id u' y)
  (δ : Id x v) (ε : Id v v') (ζ : Id v' y) →
  coherence-hexagon α β γ δ ε ζ →
  coherence-hexagon (inv γ) (inv β) (inv α) (inv ζ) (inv ε) (inv δ)
hexagon-mirror-C refl refl refl refl refl .refl refl = refl

{- Since the specification of a cube is rather lengthy, we use Agda's
   parametrized module system in order to avoid having to specify the same
   variables multiple times.
-}

module Cubes
  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
  (f : A → B) (g : A → C) (h : B → D) (k : C → D)
  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
  (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
  (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
  (top : (h' ∘ f') ~ (k' ∘ g'))
  (back-left : (f ∘ hA) ~ (hB ∘ f'))
  (back-right : (g ∘ hA) ~ (hC ∘ g'))
  (front-left : (h ∘ hB) ~ (hD ∘ h'))
  (front-right : (k ∘ hC) ~ (hD ∘ k'))
  (bottom : (h ∘ f) ~ (k ∘ g))
  (c : coherence-cube
    f g h k f' g' h' k' hA hB hC hD
    top back-left back-right front-left front-right bottom)
  where

  {-
    The symmetry group D_3 acts on a cube. However, the coherence filling a
    a cube needs to be modified to show that the rotated/reflected cube again
    commutes. In the following definitions we provide the homotopies witnessing
    that the rotated/reflected cubes again commute.

    Note: although in principle it ought to be enough to show this for the
    generators of the symmetry group D_3, in practice it is more
    straightforward to just do the work for each of the symmetries separately.
    One reason is that some of the homotopies witnessing that the faces
    commute will be inverted as the result of an application of a symmetry.
    Inverting a homotopy twice results in a new homotopy that is only
    homotopic to the original homotopy.

    We first provide some constructions involving homotopies that will help us
    manipulating coherences of cubes.
  -}

  -- We show that a rotation of a commuting cube again commutes.
  coherence-cube-rotate-120 :
    coherence-cube
      hC k' k hD hA f' f hB g' g h' h
      back-left
      (htpy-inv back-right) (htpy-inv top)
      (htpy-inv bottom) (htpy-inv front-left)
      front-right
  coherence-cube-rotate-120 a' =
    ( ap (λ t → t ∙ (ap h (back-left a')))
      ( ap (λ t' → t' ∙ inv (bottom (hA a')))
        ( ap-inv k (back-right a')))) ∙
    ( ( hexagon-rotate-120
        ( ap h (back-left a'))
        ( front-left (f' a'))
        ( ap hD (top a'))
        ( bottom (hA a'))
        ( ap k (back-right a'))
        ( front-right (g' a'))
        ( c a')) ∙
      ( inv
        ( ap (λ t → (front-right (g' a')) ∙ t)
          ( ap (λ t' → t' ∙ inv (front-left (f' a')))
            ( ap-inv hD (top a'))))))

  coherence-cube-rotate-240 :
    coherence-cube
      h' hB hD h g' hA hC g f' k' f k
      (htpy-inv back-right)
      top (htpy-inv back-left)
      (htpy-inv front-right) bottom
      (htpy-inv front-left)
  coherence-cube-rotate-240 a' =
    ( ap (λ t → _ ∙ t) (ap-inv k (back-right a'))) ∙
    ( ( hexagon-rotate-240
        ( ap h (back-left a'))
        ( front-left (f' a'))
        ( ap hD (top a'))
        ( bottom (hA a'))
        ( ap k (back-right a'))
        ( front-right (g' a'))
        ( c a')) ∙
      ( inv
        ( ap
          ( λ t → inv (front-left (f' a')) ∙ t)
          ( ap (λ t' → t' ∙ _) (ap-inv h (back-left a'))))))

  {-
    We show that a reflection through the plane spanned by the vertices
    A', A, and D of a commuting cube again commutes.

    Note: Since the vertices A' and D must always be fixed, the vertex A
    determines the mirror symmetry.
  -}

  coherence-cube-mirror-A :
    coherence-cube g f k h g' f' k' h' hA hC hB hD
      (htpy-inv top) back-right back-left front-right front-left (htpy-inv bottom)
  coherence-cube-mirror-A a' =
    ( ap (λ t → _ ∙ t) (ap-inv hD (top a'))) ∙
    ( hexagon-mirror-A
      ( ap h (back-left a'))
      ( front-left (f' a'))
      ( ap hD (top a'))
      ( bottom (hA a'))
      ( ap k (back-right a'))
      ( front-right (g' a'))
      ( c a'))

  coherence-cube-mirror-B :
    coherence-cube hB h' h hD hA g' g hC f' f k' k
    back-right (htpy-inv back-left) top bottom (htpy-inv front-right) front-left
  coherence-cube-mirror-B a' =
    ( ap (λ t → t ∙ (ap k (back-right a')))
      ( ap (λ t → t ∙ _) (ap-inv h (back-left a')))) ∙
    ( hexagon-mirror-B
      ( ap h (back-left a'))
      ( front-left (f' a'))
      ( ap hD (top a'))
      ( bottom (hA a'))
      ( ap k (back-right a'))
      ( front-right (g' a'))
      ( c a'))

  coherence-cube-mirror-C :
    coherence-cube k' hC hD k f' hA hB f g' h' g h
    (htpy-inv back-left) (htpy-inv top) (htpy-inv back-right)
    (htpy-inv front-left) (htpy-inv bottom) (htpy-inv front-right)
  coherence-cube-mirror-C a' =
    ( ap
      ( λ t → (t ∙ inv (front-left (f' a'))) ∙ (ap h (inv (back-left a'))))
      ( ap-inv hD (top a'))) ∙
    ( ( ap (λ t → _ ∙ t) (ap-inv h (back-left a'))) ∙
      ( ( hexagon-mirror-C
          ( ap h (back-left a'))
          ( front-left (f' a'))
          ( ap hD (top a'))
          ( bottom (hA a'))
          ( ap k (back-right a'))
          ( front-right (g' a'))
          ( c a')) ∙
        ( inv
          ( ap
            ( λ t → inv (front-right (g' a')) ∙ t)
            ( ap (λ t' → t' ∙ _) (ap-inv k (back-right a')))))))

open Cubes public

rectangle-back-left-front-left-cube :
  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
  (f : A → B) (g : A → C) (h : B → D) (k : C → D)
  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
  (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
  (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
  (top : (h' ∘ f') ~ (k' ∘ g'))
  (back-left : (f ∘ hA) ~ (hB ∘ f'))
  (back-right : (g ∘ hA) ~ (hC ∘ g'))
  (front-left : (h ∘ hB) ~ (hD ∘ h'))
  (front-right : (k ∘ hC) ~ (hD ∘ k'))
  (bottom : (h ∘ f) ~ (k ∘ g)) →
  ((h ∘ f) ∘ hA) ~ (hD ∘ (h' ∘ f'))
rectangle-back-left-front-left-cube f g h k f' g' h' k' hA hB hC hD
  top back-left back-right front-left front-right bottom =
  (h ·l back-left) ∙h (front-left ·r f')

rectangle-back-right-front-right-cube :
  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
  (f : A → B) (g : A → C) (h : B → D) (k : C → D)
  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
  (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
  (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
  (top : (h' ∘ f') ~ (k' ∘ g'))
  (back-left : (f ∘ hA) ~ (hB ∘ f'))
  (back-right : (g ∘ hA) ~ (hC ∘ g'))
  (front-left : (h ∘ hB) ~ (hD ∘ h'))
  (front-right : (k ∘ hC) ~ (hD ∘ k'))
  (bottom : (h ∘ f) ~ (k ∘ g)) →
  ((k ∘ g) ∘ hA) ~ (hD ∘ (k' ∘ g'))
rectangle-back-right-front-right-cube f g h k f' g' h' k' hA hB hC hD
  top back-left back-right front-left front-right bottom =
  (k ·l back-right) ∙h (front-right ·r g')

coherence-htpy-square-rectangle-bl-fl-rectangle-br-fr-cube :
  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
  (f : A → B) (g : A → C) (h : B → D) (k : C → D)
  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
  (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
  (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
  (top : (h' ∘ f') ~ (k' ∘ g'))
  (back-left : (f ∘ hA) ~ (hB ∘ f'))
  (back-right : (g ∘ hA) ~ (hC ∘ g'))
  (front-left : (h ∘ hB) ~ (hD ∘ h'))
  (front-right : (k ∘ hC) ~ (hD ∘ k'))
  (bottom : (h ∘ f) ~ (k ∘ g))
  (c : coherence-cube f g h k f' g' h' k' hA hB hC hD
    top back-left back-right front-left front-right bottom) →
  coherence-htpy-square
    ( bottom)
    ( htpy-refl' hD)
    ( pair hA
      ( pair
        ( h' ∘ f')
        ( rectangle-back-left-front-left-cube
          f g h k f' g' h' k' hA hB hC hD
          top back-left back-right front-left front-right bottom)))
    ( pair hA
      ( pair
        ( k' ∘ g')
        ( rectangle-back-right-front-right-cube
          f g h k f' g' h' k' hA hB hC hD
          top back-left back-right front-left front-right bottom)))
    ( htpy-refl' hA)
    ( top)
coherence-htpy-square-rectangle-bl-fl-rectangle-br-fr-cube
  f g h k f' g' h' k' hA hB hC hD
  top back-left back-right front-left front-right bottom c =
  ( λ a' →
    ( ap
      ( concat
        ( rectangle-back-left-front-left-cube
          f g h k f' g' h' k' hA hB hC hD
          top back-left back-right front-left front-right bottom a')
        ( hD (k' (g' a'))))
      ( right-unit))) ∙h
  ( c)

rectangle-top-front-left-cube :
  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
  (f : A → B) (g : A → C) (h : B → D) (k : C → D)
  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
  (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
  (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
  (top : (h' ∘ f') ~ (k' ∘ g'))
  (back-left : (f ∘ hA) ~ (hB ∘ f'))
  (back-right : (g ∘ hA) ~ (hC ∘ g'))
  (front-left : (h ∘ hB) ~ (hD ∘ h'))
  (front-right : (k ∘ hC) ~ (hD ∘ k'))
  (bottom : (h ∘ f) ~ (k ∘ g)) →
  ((h ∘ hB) ∘ f') ~ ((hD ∘ k') ∘ g')
rectangle-top-front-left-cube
  f g h k f' g' h' k' hA hB hC hD
  top back-left back-right front-left front-right bottom =
  (front-left ·r f') ∙h (hD ·l top)

rectangle-back-right-bottom-cube :
  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
  (f : A → B) (g : A → C) (h : B → D) (k : C → D)
  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
  (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
  (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
  (top : (h' ∘ f') ~ (k' ∘ g'))
  (back-left : (f ∘ hA) ~ (hB ∘ f'))
  (back-right : (g ∘ hA) ~ (hC ∘ g'))
  (front-left : (h ∘ hB) ~ (hD ∘ h'))
  (front-right : (k ∘ hC) ~ (hD ∘ k'))
  (bottom : (h ∘ f) ~ (k ∘ g)) →
  ((h ∘ f) ∘ hA) ~ ((k ∘ hC) ∘ g')
rectangle-back-right-bottom-cube
  f g h k f' g' h' k' hA hB hC hD
  top back-left back-right front-left front-right bottom =
  ( bottom ·r hA) ∙h (k ·l back-right)

{-
coherence-htpy-square-rectangle-top-fl-rectangle-br-bot-cube :
  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
  (f : A → B) (g : A → C) (h : B → D) (k : C → D)
  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
  (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
  (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
  (top : (h' ∘ f') ~ (k' ∘ g'))
  (back-left : (f ∘ hA) ~ (hB ∘ f'))
  (back-right : (g ∘ hA) ~ (hC ∘ g'))
  (front-left : (h ∘ hB) ~ (hD ∘ h'))
  (front-right : (k ∘ hC) ~ (hD ∘ k'))
  (bottom : (h ∘ f) ~ (k ∘ g))
  (c : coherence-cube f g h k f' g' h' k' hA hB hC hD
    top back-left back-right front-left front-right bottom) →
  coherence-htpy-square
    ( htpy-inv front-right)
    ( htpy-refl' h)
    ( pair g' (pair (hB ∘ f')
      ( htpy-inv (rectangle-top-front-left-cube f g h k f' g' h' k' hA hB hC hD
        top back-left back-right front-left front-right bottom))))
    ( pair g' (pair (f ∘ hA)
      ( htpy-inv
        ( rectangle-back-right-bottom-cube f g h k f' g' h' k' hA hB hC hD
          top back-left back-right front-left front-right bottom))))
    ( htpy-refl' g')
    ( htpy-inv back-left)
coherence-htpy-square-rectangle-top-fl-rectangle-br-bot-cube = {!!}
-}

rectangle-top-front-right-cube :
  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
  (f : A → B) (g : A → C) (h : B → D) (k : C → D)
  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
  (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
  (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
  (top : (h' ∘ f') ~ (k' ∘ g'))
  (back-left : (f ∘ hA) ~ (hB ∘ f'))
  (back-right : (g ∘ hA) ~ (hC ∘ g'))
  (front-left : (h ∘ hB) ~ (hD ∘ h'))
  (front-right : (k ∘ hC) ~ (hD ∘ k'))
  (bottom : (h ∘ f) ~ (k ∘ g)) →
  ((hD ∘ h') ∘ f') ~ ((k ∘ hC) ∘ g')
rectangle-top-front-right-cube
  f g h k f' g' h' k' hA hB hC hD
  top back-left back-right front-left front-right bottom =
  (hD ·l top) ∙h (htpy-inv (front-right) ·r g')

rectangle-back-left-bottom-cube :
  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
  (f : A → B) (g : A → C) (h : B → D) (k : C → D)
  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
  (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
  (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
  (top : (h' ∘ f') ~ (k' ∘ g'))
  (back-left : (f ∘ hA) ~ (hB ∘ f'))
  (back-right : (g ∘ hA) ~ (hC ∘ g'))
  (front-left : (h ∘ hB) ~ (hD ∘ h'))
  (front-right : (k ∘ hC) ~ (hD ∘ k'))
  (bottom : (h ∘ f) ~ (k ∘ g))→
  ((h ∘ hB) ∘ f') ~ ((k ∘ g) ∘ hA)
rectangle-back-left-bottom-cube
  f g h k f' g' h' k' hA hB hC hD
  top back-left back-right front-left front-right bottom =
  (h ·l (htpy-inv back-left)) ∙h (bottom ·r hA)

is-pullback-back-left-is-pullback-back-right-cube :
  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
  {f : A → B} {g : A → C} {h : B → D} {k : C → D}
  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
  {f' : A' → B'} {g' : A' → C'} {h' : B' → D'} {k' : C' → D'}
  {hA : A' → A} {hB : B' → B} {hC : C' → C} {hD : D' → D}
  (top : (h' ∘ f') ~ (k' ∘ g'))
  (back-left : (f ∘ hA) ~ (hB ∘ f'))
  (back-right : (g ∘ hA) ~ (hC ∘ g'))
  (front-left : (h ∘ hB) ~ (hD ∘ h'))
  (front-right : (k ∘ hC) ~ (hD ∘ k'))
  (bottom : (h ∘ f) ~ (k ∘ g)) →
  (c : coherence-cube f g h k f' g' h' k' hA hB hC hD
    top back-left back-right front-left front-right bottom) →
  is-pullback h hD (pair hB (pair h' front-left)) →
  is-pullback k hD (pair hC (pair k' front-right)) →
  is-pullback g hC (pair hA (pair g' back-right)) →
  is-pullback f hB (pair hA (pair f' back-left))
is-pullback-back-left-is-pullback-back-right-cube
  {f = f} {g} {h} {k} {f' = f'} {g'} {h'} {k'} {hA = hA} {hB} {hC} {hD}
  top back-left back-right front-left front-right bottom c
  is-pb-front-left is-pb-front-right is-pb-back-right =
  is-pullback-left-square-is-pullback-rectangle f h hD
    ( pair hB (pair h' front-left))
    ( pair hA (pair f' back-left))
    ( is-pb-front-left)
    ( is-pullback-htpy
      { f = h ∘ f}
      ( k ∘ g)
      ( bottom)
      { g = hD}
      ( hD)
      ( htpy-refl)
      { c = pair hA (pair (h' ∘ f')
        ( rectangle-back-left-front-left-cube
          f g h k f' g' h' k' hA hB hC hD
          top back-left back-right front-left front-right bottom))}
      ( pair hA (pair (k' ∘ g')
        ( rectangle-back-right-front-right-cube
          f g h k f' g' h' k' hA hB hC hD
          top back-left back-right front-left front-right bottom)))
      ( pair
        ( htpy-refl)
        ( pair top
          ( coherence-htpy-square-rectangle-bl-fl-rectangle-br-fr-cube
            f g h k f' g' h' k' hA hB hC hD
            top back-left back-right front-left front-right bottom c)))
      ( is-pullback-rectangle-is-pullback-left-square g k hD
        ( pair hC (pair k' front-right))
        ( pair hA (pair g' back-right))
        ( is-pb-front-right)
        ( is-pb-back-right)))

is-pullback-back-right-is-pullback-back-left-cube :
  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
  {f : A → B} {g : A → C} {h : B → D} {k : C → D}
  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
  {f' : A' → B'} {g' : A' → C'} {h' : B' → D'} {k' : C' → D'}
  {hA : A' → A} {hB : B' → B} {hC : C' → C} {hD : D' → D}
  (top : (h' ∘ f') ~ (k' ∘ g'))
  (back-left : (f ∘ hA) ~ (hB ∘ f'))
  (back-right : (g ∘ hA) ~ (hC ∘ g'))
  (front-left : (h ∘ hB) ~ (hD ∘ h'))
  (front-right : (k ∘ hC) ~ (hD ∘ k'))
  (bottom : (h ∘ f) ~ (k ∘ g)) →
  (c : coherence-cube f g h k f' g' h' k' hA hB hC hD
    top back-left back-right front-left front-right bottom) →
  is-pullback h hD (pair hB (pair h' front-left)) →
  is-pullback k hD (pair hC (pair k' front-right)) →
  is-pullback f hB (pair hA (pair f' back-left)) →
  is-pullback g hC (pair hA (pair g' back-right))
is-pullback-back-right-is-pullback-back-left-cube
  {f = f} {g} {h} {k} {f' = f'} {g'} {h'} {k'} {hA = hA} {hB} {hC} {hD}
  top back-left back-right front-left front-right bottom c
  is-pb-front-left is-pb-front-right is-pb-back-left =
  is-pullback-left-square-is-pullback-rectangle g k hD
    ( pair hC (pair k' front-right))
    ( pair hA (pair g' back-right))
    ( is-pb-front-right)
    ( is-pullback-htpy'
      ( h ∘ f)
      { f' = k ∘ g}
      ( bottom)
      ( hD)
      { g' = hD}
      ( htpy-refl)
      ( pair hA (pair (h' ∘ f')
        ( rectangle-back-left-front-left-cube
          f g h k f' g' h' k' hA hB hC hD
          top back-left back-right front-left front-right bottom)))
      { c' = pair hA (pair (k' ∘ g')
        ( rectangle-back-right-front-right-cube
          f g h k f' g' h' k' hA hB hC hD
          top back-left back-right front-left front-right bottom))}
      ( pair
        ( htpy-refl)
        ( pair top
          ( coherence-htpy-square-rectangle-bl-fl-rectangle-br-fr-cube
            f g h k f' g' h' k' hA hB hC hD
            top back-left back-right front-left front-right bottom c)))
      ( is-pullback-rectangle-is-pullback-left-square f h hD
        ( pair hB (pair h' front-left))
        ( pair hA (pair f' back-left))
        ( is-pb-front-left)
        ( is-pb-back-left)))

descent-is-equiv :
  {l1 l2 l3 l4 l5 l6 : Level}
  {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} {Y : UU l5} {Z : UU l6}
  (i : X → Y) (j : Y → Z) (h : C → Z)
  (c : cone j h B) (d : cone i (pr1 c) A) →
  is-equiv i → is-equiv (pr1 (pr2 d)) →
  is-pullback (j ∘ i) h (cone-comp-horizontal i j h c d) →
  is-pullback j h c
descent-is-equiv i j h c d
  is-equiv-i is-equiv-k is-pb-rectangle =
  is-pullback-is-fiberwise-equiv-fib-square j h c
    ( ind-is-equiv
      ( λ y → is-equiv (fib-square j h c y))
      ( i)
      ( is-equiv-i)
      ( λ x → is-equiv-left-factor
        ( fib-square (j ∘ i) h
          ( cone-comp-horizontal i j h c d) x)
        ( fib-square j h c (i x))
        ( fib-square i (pr1 c) d x)
        ( fib-square-comp-horizontal i j h c d x)
        ( is-fiberwise-equiv-fib-square-is-pullback (j ∘ i) h
          ( cone-comp-horizontal i j h c d)
          ( is-pb-rectangle)
          ( x))
        ( is-fiberwise-equiv-fib-square-is-pullback i (pr1 c) d
          ( is-pullback-is-equiv' i (pr1 c) d is-equiv-i is-equiv-k) x)))

coherence-htpy-square-is-pullback-bottom-is-pullback-top-cube-is-equiv :
  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
  (f : A → B) (g : A → C) (h : B → D) (k : C → D)
  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
  (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
  (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
  (top : (h' ∘ f') ~ (k' ∘ g'))
  (back-left : (f ∘ hA) ~ (hB ∘ f'))
  (back-right : (g ∘ hA) ~ (hC ∘ g'))
  (front-left : (h ∘ hB) ~ (hD ∘ h'))
  (front-right : (k ∘ hC) ~ (hD ∘ k'))
  (bottom : (h ∘ f) ~ (k ∘ g)) →
  (c : coherence-cube f g h k f' g' h' k' hA hB hC hD
       top back-left back-right front-left front-right bottom) →
  coherence-htpy-square
    ( front-left)
    ( htpy-refl' k)
    ( pair f'
      ( pair
        ( g ∘ hA)
        ( rectangle-back-left-bottom-cube
          f g h k f' g' h' k' hA hB hC hD
          top back-left back-right front-left front-right bottom)))
    ( pair f'
      ( pair
        ( hC ∘ g')
        ( rectangle-top-front-right-cube
          f g h k f' g' h' k' hA hB hC hD
          top back-left back-right front-left front-right bottom)))
    ( htpy-refl' f')
    ( back-right)
coherence-htpy-square-is-pullback-bottom-is-pullback-top-cube-is-equiv
  f g h k f' g' h' k' hA hB hC hD
  top back-left back-right front-left front-right bottom c =
  ( htpy-inv
    ( htpy-inv
      ( htpy-assoc
        ( h ·l (htpy-inv back-left))
        ( bottom ·r hA)
        ( (k ·l back-right) ∙h (htpy-refl' (k ∘ (hC ∘ g'))))))) ∙h
  ( ( htpy-ap-concat'
      ( h ·l (htpy-inv back-left))
      ( htpy-inv (h ·l back-left))
      ( _)
      ( htpy-left-whisk-htpy-inv h back-left)) ∙h
      ( htpy-inv (htpy-inv-con (h ·l back-left) _ _
        ( ( ( htpy-inv (htpy-assoc (h ·l back-left) (front-left ·r f') _)) ∙h
            ( ( htpy-inv
                ( htpy-assoc
                  ( (h ·l back-left) ∙h (front-left ·r f'))
                  ( hD ·l top)
                  ( (htpy-inv front-right) ·r g'))) ∙h
              htpy-inv
              ( htpy-con-inv _ (front-right ·r g') _
                ( (htpy-assoc (bottom ·r hA) _ _) ∙h (htpy-inv (c)))))) ∙h
          ( htpy-inv
            ( htpy-ap-concat (bottom ·r hA) _ _ htpy-right-unit))))))

is-pullback-bottom-is-pullback-top-cube-is-equiv :
  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
  (f : A → B) (g : A → C) (h : B → D) (k : C → D)
  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
  (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
  (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
  (top : (h' ∘ f') ~ (k' ∘ g'))
  (back-left : (f ∘ hA) ~ (hB ∘ f'))
  (back-right : (g ∘ hA) ~ (hC ∘ g'))
  (front-left : (h ∘ hB) ~ (hD ∘ h'))
  (front-right : (k ∘ hC) ~ (hD ∘ k'))
  (bottom : (h ∘ f) ~ (k ∘ g)) →
  (c : coherence-cube f g h k f' g' h' k' hA hB hC hD
       top back-left back-right front-left front-right bottom) →
  is-equiv hA → is-equiv hB → is-equiv hC → is-equiv hD →
  is-pullback h' k' (pair f' (pair g' top)) →
  is-pullback h k (pair f (pair g bottom))
is-pullback-bottom-is-pullback-top-cube-is-equiv
  f g h k f' g' h' k' hA hB hC hD
  top back-left back-right front-left front-right bottom c
  is-equiv-hA is-equiv-hB is-equiv-hC is-equiv-hD is-pb-top =
  descent-is-equiv hB h k
    ( pair f (pair g bottom))
    ( pair f' (pair hA (htpy-inv (back-left))))
    ( is-equiv-hB)
    ( is-equiv-hA)
    ( is-pullback-htpy
      {f = h ∘ hB}
      ( hD ∘ h')
      ( front-left)
      {g = k}
      ( k)
      ( htpy-refl' k)
      { c = pair f'
        ( pair
          ( g ∘ hA)
          ( rectangle-back-left-bottom-cube
            f g h k f' g' h' k' hA hB hC hD
            top back-left back-right front-left front-right bottom))}
       ( pair
        ( f')
        ( pair
          ( hC ∘ g')
          ( rectangle-top-front-right-cube
            f g h k f' g' h' k' hA hB hC hD
            top back-left back-right front-left front-right bottom)))
      ( pair
        ( htpy-refl' f')
        ( pair
          ( back-right)
          ( coherence-htpy-square-is-pullback-bottom-is-pullback-top-cube-is-equiv
            f g h k f' g' h' k' hA hB hC hD
            top back-left back-right front-left front-right bottom c)))
      ( is-pullback-rectangle-is-pullback-left-square
        ( h')
        ( hD)
        ( k)
        ( pair k' (pair hC (htpy-inv front-right)))
        ( pair f' (pair g' top))
        ( is-pullback-is-equiv' hD k
          ( pair k' (pair hC (htpy-inv front-right)))
          ( is-equiv-hD)
          ( is-equiv-hC))
        ( is-pb-top)))

is-pullback-top-is-pullback-bottom-cube-is-equiv :
  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
  (f : A → B) (g : A → C) (h : B → D) (k : C → D)
  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
  (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
  (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
  (top : (h' ∘ f') ~ (k' ∘ g'))
  (back-left : (f ∘ hA) ~ (hB ∘ f'))
  (back-right : (g ∘ hA) ~ (hC ∘ g'))
  (front-left : (h ∘ hB) ~ (hD ∘ h'))
  (front-right : (k ∘ hC) ~ (hD ∘ k'))
  (bottom : (h ∘ f) ~ (k ∘ g)) →
  (c : coherence-cube f g h k f' g' h' k' hA hB hC hD
       top back-left back-right front-left front-right bottom) →
  is-equiv hA → is-equiv hB → is-equiv hC → is-equiv hD →
  is-pullback h k (pair f (pair g bottom)) →
  is-pullback h' k' (pair f' (pair g' top))
is-pullback-top-is-pullback-bottom-cube-is-equiv
  f g h k f' g' h' k' hA hB hC hD
  top back-left back-right front-left front-right bottom c
  is-equiv-hA is-equiv-hB is-equiv-hC is-equiv-hD is-pb-bottom =
  is-pullback-top-is-pullback-rectangle h hD k'
    ( pair hB (pair h' front-left))
    ( pair f' (pair g' top))
    ( is-pullback-is-equiv h hD
      ( pair hB (pair h' front-left))
      is-equiv-hD is-equiv-hB)
    ( is-pullback-htpy' h htpy-refl (k ∘ hC) front-right
      ( cone-comp-vertical h k hC
        ( pair f (pair g bottom))
        ( pair hA (pair g' back-right)))
      { c' = cone-comp-vertical h hD k'
        ( pair hB (pair h' front-left))
        ( pair f' (pair g' top))}
      ( pair back-left
        ( pair
          ( htpy-refl)
          ( ( ( ( htpy-assoc
                    ( bottom ·r hA) (k ·l back-right) (front-right ·r g')) ∙h
                ( htpy-inv c)) ∙h
              ( htpy-assoc
                  ( h ·l back-left) (front-left ·r f') (hD ·l top))) ∙h
            ( htpy-ap-concat'
              ( h ·l back-left)
              ( (h ·l back-left) ∙h htpy-refl)
              ( (front-left ·r f') ∙h (hD ·l top))
              ( htpy-inv htpy-right-unit)))))
      ( is-pullback-rectangle-is-pullback-top h k hC
        ( pair f (pair g bottom))
        ( pair hA (pair g' back-right))
        ( is-pb-bottom)
        ( is-pullback-is-equiv g hC
          ( pair hA (pair g' back-right))
          is-equiv-hC is-equiv-hA)))

is-pullback-front-left-is-pullback-back-right-cube-is-equiv :
  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
  (f : A → B) (g : A → C) (h : B → D) (k : C → D)
  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
  (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
  (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
  (top : (h' ∘ f') ~ (k' ∘ g'))
  (back-left : (f ∘ hA) ~ (hB ∘ f'))
  (back-right : (g ∘ hA) ~ (hC ∘ g'))
  (front-left : (h ∘ hB) ~ (hD ∘ h'))
  (front-right : (k ∘ hC) ~ (hD ∘ k'))
  (bottom : (h ∘ f) ~ (k ∘ g)) →
  (c : coherence-cube f g h k f' g' h' k' hA hB hC hD
       top back-left back-right front-left front-right bottom) →
  is-equiv f' → is-equiv f → is-equiv k' → is-equiv k →
  is-pullback g hC (pair hA (pair g' back-right)) →
  is-pullback h hD (pair hB (pair h' front-left))
is-pullback-front-left-is-pullback-back-right-cube-is-equiv
  f g h k f' g' h' k' hA hB hC hD
  top back-left back-right front-left front-right bottom c
  is-equiv-f' is-equiv-f is-equiv-k' is-equiv-k is-pb-back-right =
  is-pullback-bottom-is-pullback-top-cube-is-equiv
    hB h' h hD hA g' g hC f' f k' k
    back-right (htpy-inv back-left) top bottom (htpy-inv front-right) front-left
    ( coherence-cube-mirror-B f g h k f' g' h' k' hA hB hC hD top
      back-left back-right front-left front-right bottom c)
    is-equiv-f' is-equiv-f is-equiv-k' is-equiv-k is-pb-back-right

is-pullback-front-right-is-pullback-back-left-cube-is-equiv :
  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
  (f : A → B) (g : A → C) (h : B → D) (k : C → D)
  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
  (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
  (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
  (top : (h' ∘ f') ~ (k' ∘ g'))
  (back-left : (f ∘ hA) ~ (hB ∘ f'))
  (back-right : (g ∘ hA) ~ (hC ∘ g'))
  (front-left : (h ∘ hB) ~ (hD ∘ h'))
  (front-right : (k ∘ hC) ~ (hD ∘ k'))
  (bottom : (h ∘ f) ~ (k ∘ g)) →
  (c : coherence-cube f g h k f' g' h' k' hA hB hC hD
       top back-left back-right front-left front-right bottom) →
  is-equiv g' → is-equiv h' → is-equiv g → is-equiv h →
  is-pullback f hB (pair hA (pair f' back-left)) →
  is-pullback k hD (pair hC (pair k' front-right))
is-pullback-front-right-is-pullback-back-left-cube-is-equiv
  f g h k f' g' h' k' hA hB hC hD
  top back-left back-right front-left front-right bottom c
  is-equiv-g' is-equiv-h' is-equiv-g is-equiv-h is-pb-back-left =
  is-pullback-bottom-is-pullback-top-cube-is-equiv
    hC k' k hD hA f' f hB g' g h' h
    back-left (htpy-inv back-right) (htpy-inv top)
    ( htpy-inv bottom) (htpy-inv front-left) front-right
    ( coherence-cube-rotate-120 f g h k f' g' h' k' hA hB hC hD
      top back-left back-right front-left front-right bottom c)
    is-equiv-g' is-equiv-g is-equiv-h' is-equiv-h is-pb-back-left

-- Section 15.2 Fiberwise pullbacks.

{- We show that if we have a square of families, such that the base square is
   a pullback square, then each square of fibers is a pullback square if and
   only if the square of total spaces is a pullback square. -}

cone-family :
  {l1 l2 l3 l4 l5 l6 l7 l8 : Level}
  {X : UU l1} {A : UU l2} {B : UU l3} {C : UU l4}
  (PX : X → UU l5) {PA : A → UU l6} {PB : B → UU l7}
  {f : A → X} {g : B → X} →
  (f' : (a : A) → PA a → PX (f a)) (g' : (b : B) → PB b → PX (g b)) →
  cone f g C → (C → UU l8) → UU (l4 ⊔ (l5 ⊔ (l6 ⊔ (l7 ⊔ l8))))
cone-family {C = C} PX f' g' c PC =
  (x : C) →
  cone ((tr PX (pr2 (pr2 c) x)) ∘ (f' (pr1 c x))) (g' (pr1 (pr2 c) x)) (PC x)

htpy-toto :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {P : A → UU l3} (Q : B → UU l4)
  {f f' : A → B} (H : f ~ f') (g : (x : A) → P x → Q (f x)) {g' : (x : A) → P x → Q (f' x)} (K : (x : A) → ((tr Q (H x)) ∘ (g x)) ~ (g' x)) →
  (toto Q f g) ~ (toto Q f' g')
htpy-toto Q H g K t = eq-pair (H (pr1 t)) (K (pr1 t) (pr2 t))

tot-cone-cone-family :
  {l1 l2 l3 l4 l5 l6 l7 l8 : Level}
  {X : UU l1} {A : UU l2} {B : UU l3} {C : UU l4}
  (PX : X → UU l5) {PA : A → UU l6} {PB : B → UU l7} {PC : C → UU l8}
  {f : A → X} {g : B → X} →
  (f' : (a : A) → PA a → PX (f a)) (g' : (b : B) → PB b → PX (g b)) →
  (c : cone f g C) → cone-family PX f' g' c PC →
  cone (toto PX f f') (toto PX g g') (Σ C PC)
tot-cone-cone-family PX f' g' c c' =
  pair
    ( toto _ (pr1 c) (λ x → pr1 (c' x)))
    ( pair
      ( toto _ (pr1 (pr2 c)) (λ x → (pr1 (pr2 (c' x)))))
      ( htpy-toto PX
        ( pr2 (pr2 c))
        ( λ z → (f' (pr1 c z)) ∘ (pr1 (c' z)))
        ( λ z → pr2 (pr2 (c' z)))))

map-canpb-tot-cone-cone-fam-right-factor :
  {l1 l2 l3 l4 l5 l6 l7 l8 : Level}
  {X : UU l1} {A : UU l2} {B : UU l3} {C : UU l4}
  (PX : X → UU l5) {PA : A → UU l6} {PB : B → UU l7} {PC : C → UU l8}
  {f : A → X} {g : B → X} →
  (f' : (a : A) → PA a → PX (f a)) (g' : (b : B) → PB b → PX (g b)) →
  (c : cone f g C) (c' : cone-family PX f' g' c PC) →
  Σ ( canonical-pullback f g)
    ( λ t → canonical-pullback ((tr PX (π₃ t)) ∘ (f' (π₁ t))) (g' (π₂ t))) →
  Σ ( Σ A PA)
    ( λ aa' → Σ (Σ B (λ b → Id (f (pr1 aa')) (g b)))
      ( λ bα → Σ (PB (pr1 bα))
        ( λ b' → Id
          ( tr PX (pr2 bα) (f' (pr1 aa') (pr2 aa')))
          ( g' (pr1 bα) b'))))
map-canpb-tot-cone-cone-fam-right-factor
  {X = X} {A} {B} {C} PX {PA} {PB} {PC} {f} {g} f' g' c c' =
  swap-total-Eq-structure
    ( λ a → Σ B (λ b → Id (f a) (g b)))
    ( PA)
    ( λ a bα a' → Σ (PB (pr1 bα))
      ( λ b' → Id (tr PX (pr2 bα) (f' a a')) (g' (pr1 bα) b')))

map-canpb-tot-cone-cone-fam-left-factor :
  {l1 l2 l3 l4 l5 l6 l7 l8 : Level}
  {X : UU l1} {A : UU l2} {B : UU l3} {C : UU l4}
  (PX : X → UU l5) {PA : A → UU l6} {PB : B → UU l7} {PC : C → UU l8}
  {f : A → X} {g : B → X} →
  (f' : (a : A) → PA a → PX (f a)) (g' : (b : B) → PB b → PX (g b)) →
  (c : cone f g C) (c' : cone-family PX f' g' c PC) → (aa' : Σ A PA) →
  Σ (Σ B (λ b → Id (f (pr1 aa')) (g b)))
    ( λ bα → Σ (PB (pr1 bα))
      ( λ b' → Id
        ( tr PX (pr2 bα) (f' (pr1 aa') (pr2 aa')))
        ( g' (pr1 bα) b'))) →
  Σ ( Σ B PB)
    ( λ bb' → Σ (Id (f (pr1 aa')) (g (pr1 bb')))
      ( λ α → Id (tr PX α (f' (pr1 aa') (pr2 aa'))) (g' (pr1 bb') (pr2 bb'))))
map-canpb-tot-cone-cone-fam-left-factor
  {X = X} {A} {B} {C} PX {PA} {PB} {PC} {f} {g} f' g' c c' aa' =
  ( swap-total-Eq-structure
    ( λ b → Id (f (pr1 aa')) (g b))
      ( PB)
      ( λ b α b' → Id (tr PX α (f' (pr1 aa') (pr2 aa'))) (g' b b')))

map-canonical-pullback-tot-cone-cone-family :
  {l1 l2 l3 l4 l5 l6 l7 l8 : Level}
  {X : UU l1} {A : UU l2} {B : UU l3} {C : UU l4}
  (PX : X → UU l5) {PA : A → UU l6} {PB : B → UU l7} {PC : C → UU l8}
  {f : A → X} {g : B → X} →
  (f' : (a : A) → PA a → PX (f a)) (g' : (b : B) → PB b → PX (g b)) →
  (c : cone f g C) (c' : cone-family PX f' g' c PC) →
  Σ ( canonical-pullback f g)
    ( λ t → canonical-pullback ((tr PX (π₃ t)) ∘ (f' (π₁ t))) (g' (π₂ t))) →
  canonical-pullback (toto PX f f') (toto PX g g')
map-canonical-pullback-tot-cone-cone-family
  {X = X} {A} {B} {C} PX {PA} {PB} {PC} {f} {g} f' g' c c' =
  ( tot (λ aa' →
    ( tot (λ bb' → eq-pair')) ∘
    ( map-canpb-tot-cone-cone-fam-left-factor PX f' g' c c' aa'))) ∘
  ( map-canpb-tot-cone-cone-fam-right-factor PX f' g' c c')

is-equiv-map-canonical-pullback-tot-cone-cone-family :
  {l1 l2 l3 l4 l5 l6 l7 l8 : Level}
  {X : UU l1} {A : UU l2} {B : UU l3} {C : UU l4}
  (PX : X → UU l5) {PA : A → UU l6} {PB : B → UU l7} {PC : C → UU l8}
  {f : A → X} {g : B → X} →
  (f' : (a : A) → PA a → PX (f a)) (g' : (b : B) → PB b → PX (g b)) →
  (c : cone f g C) (c' : cone-family PX f' g' c PC) →
  is-equiv (map-canonical-pullback-tot-cone-cone-family PX f' g' c c')
is-equiv-map-canonical-pullback-tot-cone-cone-family
  {X = X} {A} {B} {C} PX {PA} {PB} {PC} {f} {g} f' g' c c' =
  is-equiv-comp
    ( map-canonical-pullback-tot-cone-cone-family PX f' g' c c')
    ( tot (λ aa' →
      ( tot (λ bb' → eq-pair')) ∘
      ( map-canpb-tot-cone-cone-fam-left-factor PX f' g' c c' aa')))
    ( map-canpb-tot-cone-cone-fam-right-factor PX f' g' c c')
    ( htpy-refl)
    ( is-equiv-swap-total-Eq-structure
      ( λ a → Σ B (λ b → Id (f a) (g b)))
      ( PA)
      ( λ a bα a' → Σ (PB (pr1 bα))
        ( λ b' → Id (tr PX (pr2 bα) (f' a a')) (g' (pr1 bα) b'))))
    ( is-equiv-tot-is-fiberwise-equiv (λ aa' → is-equiv-comp
      ( ( tot (λ bb' → eq-pair')) ∘
        ( map-canpb-tot-cone-cone-fam-left-factor PX f' g' c c' aa'))
      ( tot (λ bb' → eq-pair'))
      ( map-canpb-tot-cone-cone-fam-left-factor PX f' g' c c' aa')
      ( htpy-refl)
      ( is-equiv-swap-total-Eq-structure _ _ _)
      ( is-equiv-tot-is-fiberwise-equiv (λ bb' → is-equiv-eq-pair
        ( pair (f (pr1 aa')) (f' (pr1 aa') (pr2 aa')))
        ( pair (g (pr1 bb')) (g' (pr1 bb') (pr2 bb')))))))

triangle-canonical-pullback-tot-cone-cone-family :
  {l1 l2 l3 l4 l5 l6 l7 l8 : Level}
  {X : UU l1} {A : UU l2} {B : UU l3} {C : UU l4}
  (PX : X → UU l5) {PA : A → UU l6} {PB : B → UU l7} {PC : C → UU l8}
  {f : A → X} {g : B → X} →
  (f' : (a : A) → PA a → PX (f a)) (g' : (b : B) → PB b → PX (g b)) →
  (c : cone f g C) (c' : cone-family PX f' g' c PC) →
  ( gap (toto PX f f') (toto PX g g') (tot-cone-cone-family PX f' g' c c')) ~
  ( ( map-canonical-pullback-tot-cone-cone-family PX f' g' c c') ∘
    ( toto _
      ( gap f g c)
      ( λ x → gap
        ( (tr PX (pr2 (pr2 c) x)) ∘ (f' (pr1 c x)))
        ( g' (pr1 (pr2 c) x))
        ( c' x))))
triangle-canonical-pullback-tot-cone-cone-family PX f' g' c c' (pair x y) =
  refl

is-pullback-family-is-pullback-tot :
  {l1 l2 l3 l4 l5 l6 l7 l8 : Level}
  {X : UU l1} {A : UU l2} {B : UU l3} {C : UU l4}
  (PX : X → UU l5) {PA : A → UU l6} {PB : B → UU l7} {PC : C → UU l8}
  {f : A → X} {g : B → X} →
  (f' : (a : A) → PA a → PX (f a)) (g' : (b : B) → PB b → PX (g b)) →
  (c : cone f g C) (c' : cone-family PX f' g' c PC) →
  is-pullback f g c →
  is-pullback
    (toto PX f f') (toto PX g g') (tot-cone-cone-family PX f' g' c c') →
  (x : C) →
  is-pullback
    ( (tr PX (pr2 (pr2 c) x)) ∘ (f' (pr1 c x)))
    ( g' (pr1 (pr2 c) x))
    ( c' x)
is-pullback-family-is-pullback-tot
  PX {PA} {PB} {PC} {f} {g} f' g' c c' is-pb-c is-pb-tot =
  is-fiberwise-equiv-is-equiv-toto-is-equiv-base-map _
    ( gap f g c)
    ( λ x → gap
      ( (tr PX (pr2 (pr2 c) x)) ∘ (f' (pr1 c x)))
      ( g' (pr1 (pr2 c) x))
      ( c' x))
    ( is-pb-c)
    ( is-equiv-right-factor
      ( gap (toto PX f f') (toto PX g g') (tot-cone-cone-family PX f' g' c c'))
      ( map-canonical-pullback-tot-cone-cone-family PX f' g' c c')
      ( toto _
        ( gap f g c)
        ( λ x → gap
          ( (tr PX (pr2 (pr2 c) x)) ∘ (f' (pr1 c x)))
          ( g' (pr1 (pr2 c) x))
          ( c' x)))
      ( triangle-canonical-pullback-tot-cone-cone-family PX f' g' c c')
      ( is-equiv-map-canonical-pullback-tot-cone-cone-family PX f' g' c c')
      ( is-pb-tot))

is-pullback-tot-is-pullback-family :
  {l1 l2 l3 l4 l5 l6 l7 l8 : Level}
  {X : UU l1} {A : UU l2} {B : UU l3} {C : UU l4}
  (PX : X → UU l5) {PA : A → UU l6} {PB : B → UU l7} {PC : C → UU l8}
  {f : A → X} {g : B → X} →
  (f' : (a : A) → PA a → PX (f a)) (g' : (b : B) → PB b → PX (g b)) →
  (c : cone f g C) (c' : cone-family PX f' g' c PC) →
  is-pullback f g c →
  ( (x : C) →
    is-pullback
      ( (tr PX (pr2 (pr2 c) x)) ∘ (f' (pr1 c x)))
      ( g' (pr1 (pr2 c) x))
      ( c' x)) →
  is-pullback
    (toto PX f f') (toto PX g g') (tot-cone-cone-family PX f' g' c c')
is-pullback-tot-is-pullback-family
  PX {PA} {PB} {PC} {f} {g} f' g' c c' is-pb-c is-pb-c' =
  is-equiv-comp
    ( gap (toto PX f f') (toto PX g g') (tot-cone-cone-family PX f' g' c c'))
    ( map-canonical-pullback-tot-cone-cone-family PX f' g' c c')
    ( toto _
      ( gap f g c)
      ( λ x → gap
        ( (tr PX (pr2 (pr2 c) x)) ∘ (f' (pr1 c x)))
        ( g' (pr1 (pr2 c) x))
        ( c' x)))
    ( triangle-canonical-pullback-tot-cone-cone-family PX f' g' c c')
    ( is-equiv-toto-is-fiberwise-equiv-is-equiv-base-map _
      ( gap f g c)
      ( λ x → gap
        ( (tr PX (pr2 (pr2 c) x)) ∘ (f' (pr1 c x)))
        ( g' (pr1 (pr2 c) x))
        ( c' x))
        ( is-pb-c)
        ( is-pb-c'))
    ( is-equiv-map-canonical-pullback-tot-cone-cone-family PX f' g' c c')

{- We show that identity types commute with pullbacks. -}

cone-ap :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
  (f : A → X) (g : B → X) (c : cone f g C) (c1 c2 : C) →
  let p = pr1 c
      q = pr1 (pr2 c)
      H = pr2 (pr2 c)
  in
  cone
    ( λ (α : Id (p c1) (p c2)) → (ap f α) ∙ (H c2))
    ( λ (β : Id (q c1) (q c2)) → (H c1) ∙ (ap g β))
    ( Id c1 c2)
cone-ap f g (pair p (pair q H)) c1 c2 =
  pair
    ( ap p)
    ( pair
      ( ap q)
      ( λ γ →
        ( ap (λ t → t ∙ (H c2)) (inv (ap-comp f p γ))) ∙
        ( ( inv (htpy-nat H γ)) ∙
          ( ap (λ t → (H c1) ∙ t) (ap-comp g q γ)))))

tr-id-right :
  {l1 : Level} {A : UU l1} {a b c : A} (q : Id b c) (p : Id a b) →
  Id (tr (λ y → Id a y) q p) (p ∙ q)
tr-id-right refl refl = refl

cone-ap' :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
  (f : A → X) (g : B → X) (c : cone f g C) (c1 c2 : C) →
  let p = pr1 c
      q = pr1 (pr2 c)
      H = pr2 (pr2 c)
  in
  cone
    ( λ (α : Id (p c1) (p c2)) → tr (λ t → Id (f (p c1)) t) (H c2) (ap f α))
    ( λ (β : Id (q c1) (q c2)) → (H c1) ∙ (ap g β))
    ( Id c1 c2)
cone-ap' f g (pair p (pair q H)) c1 c2 =
  pair
    ( ap p)
    ( pair
      ( ap q)
      ( λ γ →
        ( tr-id-right (H c2) (ap f (ap p γ))) ∙
        ( ( ap (λ t → t ∙ (H c2)) (inv (ap-comp f p γ))) ∙
          ( ( inv (htpy-nat H γ)) ∙
            ( ap (λ t → (H c1) ∙ t) (ap-comp g q γ))))))

is-pullback-cone-ap :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
  (f : A → X) (g : B → X) (c : cone f g C) → is-pullback f g c →
  (c1 c2 : C) →
  let p = pr1 c
      q = pr1 (pr2 c)
      H = pr2 (pr2 c)
  in
  is-pullback
    ( λ (α : Id (p c1) (p c2)) → (ap f α) ∙ (H c2))
    ( λ (β : Id (q c1) (q c2)) → (H c1) ∙ (ap g β))
    ( cone-ap f g c c1 c2)
is-pullback-cone-ap f g (pair p (pair q H)) is-pb-c c1 c2 =
  is-pullback-htpy'
    ( λ α → tr (λ x → Id (f (p c1)) x) (H c2) (ap f α))
    ( λ α → tr-id-right (H c2) (ap f α))
    ( λ β → (H c1) ∙ (ap g β))
    ( htpy-refl)
    ( cone-ap' f g (pair p (pair q H)) c1 c2)
    { c' = cone-ap f g (pair p (pair q H)) c1 c2}
    ( pair htpy-refl (pair htpy-refl htpy-right-unit))
    ( is-pullback-family-is-pullback-tot
      ( λ x → Id (f (p c1)) x)
      ( λ a → ap f {x = p c1} {y = a})
      ( λ b β → (H c1) ∙ (ap g β))
      ( pair p (pair q H))
      ( cone-ap' f g (pair p (pair q H)) c1)
      ( is-pb-c)
      ( is-pullback-is-equiv
        ( toto _ f (λ a α → ap f α))
        ( toto _ g (λ b β → (H c1) ∙ (ap g β)))
        ( tot-cone-cone-family
          ( Id (f (p c1)))
          ( λ a → ap f)
          ( λ b β → (H c1) ∙ (ap g β))
          ( pair p (pair q H))
          ( cone-ap' f g (pair p (pair q H)) c1))
        ( is-equiv-is-contr _
          ( is-contr-total-path (q c1))
          ( is-contr-total-path (f (p c1))))
        ( is-equiv-is-contr _
          ( is-contr-total-path c1)
          ( is-contr-total-path (p c1))))
      ( c2))

{- Next we show that for any commuting cube, if the bottom and top squares are
   pullback squares, then so is the square of fibers of the vertical maps in
   cube. -}

{-

square-fib-cube :
  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
  (f : A → B) (g : A → C) (h : B → D) (k : C → D)
  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
  (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
  (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
  (top : (h' ∘ f') ~ (k' ∘ g'))
  (back-left : (f ∘ hA) ~ (hB ∘ f'))
  (back-right : (g ∘ hA) ~ (hC ∘ g'))
  (front-left : (h ∘ hB) ~ (hD ∘ h'))
  (front-right : (k ∘ hC) ~ (hD ∘ k'))
  (bottom : (h ∘ f) ~ (k ∘ g)) →
  (c : coherence-cube f g h k f' g' h' k' hA hB hC hD
       top back-left back-right front-left front-right bottom) →
  (a : A) →
  ( ( tot (λ d' p → p ∙ (bottom a)) ∘
      ( fib-square h hD (pair hB (pair h' front-left)) (f a))) ∘
    ( fib-square f hB (pair hA (pair f' back-left)) a)) ~
  ( ( fib-square k hD (pair hC (pair k' front-right)) (g a)) ∘
    ( fib-square g hC (pair hA (pair g' back-right)) a))
square-fib-cube f g h k f' g' h' k' hA hB hC hD
  top back-left back-right front-left front-right bottom c
  .(hA a') (pair a' refl) =
  eq-pair
    ( pair
      ( top a')
      ( ( tr-id-left-subst
          ( top a')
          ( k (g (hA a')))
          ( ( ( inv (front-left (f' a'))) ∙
              ( ap h ((inv (back-left a')) ∙ refl))) ∙
            ( bottom (hA a')))) ∙
        ( ( ( assoc (inv (ap hD (top a'))) _ (bottom (hA a'))) ∙
            {!!}) ∙
          ( distributive-inv-concat (ap k (back-right a')) (front-right (g' a')) ∙
            ( ( ap
                ( concat (inv (front-right (g' a'))) ?)
                ( inv (ap-inv k (back-right a')))) ∙
              ( ap
                ( concat (inv (front-right (g' a'))) ?)
                ( ap (ap k) (inv right-unit))))))))
-}

max_stars_repo_name: tadejpetric/HoTT-Intro

max_issues_repo_name: tadejpetric/HoTT-Intro

max_forks_repo_name: tadejpetric/HoTT-Intro


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

open import LogicalFormulae
open import Setoids.Setoids
open import Functions.Definition
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Sets.FinSet.Definition
open import Groups.Definition
open import Groups.SymmetricGroups.Definition
open import Decidable.Sets
open import Boolean.Definition

module Groups.FreeGroup.Definition where

data FreeCompletion {a : _} (A : Set a) : Set a where
  ofLetter : A → FreeCompletion A
  ofInv : A → FreeCompletion A

freeCompletionMap : {a b : _} {A : Set a} {B : Set b} (f : A → B) (w : FreeCompletion A) → FreeCompletion B
freeCompletionMap f (ofLetter x) = ofLetter (f x)
freeCompletionMap f (ofInv x) = ofInv (f x)

freeInverse : {a : _} {A : Set a} (l : FreeCompletion A) → FreeCompletion A
freeInverse (ofLetter x) = ofInv x
freeInverse (ofInv x) = ofLetter x

ofLetterInjective : {a : _} {A : Set a} {x y : A} → (ofLetter x ≡ ofLetter y) → x ≡ y
ofLetterInjective refl = refl

ofInvInjective : {a : _} {A : Set a} {x y : A} → (ofInv x ≡ ofInv y) → x ≡ y
ofInvInjective refl = refl

ofLetterOfInv : {a : _} {A : Set a} {x y : A} → ofLetter x ≡ ofInv y → False
ofLetterOfInv ()

decidableFreeCompletion : {a : _} {A : Set a} → DecidableSet A → DecidableSet (FreeCompletion A)
decidableFreeCompletion {A = A} dec = pr
  where
    pr : (a b : FreeCompletion A) → (a ≡ b) || (a ≡ b → False)
    pr (ofLetter x) (ofLetter y) with dec x y
    ... | inl refl = inl refl
    ... | inr x!=y = inr λ p → x!=y (ofLetterInjective p)
    pr (ofLetter x) (ofInv y) = inr λ ()
    pr (ofInv x) (ofLetter y) = inr λ ()
    pr (ofInv x) (ofInv y) with dec x y
    ... | inl refl = inl refl
    ... | inr x!=y = inr λ p → x!=y (ofInvInjective p)

freeCompletionEqual : {a : _} {A : Set a} (dec : DecidableSet A) (x y : FreeCompletion A) → Bool
freeCompletionEqual dec x y with decidableFreeCompletion dec x y
freeCompletionEqual dec x y | inl x₁ = BoolTrue
freeCompletionEqual dec x y | inr x₁ = BoolFalse

freeCompletionEqualFalse : {a : _} {A : Set a} (dec : DecidableSet A) {x y : FreeCompletion A} → ((x ≡ y) → False) → (freeCompletionEqual dec x y) ≡ BoolFalse
freeCompletionEqualFalse dec {x = x} {y} x!=y with decidableFreeCompletion dec x y
freeCompletionEqualFalse dec {x} {y} x!=y | inl x=y = exFalso (x!=y x=y)
freeCompletionEqualFalse dec {x} {y} x!=y | inr _ = refl

freeCompletionEqualFalse' : {a : _} {A : Set a} (dec : DecidableSet A) {x y : FreeCompletion A} → .((freeCompletionEqual dec x y) ≡ BoolFalse) → (x ≡ y) → False
freeCompletionEqualFalse' dec {x} {y} pr with decidableFreeCompletion dec x y
freeCompletionEqualFalse' dec {x} {y} () | inl x₁
freeCompletionEqualFalse' dec {x} {y} pr | inr ans = ans

ext: agda


text:
{-# OPTIONS --without-K #-}
module PathStructure.Id.Tr {a b} {A : Set a} {B : Set b} where

open import Equivalence
open import PathOperations
open import Types

tr-split : {a a′ : A} {b b′ : B} (p : a ≡ a′) →
  tr (λ _ → B) p b ≡ b′ → b ≡ b′
tr-split {b = b} {b′ = b′} = J
  (λ _ _ p → tr (λ _ → B) p b ≡ b′ → b ≡ b′)
  (λ _ p → p) _ _

tr-merge : {a a′ : A} {b b′ : B} (p : a ≡ a′) →
  b ≡ b′ → tr (λ _ → B) p b ≡ b′
tr-merge {b = b} {b′ = b′} = J
  (λ _ _ p → b ≡ b′ → tr (λ _ → B) p b ≡ b′)
  (λ _ p → p) _ _

tr-eq : {a a′ : A} {b b′ : B} (p : a ≡ a′) →
  (tr (λ _ → B) p b ≡ b′) ≃ (b ≡ b′)
tr-eq p
  = tr-split p
  , (tr-merge p , λ q → J
      (λ _ _ p → tr-split p (tr-merge p q) ≡ q)
      (λ _ → refl) _ _ p)
  , (tr-merge p , λ q → J
      (λ _ _ p → (b b′ : B) (q : tr (λ _ → B) p b ≡ b′) →
        tr-merge p (tr-split p q) ≡ q)
      (λ _ _ _ _ → refl) _ _ p _ _ q)

-- In presence of univalence axiom, this statement
-- can also be proven from tr-eq.
tr-≡ : {a a′ : A} {b b′ : B} (p : a ≡ a′) →
  (tr (λ _ → B) p b ≡ b′) ≡ (b ≡ b′)
tr-≡ {b = b} {b′ = b′} = J
  (λ _ _ p → (tr (λ _ → B) p b ≡ b′) ≡ (b ≡ b′))
  (λ _ → refl) _ _

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.Ints.DiffInt.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Univalence

open import Cubical.HITs.Ints.DiffInt.Base
open import Cubical.Data.Nat
open import Cubical.Data.Sigma
open import Cubical.Data.Bool

open import Cubical.Relation.Binary.Base
open import Cubical.Relation.Nullary

open import Cubical.HITs.SetQuotients

open BinaryRelation

relIsEquiv : isEquivRel rel
relIsEquiv = equivRel {A = ℕ × ℕ} relIsRefl relIsSym relIsTrans
  where
    relIsRefl : isRefl rel
    relIsRefl (a0 , a1) = refl

    relIsSym : isSym rel
    relIsSym (a0 , a1) (b0 , b1) p = sym p

    relIsTrans : isTrans rel
    relIsTrans (a0 , a1) (b0 , b1) (c0 , c1) p0 p1 =
      inj-m+ {m = (b0 + b1)} ((b0 + b1) + (a0 + c1) ≡⟨ +-assoc (b0 + b1) a0 c1  ⟩
            ((b0 + b1) + a0) + c1 ≡[ i ]⟨ +-comm b0 b1 i + a0   + c1 ⟩
            ((b1 + b0) + a0) + c1 ≡[ i ]⟨ +-comm (b1 + b0) a0 i + c1 ⟩
            (a0 + (b1 + b0)) + c1 ≡[ i ]⟨ +-assoc a0 b1 b0 i    + c1 ⟩
            (a0 + b1) + b0 + c1 ≡⟨ sym (+-assoc (a0 + b1) b0 c1) ⟩
            (a0 + b1) + (b0 + c1) ≡⟨ cong (λ p → p . fst + p .snd) (transport ΣPath≡PathΣ (p0 , p1))⟩
            (b0 + a1) + (c0 + b1) ≡⟨ sym (+-assoc b0 a1 (c0 + b1))⟩
            b0 + (a1 + (c0 + b1)) ≡[ i ]⟨ b0 + (a1 + +-comm c0 b1 i) ⟩
            b0 + (a1 + (b1 + c0)) ≡[ i ]⟨ b0 + +-comm a1 (b1 + c0) i ⟩
            b0 + ((b1 + c0) + a1) ≡[ i ]⟨ b0 + +-assoc b1 c0 a1 (~ i) ⟩
            b0 + (b1 + (c0 + a1)) ≡⟨ +-assoc b0 b1 (c0 + a1)⟩
            (b0 + b1) + (c0 + a1) ∎ )

relIsProp : BinaryRelation.isPropValued rel
relIsProp a b x y = isSetℕ _ _ _ _

discreteℤ : Discrete ℤ
discreteℤ = discreteSetQuotients (discreteΣ discreteℕ λ _ → discreteℕ) relIsProp relIsEquiv (λ _ _ → discreteℕ _ _)

private
  _ : Dec→Bool (discreteℤ [ (3 , 5) ] [ (4 , 6) ]) ≡ true
  _ = refl

  _ : Dec→Bool (discreteℤ [ (3 , 5) ] [ (4 , 7) ]) ≡ false
  _ = refl

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
postulate FunctorOps : Set
module FunctorOps (ops : FunctorOps) where
  postulate map : Set

postulate IsFunctor : Set
module IsFunctor (fun : IsFunctor) where
  postulate ops : FunctorOps
  open FunctorOps ops public
  -- inside here `FunctorOps.map ops` gets printed as `map`

open IsFunctor

-- out here it should too
test : (F : IsFunctor) → FunctorOps.map (ops F)
test F = F

-- EXPECTED: IsFunctor !=< map F

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Issue208 where

record R : Set where
  foo : Set
  foo = {!!}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import HoTT
open import cohomology.Exactness
open import cohomology.Theory

module cohomology.Unit {i} (CT : CohomologyTheory i) where

open CohomologyTheory CT

module _ (n : ℤ) where

  private
    ⊙LU = ⊙Lift {j = i} ⊙Unit

  Cof-Unit-is-Unit : ⊙Cof (⊙idf ⊙LU) == ⊙LU
  Cof-Unit-is-Unit = ⊙ua (⊙≃-in {X = _ , cfbase} e idp)
    where
    e : Cofiber (idf (Lift {j = i} Unit)) ≃ Lift Unit
    e = equiv (λ _ → lift unit)
              (λ _ → cfbase)
              (λ _ → idp)
              (Cofiber-elim {f = idf _}
                 {P = λ c → cfbase == c}
                 idp
                 (λ _ → cfglue (lift unit))
                 (λ _ → ↓-cst=idf-in idp))

  C-Unit-is-contr : is-contr (CEl n ⊙LU)
  C-Unit-is-contr =
    (Cid n ⊙LU , λ x → lemma₂ x ∙ app= (ap GroupHom.f (CF-ident n)) x)
    where
    lemma₁ : (x : CEl n (⊙Cof (⊙idf _)))
      → Cid n ⊙LU == CF n (⊙cfcod' (⊙idf _)) x
    lemma₁ x = ! (itok (C-exact n (⊙idf _)) _ [ x , idp ])
               ∙ app= (ap GroupHom.f (CF-ident n))
                      (CF n (⊙cfcod' (⊙idf _)) x)

    lemma₂ : (x : CEl n ⊙LU) → Cid n ⊙LU == CF n (⊙idf _) x
    lemma₂ = transport
      {A = Σ (Ptd i) (λ X → fst (⊙LU ⊙→ X))}
      (λ {(X , H) → (c : CEl n X) → Cid n ⊙LU == CF n H c})
      (pair= Cof-Unit-is-Unit
             (prop-has-all-paths-↓ (⊙→-level (Lift-level Unit-is-prop))))
      lemma₁

  C-Unit : C n ⊙LU == 0ᴳ
  C-Unit = contr-is-0ᴳ _ C-Unit-is-contr

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
module Numeral.Natural.Decidable where

open import Data
open import Data.Boolean
open import Functional
open import Lang.Inspect
open import Logic.Propositional
open import Numeral.Natural
open import Structure.Function
open import Structure.Function.Domain
open import Structure.Relator.Properties
open import Type.Properties.Decidable

module _ where
  open import Numeral.Natural.Oper.Comparisons
  open import Numeral.Natural.Oper.Proofs
  open import Relator.Equals
  open import Relator.Equals.Proofs.Equiv

  instance
    [≡?]-decider : Decider(2)(_≡_)(_≡?_)
    [≡?]-decider {𝟎}   {𝟎}   = true [≡]-intro
    [≡?]-decider {𝟎}   {𝐒 y} = false \()
    [≡?]-decider {𝐒 x} {𝟎}   = false \()
    [≡?]-decider {𝐒 x} {𝐒 y} with (x ≡? y) | [≡?]-decider {x} {y}
    ... | 𝑇 | true  xy  = true  (congruence₁(𝐒) xy)
    ... | 𝐹 | false nxy = false (nxy ∘ injective(𝐒))

  zero?-decider : Decider(1)(_≡ 𝟎)(zero?)
  zero?-decider {𝟎}   = true [≡]-intro
  zero?-decider {𝐒 x} = false \()

module _ where
  open import Numeral.Natural.Oper.Comparisons
  open import Numeral.Natural.Oper.Proofs
  open import Numeral.Natural.Oper.Divisibility
  open import Numeral.Natural.Oper.Modulo
  open import Numeral.Natural.Oper.Modulo.Proofs
  open import Numeral.Natural.Relation.Divisibility
  open import Numeral.Natural.Relation.Divisibility.Proofs
  open import Relator.Equals
  open import Relator.Equals.Proofs.Equiv

  instance
    [∣]-decider : Decider(2)(_∣_)(_∣₀?_)
    [∣]-decider {𝟎} {𝟎}   = true Div𝟎
    [∣]-decider {𝟎} {𝐒 y} = false [0]-divides-not
    [∣]-decider {𝐒 x} {y} with y mod 𝐒(x) | inspect(\x → y mod 𝐒(x)) x
    ... | 𝟎   | intro eq = true  ([↔]-to-[→] mod-divisibility eq)
    ... | 𝐒 _ | intro eq = false ([𝐒]-not-0 ∘ transitivity(_≡_) (symmetry(_≡_) eq) ∘ [↔]-to-[←] mod-divisibility)

module _ where
  open import Data.Boolean.Stmt
  open import Data.Boolean.Stmt.Proofs
  open import Data.List
  open import Data.List.Decidable as List
  open import Data.List.Equiv.Id
  open import Lang.Inspect
  open import Logic.Classical
  open import Logic.Predicate
  open import Numeral.Natural.LinearSearch
  open import Numeral.Natural.Oper.Divisibility
  open import Numeral.Natural.Prime
  open import Numeral.Natural.Prime.Proofs
  open import Numeral.Natural.Relation.Divisibility
  open import Numeral.Natural.Relation.Divisibility.Proofs
  open import Numeral.Natural.Relation.Order
  open import Numeral.Natural.Relation.Order.Classical
  open import Numeral.Natural.Relation.Order.Proofs
  open import Relator.Equals
  open import Relator.Equals.Proofs.Equiv
  open import Type.Properties.Decidable.Proofs
  open import Syntax.Implication.Dependent
  open import Syntax.Implication using (•_•_⇒₂-[_]_)

  -- A naive primality test using bruteforce.
  -- It checks if there are any divisors between 2 and p.
  -- Note: The performance and space should be terrible on this implementation because it checks whether the list of all divisors is empty.
  prime? : ℕ → Bool
  prime? 0          = 𝐹
  prime? 1          = 𝐹
  prime? n@(𝐒(𝐒 _)) = decide(2)(_≡_) ⦃ [∃]-intro _ ⦃ List.[≡]-decider ⦃ dec = [≡?]-decider ⦄ ⦄ ⦄ (findBoundedAll 2 n (_∣₀? n)) ∅

  instance
    Prime-decider : Decider(1)(Prime)(prime?)
    Prime-decider {𝟎} = false \()
    Prime-decider {𝐒 𝟎} = false \()
    Prime-decider {n@(𝐒(𝐒 x))} with prime? n | inspect prime? n
    ... | 𝑇 | intro eq = true $
      eq ⇒
      (prime? n ≡ 𝑇)                                     ⇒-[ [↔]-to-[←] IsTrue.is-𝑇 ]
      IsTrue(prime? n)                                   ⇒-[ [↔]-to-[←] (decider-true ⦃ List.[≡]-decider ⦃ dec = [≡?]-decider ⦄ ⦄) ]
      findBoundedAll 2 n (_∣₀? n) ≡ ∅                    ⇒-[ (\empty {_} → [↔]-to-[←] (findBoundedAll-emptyness{f = _∣₀? n}) empty) ]
      (∀{d} → (2 ≤ d) → (d < n) → IsFalse(d ∣₀? n))      ⇒-[ (\p {i} → [↔]-to-[←] (decider-false ⦃ [∣]-decider ⦄) ∘₂ p) ]
      (∀{d} → (2 ≤ d) → (d < n) → ¬(d ∣ n))              ⇒-[]
      (∀{d} → (2 ≤ d) → (d < 𝐒(𝐒(x))) → ¬(d ∣ 𝐒(𝐒(x))))  ⇒-[ (\p {d} div 2d dx → p{d} 2d (succ dx) div) ]
      (∀{d} → (d ∣ 𝐒(𝐒(x))) → (2 ≤ d) → ¬(d ≤ 𝐒(x)))     ⇒-[ (\p {d} div → [¬→]-disjunctive-formᵣ ⦃ decider-to-classical ⦃ [≡?]-decider ⦄ ⦄ \ nd0 → antisymmetry(_≤_)(_≡_) ([≤]-without-[𝐒] (divides-upper-limit div)) (sub₂(_≯_)(_≤_) (p{𝐒 d} div (succ ([≢]-to-[<]-of-0ᵣ nd0))))) ]
      (∀{d} → (𝐒(d) ∣ 𝐒(𝐒(x))) → ((d ≡ 0) ∨ (d ≡ 𝐒(x)))) ⇒-[ intro ]
      Prime n                                            ⇒-end
    ... | 𝐹 | intro eq = false \p →
      • (
        p ⇒
        Prime(n)                                      ⇒-[ prime-only-divisors ]
        (∀{d} → (d ∣ n) → ((d ≡ 1) ∨ (d ≡ n)))        ⇒-[ (\p {d} 2d dn div → [∨]-elim (\{[≡]-intro → [≤][0]ᵣ-negation ([≤]-without-[𝐒] 2d)}) (\{[≡]-intro → irreflexivity(_<_) dn}) (p div)) ]
        (∀{d} → (2 ≤ d) → (d < n) → ¬(d ∣ n))         ⇒-[ ((\p {i} → [↔]-to-[→] (decider-false ⦃ [∣]-decider ⦄) ∘₂ p)) ]
        (∀{d} → (2 ≤ d) → (d < n) → IsFalse(d ∣₀? n)) ⇒-[ [↔]-to-[→] findBoundedAll-emptyness ]
        findBoundedAll 2 n (_∣₀? n) ≡ ∅               ⇒-[ [↔]-to-[→] (decider-true ⦃ List.[≡]-decider ⦃ dec = [≡?]-decider ⦄ ⦄) ]
        IsTrue(prime? n)                              ⇒-end
      )
      • (
        eq ⇒
        (prime? n ≡ 𝐹)                    ⇒-[ [↔]-to-[←] IsFalse.is-𝐹 ]
        IsFalse(prime? n)                 ⇒-end
      )
      ⇒₂-[ disjointness ]
      Empty ⇒-end

  import      Data.Either as Either
  open import Data.List.Relation.Membership using (_∈_)
  open import Data.List.Relation.Membership.Proofs
  open import Data.Tuple as Tuple using (_⨯_ ; _,_)
  open import Logic.Propositional.Theorems
  open import Numeral.Natural.Oper
  open import Numeral.Natural.Oper.Proofs
  open import Numeral.Natural.Proofs
  open import Numeral.Natural.Relation.Order.Existence using ([≤]-equivalence)
  open import Structure.Function.Domain
  open import Structure.Operator
  open import Structure.Operator.Properties
  open import Syntax.Transitivity

  prime-composite-not : ∀{n} → Prime(n) → Composite(n) → ⊥
  prime-composite-not {.(𝐒(𝐒(a)) ⋅ 𝐒(𝐒(b)))} p (intro a b) =
    Either.map1
      (\())
      ((\()) ∘ cancellationₗ(_+_) {x = a} ∘ injective(𝐒) ∘ injective(𝐒))
      (prime-only-divisors p {𝐒(𝐒(a))} (divides-with-[⋅] {c = 𝐒(𝐒(b))} ([∨]-introₗ divides-reflexivity)))

  -- Using Numeral.Natural.Decidable.prime?, when it is false, there is a divisor d between 2 and n for n. This means that (d ∣ n). Equivalently ∃(k ↦ d ⋅ k ≡ n). The proof of Composite uses these d and k.
  prime-or-composite : ∀{n} → Prime(𝐒(𝐒(n))) ∨ Composite(𝐒(𝐒(n)))
  prime-or-composite{n} = [¬→]-disjunctive-formᵣ ⦃ decider-to-classical ⦃ Prime-decider ⦄ ⦄ $
    ¬ Prime(𝐒(𝐒(n)))                                                                ⇒-[ [↔]-to-[→] (decider-false ⦃ Prime-decider ⦄) ]
    IsFalse(prime? (𝐒(𝐒(n))))                                                       ⇒-[ [↔]-to-[←] (decider-false ⦃ List.[≡]-decider ⦃ dec = [≡?]-decider ⦄ ⦄) ]
    findBoundedAll 2 (𝐒(𝐒(n))) (_∣₀? 𝐒(𝐒(n))) ≢ ∅                                   ⇒-[ non-empty-inclusion-existence ]
    ∃(_∈ findBoundedAll 2 (𝐒(𝐒(n))) (_∣₀? 𝐒(𝐒(n))))                                 ⇒-[ [∃]-map-proof ([↔]-to-[→] (findBoundedAll-membership {f = _∣₀? 𝐒(𝐒(n))})) ]
    ∃(d ↦ (2 ≤ d) ∧ (d < 𝐒(𝐒(n))) ∧ IsTrue(d ∣₀? 𝐒(𝐒(n))))                          ⇒-[ [∃]-map-proof ([∧]-map id ([↔]-to-[←] (decider-true ⦃ [∣]-decider ⦄))) ]
    ∃(d ↦ (2 ≤ d) ∧ (d < 𝐒(𝐒(n))) ∧ (d ∣ 𝐒(𝐒(n))))                                  ⇒-[ (\{([∃]-intro (𝐒 𝟎) ⦃ [∧]-intro ([∧]-intro (succ()) _) _ ⦄) ; ([∃]-intro (𝐒(𝐒 d)) ⦃ [∧]-intro ([∧]-intro d2 dn) div ⦄) → [∃]-intro d ⦃ [∧]-intro dn div ⦄}) ]
    ∃(d ↦ (𝐒(𝐒(d)) < 𝐒(𝐒(n))) ∧ (𝐒(𝐒(d)) ∣ 𝐒(𝐒(n))))                                ⇒-[ (\{([∃]-intro d ⦃ [∧]-intro dn div ⦄) → [∃]-intro d ⦃ [∧]-intro dn ([∃]-intro div ⦃ divides-quotient-correctness {yx = div} ⦄) ⦄}) ]
    ∃(d ↦ (𝐒(𝐒(d)) < 𝐒(𝐒(n))) ∧ ∃{Obj = 𝐒(𝐒(d)) ∣ 𝐒(𝐒(n))}(q ↦ (𝐒(𝐒(d)) ⋅ divides-quotient q ≡ 𝐒(𝐒(n))))) ⇒-[ (\{([∃]-intro d ⦃ [∧]-intro dn ([∃]-intro q ⦃ prod ⦄) ⦄) → [∃]-intro (d , [∃]-witness ([↔]-to-[←] [≤]-equivalence (divides-quotient-composite (succ (succ min)) dn {q}))) ⦃ congruence₂ᵣ(_⋅_)(𝐒(𝐒(d))) (([∃]-proof ([↔]-to-[←] [≤]-equivalence (divides-quotient-composite (succ (succ min)) dn {q})))) 🝖 prod ⦄}) ]
    ∃{Obj = ℕ ⨯ ℕ}(\(a , b) → (𝐒(𝐒(a)) ⋅ 𝐒(𝐒(b)) ≡ 𝐒(𝐒(n))))                        ⇒-[ [↔]-to-[←] composite-existence ]
    Composite(𝐒(𝐒 n))                                                               ⇒-end

  prime-xor-composite : ∀{n} → Prime(𝐒(𝐒(n))) ⊕ Composite(𝐒(𝐒(n)))
  prime-xor-composite {n} = [⊕]-or-not-both prime-or-composite (Tuple.uncurry prime-composite-not)

  open import Data.Tuple
  -- open import Numeral.Natural.Inductions
  {-# TERMINATING #-}
  -- TODO: Use strong induction. (a < n) because (a ⋅ b = n).
  prime-factor-existence : ∀{n} → ∃(PrimeFactor(𝐒(𝐒(n))))
  prime-factor-existence {n} with prime-or-composite{n}
  ... | Either.Left  p = [∃]-intro (𝐒(𝐒(n))) ⦃ intro ⦃ p ⦄ ⦄
  ... | Either.Right c
    with [∃]-intro(a , b) ⦃ p ⦄ ← [↔]-to-[→] composite-existence c
    with [∃]-intro d ⦃ pa ⦄ ← prime-factor-existence{a}
    = [∃]-intro d ⦃ divisor-primeFactors ([↔]-to-[→] divides-[⋅]-existence ([∃]-intro (𝐒 (𝐒 b)) ⦃ p ⦄)) pa ⦄

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
open import Level using (0ℓ)
open import Function using (_$_)

open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; sym; trans; cong; cong₂; isEquivalence; setoid; module ≡-Reasoning)
open import Relation.Binary.PropositionalEquality.WithK using (≡-irrelevant)
open import Relation.Nullary.Negation using (contradiction)
open ≡-Reasoning

open import Data.Unit using (⊤; tt)
open import Agda.Builtin.FromNat using (Number)

open import Data.Product using (_,_)

open import AKS.Primality using (IsPrime; Prime; bézout-prime)

module AKS.Modular.Quotient.Properties {P : Prime} where

open Prime P using () renaming (prime to p; isPrime to p-isPrime)
open IsPrime p-isPrime using (1<p)

open import AKS.Nat using (ℕ; zero; suc; _<_; _≤_; _∸_) renaming (_+_ to _+ℕ_; _*_ to _*ℕ_; _≟_ to _≟ℕ_)
open import AKS.Nat using (<⇒≤; [n∸m]+m≡n; suc-mono-≤; *-mono-≤; ≤-refl)
import AKS.Nat as Nat
import Data.Nat.Properties as Nat
open import AKS.Nat.Divisibility using (_%_; %-distribˡ-+; %-distribˡ-∸; %-distribˡ-*; m%n%n≡m%n; n<m⇒n%m≡n; n%m<m; n%n≡0; 0%m≡0; 1%m≡1; [m+kn]%n≡m%n)
open import AKS.Nat.GCD using (+ʳ; +ˡ)
open import AKS.Modular.Quotient.Base using (ℤ/[_]; ℤ✓; mod; mod<p; module Operations)
open Operations {P} using ([_]; _+_; _*_; -_; _⁻¹; _/_; _≟_; p≢0; ℤ/[]-irrelevance; n≢0⇒mod[n]≢0)

open import Algebra.Structures {A = ℤ/[ P ]} _≡_ using
  ( IsCommutativeRing; IsRing; IsAbelianGroup
  ; IsGroup; IsMonoid; IsSemigroup; IsMagma
  )
open import Algebra.Definitions {A = ℤ/[ P ]} _≡_ using
  ( _DistributesOver_; _DistributesOverʳ_; _DistributesOverˡ_
  ; RightIdentity; LeftIdentity; Identity; Associative; Commutative
  ; RightInverse; LeftInverse; Inverse
  )
open import AKS.Algebra.Structures (ℤ/[ P ]) _≡_ using (IsNonZeroCommutativeRing; IsIntegralDomain; IsGCDDomain; IsDecField)
open import Algebra.Bundles using (Ring; CommutativeRing)
open import AKS.Algebra.Bundles using (NonZeroCommutativeRing; DecField)

open import AKS.Unsafe using (≢-irrelevant)

+-isMagma : IsMagma _+_
+-isMagma = record
  { isEquivalence = isEquivalence
  ; ∙-cong = cong₂ _+_
  }

mod≡mod%p : ∀ (x : ℤ/[ P ]) → mod x ≡ (mod x % p) {p≢0}
mod≡mod%p (ℤ✓ x x<p) = sym (n<m⇒n%m≡n x<p)

mod≡mod%p%p : ∀ (x : ℤ/[ P ]) → mod x ≡ ((mod x % p) {p≢0} % p) {p≢0}
mod≡mod%p%p x = begin
  mod x         ≡⟨ mod≡mod%p x ⟩
  mod x % p     ≡⟨ sym (m%n%n≡m%n (mod x) p) ⟩
  mod x % p % p ∎

+-assoc : Associative _+_
+-assoc x y z = ℤ/[]-irrelevance $ begin
  ((mod x +ℕ mod y) % p +ℕ mod z) % p             ≡⟨ cong₂ (λ a b → (a +ℕ b) % p) (%-distribˡ-+ (mod x) (mod y) p {p≢0}) (mod≡mod%p z) ⟩
  ((mod x % p +ℕ mod y % p) % p +ℕ mod z % p) % p ≡⟨ sym (%-distribˡ-+ (mod x % p +ℕ mod y % p) (mod z) p) ⟩
  ((mod x % p +ℕ mod y % p) +ℕ mod z) % p         ≡⟨ cong (λ a → (a % p) {p≢0}) (Nat.+-assoc (mod x % p) (mod y % p) (mod z)) ⟩
  (mod x % p +ℕ (mod y % p +ℕ mod z)) % p         ≡⟨ %-distribˡ-+ (mod x % p) (mod y % p +ℕ mod z) p ⟩
  (mod x % p % p +ℕ (mod y % p +ℕ mod z) % p) % p ≡⟨ cong₂ (λ a b → (a +ℕ (b +ℕ mod z) % p) % p) (sym (mod≡mod%p%p x)) (sym (mod≡mod%p y)) ⟩
  (mod x +ℕ (mod y +ℕ mod z) % p) % p ∎

+-isSemigroup : IsSemigroup _+_
+-isSemigroup = record
  { isMagma = +-isMagma
  ; assoc = +-assoc
  }

+-comm : Commutative _+_
+-comm x y = ℤ/[]-irrelevance $ begin
  (mod x +ℕ mod y) % p ≡⟨ cong (λ a → (a % p) {p≢0}) (Nat.+-comm (mod x) (mod y)) ⟩
  (mod y +ℕ mod x) % p ∎

+-identityˡ : LeftIdentity 0 _+_
+-identityˡ x = ℤ/[]-irrelevance $ begin
  (0 % p +ℕ mod x) % p     ≡⟨ cong (λ a → (0 % p +ℕ a) % p) (mod≡mod%p x) ⟩
  (0 % p +ℕ mod x % p) % p ≡⟨ sym (%-distribˡ-+ 0 (mod x) p) ⟩
  (0 +ℕ mod x) % p         ≡⟨ sym (mod≡mod%p x) ⟩
  mod x                    ∎

open import Algebra.FunctionProperties.Consequences.Propositional using (comm+idˡ⇒idʳ; comm+invˡ⇒invʳ; comm+distrˡ⇒distrʳ)

+-identityʳ : RightIdentity 0 _+_
+-identityʳ = comm+idˡ⇒idʳ +-comm {0} +-identityˡ

+-identity : Identity 0 _+_
+-identity = +-identityˡ , +-identityʳ

+-isMonoid : IsMonoid _+_ 0
+-isMonoid = record
  { isSemigroup = +-isSemigroup
  ; identity = +-identity
  }

-‿inverseˡ : LeftInverse 0 -_ _+_
-‿inverseˡ (ℤ✓ zero x<p) = refl
-‿inverseˡ (ℤ✓ (suc x) x<p) = ℤ/[]-irrelevance $ begin
  ((p ∸ suc x) +ℕ suc x) % p ≡⟨ cong (λ a → (a % p) {p≢0}) ([n∸m]+m≡n (<⇒≤ x<p)) ⟩
  p % p ≡⟨ n%n≡0 p ⟩
  0     ≡⟨ sym (0%m≡0 p {p≢0}) ⟩
  0 % p ∎

-‿inverseʳ : RightInverse 0 -_ _+_
-‿inverseʳ = comm+invˡ⇒invʳ {_⁻¹ = -_} +-comm -‿inverseˡ

-‿inverse : Inverse 0 -_ _+_
-‿inverse = -‿inverseˡ , -‿inverseʳ

+-isGroup : IsGroup _+_ 0 -_
+-isGroup = record
  { isMonoid = +-isMonoid
  ; inverse = -‿inverse
  ; ⁻¹-cong = cong -_
  }

+-isAbelianGroup : IsAbelianGroup _+_ 0 -_
+-isAbelianGroup = record
  { isGroup = +-isGroup
  ; comm = +-comm
  }

*-isMagma : IsMagma _*_
*-isMagma = record
  { isEquivalence = isEquivalence
  ; ∙-cong = cong₂ _*_
  }

*-assoc : Associative _*_
*-assoc x y z = ℤ/[]-irrelevance $ begin
  ((mod x *ℕ mod y) % p *ℕ mod z) % p                   ≡⟨ cong₂ (λ a b → (a *ℕ b) % p) (%-distribˡ-* (mod x) (mod y) p {p≢0}) (mod≡mod%p z) ⟩
  (((mod x % p) *ℕ (mod y % p)) % p *ℕ (mod z % p)) % p ≡⟨ sym (%-distribˡ-* ((mod x % p) *ℕ (mod y % p)) (mod z) p) ⟩
  (((mod x % p) *ℕ (mod y % p)) *ℕ mod z) % p           ≡⟨ cong (λ a → (a % p) {p≢0}) (Nat.*-assoc (mod x % p) (mod y % p) (mod z)) ⟩
  ((mod x % p) *ℕ ((mod y % p) *ℕ mod z)) % p           ≡⟨ %-distribˡ-* (mod x % p) ((mod y % p) *ℕ mod z) p ⟩
  ((mod x % p % p) *ℕ (((mod y % p) *ℕ mod z) % p)) % p ≡⟨ cong₂ (λ a b → (a *ℕ ((b *ℕ mod z) % p)) % p) (sym (mod≡mod%p%p x)) (sym (mod≡mod%p y)) ⟩
  (mod x *ℕ ((mod y *ℕ mod z) % p)) % p ∎

*-isSemigroup : IsSemigroup _*_
*-isSemigroup = record
  { isMagma = *-isMagma
  ; assoc = *-assoc
  }

*-comm : Commutative _*_
*-comm x y = ℤ/[]-irrelevance $ begin
  (mod x *ℕ mod y) % p ≡⟨ cong (λ a → (a % p) {p≢0}) (Nat.*-comm (mod x) (mod y)) ⟩
  (mod y *ℕ mod x) % p ∎

*-identityˡ : LeftIdentity 1 _*_
*-identityˡ x = ℤ/[]-irrelevance $ begin
  (1 % p *ℕ mod x) % p ≡⟨ cong (λ a → ((a *ℕ mod x) % p) {p≢0}) (1%m≡1 1<p) ⟩
  (1 *ℕ mod x) % p     ≡⟨ cong (λ a → a % p) (Nat.*-identityˡ (mod x)) ⟩
  mod x % p            ≡⟨ sym (mod≡mod%p x) ⟩
  mod x                ∎

*-identityʳ : RightIdentity 1 _*_
*-identityʳ = comm+idˡ⇒idʳ *-comm {1} *-identityˡ

*-identity : Identity 1 _*_
*-identity = *-identityˡ , *-identityʳ

*-isMonoid : IsMonoid _*_ 1
*-isMonoid = record
  { isSemigroup = *-isSemigroup
  ; identity = *-identity
  }

*-distribˡ-+ : _*_ DistributesOverˡ _+_
*-distribˡ-+ r x y = ℤ/[]-irrelevance $ begin
  (mod r *ℕ ((mod x +ℕ mod y) % p)) % p              ≡⟨ cong (λ a → (a *ℕ ((mod x +ℕ mod y) % p)) % p) (mod≡mod%p r) ⟩
  (mod r % p *ℕ ((mod x +ℕ mod y) % p)) % p          ≡⟨ sym (%-distribˡ-* (mod r) (mod x +ℕ mod y) p) ⟩
  (mod r *ℕ (mod x +ℕ mod y)) % p                    ≡⟨ cong (λ a → (a % p) {p≢0}) (Nat.*-distribˡ-+ (mod r) (mod x) (mod y)) ⟩
  (mod r *ℕ mod x +ℕ mod r *ℕ mod y) % p             ≡⟨ %-distribˡ-+ (mod r *ℕ mod x) (mod r *ℕ mod y) p ⟩
  ((mod r *ℕ mod x) % p +ℕ (mod r *ℕ mod y) % p) % p ∎

*-distribʳ-+ : _*_ DistributesOverʳ _+_
*-distribʳ-+ = comm+distrˡ⇒distrʳ {_} {_} {_*_} {_+_} *-comm *-distribˡ-+

*-distrib-+ : _*_ DistributesOver _+_
*-distrib-+ = *-distribˡ-+ , *-distribʳ-+

+-*-isRing : IsRing _+_ _*_ -_ 0 1
+-*-isRing = record
  { +-isAbelianGroup = +-isAbelianGroup
  ; *-isMonoid = *-isMonoid
  ; distrib = *-distrib-+
  }

+-*-isCommutativeRing : IsCommutativeRing _+_ _*_ -_ 0 1
+-*-isCommutativeRing = record
  { isRing = +-*-isRing
  ; *-comm = *-comm
  }

open import Data.Empty using (⊥)

0≢1 : [ 0 ] ≢ [ 1 ]
0≢1 [0]≡[1] = false
  where
  0≡1 : zero ≡ 1
  0≡1 = begin
    0     ≡⟨ sym (0%m≡0 p {p≢0}) ⟩
    0 % p ≡⟨ cong mod [0]≡[1] ⟩
    1 % p ≡⟨ 1%m≡1 1<p ⟩
    1     ∎
  false : ⊥
  false with 0≡1
  ... | ()

+-*-isNonZeroCommutativeRing : IsNonZeroCommutativeRing _+_ _*_ -_ 0 1
+-*-isNonZeroCommutativeRing = record
  { isCommutativeRing = +-*-isCommutativeRing
  ; 0#≉1# = 0≢1
  }

+-*-nonZeroCommutativeRing : NonZeroCommutativeRing 0ℓ 0ℓ
+-*-nonZeroCommutativeRing = record { isNonZeroCommutativeRing = +-*-isNonZeroCommutativeRing }

⁻¹-inverse-lemma₁ : ∀ (n : ℤ/[ P ]) x y → 1 +ℕ x *ℕ mod n ≡ y *ℕ p → ((mod n *ℕ (p ∸ (x % p) {p≢0})) % p) {p≢0} ≡ (1 % p) {p≢0}
⁻¹-inverse-lemma₁ n x y 1+x*n≡y*p = begin
  (mod n *ℕ (p ∸ x % p)) % p                             ≡⟨ cong (λ t → (t % p) {p≢0}) (Nat.*-distribˡ-∸ (mod n) p (x % p)) ⟩
  ((1 +ℕ mod n *ℕ p) ∸ (1 +ℕ mod n *ℕ (x % p))) % p     ≡⟨ %-distribˡ-∸ (1 +ℕ mod n *ℕ p) (1 +ℕ mod n *ℕ (x % p)) p 1+n*x%p≤1+n*p ⟩
  ((1 +ℕ mod n *ℕ p) ∸ (1 +ℕ mod n *ℕ (x % p)) % p) % p ≡⟨ cong (λ t → ((1 +ℕ mod n *ℕ p) ∸ t) % p) lemma ⟩
  ((1 +ℕ mod n *ℕ p) ∸ 0) % p                           ≡⟨ [m+kn]%n≡m%n 1 (mod n) p ⟩
  1 % p                                                  ∎
  where
  lemma : ((1 +ℕ mod n *ℕ (x % p) {p≢0}) % p) {p≢0} ≡ 0
  lemma = begin
    (1 +ℕ mod n *ℕ (x % p)) % p                 ≡⟨ cong (λ t → ((1 +ℕ t *ℕ (x % p) {p≢0}) % p) {p≢0}) (mod≡mod%p n) ⟩
    (1 +ℕ (mod n % p) *ℕ (x % p)) % p           ≡⟨ %-distribˡ-+ 1 ((mod n % p) *ℕ (x % p)) p ⟩
    (1 % p +ℕ ((mod n % p) *ℕ (x % p)) % p) % p ≡⟨ cong (λ t → (1 % p +ℕ t) % p) (sym (%-distribˡ-* (mod n) x p)) ⟩
    (1 % p +ℕ (mod n *ℕ x) % p) % p             ≡⟨ sym (%-distribˡ-+ 1 (mod n *ℕ x) p) ⟩
    (1 +ℕ mod n *ℕ x) % p                       ≡⟨ cong (λ t → ((1 +ℕ t) % p) {p≢0}) (Nat.*-comm (mod n) x) ⟩
    (1 +ℕ x *ℕ mod n) % p                       ≡⟨ cong (λ t → (t % p) {p≢0}) 1+x*n≡y*p ⟩
    (y *ℕ p) % p                                ≡⟨ [m+kn]%n≡m%n 0 y p ⟩
    0 % p                                       ≡⟨ 0%m≡0 p ⟩
    0 ∎
  1+n*x%p≤1+n*p : 1 +ℕ mod n *ℕ (x % p) {p≢0} ≤ 1 +ℕ mod n *ℕ p
  1+n*x%p≤1+n*p = suc-mono-≤ (*-mono-≤ {mod n} ≤-refl (<⇒≤ (n%m<m x p)))

⁻¹-inverse-lemma₂ : ∀ (n : ℤ/[ P ]) x y → 1 +ℕ y *ℕ p ≡ x *ℕ mod n → ((mod n *ℕ (x % p) {p≢0}) % p) {p≢0} ≡ (1 % p) {p≢0}
⁻¹-inverse-lemma₂ n x y 1+y*p≡x*n = begin
  (mod n *ℕ (x % p)) % p       ≡⟨ cong (λ t → (t *ℕ (x % p)) % p) (mod≡mod%p n) ⟩
  ((mod n % p) *ℕ (x % p)) % p ≡⟨ sym (%-distribˡ-* (mod n) x p) ⟩
  (mod n *ℕ x) % p             ≡⟨ cong (λ t → (t % p) {p≢0}) (Nat.*-comm (mod n) x) ⟩
  (x *ℕ mod n) % p             ≡⟨ cong (λ t → (t % p) {p≢0}) (sym 1+y*p≡x*n) ⟩
  (1 +ℕ y *ℕ p) % p            ≡⟨ [m+kn]%n≡m%n 1 y p ⟩
  1 % p ∎

⁻¹-inverse : ∀ n {n≢0} → n * (n ⁻¹) {n≢0} ≡ 1
⁻¹-inverse n {n≢0} with bézout-prime (mod n) p (n≢0⇒mod[n]≢0 n≢0) (mod<p n) p-isPrime
... | +ʳ x y 1+x*n≡y*p = ℤ/[]-irrelevance (⁻¹-inverse-lemma₁ n x y 1+x*n≡y*p)
... | +ˡ x y 1+y*p≡x*n = ℤ/[]-irrelevance (⁻¹-inverse-lemma₂ n x y 1+y*p≡x*n)

/-inverse : ∀ x y {y≢0} → x ≡ y * (x / y) {y≢0}
/-inverse x y {y≢0} = begin
  x                      ≡⟨ sym (*-identityʳ x) ⟩
  x * 1                  ≡⟨ cong (λ a → x * a) (sym (⁻¹-inverse y {y≢0})) ⟩
  x * (y * (y ⁻¹) {y≢0}) ≡⟨ sym (*-assoc x y ((y ⁻¹) {y≢0})) ⟩
  (x * y) * (y ⁻¹) {y≢0} ≡⟨ cong (λ a → a * (y ⁻¹) {y≢0}) (*-comm x y) ⟩
  (y * x) * (y ⁻¹) {y≢0} ≡⟨ *-assoc y x ((y ⁻¹) {y≢0}) ⟩
  y * (x / y) {y≢0} ∎

open import AKS.Algebra.Consequences +-*-nonZeroCommutativeRing using (module Inverse⇒Field)

open Inverse⇒Field _≟_ ≡-irrelevant ≢-irrelevant _/_ /-inverse
  using (gcd)
  renaming (isField to +-*-/-isField; [field] to +-*-/-field) public

+-*-/-isDecField : IsDecField _≟_ _+_ _*_ -_ 0 1 _/_ gcd
+-*-/-isDecField = record { isField = +-*-/-isField }

+-*-/-decField : DecField 0ℓ 0ℓ
+-*-/-decField = record { isDecField = +-*-/-isDecField }

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


text:
-- {-# OPTIONS -v tc.term.exlam:100 -v extendedlambda:100 -v int2abs.reifyterm:100 #-}
-- Andreas, 2013-02-26
module Issue778 (Param : Set) where

open import Common.Prelude

works : Nat → Nat
works with zero
... | zero = λ { zero → zero; (suc x) → suc x }
... | suc _ = λ { x → x }

test : Nat → Nat
test = λ { zero → zero; (suc x) → aux x }
  where aux : Nat → Nat
        aux x with works x
        ... | zero  = zero
        ... | suc y = works y
-- There was a internal error in connection to extended lambda and
-- where blocks in parametrized modules.


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

open import Cubical.Core.Everything

open import Cubical.Functions.Embedding
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Transport

-- A helper module for deriving univalence for a higher inductive-recursive
-- universe.
--
--  U is the type of codes
--  El is the decoding
--  un is a higher constructor that requires paths between codes to exist
--    for equivalences of decodings
--  comp is intended to be the computational behavior of El on un, although
--    it seems that being a path is sufficient.
--
-- Given a universe defined as above, it's possible to show that the path
-- space of the code type is equivalent to the path space of the actual
-- decodings, which are themselves determined by equivalences.
--
-- The levels are left independent, but of course it will generally be
-- impossible to define this sort of universe unless ℓ' < ℓ, because El will
-- be too big to go in a constructor of U. The exception would be if U could
-- be defined independently of El, though it might be tricky to get the right
-- higher structure in such a case.
module Cubical.Foundations.Univalence.Universe {ℓ ℓ'}
    (U : Type ℓ)
    (El : U → Type ℓ')
    (un : ∀ s t → El s ≃ El t → s ≡ t)
    (comp : ∀{s t} (e : El s ≃ El t) → cong El (un s t e) ≡ ua e)
  where
private
  variable
    A : Type ℓ'

module UU-Lemmas where
  reg : transport (λ _ → A) ≡ idfun A
  reg {A} i z = transp (λ _ → A) i z

  nu : ∀ x y → x ≡ y → El x ≃ El y
  nu x y p = transportEquiv (cong El p)

  cong-un-te
    : ∀ x y (p : El x ≡ El y)
    → cong El (un x y (transportEquiv p)) ≡ p
  cong-un-te x y p
    = comp (transportEquiv p) ∙ uaTransportη p

  nu-un : ∀ x y (e : El x ≃ El y) → nu x y (un x y e) ≡ e
  nu-un x y e
    = equivEq {e = nu x y (un x y e)} {f = e} λ i z
        → (cong (λ p → transport p z) (comp e) ∙ uaβ e z) i

  El-un-equiv : ∀ x i → El (un x x (idEquiv _) i) ≃ El x
  El-un-equiv x i = λ where
      .fst → transp (λ j → p j) (i ∨ ~ i)
      .snd → transp (λ j → isEquiv (transp (λ k → p (j ∧ k)) (~ j ∨ i ∨ ~ i)))
                (i ∨ ~ i) (idIsEquiv T)
    where
    T = El (un x x (idEquiv _) i)
    p : T ≡ El x
    p j = (comp (idEquiv _) ∙ uaIdEquiv {A = El x}) j i

  un-refl : ∀ x → un x x (idEquiv (El x)) ≡ refl
  un-refl x i j
    = hcomp (λ k → λ where
          (i = i0) → un x x (idEquiv (El x)) j
          (i = i1) → un x x (idEquiv (El x)) (j ∨ k)
          (j = i0) → un x x (idEquiv (El x)) (~ i ∨ k)
          (j = i1) → x)
        (un (un x x (idEquiv (El x)) (~ i)) x (El-un-equiv x (~ i)) j)

  nu-refl : ∀ x → nu x x refl ≡ idEquiv (El x)
  nu-refl x = equivEq {e = nu x x refl} {f = idEquiv (El x)} reg

  un-nu : ∀ x y (p : x ≡ y) → un x y (nu x y p) ≡ p
  un-nu x y p
    = J (λ z q → un x z (nu x z q) ≡ q) (cong (un x x) (nu-refl x) ∙ un-refl x) p

open UU-Lemmas
open Iso

equivIso : ∀ s t → Iso (s ≡ t) (El s ≃ El t)
equivIso s t .fun = nu s t
equivIso s t .inv = un s t
equivIso s t .rightInv = nu-un s t
equivIso s t .leftInv = un-nu s t

pathIso : ∀ s t → Iso (s ≡ t) (El s ≡ El t)
pathIso s t .fun = cong El
pathIso s t .inv = un s t ∘ transportEquiv
pathIso s t .rightInv = cong-un-te s t
pathIso s t .leftInv = un-nu s t

minivalence : ∀{s t} → (s ≡ t) ≃ (El s ≃ El t)
minivalence {s} {t} = isoToEquiv (equivIso s t)

path-reflection : ∀{s t} → (s ≡ t) ≃ (El s ≡ El t)
path-reflection {s} {t} = isoToEquiv (pathIso s t)

isEmbeddingEl : isEmbedding El
isEmbeddingEl s t = snd path-reflection

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:
open import Agda.Builtin.FromNat
open import Data.Nat.Base  as ℕ using (ℕ; suc; zero; _>_; _≤?_)
open import Data.List.Base as L using (List; _∷_; []; _++_)
open import Relation.Nullary.Decidable using (True)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

module Data.Pos where

open import Data.Nat.FromNat public

data ℕ⁺ : Set where
  suc : ℕ → ℕ⁺

instance
  NumberPos : Number ℕ⁺
  NumberPos = record { Constraint = Pos; fromNat = fromℕ }
    where
      Pos : ℕ → Set
      Pos n = True (suc zero ≤? n)
      fromℕ : (n : ℕ) {{p : Pos n}} → ℕ⁺
      fromℕ zero {{()}}
      fromℕ (suc zero)    = suc zero
      fromℕ (suc (suc n)) = suc (suc n)

toℕ : ℕ⁺ → ℕ
toℕ (suc n) = suc n

_+_ : ℕ⁺ → ℕ⁺ → ℕ⁺
suc m + n = suc (m ℕ.+ toℕ n)

toℕ-+ : (m {n} : ℕ⁺) → toℕ m ℕ.+ toℕ n ≡ toℕ (m + n)
toℕ-+ (suc m) = P.refl

replicate⁺ : ∀ {a} {A : Set a} → ℕ⁺ → A → List A
replicate⁺ (suc n) x = x ∷ L.replicate n x

replicate⁺-++-commute : ∀ {a} {A : Set a} {x : A} (m n : ℕ⁺) →
  replicate⁺ m x ++ replicate⁺ n x ≡ replicate⁺ (m + n) x
replicate⁺-++-commute (suc m) (suc n)
  = P.cong (_ ∷_) (replicate-++-commute m (suc n))
  where
    replicate-++-commute : ∀ {a} {A : Set a} {x : A} (m n : ℕ) →
      L.replicate m x ++ L.replicate n x ≡ L.replicate (m ℕ.+ n) x
    replicate-++-commute  zero   n = P.refl
    replicate-++-commute (suc m) n = P.cong (_ ∷_) (replicate-++-commute m n)

max_stars_repo_name: wenkokke/nodcap

max_issues_repo_name: pepijnkokke/nodcap

max_forks_repo_name: pepijnkokke/nodcap


text:
-- Andreas, 2011-09-12
-- eta for records in unifier

-- {-# OPTIONS -v tc.lhs.unify:25 #-}

module Issue455 where

postulate
  A : Set
  a : A

record Fork : Set where
  constructor pair
  field fst : A
        snd : A
open Fork

data D : Fork -> Set where
  c : (x y : A) -> D (pair x y)

postulate p : Fork

f : D p -> Set
f (c .(fst p) .(snd p)) = A  -- should work!

{- Unifier gives up on:
f z = {!z!}
Cannot decide whether there should be a case for the constructor c,
since the unification gets stuck on unifying the inferred indices
[pair x y] with the expected indices [p]
-}

record ⊤ : Set where
  constructor tt

data E : ⊤ -> Set where
  e : E tt

postulate q : ⊤

g : E q -> Set
g e = ⊤


text:
open import Nat
open import Prelude
open import contexts
open import core

module canonical-value-forms where
  canonical-value-forms-b : ∀{Δ d} →
                            Δ , ∅ ⊢ d :: b →
                            d val →
                            d == c
  canonical-value-forms-b TAConst VConst = refl
  canonical-value-forms-b (TAVar x₁) ()
  canonical-value-forms-b (TAAp wt wt₁) ()
  canonical-value-forms-b (TAEHole x x₁) ()
  canonical-value-forms-b (TANEHole x wt x₁) ()
  canonical-value-forms-b (TACast wt x) ()
  canonical-value-forms-b (TAFailedCast wt x x₁ x₂) ()
  canonical-value-forms-b (TAFst wt) ()
  canonical-value-forms-b (TASnd wt) ()

  canonical-value-forms-arr : ∀{Δ d τ1 τ2} →
                              Δ , ∅ ⊢ d :: (τ1 ==> τ2) →
                              d val →
                              Σ[ x ∈ Nat ] Σ[ d' ∈ iexp ]
                                ((d == (·λ x [ τ1 ] d')) ×
                                 (Δ , ■ (x , τ1) ⊢ d' :: τ2))
  canonical-value-forms-arr (TAVar x₁) ()
  canonical-value-forms-arr (TALam _ wt) VLam = _ , _ , refl , wt
  canonical-value-forms-arr (TAAp wt wt₁) ()
  canonical-value-forms-arr (TAEHole x x₁) ()
  canonical-value-forms-arr (TANEHole x wt x₁) ()
  canonical-value-forms-arr (TACast wt x) ()
  canonical-value-forms-arr (TAFailedCast x x₁ x₂ x₃) ()
  canonical-value-forms-arr (TAFst wt) ()
  canonical-value-forms-arr (TASnd wt) ()

  canonical-value-forms-prod : ∀{Δ d τ1 τ2} →
                               Δ , ∅ ⊢ d :: (τ1 ⊗ τ2) →
                               d val →
                               Σ[ d1 ∈ iexp ] Σ[ d2 ∈ iexp ]
                                 ((d == ⟨ d1 , d2 ⟩ ) ×
                                  (Δ , ∅ ⊢ d1 :: τ1) ×
                                  (Δ , ∅ ⊢ d2 :: τ2))
  canonical-value-forms-prod (TAVar x₁) ()
  canonical-value-forms-prod (TAAp wt wt₁) ()
  canonical-value-forms-prod (TAEHole x x₁) ()
  canonical-value-forms-prod (TANEHole x wt x₁) ()
  canonical-value-forms-prod (TACast wt x) ()
  canonical-value-forms-prod (TAFailedCast wt x x₁ x₂) ()
  canonical-value-forms-prod (TAFst wt) ()
  canonical-value-forms-prod (TASnd wt) ()
  canonical-value-forms-prod (TAPair wt wt₁) (VPair dv dv₁) = _ , _ , refl , wt , wt₁

  -- this argues (somewhat informally, because you still have to inspect
  -- the types of the theorems above and manually verify this property)
  -- that we didn't miss any cases above; this intentionally will make this
  -- file fail to typecheck if we added more types, hopefully forcing us to
  -- remember to add canonical forms lemmas as appropriate
  canonical-value-forms-coverage1 : ∀{Δ d τ} →
                                   Δ , ∅ ⊢ d :: τ →
                                   d val →
                                   τ ≠ b →
                                   ((τ1 : typ) (τ2 : typ) → τ ≠ (τ1 ==> τ2)) →
                                   ((τ1 : typ) (τ2 : typ) → τ ≠ (τ1 ⊗ τ2)) →
                                   ⊥
  canonical-value-forms-coverage1 TAConst VConst = λ z _ _ → z refl
  canonical-value-forms-coverage1 (TAVar x₁) ()
  canonical-value-forms-coverage1 (TALam _ wt) VLam = λ _ z _ → z _ _ refl
  canonical-value-forms-coverage1 (TAAp wt wt₁) ()
  canonical-value-forms-coverage1 (TAEHole x x₁) ()
  canonical-value-forms-coverage1 (TANEHole x wt x₁) ()
  canonical-value-forms-coverage1 (TACast wt x) ()
  canonical-value-forms-coverage1 (TAFailedCast wt x x₁ x₂) ()
  canonical-value-forms-coverage1 (TAFst wt) ()
  canonical-value-forms-coverage1 (TASnd wt) ()
  canonical-value-forms-coverage1 (TAPair wt wt₁) (VPair dv dv₁) ne h = λ z → z _ _ refl

  canonical-value-forms-coverage2 : ∀{Δ d} →
                                   Δ , ∅ ⊢ d :: ⦇·⦈ →
                                   d val →
                                   ⊥
  canonical-value-forms-coverage2 (TAVar x₁) ()
  canonical-value-forms-coverage2 (TAAp wt wt₁) ()
  canonical-value-forms-coverage2 (TAEHole x x₁) ()
  canonical-value-forms-coverage2 (TANEHole x wt x₁) ()
  canonical-value-forms-coverage2 (TACast wt x) ()
  canonical-value-forms-coverage2 (TAFailedCast wt x x₁ x₂) ()
  canonical-value-forms-coverage2 (TAFst wt) ()
  canonical-value-forms-coverage2 (TASnd wt) ()

max_stars_repo_name: hazelgrove/hazel-palette-agda

max_issues_repo_name: hazelgrove/hazel-palette-agda

max_forks_repo_name: hazelgrove/hazelnut-livelits-agda


text:
module Arith where

open import Common.IO
open import Common.Nat renaming (_∸_ to _-_)  -- workaround for #1855
open import Common.Unit

test : Nat
test = 4

foobar : Nat -> Nat
foobar zero = zero
foobar (suc n) = suc (suc n)

main : IO Unit
main =
--  n <- readNat ,
  printNat 0 ,,
  printNat (0 + 1) ,,
  printNat (1 * 2) ,,
  printNat (suc (suc (suc (suc zero))) - suc zero) ,,
  printNat test    ,,
  printNat (foobar 4) ,,
--  printNat n ,,
  return unit


text:
module SafeFlagPostulate where

data Empty : Set where

postulate inhabitant : Empty

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


text:
module Data.Bin.NatHelpers where

    open import Relation.Binary.PropositionalEquality
    open import Data.Empty
    open import Data.Fin using (Fin; zero; suc) renaming (toℕ to finToℕ)
    open import Data.Nat using(ℕ; zero; suc; _≤_; _+_; _*_; s≤s; z≤n; ≤′-step; ≤′-refl; _<_; _∸_)
    open import Data.Nat.Properties using(_*-mono_; ≤′⇒≤; ≤⇒≤′)
    open import Function using (_∘_)
    open import Relation.Nullary

    ≤-step : ∀ {a b} → a ≤ b → a ≤ suc b
    ≤-step = ≤′⇒≤ ∘ ≤′-step ∘ ≤⇒≤′

    *2-mono : ∀ x → x ≤ x * 2
    *2-mono zero = z≤n
    *2-mono (suc x) = s≤s (≤-step (*2-mono x))

    kojojo : ∀ (b : Fin 2) x → x ≢ 0 → suc x ≤ finToℕ b + x * 2
    kojojo b zero nz = ⊥-elim (nz refl)
    kojojo zero (suc y) nz = s≤s (s≤s (*2-mono y))
    kojojo (suc zero) (suc y) nz = s≤s (s≤s (≤-step (*2-mono y)))
    kojojo (suc (suc ())) (suc y) nz

    *2-gives-space : ∀ {x y z} → (x < y) → z < 2 → x * 2 + z < y * 2
    *2-gives-space {suc x} {suc (suc y)} (s≤s (s≤s less)) zz = s≤s (s≤s (*2-gives-space {x} {suc y} (s≤s less) zz))
    *2-gives-space (s≤s z≤n) (s≤s (s≤s z≤n)) = s≤s (s≤s z≤n)
    *2-gives-space (s≤s z≤n) (s≤s z≤n) = s≤s z≤n

    open import Data.Product

    x≮z→x≡z+y : ∀ {x z} → ¬ x < z → ∃ λ y → x ≡ z + y
    x≮z→x≡z+y {zero} {zero} x≮z = zero , refl
    x≮z→x≡z+y {suc x} {zero} x≮z = suc x , refl
    x≮z→x≡z+y {zero} {suc z} x≮z = ⊥-elim (x≮z (s≤s z≤n))
    x≮z→x≡z+y {suc x} {suc z} x≮z with x≮z→x≡z+y {x} {z} (λ z' → x≮z (s≤s z'))
    x≮z→x≡z+y {suc .(z + y)} {suc z} x≮z | y , refl = y , refl

    +-elim₁ : ∀ {x y z} → z + x < z + y → x < y
    +-elim₁ {x} {y} {zero} lt = lt
    +-elim₁ {x} {y} {suc z} (s≤s lt) = +-elim₁ {x} {y} {z} lt

    import Data.Nat.Properties
    open import Algebra.Structures
    open IsCommutativeSemiring (Data.Nat.Properties.isCommutativeSemiring)

    +-elim₂ : ∀ {x y z} → x + z < y + z → x < y
    +-elim₂ {x} {y} {z} lt rewrite +-comm x z | +-comm y z = +-elim₁ {x} {y} {z} lt

max_stars_repo_name: Rotsor/BinDivMod

max_issues_repo_name: Rotsor/BinDivMod

max_forks_repo_name: Rotsor/BinDivMod


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Group.Base where
{-
  Defines groups and adds the smart constructors [makeGroup-right] and [makeGroup-left]
  for constructing groups from less data than the standard [makeGroup] constructor.
-}

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Structure
open import Cubical.Data.Sigma
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Semigroup

open import Cubical.Reflection.RecordEquiv

private
  variable
    ℓ : Level

record IsGroup {G : Type ℓ}
               (1g : G) (_·_ : G → G → G) (inv : G → G) : Type ℓ where

  constructor isgroup

  field
    isMonoid  : IsMonoid 1g _·_
    ·InvR : (x : G) → x · inv x ≡ 1g
    ·InvL : (x : G) → inv x · x ≡ 1g

  open IsMonoid isMonoid public

unquoteDecl IsGroupIsoΣ = declareRecordIsoΣ IsGroupIsoΣ (quote IsGroup)

record GroupStr (G : Type ℓ) : Type ℓ where

  constructor groupstr

  field
    1g      : G
    _·_     : G → G → G
    inv     : G → G
    isGroup : IsGroup 1g _·_ inv

  infixr 7 _·_

  open IsGroup isGroup public

Group : ∀ ℓ → Type (ℓ-suc ℓ)
Group ℓ = TypeWithStr ℓ GroupStr

Group₀ : Type₁
Group₀ = Group ℓ-zero

group : (G : Type ℓ) (1g : G) (_·_ : G → G → G) (inv : G → G) (h : IsGroup 1g _·_ inv) → Group ℓ
group G 1g _·_ inv h = G , groupstr 1g _·_ inv h

isSetGroup : (G : Group ℓ) → isSet ⟨ G ⟩
isSetGroup G = GroupStr.isGroup (snd G) .IsGroup.isMonoid .IsMonoid.isSemigroup .IsSemigroup.is-set

makeIsGroup : {G : Type ℓ} {e : G} {_·_ : G → G → G} { inv : G → G}
              (is-setG : isSet G)
              (·Assoc : (x y z : G) → x · (y · z) ≡ (x · y) · z)
              (·IdR : (x : G) → x · e ≡ x)
              (·IdL : (x : G) → e · x ≡ x)
              (·InvR : (x : G) → x · inv x ≡ e)
              (·InvL : (x : G) → inv x · x ≡ e)
            → IsGroup e _·_ inv
IsGroup.isMonoid (makeIsGroup is-setG ·Assoc ·IdR ·IdL ·InvR ·InvL) = makeIsMonoid is-setG ·Assoc ·IdR ·IdL
IsGroup.·InvR (makeIsGroup is-setG ·Assoc ·IdR ·IdL ·InvR ·InvL) = ·InvR
IsGroup.·InvL (makeIsGroup is-setG ·Assoc ·IdR ·IdL ·InvR ·InvL) = ·InvL

makeGroup : {G : Type ℓ} (1g : G) (_·_ : G → G → G) (inv : G → G)
            (is-setG : isSet G)
            (·Assoc : (x y z : G) → x · (y · z) ≡ (x · y) · z)
            (·IdR : (x : G) → x · 1g ≡ x)
            (·IdL : (x : G) → 1g · x ≡ x)
            (·InvR : (x : G) → x · inv x ≡ 1g)
            (·InvL : (x : G) → inv x · x ≡ 1g)
          → Group ℓ
makeGroup 1g _·_ inv is-setG ·Assoc ·IdR ·IdL ·InvR ·InvL = _ , helper
  where
  helper : GroupStr _
  GroupStr.1g helper = 1g
  GroupStr._·_ helper = _·_
  GroupStr.inv helper = inv
  GroupStr.isGroup helper = makeIsGroup is-setG ·Assoc ·IdR ·IdL ·InvR ·InvL

Group→Monoid : Group ℓ → Monoid ℓ
Group→Monoid (A , groupstr  _ _ _ G) = A , monoidstr _ _ (IsGroup.isMonoid G)

makeGroup-right : {A : Type ℓ}
  → (1g : A)
  → (_·_ : A → A → A)
  → (inv : A → A)
  → (set : isSet A)
  → (·Assoc : ∀ a b c → a · (b · c) ≡ (a · b) · c)
  → (·IdR : ∀ a → a · 1g ≡ a)
  → (·InvR : ∀ a → a · inv a ≡ 1g)
  → Group ℓ
makeGroup-right 1g _·_ inv set ·Assoc ·IdR ·InvR =
  makeGroup 1g _·_ inv set ·Assoc ·IdR ·IdL ·InvR ·InvL
  where
    abstract
      ·InvL : ∀ a → inv a · a ≡ 1g
      ·InvL a =
        inv a · a
          ≡⟨ sym (·IdR _)  ⟩
        (inv a · a) · 1g
          ≡⟨ cong (_·_ _) (sym (·InvR (inv a))) ⟩
        (inv a · a) · (inv a · (inv (inv a)))
          ≡⟨ ·Assoc _ _ _ ⟩
        ((inv a · a) · (inv a)) · (inv (inv a))
          ≡⟨ cong (λ □ → □ · _) (sym (·Assoc _ _ _)) ⟩
        (inv a · (a · inv a)) · (inv (inv a))
          ≡⟨ cong (λ □ → (inv a · □) · (inv (inv a))) (·InvR a) ⟩
        (inv a · 1g) · (inv (inv a))
          ≡⟨ cong (λ □ → □ · (inv (inv a))) (·IdR (inv a)) ⟩
        inv a · (inv (inv a))
          ≡⟨ ·InvR (inv a) ⟩
        1g
          ∎

      ·IdL : ∀ a → 1g · a ≡ a
      ·IdL a =
        1g · a
          ≡⟨ cong (λ b → b · a) (sym (·InvR a)) ⟩
        (a · inv a) · a
          ≡⟨ sym (·Assoc _ _ _) ⟩
        a · (inv a · a)
          ≡⟨ cong (a ·_) (·InvL a) ⟩
        a · 1g
          ≡⟨ ·IdR a ⟩
        a
          ∎

makeGroup-left : {A : Type ℓ}
  → (1g : A)
  → (_·_ : A → A → A)
  → (inv : A → A)
  → (set : isSet A)
  → (·Assoc : ∀ a b c → a · (b · c) ≡ (a · b) · c)
  → (·IdL : ∀ a → 1g · a ≡ a)
  → (·InvL : ∀ a → (inv a) · a ≡ 1g)
  → Group ℓ
makeGroup-left 1g _·_ inv set ·Assoc ·IdL ·InvL =
  makeGroup 1g _·_ inv set ·Assoc ·IdR ·IdL ·InvR ·InvL
  where
    abstract
      ·InvR : ∀ a → a · inv a ≡ 1g
      ·InvR a =
        a · inv a
          ≡⟨ sym (·IdL _)  ⟩
        1g · (a · inv a)
          ≡⟨ cong (λ b → b · (a · inv a)) (sym (·InvL (inv a))) ⟩
        (inv (inv a) · inv a) · (a · inv a)
          ≡⟨ sym (·Assoc (inv (inv a)) (inv a) _) ⟩
        inv (inv a) · (inv a · (a · inv a))
          ≡⟨ cong (inv (inv a) ·_) (·Assoc (inv a) a (inv a)) ⟩
        (inv (inv a)) · ((inv a · a) · (inv a))
          ≡⟨ cong (λ b → (inv (inv a)) · (b · (inv a))) (·InvL a) ⟩
        inv (inv a) · (1g · inv a)
          ≡⟨ cong (inv (inv a) ·_) (·IdL (inv a)) ⟩
        inv (inv a) · inv a
          ≡⟨ ·InvL (inv a) ⟩
        1g
          ∎

      ·IdR : ∀ a → a · 1g ≡ a
      ·IdR a =
        a · 1g
          ≡⟨ cong (a ·_) (sym (·InvL a)) ⟩
        a · (inv a · a)
          ≡⟨ ·Assoc a (inv a) a ⟩
        (a · inv a) · a
          ≡⟨ cong (λ b → b · a) (·InvR a) ⟩
        1g · a
          ≡⟨ ·IdL a ⟩
        a
          ∎

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --without-K #-}
module NTypes.Id where

open import GroupoidStructure
open import NTypes
open import PathOperations
open import Transport
open import Types

-- This should also be derivable from hLevel-suc from
-- HomotopyTypes.HLevel module.
Id-isSet : ∀ {a} {A : Set a} {x y : A} →
  isSet A → isSet (x ≡ y)
Id-isSet {x = x} {y = y} A-set _ _ pp qq
  = path pp ⁻¹ · path qq
  where
  split-path : {p q : x ≡ y} (pp : p ≡ q) →
    A-set _ _ p q ≡ pp · A-set _ _ q q
  split-path pp = J
    (λ p q pp → A-set _ _ p q ≡ pp · A-set _ _ q q)
    (λ _ → refl) _ _ pp

  path : {p q : x ≡ y} (pp : p ≡ q) →
    A-set _ _ p q ≡ pp
  path pp = J
    (λ p q pp → A-set _ _ p q ≡ pp)
    (λ p → split-path (A-set _ _ p p ⁻¹) · p⁻¹·p (A-set _ _ p p))
    _ _ pp

-- From the lectures.
Id-isSet-alt : ∀ {a} {A : Set a} {u v : A} →
  isSet A → isSet (u ≡ v)
Id-isSet-alt {u = u} {v = v} H r s α β
  = id·p α ⁻¹
  · ap (λ z → z · α)
    (p⁻¹·p (H′ r)) ⁻¹
  · p·q·r (H′ r ⁻¹) (H′ r) α ⁻¹
  · ap (λ z → H′ r ⁻¹ · z)
    ( tr-post r α (H′ r) ⁻¹
    · apd H′ α
    · apd H′ β ⁻¹
    · tr-post r β (H′ r)
    )
  · p·q·r (H′ r ⁻¹) (H′ r) β
  · ap (λ z → z · β)
    (p⁻¹·p (H′ r))
  · id·p β
  where
    H′ = λ q → H u v r q


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

module Data.Binary.PerformanceTests.Conversion where

open import Prelude
open import Data.Binary.Definition
open import Data.Binary.Conversion using (⟦_⇓⟧)
-- open import Data.Binary.Conversion.Strict
open import Data.Binary.Conversion.Fast

-- one-thousand : 𝔹
-- one-thousand = 2ᵇ 1ᵇ 1ᵇ 2ᵇ 1ᵇ 2ᵇ 2ᵇ 2ᵇ 2ᵇ 0ᵇ

-- f : 𝔹
-- f = one-thousand

n : ℕ
n = 5000000

-- The actual performance test (uncomment and time how long it takes to type-check)
-- _ : ⟦ ⟦ n ⇑⟧ ⇓⟧ ≡ n
-- _ = refl

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module ModuleArgs where

open import Common.Nat
open import Common.IO
open import Common.Unit

module X (y : Nat) where
  addTo : Nat -> Nat
  addTo x = y + x

open X 23

-- should return 35
main : IO Unit
main = printNat (addTo 12)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda