text:
-- ------------------------------------------------------------------------------------------------------
-- | ███████╗ ██████╗ ██╗     ██╗   ██╗██╗███╗   ██╗ ██████╗     ██████╗ ██╗███╗   ██╗ ██████╗ ███████╗ |
-- | ██╔════╝██╔═══██╗██║     ██║   ██║██║████╗  ██║██╔════╝     ██╔══██╗██║████╗  ██║██╔════╝ ██╔════╝ |
-- | ███████╗██║   ██║██║     ██║   ██║██║██╔██╗ ██║██║  ███╗    ██████╔╝██║██╔██╗ ██║██║  ███╗███████╗ |
-- | ╚════██║██║   ██║██║     ╚██╗ ██╔╝██║██║╚██╗██║██║   ██║    ██╔══██╗██║██║╚██╗██║██║   ██║╚════██║ |
-- | ███████║╚██████╔╝███████╗ ╚████╔╝ ██║██║ ╚████║╚██████╔╝    ██║  ██║██║██║ ╚████║╚██████╔╝███████║ |
-- | ╚══════╝ ╚═════╝ ╚══════╝  ╚═══╝  ╚═╝╚═╝  ╚═══╝ ╚═════╝     ╚═╝  ╚═╝╚═╝╚═╝  ╚═══╝ ╚═════╝ ╚══════╝ |
-- |                                                                                |
-- |                         ██╗███╗   ██╗     █████╗  ██████╗ ██████╗  █████╗                          |
-- |                         ██║████╗  ██║    ██╔══██╗██╔════╝ ██╔══██╗██╔══██╗                         |
-- |                         ██║██╔██╗ ██║    ███████║██║  ███╗██║  ██║███████║                         |
-- |                         ██║██║╚██╗██║    ██╔══██║██║   ██║██║  ██║██╔══██║                         |
-- |                         ██║██║ ╚████║    ██║  ██║╚██████╔╝██████╔╝██║  ██║                         |
-- |                         ╚═╝╚═╝  ╚═══╝    ╚═╝  ╚═╝ ╚═════╝ ╚═════╝ ╚═╝  ╚═╝                         |
-- ------------------------------------------------------------------------------------------------------
--
--                                        Donnacha Oisín Kidney
--                                            17 April 2019
--
-- Compiled with Agda version 2.6.1, and standard library commit 84d7962cfd90379a6d1d5ef2cdd9d3ae411ee603

-- This contains the worked-through source code for:
--
--     "Automatically And Efficiently Illustrating Polynomial Equalities in Agda"
--
--     We present a new library which automates the construction of equivalence
--     proofs between polynomials over commutative rings and semirings in the
--     programming language Agda. It is asymptotically faster than Agda's existing
--     solver. We use Agda's reflection machinery to provide a simple interface to
--     the solver, and demonstrate an interesting use of the constructed relations:
--     step-by-step solutions.
--
-- Which is (at time of writing) a work-in-progress.
--
-- This code is available on github:
--     https://github.com/oisdk/agda-ring-solver
--
-- As is the paper:
--     https://github.com/oisdk/agda-ring-solver-report

module README where

--------------------------------------------------------------------------------
-- There are 3 main contributions in this library:                            --
--                                                                            --
--   * A solver for polynomials over "almost commutative rings".              --
--         Agda already has one these in the standard library, but this one   --
--         is much more efficient. "Almost commutative rings" encapsulates a  --
--         bunch of things, including ℕ.                                      --
--                                                                            --
--   * A reflection-based interface.                                          --
--         Not many people used the old solver, mainly (I think) because the  --
--         interface was difficult and irritating. This library provides a    --
--         super-simple interface using reflection.                           --
--                                                                            --
--   * An implementation of "step-by-step solutions".                         --
--         I don't know a huge amount about computer algebra systems, but I   --
--         have used Wolfram Alpha countless times (especially when I was in  --
--         school) to help with basic maths. I was able to get this solver to --
--         produce step-by-step solutions, and learned something about the    --
--         theory behind them along the way.                                  --
--------------------------------------------------------------------------------
--
-- ██████╗ ███████╗███╗   ██╗ ██████╗██╗  ██╗███╗   ███╗ █████╗ ██████╗ ██╗  ██╗███████╗
-- ██╔══██╗██╔════╝████╗  ██║██╔════╝██║  ██║████╗ ████║██╔══██╗██╔══██╗██║ ██╔╝██╔════╝
-- ██████╔╝█████╗  ██╔██╗ ██║██║     ███████║██╔████╔██║███████║██████╔╝█████╔╝ ███████╗ ███████╗
-- ██╔══██╗██╔══╝  ██║╚██╗██║██║     ██╔══██║██║╚██╔╝██║██╔══██║██╔══██╗██╔═██╗ ╚════██║ ╚════██║
-- ██████╔╝███████╗██║ ╚████║╚██████╗██║  ██║██║ ╚═╝ ██║██║  ██║██║  ██║██║  ██╗███████║      ██║
-- ╚═════╝ ╚══════╝╚═╝  ╚═══╝ ╚═════╝╚═╝  ╚═╝╚═╝     ╚═╝╚═╝  ╚═╝╚═╝  ╚═╝╚═╝  ╚═╝╚══════╝      ██║
--                                                                                ██║
-- ███████╗██╗  ██╗ █████╗ ███╗   ███╗██████╗ ██╗     ███████╗███████╗                        ██║
-- ██╔════╝╚██╗██╔╝██╔══██╗████╗ ████║██╔══██╗██║     ██╔════╝██╔════╝                        ██║
-- █████╗   ╚███╔╝ ███████║██╔████╔██║██████╔╝██║     █████╗  ███████╗ ████████████████████╗  ██║
-- ██╔══╝   ██╔██╗ ██╔══██║██║╚██╔╝██║██╔═══╝ ██║     ██╔══╝  ╚════██║ ╚═════════════════██║  ██║
-- ███████╗██╔╝ ██╗██║  ██║██║ ╚═╝ ██║██║     ███████╗███████╗███████║                   ██║  ██║
-- ╚══════╝╚═╝  ╚═╝╚═╝  ╚═╝╚═╝     ╚═╝╚═╝     ╚══════╝╚══════╝╚══════╝                   ██║  ██║
--                                                                                ██║  ██║
--------------------------------------------------------------------------------         ██║  ██║
-- You can ignore this bit! We're just overloading the literals Agda uses for --         ██║  ██║
-- numbers This bit isn't necessary if you're just using Nats, or if you      --         ██║  ██║
-- construct your type directly. We only really do it here so that we can use --         ██║  ██║
-- different numeric types in the same file.                                  --         ██║  ██║
                                                                              --         ██║  ██║
open import Agda.Builtin.FromNat                                              --         ██║  ██║
open import Data.Nat using (ℕ; suc)                                           --         ██║  ██║
open import Data.Integer using (ℤ)                                            --         ██║  ██║
                                                                              --         ██║  ██║
instance                                                                      --         ██║  ██║
  numberNat : Number ℕ                                                        --         ██║  ██║
  numberNat = Data.Nat.Literals.number                                        --         ██║  ██║
    where import Data.Nat.Literals                                            --         ██║  ██║
                                                                              --         ██║  ██║
instance                                                                      --         ██║  ██║
  numberInt : Number ℤ                                                        --         ██║  ██║
  numberInt = Data.Integer.Literals.number                                    --         ██║  ██║
    where import Data.Integer.Literals                                        --         ██║  ██║
                                                                              --         ██║  ██║
--------------------------------------------------------------------------------         ██║  ██║
-- Imports!                                                                   --         ██║  ██║
                                                                              --         ██║  ██║
open import Polynomial.Simple.AlmostCommutativeRing                           --         ██║  ██║
open import Polynomial.Simple.AlmostCommutativeRing.Instances                 --         ██║  ██║
open import Polynomial.Simple.Reflection                                      --         ██║  ██║
open import Data.List as List using (List; _∷_; [])                           --         ██║  ██║
open import Function                                                          --         ██║  ██║
open import Relation.Binary.PropositionalEquality as ≡ using (subst; _≡_)     --         ██║  ██║
open import Data.Bool as Bool using (Bool; true; false; if_then_else_)        --         ██║  ██║
open import Data.Unit using (⊤; tt)                                           --         ██║  ██║
--                                                                            --         ██║  ██║
--------------------------------------------------------------------------------         ██║  ██║
--                                                                            --         ██║  ██║
--                           8888888888',8888'                                --         ██║  ██║
--                                  ,8',8888'                                 --         ██║  ██║
--                                 ,8',8888'                                  --         ██║  ██║
--                                ,8',8888'                                   --         ██║  ██║
--                               ,8',8888'                                    --         ██║  ██║
--                              ,8',8888'                                     --         ██║  ██║
--                             ,8',8888'                                      --         ██║  ██║
--                            ,8',8888'                                       --         ██║  ██║
--                           ,8',8888'                                        --         ██║  ██║
--                          ,8',8888888888888                                 --         ██║  ██║
--                                                                            --         ██║  ██║
--------------------------------------------------------------------------------         ██║  ██║
--                                                                            --         ██║  ██║
module IntExamples where                                                      --         ██║  ██║
  open AlmostCommutativeRing Int.ring                                         --         ██║  ██║
  -- Everything is automatic: you just ask Agda to solve it and it does!      --     ██╗ ██║  ██║
  lemma₁ : ∀ x y → x + y * 1 + 3 ≈ 3 + 1 + y + x + - 1                        --   ████║ ██║  ██║
  lemma₁ = solve Int.ring                                                     -- ██████████║  ██║
                                                                              --   ████╔═██║  ██║
  lemma₂ : ∀ x y → (x + y) ^ 2 ≈ x ^ 2 + 2 * x * y + y ^ 2                    --     ██║ ██║  ██║
  lemma₂ = solve Int.ring                                                     --     ╚═╝ ██║  ██║
                                                                              --         ██║  ██║
  open import Relation.Binary.Reasoning.Inference setoid                      --         ██║  ██║
                                                                              --         ██║  ██║
  -- It can interact with manual proofs as well.                              --         ██║  ██║
  lemma₃ : ∀ x y → x + y * 1 + 3 ≈ 2 + 1 + y + x                              --         ██║  ██║
  lemma₃ x y = begin                                                          --         ██║  ██║
    x + y * 1 + 3 ≈⟨ +-comm x (y * 1) ⟨ +-cong ⟩ refl ⟩                       --         ██║  ██║
    y * 1 + x + 3 ≈⟨ solveOver (x ∷ y ∷ []) Int.ring ⟩                        --         ██║  ██║
    3 + y + x     ≡⟨⟩                                                         --         ██║  ██║
    2 + 1 + y + x ∎                                                           --         ██║  ██║
                                                                              --         ██║  ██║
  open Int.Reflection                                                         --         ██║  ██║
                                                                              --         ██║  ██║
  -- There's a shorthand included for Int and Nat.                            --         ██║  ██║
  lemma₄ : ∀ x y → x + y * 1 + 3 ≈ 2 + 1 + y + x                              --         ██║  ██║
  lemma₄ x y = begin                                                          --         ██║  ██║
    x + y * 1 + 3 ≈⟨ +-comm x (y * 1) ⟨ +-cong ⟩ refl ⟩                       --         ██║  ██║
    y * 1 + x + 3 ≈⟨ ∀⟨ x ∷ y ∷ [] ⟩ ⟩                                        --         ██║  ██║
    3 + y + x     ≡⟨⟩                                                         --         ██║  ██║
    2 + 1 + y + x ∎                                                           --         ██║  ██║
--                                                                            --         ██║  ██║
--------------------------------------------------------------------------------         ██║  ██║
--                                                                            --         ██║  ██║
--                          b.             8                                  --         ██║  ██║
--                          888o.          8                                  --         ██║  ██║
--                          Y88888o.       8                                  --         ██║  ██║
--                          .`Y888888o.    8                                  --         ██║  ██║
--                          8o. `Y888888o. 8                                  --         ██║  ██║
--                          8`Y8o. `Y88888o8                                  --         ██║  ██║
--                          8   `Y8o. `Y8888                                  --         ██║  ██║
--                          8      `Y8o. `Y8                                  --         ██║  ██║
--                          8         `Y8o.`                                  --         ██║  ██║
--                          8            `Yo                                  --         ██║  ██║
--                                                                            --         ██║  ██║
--------------------------------------------------------------------------------         ██║  ██║
--                                                                            --         ██║  ██║
module NatExamples where                                                      --         ██║  ██║
  open AlmostCommutativeRing Nat.ring                                         --     ██╗ ██║  ██║
  -- The solver is flexible enough to work with Nats (even though it asks     --   ████║ ██║  ██║
  -- for rings!)                                                              -- ██████████║  ██║
  lemma₁ : ∀ x y → x + y * 1 + 3 ≈ 2 + 1 + y + x                              --   ████╔═██║  ██║
  lemma₁ = solve Nat.ring                                                     --     ██║ ██║  ██║
                                                                              --     ╚═╝ ██║  ██║
  lemma₂ : ∀ x y → x + y * 1 + 3 ≈ 2 + suc y + x                              --         ██║  ██║
  lemma₂ = solve Nat.ring                                                     --         ██║  ██║
--                                                                            --         ██║  ██║
--------------------------------------------------------------------------------         ██║  ██║
--                                                                            --         ██║  ██║
--          #####  #     # #######  #####  #    # ### #     #  #####          --         ██║  ██║
--         #     # #     # #       #     # #   #   #  ##    # #     #         --         ██║  ██║
--         #       #     # #       #       #  #    #  # #   # #               --         ██║  ██║
--         #       ####### #####   #       ###     #  #  #  # #  ####         --         ██║  ██║
--         #       #     # #       #       #  #    #  #   # # #     #         --         ██║  ██║
--         #     # #     # #       #     # #   #   #  #    ## #     #         --         ██║  ██║
--          #####  #     # #######  #####  #    # ### #     #  #####          --         ██║  ██║
--                                                                            --         ██║  ██║
--   ### #     # #     #    #    ######  ###    #    #     # #######  #####   --         ██║  ██║
--    #  ##    # #     #   # #   #     #  #    # #   ##    #    #    #     #  --         ██║  ██║
--    #  # #   # #     #  #   #  #     #  #   #   #  # #   #    #    #        --         ██║  ██║
--    #  #  #  # #     # #     # ######   #  #     # #  #  #    #     #####   --         ██║  ██║
--    #  #   # #  #   #  ####### #   #    #  ####### #   # #    #          #  --         ██║  ██║
--    #  #    ##   # #   #     # #    #   #  #     # #    ##    #    #     #  --         ██║  ██║
--   ### #     #    #    #     # #     # ### #     # #     #    #     #####   --         ██║  ██║
--                                                                            --         ██║  ██║
--------------------------------------------------------------------------------         ██║  ██║
-- The solver makes it easy to prove invariants, without having to rewrite    --         ██║  ██║
-- proof code every time something changes in the data structure.             --         ██║  ██║
--                                                                            --         ██║  ██║
  module _ {a} {A : Set a} (_≤_ : A → A → Bool) where                         --         ██║  ██║
   -- A Skew Heap, indexed by its size.                                       --         ██║  ██║
   data Tree : ℕ → Set a where                                                --         ██║  ██║
     leaf : Tree 0                                                            --         ██║  ██║
     node : ∀ {n m} → A → Tree n → Tree m → Tree (n + m + 1)                  --         ██║  ██║
                                                                              --         ██║  ██║
   -- A substitution operator, to clean things up.                            --         ██║  ██║
   _⇒_ : ∀ {n} → Tree n → ∀ {m} → n ≈ m → Tree m                              --         ██║  ██║
   x ⇒ n≈m  = subst Tree n≈m x                                                --         ██║  ██║
                                                                              --         ██║  ██║
   open Nat.Reflection                                                        --         ██║  ██║
                                                                              --         ██║  ██║
-- _∪_ : ∀ {n m} → Tree n → Tree m → Tree (n + m)                             --         ██║  ██║
-- leaf ∪ ys = ys                                                             --         ██║  ██║
-- node {a} {b} x xl xr ∪ leaf =                                              --         ██║  ██║
--   node x xl xr ⇒ ∀⟨ a ∷ b ∷ [] ⟩                                           --     ██╗ ██║  ██║
-- node {a} {b} x xl xr ∪ node {c} {d} y yl yr = if x ≤ y                     --   ████║ ██║  ██║
--          then node x (node y yl yr ∪ xr) xl                                -- ██████████║  ██║
--                 ⇒ ∀⟨ a ∷ b ∷ c ∷ d ∷ [] ⟩                                  --   ████╔═██║  ██║
--          else (node y (node x xl xr ∪ yr) yl                               --     ██║ ██║  ██║
--                 ⇒ ∀⟨ a ∷ b ∷ c ∷ d ∷ [] ⟩)                                 --     ╚═╝ ██║  ██║
--                                                                            --         ██║  ██║
--------------------------------------------------------------------------------         ██║  ██║
--                                                                            --         ██║  ██║
--             8888888 8888888888 8 8888        8 8 8888888888                --         ██║  ██║
--                   8 8888       8 8888        8 8 8888                      --         ██║  ██║
--                   8 8888       8 8888        8 8 8888                      --         ██║  ██║
--                   8 8888       8 8888        8 8 8888                      --         ██║  ██║
--                   8 8888       8 8888        8 8 888888888888              --         ██║  ██║
--                   8 8888       8 8888        8 8 8888                      --         ██║  ██║
--                   8 8888       8 8888888888888 8 8888                      --         ██║  ██║
--                   8 8888       8 8888        8 8 8888                      --         ██║  ██║
--                   8 8888       8 8888        8 8 8888                      --         ██║  ██║
--                   8 8888       8 8888        8 8 888888888888              --         ██║  ██║
--                                                                            --         ██║  ██║
--                 ,o888888o.     8 8888         8 888888888o.                --         ██║  ██║
--              . 8888     `88.   8 8888         8 8888    `^888.             --         ██║  ██║
--             ,8 8888       `8b  8 8888         8 8888        `88.           --         ██║  ██║
--             88 8888        `8b 8 8888         8 8888         `88           --         ██║  ██║
--             88 8888         88 8 8888         8 8888          88           --         ██║  ██║
--             88 8888         88 8 8888         8 8888          88           --         ██║  ██║
--             88 8888        ,8P 8 8888         8 8888         ,88           --         ██║  ██║
--             `8 8888       ,8P  8 8888         8 8888        ,88'           --         ██║  ██║
--              ` 8888     ,88'   8 8888         8 8888    ,o88P'             --         ██║  ██║
--                 `8888888P'     8 888888888888 8 888888888P'                --         ██║  ██║
--                                                                            --         ██║  ██║
--             `8.`888b                 ,8' .8.   `8.`8888.      ,8'          --         ██║  ██║
--              `8.`888b               ,8' .888.   `8.`8888.    ,8'           --         ██║  ██║
--               `8.`888b             ,8' :88888.   `8.`8888.  ,8'            --         ██║  ██║
--                `8.`888b     .b    ,8' . `88888.   `8.`8888.,8'             --         ██║  ██║
--                 `8.`888b    88b  ,8' .8. `88888.   `8.`88888'              --         ██║  ██║
--                  `8.`888b .`888b,8' .8`8. `88888.   `8. 8888               --         ██║  ██║
--                   `8.`888b8.`8888' .8' `8. `88888.   `8 8888               --         ██║  ██║
--                    `8.`888`8.`88' .8'   `8. `88888.   8 8888               --         ██║  ██║
--                     `8.`8' `8,`' .888888888. `88888.  8 8888               --         ██║  ██║
--                      `8.`   `8' .8'       `8. `88888. 8 8888               --         ██║  ██║
--                                                                            --         ██║  ██║
--------------------------------------------------------------------------------         ██║  ██║
-- Previously, you had to construct the expression you wanted to solve twice: --         ██║  ██║
-- once in the type signature, and again using the special solver syntax.     --         ██║  ██║
--                                                                            --         ██║  ██║
-- This is difficult to learn, and error-prone: if I change an x + y          --         ██║  ██║
-- somewhere to a y + x, I *also* have to change the proofs now! The          --         ██║  ██║
-- reflection-based solver will automatically construct the new proof.        --         ██║  ██║
--                                                                            --         ██║  ██║
module OldSolver where                                                        --         ██║  ██║
  open import Data.Nat                                                        --         ██║  ██║
  open import Data.Nat.Solver using (module +-*-Solver)                       --         ██║  ██║
  open +-*-Solver                                                             --         ██║  ██║
                                                                              --     ██╗ ██║  ██║
--lemma : ∀ x y → x + y * 1 + 3 ≡ 2 + 1 + y + x                               --   ████║ ██║  ██║
--lemma = +-*-Solver.solve 2                                                  -- ██████████║  ██║
--  (λ x y → x :+ y :* con 1 :+ con 3 := con 2 :+ con 1 :+ y :+ x) ≡.refl     --   ████╔═██║  ██║
--                                                                            --     ██║ ██║  ██║
--------------------------------------------------------------------------------     ╚═╝ ██║  ██║
--                                                                            --         ██║  ██║
--          d888888o.   8888888 8888888888 8 8888888888   8 888888888o        --         ██║  ██║
--        .`8888:' `88.       8 8888       8 8888         8 8888    `88.      --         ██║  ██║
--        8.`8888.   Y8       8 8888       8 8888         8 8888     `88      --         ██║  ██║
--        `8.`8888.           8 8888       8 8888         8 8888     ,88      --         ██║  ██║
--         `8.`8888.          8 8888       8 888888888888 8 8888.   ,88'      --         ██║  ██║
--          `8.`8888.         8 8888       8 8888         8 888888888P'       --         ██║  ██║
--           `8.`8888.        8 8888       8 8888         8 8888              --         ██║  ██║
--       8b   `8.`8888.       8 8888       8 8888         8 8888              --         ██║  ██║
--       `8b.  ;8.`8888       8 8888       8 8888         8 8888              --         ██║  ██║
--        `Y8888P ,88P'       8 8888       8 888888888888 8 8888              --         ██║  ██║
--                                                                            --         ██║  ██║
--                      8 888888888o   `8.`8888.      ,8'                     --         ██║  ██║
--                      8 8888    `88.  `8.`8888.    ,8'                      --         ██║  ██║
--                      8 8888     `88   `8.`8888.  ,8'                       --         ██║  ██║
--                      8 8888     ,88    `8.`8888.,8'                        --         ██║  ██║
--                      8 8888.   ,88'     `8.`88888'                         --         ██║  ██║
--                      8 8888888888        `8. 8888                          --         ██║  ██║
--                      8 8888    `88.       `8 8888                          --         ██║  ██║
--                      8 8888      88        8 8888                          --         ██║  ██║
--                      8 8888    ,88'        8 8888                          --         ██║  ██║
--                      8 888888888P          8 8888                          --         ██║  ██║
--                                                                            --         ██║  ██║
--          d888888o.   8888888 8888888888 8 8888888888   8 888888888o        --         ██║  ██║
--        .`8888:' `88.       8 8888       8 8888         8 8888    `88.      --         ██║  ██║
--        8.`8888.   Y8       8 8888       8 8888         8 8888     `88      --         ██║  ██║
--        `8.`8888.           8 8888       8 8888         8 8888     ,88      --         ██║  ██║
--         `8.`8888.          8 8888       8 888888888888 8 8888.   ,88'      --         ██║  ██║
--          `8.`8888.         8 8888       8 8888         8 888888888P'       --         ██║  ██║
--           `8.`8888.        8 8888       8 8888         8 8888              --         ██║  ██║
--       8b   `8.`8888.       8 8888       8 8888         8 8888              --         ██║  ██║
--       `8b.  ;8.`8888       8 8888       8 8888         8 8888              --         ██║  ██║
--        `Y8888P ,88P'       8 8888       8 888888888888 8 8888              --         ██║  ██║
--                                                                            --         ██║  ██║
--------------------------------------------------------------------------------         ██║  ██║
-- Don't understand why something works? Wanna get it explained to you? Now   --         ██║  ██║
-- you can! The solver can generate step-by-step, human-readable solutions    --         ██║  ██║
-- for learning purposes.                                                     --         ██║  ██║
--                                                                            --         ██║  ██║
module TracedExamples where                                                   --         ██║  ██║
  import Data.Nat.Show                                                        --         ██║  ██║
  open import EqBool                                                          --         ██║  ██║
  open import Relation.Traced Nat.ring  Data.Nat.Show.show public             --         ██║  ██║
  open AlmostCommutativeRing tracedRing                                       --         ██║  ██║
                                                                              --         ██║  ██║
  lemma : ∀ x y → x + y * 1 + 3 ≈ 2 + 1 + y + x                               --         ██║  ██║
  lemma = solve tracedRing                                                    --         ██║  ██║
                                                                              --      ██╗██║  ██║
  explained                                                                   --    ████║██║  ██║
    : showProof (lemma "x" "y") ≡ "x + y + 3"                                 --  █████████║  ██║
                                ∷ "    ={ +-comm(x, y + 3) }"                 --    ████╔══╝  ██║
                                ∷ "y + 3 + x"                                 --      ██║     ██║
                                ∷ "    ={ +-comm(y, 3) }"                     --      ╚═╝     ██║
                                ∷ "3 + y + x"                                 --              ██║
                                ∷ []                                          --              ██║
  explained = ≡.refl                                                          --              ██║
--------------------------------------------------------------------------------              ██║
--                                                                            --              ██║
-- The new solver uses a sparse representation, which is much faster than the --              ██║
-- dense one the old solver used. The following graph shows the time (in      --              ██║
-- seconds) to prove that:                                                    --              ██║
--                                                                            --              ██║
--     (1 + x₁¹ + x₂² + x₃³ + x₄⁴ + x₅⁵)ᵈ                                     --              ██║
--                                                                            --              ██║
-- is equal to its expanded form. (to run the benchmarks yourself, run the    --              ██║
-- run_benchmarks.py file. You'll need python 3 and sympy.)                   --              ██║
--                                                                            --              ██║
-- 540 |  * = old                                                       *     --              ██║
-- 525 |  + = new                                                       *     --              ██║
-- 510 |                                                                *     --              ██║
-- 495 |                                                                *     --              ██║
-- 480 |                                                                *     --              ██║
-- 465 |                                                               *      --              ██║
-- 450 |                                                               *      --              ██║
-- 435 |                                                               *      --              ██║
-- 420 |                                                              *       --              ██║
-- 405 |                                                              *       --              ██║
-- 390 |                                                              *       --              ██║
-- 375 |                                                             *        --              ██║
-- 360 |                                                             *        --              ██║
-- 345 |                                                             *        --              ██║
-- 330 |                                                            *         --              ██║
-- 315 |                                                            *         --              ██║
-- 300 |                                                            *         --              ██║
-- 285 |                                                           *          --              ██║
-- 270 |                                                           *          --              ██║
-- 255 |                                                           *          --              ██║
-- 240 |                                                          *           --           ██╗██║
-- 225 |                                                          *           --         ████║██║
-- 210 |                                                          *           --       █████████║
-- 195 |                                                         *            --         ████╔══╝
-- 180 |                                                         *            --           ██║
-- 165 |                                                         *            --           ╚═╝
-- 150 |                                                        *             --
-- 135 |                                                        *             --
-- 120 |                                                        *             --
-- 105 |                                                       *              --
--  90 |                                                      *               --
--  75 |                                                     *                --
--  60 |                                                   **                 --
--  45 |                                                 **                   --
--  30 |                                               **           +++++     --
--  15 |                                          *****    +++++++++          --
--   0 | *****************************************+++++++++                   --
--     ------------------------------------------------------------------     --
--   d = 1        2        3        4        5        6        7        8     --
--------------------------------------------------------------------------------
--
-- * How does it work? Why is it fast?
--       The solver works by converting expressions to "Horner Normal Form".
--       This representation is special: x + y is represented in the same way
--       as y + x. This is what lets us check that two expressions are equal.
--       The implementation here is *sparse*, also, which is why it's faster
--       than the old implementation.
--
--       Want to learn more? Then this is the place for you:
import Polynomial.NormalForm
--
-- * Prove it!
--       The type of proofs we need are *homomorphisms*. They basically mean
--       that the operations on the normal form correspond to the operations
--       on expressions. Also, we don't use propositional equality: we use
--       any equivalence relation the user supplies.
--
--       Don't believe me? Check it out:
import Polynomial.Homomorphism
--
-- * How do I use it?
--       Copy the examples above! For the full solver, check out:
import Polynomial.Solver
--
-- * Wait! Don't!
--       The "full" solver lets you use different types for the coefficient
--       and carrier. You probably don't want that, unless you need the extra
--       efficiency. You'll want the *simple* solver:
import Polynomial.Simple.Solver
--
-- * Is that all?
--       No! As it happens, even the simple solver is complicated to use.
--       You'll *actually* want to use the reflection-based interface:
import Polynomial.Simple.Reflection
--
-- * And what about the step-by-step stuff?
--       That all uses the same underlying solver as the other stuff, with a
--       special *relation*. You can check that out here:
import Relation.Traced

max_stars_repo_name: mckeankylej/agda-ring-solver

max_issues_repo_name: mckeankylej/agda-ring-solver

max_forks_repo_name: mckeankylej/agda-ring-solver


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties satisfied by posets
------------------------------------------------------------------------

open import Relation.Binary

module Relation.Binary.Properties.Poset
         {p₁ p₂ p₃} (P : Poset p₁ p₂ p₃) where

open Relation.Binary.Poset P hiding (trans)
import Relation.Binary.NonStrictToStrict as Conv
open Conv _≈_ _≤_

------------------------------------------------------------------------
-- Posets can be turned into strict partial orders

strictPartialOrder : StrictPartialOrder _ _ _
strictPartialOrder = record
  { isStrictPartialOrder = record
    { isEquivalence = isEquivalence
    ; irrefl        = irrefl
    ; trans         = trans isPartialOrder
    ; <-resp-≈      = <-resp-≈ isEquivalence ≤-resp-≈
    }
  }

open StrictPartialOrder strictPartialOrder

ext: agda


text:
postulate
  f : {A B : Set₁} (C : Set) → A → B → C

module _ (A B C : Set) where
  test : (X : Set) → Set → Set → X
  test = f { A₁ = Set } { B₁ = Set }

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
--
-- Created by Dependently-Typed Lambda Calculus on 2020-09-23
-- Commerce
-- Author: dplaindoux
--

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

module Commerce where

open import Relation.Nullary using (Reflects; Dec; yes; no)
open import Data.Bool using (Bool; true; false)
open import Data.Nat using (ℕ; _+_; _≥?_; _≥_)
open import Agda.Builtin.Nat using (_-_)

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎; step-≡)

module Customer where
    record Account : Set where
        field
            balance : ℕ

    account : ℕ -> Account
    account n = record { balance = n }

    _↑_ : Account → ℕ → Account
    c ↑ n = account (Account.balance c + n)

    _↓_ : Account → ℕ → Account
    c ↓ n = account (Account.balance c - n )

    infixl 50 _↑_
    infixl 50 _↓_

module Product where
    record Item : Set where
        field
            price : ℕ

    data Basket : Set where
        ∅      : Basket
        _then_ : Item → Basket → Basket

    total : Basket → ℕ
    total ∅ = 0
    total (a then b) = Item.price a + total b

module Payment where
    open Customer
    open Product

    pay : (c : Account) → (p : Basket) → {Account.balance c ≥ total p} → Account
    pay c p = c ↓ total p

    module Front where
        pay? : Account → Basket → Account
        pay? c p with Account.balance c ≥? total p
        ... | yes proof = pay c p {proof}
        ... | no  _     = c

max_stars_repo_name: d-plaindoux/colca

max_issues_repo_name: d-plaindoux/colca

max_forks_repo_name: d-plaindoux/colca


text:
{-
This second-order signature was created from the following second-order syntax description:

syntax PropLog | PR

type
  * : 0-ary

term
  false : * | ⊥
  or    : *  *  ->  * | _∨_ l20
  true  : * | ⊤
  and   : *  *  ->  * | _∧_ l30
  not   : *  ->  * | ¬_ r50

theory
  (⊥U∨ᴸ) a |> or (false, a) = a
  (⊥U∨ᴿ) a |> or (a, false) = a
  (∨A) a b c |> or (or(a, b), c) = or (a, or(b, c))
  (∨C) a b |> or(a, b) = or(b, a)
  (⊤U∧ᴸ) a |> and (true, a) = a
  (⊤U∧ᴿ) a |> and (a, true) = a
  (∧A) a b c |> and (and(a, b), c) = and (a, and(b, c))
  (∧D∨ᴸ) a b c |> and (a, or (b, c)) = or (and(a, b), and(a, c))
  (∧D∨ᴿ) a b c |> and (or (a, b), c) = or (and(a, c), and(b, c))
  (⊥X∧ᴸ) a |> and (false, a) = false
  (⊥X∧ᴿ) a |> and (a, false) = false
  (¬N∨ᴸ) a |> or (not (a), a) = false
  (¬N∨ᴿ) a |> or (a, not (a)) = false
  (∧C) a b |> and(a, b) = and(b, a)
  (∨I) a |> or(a, a) = a
  (∧I) a |> and(a, a) = a
  (¬²) a |> not(not (a)) = a
  (∨D∧ᴸ) a b c |> or (a, and (b, c)) = and (or(a, b), or(a, c))
  (∨D∧ᴿ) a b c |> or (and (a, b), c) = and (or(a, c), or(b, c))
  (∨B∧ᴸ) a b |> or (and (a, b), a) = a
  (∨B∧ᴿ) a b |> or (a, and (a, b)) = a
  (∧B∨ᴸ) a b |> and (or (a, b), a) = a
  (∧B∨ᴿ) a b |> and (a, or (a, b)) = a
  (⊤X∨ᴸ) a |> or (true, a) = true
  (⊤X∨ᴿ) a |> or (a, true) = true
  (¬N∧ᴸ) a |> and (not (a), a) = false
  (¬N∧ᴿ) a |> and (a, not (a)) = false
  (DM∧) a b |> not (and (a, b)) = or  (not(a), not(b))
  (DM∨) a b |> not (or  (a, b)) = and (not(a), not(b))
-}

module PropLog.Signature where

open import SOAS.Context

open import SOAS.Common

open import SOAS.Syntax.Signature *T public
open import SOAS.Syntax.Build *T public

-- Operator symbols
data PRₒ : Set where
  falseₒ orₒ trueₒ andₒ notₒ : PRₒ

-- Term signature
PR:Sig : Signature PRₒ
PR:Sig = sig λ
  {  falseₒ  → ⟼₀ *
  ;  orₒ     → (⊢₀ *) , (⊢₀ *) ⟼₂ *
  ;  trueₒ   → ⟼₀ *
  ;  andₒ    → (⊢₀ *) , (⊢₀ *) ⟼₂ *
  ;  notₒ    → (⊢₀ *) ⟼₁ *
  }

open Signature PR:Sig public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
------------------------------------------------------------------------------
-- The gcd program is correct
------------------------------------------------------------------------------

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

-- This module proves the correctness of the gcd program using
-- the Euclid's algorithm.

-- N.B This module does not contain combined proofs, but it imports
-- modules which contain combined proofs.

module FOTC.Program.GCD.Partial.CorrectnessProofATP where

open import FOTC.Base
open import FOTC.Data.Nat.Divisibility.NotBy0.PropertiesATP using ( 0∤x ; x∣S→x≤S )
open import FOTC.Data.Nat.Type
open import FOTC.Program.GCD.Partial.CommonDivisorATP using ( gcdCD )
open import FOTC.Program.GCD.Partial.Definitions using ( x≢0≢y ; gcdSpec )
open import FOTC.Program.GCD.Partial.DivisibleATP using ( gcdDivisible )
open import FOTC.Program.GCD.Partial.GCD using ( gcd )

import FOTC.Program.GCD.Partial.GreatestAnyCommonDivisor
open module GreatestAnyCommonDivisorATP =
  FOTC.Program.GCD.Partial.GreatestAnyCommonDivisor x∣S→x≤S 0∤x
  using ( gcdGACD )

open import FOTC.Program.GCD.Partial.TotalityATP using ( gcd-N )

------------------------------------------------------------------------------
-- The gcd is correct.
postulate gcdCorrect : ∀ {m n} → N m → N n → x≢0≢y m n → gcdSpec m n (gcd m n)
{-# ATP prove gcdCorrect gcdCD gcdGACD gcd-N gcdDivisible #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
open import Agda.Primitive.Cubical

record Bad : IUniv where


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

open import Fragment.Algebra.Signature

module Fragment.Algebra.Homomorphism.Equivalence (Σ : Signature) where

open import Fragment.Algebra.Algebra Σ
open import Fragment.Algebra.Homomorphism.Base Σ
open import Fragment.Algebra.Homomorphism.Properties Σ
open import Fragment.Algebra.Homomorphism.Setoid Σ

open import Level using (Level; _⊔_)
open import Relation.Binary using (Setoid; IsEquivalence)
import Relation.Binary.Reasoning.Setoid as Reasoning

private
  variable
    a b c ℓ₁ ℓ₂ ℓ₃ : Level
    A : Algebra {a} {ℓ₁}
    B : Algebra {b} {ℓ₂}
    C : Algebra {c} {ℓ₃}

module _
  (A : Algebra {a} {ℓ₁})
  (B : Algebra {b} {ℓ₂})
  where

  infix 3 _≃_

  record _≃_ : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      _⃗ : A ⟿ B
      _⃖ : B ⟿ A

      invˡ : _⃗ ⊙ _⃖ ≗ id
      invʳ : _⃖ ⊙ _⃗ ≗ id

open _≃_ public

private

  ≃-refl : A ≃ A
  ≃-refl {A = A} = record { _⃗   = id
                          ; _⃖   = id
                          ; invˡ = λ {_} → refl
                          ; invʳ = λ {_} → refl
                          }
    where open Setoid ∥ A ∥/≈

  ≃-sym : A ≃ B → B ≃ A
  ≃-sym f = record { _⃗   = f ⃖
                   ; _⃖   = f ⃗
                   ; invˡ = invʳ f
                   ; invʳ = invˡ f
                   }

  ≃-inv : ∀ (g : B ≃ C) (f : A ≃ B)
          → (g ⃗ ⊙ f ⃗) ⊙ (f ⃖ ⊙ g ⃖) ≗ id
  ≃-inv {B = B} {C = C} g f = begin
      (g ⃗ ⊙ f ⃗) ⊙ (f ⃖ ⊙ g ⃖)
    ≈⟨ ⊙-assoc (g ⃗) (f ⃗) (f ⃖ ⊙ g ⃖) ⟩
      g ⃗ ⊙ (f ⃗ ⊙ (f ⃖ ⊙ g ⃖))
    ≈⟨ ⊙-congˡ (g ⃗) (f ⃗ ⊙ (f ⃖ ⊙ g ⃖)) ((f ⃗ ⊙ f ⃖) ⊙ g ⃖) (⊙-assoc (f ⃗) (f ⃖) (g ⃖)) ⟩
      g ⃗ ⊙ ((f ⃗ ⊙ f ⃖) ⊙ g ⃖)
    ≈⟨ ⊙-congˡ (g ⃗) ((f ⃗ ⊙ f ⃖) ⊙ g ⃖) (id ⊙ g ⃖) (⊙-congʳ (g ⃖) (f ⃗ ⊙ f ⃖) id (invˡ f)) ⟩
      g ⃗ ⊙ (id ⊙ g ⃖)
    ≈⟨ ⊙-congˡ (g ⃗) (id ⊙ g ⃖) (g ⃖) (id-unitˡ {f = g ⃖}) ⟩
      g ⃗ ⊙ g ⃖
    ≈⟨ invˡ g ⟩
      id
    ∎
    where open Reasoning (C ⟿ C /≗)

  ≃-trans : A ≃ B → B ≃ C → A ≃ C
  ≃-trans f g = record { _⃗   = g ⃗ ⊙ f ⃗
                       ; _⃖   = f ⃖ ⊙ g ⃖
                       ; invˡ = ≃-inv g f
                       ; invʳ = ≃-inv (≃-sym f) (≃-sym g)
                       }

  ≃-isEquivalence : IsEquivalence (_≃_ {a} {ℓ₁} {a} {ℓ₁})
  ≃-isEquivalence =
    record { refl  = ≃-refl
           ; sym   = ≃-sym
           ; trans = ≃-trans
           }

≃-setoid : ∀ {a ℓ} → Setoid _ _
≃-setoid {a} {ℓ} = record { Carrier       = Algebra {a} {ℓ}
                          ; _≈_           = _≃_ {a} {ℓ} {a} {ℓ}
                          ; isEquivalence = ≃-isEquivalence
                          }

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
module Cat where

open import Agda.Primitive
open import CS410-Prelude
open import CS410-Nat
open import CS410-Monoid
open import CS410-Vec

record Cat {k}{l}(O : Set k)(_>>_ : O -> O -> Set l) : Set (lsuc (k ⊔ l)) where
  field
    -- OPERATIONS ---------------------------------------------------------
    iden  : {X : O} -> X >> X
    comp  : {R S T : O} -> S >> T -> R >> S -> R >> T
    -- KLUDGE -------------------------------------------------------------
    Eq : {S T : O} -> S >> T -> S >> T -> Set l
    -- LAWS ---------------------------------------------------------------
    idenL : {S T : O}(f : S >> T) -> Eq (comp iden f) f
    idenR : {S T : O}(f : S >> T) -> Eq (comp f iden) f
    assoc : {Q R S T : O}(f : S >> T)(g : R >> S)(h : Q >> R) ->
            Eq (comp f (comp g h)) (comp (comp f g) h)

SetCat : Cat Set (\ S T -> S -> T)
SetCat = record
           { iden = id
           ; comp = _o_
           ; Eq    = \ f g -> forall x -> f x == g x
           ; idenL = λ {S} {T} f x → refl
           ; idenR = λ {S} {T} f x → refl
           ; assoc = λ {Q} {R} {S} {T} f g h x → refl
           }

N>=Cat : Cat Nat _N>=_
N>=Cat = record
           { iden = \ {n} -> N>=refl n
           ; comp = \ {l}{m}{n} -> N>=trans l m n
           ; Eq = \ _ _ -> One
           ; idenL = λ {S} {T} f → <>
           ; idenR = λ {S} {T} f → <>
           ; assoc = λ {Q} {R} {S} {T} f g h → <>
           } where
           N>=refl : (n : Nat) -> n N>= n
           N>=refl zero = <>
           N>=refl (suc n) = N>=refl n
           N>=trans : forall l m n -> m N>= n -> l N>= m -> l N>= n
           N>=trans l m zero mn lm = <>
           N>=trans l zero (suc n) () lm
           N>=trans zero (suc m) (suc n) mn ()
           N>=trans (suc l) (suc m) (suc n) mn lm = N>=trans l m n mn lm

MonCat : forall {X} -> Monoid X -> Cat One \ _ _ -> X
MonCat M = record
             { iden = e
             ; comp = op
             ; Eq = _==_
             ; idenL = lunit
             ; idenR = runit
             ; assoc = assoc
             } where open Monoid M

record Functor {k l}{ObjS : Set k}{_>S>_ : ObjS -> ObjS -> Set l}
               {m n}{ObjT : Set m}{_>T>_ : ObjT -> ObjT -> Set n}
               (CS : Cat ObjS _>S>_)(CT : Cat ObjT _>T>_)
               : Set (lsuc (k ⊔ l ⊔ m ⊔ n)) where
  open Cat
  field
    -- OPERATIONS ---------------------------------------------------------
    Map      : ObjS -> ObjT
    map      : {A B : ObjS} -> A >S> B -> Map A >T> Map B
    -- LAWS ---------------------------------------------------------------
    mapId    : {A : ObjS} -> Eq CT (map (iden CS {A})) (iden CT {Map A})
    mapComp  : {A B C : ObjS}(f : B >S> C)(g : A >S> B) ->
               Eq CT (map (comp CS f g)) (comp CT (map f) (map g))
    mapEq    : {A B : ObjS}{f g : A >S> B} ->
               Eq CS f g -> Eq CT (map f) (map g)

data List (X : Set) : Set where  -- X scopes over the whole declaration...
  []    : List X                 -- ...so you can use it here...
  _::_  : X -> List X -> List X  -- ...and here.
infixr 3 _::_

listMap : {A B : Set} → (A → B) → List A → List B
listMap f [] = []
listMap f (a :: as) = f a :: listMap f as

list : Functor SetCat SetCat
list = record
  { Map = List
  ; map = listMap
  ; mapId = {!!}
  ; mapComp = {!!}
  ; mapEq = {!!}
  }

{-
goo : Functor (MonCat +Mon) SetCat
goo = ?
-}

hoo : (X : Set) -> Functor N>=Cat SetCat
hoo X = record
  { Map = Vec X
  ; map = {!!}
  ; mapId = {!!}
  ; mapComp = {!!}
  ; mapEq = {!!}
  }


text:
module Relation.Equality where

open import Data.Product

-- Identity Types
--

{-
  The type of identifications of two (x y : A).

  While this can be read as propositional equality, in HoTT identity
  can be (and is) elevated to a data type.
-}
data _≡_ {a}{A : Set a}(x : A) : A → Set a where
  refl : x ≡ x

cong : ∀ {a b} {A : Set a}{B : Set b} (f : A → B) {x y} → x ≡ y → f x ≡ f y
cong f refl = refl

-- Path Induction over the Identity Type
--
ind₌ : ∀ {a c}{A : Set a} → (C : (x y : A) → (x ≡ y) → Set c) → ((x : A) → C x x refl) → (x y : A) → (p : x ≡ y) → C x y p
ind₌ C c x .x refl = c x

max_stars_repo_name: CodaFi/HoTT-Exercises

max_issues_repo_name: CodaFi/HoTT-Exercises

max_forks_repo_name: CodaFi/HoTT-Exercises


text:
{-

Basic theory about h-levels/n-types:

- Basic properties of isContr, isProp and isSet (definitions are in Prelude)

- Hedberg's theorem can be found in Cubical/Relation/Nullary/DecidableEq

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Foundations.HLevels where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Structure
open import Cubical.Functions.FunExtEquiv
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Path
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence using (ua ; univalence)

open import Cubical.Data.Sigma
open import Cubical.Data.Nat   using (ℕ; zero; suc; _+_; +-zero; +-comm)

HLevel : Type₀
HLevel = ℕ

private
  variable
    ℓ ℓ' ℓ'' ℓ''' : Level
    A : Type ℓ
    B : A → Type ℓ
    C : (x : A) → B x → Type ℓ
    D : (x : A) (y : B x) → C x y → Type ℓ
    E : (x : A) (y : B x) → (z : C x y) → D x y z → Type ℓ
    w x y z : A
    n : HLevel

isOfHLevel : HLevel → Type ℓ → Type ℓ
isOfHLevel 0 A = isContr A
isOfHLevel 1 A = isProp A
isOfHLevel (suc (suc n)) A = (x y : A) → isOfHLevel (suc n) (x ≡ y)

isOfHLevelFun : (n : HLevel) {A : Type ℓ} {B : Type ℓ'} (f : A → B) → Type (ℓ-max ℓ ℓ')
isOfHLevelFun n f = ∀ b → isOfHLevel n (fiber f b)

TypeOfHLevel : ∀ ℓ → HLevel → Type (ℓ-suc ℓ)
TypeOfHLevel ℓ n = TypeWithStr ℓ (isOfHLevel n)

hProp hSet hGroupoid h2Groupoid : ∀ ℓ → Type (ℓ-suc ℓ)
hProp      ℓ = TypeOfHLevel ℓ 1
hSet       ℓ = TypeOfHLevel ℓ 2
hGroupoid  ℓ = TypeOfHLevel ℓ 3
h2Groupoid ℓ = TypeOfHLevel ℓ 4

-- lower h-levels imply higher h-levels

isOfHLevelSuc : (n : HLevel) → isOfHLevel n A → isOfHLevel (suc n) A
isOfHLevelSuc 0 = isContr→isProp
isOfHLevelSuc 1 = isProp→isSet
isOfHLevelSuc (suc (suc n)) h a b = isOfHLevelSuc (suc n) (h a b)

isSet→isGroupoid : isSet A → isGroupoid A
isSet→isGroupoid = isOfHLevelSuc 2

isGroupoid→is2Groupoid : isGroupoid A → is2Groupoid A
isGroupoid→is2Groupoid = isOfHLevelSuc 3

isOfHLevelPlus : (m : HLevel) → isOfHLevel n A → isOfHLevel (m + n) A
isOfHLevelPlus zero hA = hA
isOfHLevelPlus (suc m) hA = isOfHLevelSuc _ (isOfHLevelPlus m hA)

isOfHLevelPlus' : (m : HLevel) → isOfHLevel m A → isOfHLevel (m + n) A
isOfHLevelPlus' {A = A} {n = n} m hA = subst (λ m → isOfHLevel m A) (+-comm n m) (isOfHLevelPlus n hA )

isContr→isOfHLevel : (n : HLevel) → isContr A → isOfHLevel n A
isContr→isOfHLevel {A = A} n cA = isOfHLevelPlus' 0 cA

isProp→isOfHLevelSuc : (n : HLevel) → isProp A → isOfHLevel (suc n) A
isProp→isOfHLevelSuc {A = A} n pA = isOfHLevelPlus' 1 pA

-- hlevel of path and dependent path types

isProp→isContrPath : isProp A → (x y : A) → isContr (x ≡ y)
isProp→isContrPath h x y = h x y , isProp→isSet h x y _

isContr→isContrPath : isContr A → (x y : A) → isContr (x ≡ y)
isContr→isContrPath cA = isProp→isContrPath (isContr→isProp cA)

isOfHLevelPath' : (n : HLevel) → isOfHLevel (suc n) A → (x y : A) → isOfHLevel n (x ≡ y)
isOfHLevelPath' 0 = isProp→isContrPath
isOfHLevelPath' (suc n) h x y = h x y

isOfHLevelPath'⁻ : (n : HLevel) → ((x y : A) → isOfHLevel n (x ≡ y)) → isOfHLevel (suc n) A
isOfHLevelPath'⁻ zero h x y = h x y .fst
isOfHLevelPath'⁻ (suc n) h = h

isOfHLevelPath : (n : HLevel) → isOfHLevel n A → (x y : A) → isOfHLevel n (x ≡ y)
isOfHLevelPath 0 h x y = isContr→isContrPath h x y
isOfHLevelPath (suc n) h x y = isOfHLevelSuc n (isOfHLevelPath' n h x y)

isOfHLevelPathP' : {A : I → Type ℓ} (n : HLevel)
                   → isOfHLevel (suc n) (A i1)
                   → (x : A i0) (y : A i1) → isOfHLevel n (PathP A x y)
isOfHLevelPathP' {A = A} n h x y = transport⁻ (λ i → isOfHLevel n (PathP≡Path A x y i))
                                              (isOfHLevelPath' n h _ _)

isOfHLevelPathP : {A : I → Type ℓ} (n : HLevel)
                  → isOfHLevel n (A i1)
                  → (x : A i0) (y : A i1) → isOfHLevel n (PathP A x y)
isOfHLevelPathP {A = A} n h x y = transport⁻ (λ i → isOfHLevel n (PathP≡Path A x y i))
                                             (isOfHLevelPath n h _ _)

-- h-level of isOfHLevel

isPropIsOfHLevel : (n : HLevel) → isProp (isOfHLevel n A)
isPropIsOfHLevel 0 = isPropIsContr
isPropIsOfHLevel 1 = isPropIsProp
isPropIsOfHLevel (suc (suc n)) f g i a b =
  isPropIsOfHLevel (suc n) (f a b) (g a b) i

isPropIsSet : isProp (isSet A)
isPropIsSet = isPropIsOfHLevel 2

isPropIsGroupoid : isProp (isGroupoid A)
isPropIsGroupoid = isPropIsOfHLevel 3

isPropIs2Groupoid : isProp (is2Groupoid A)
isPropIs2Groupoid = isPropIsOfHLevel 4

TypeOfHLevel≡ : (n : HLevel) {X Y : TypeOfHLevel ℓ n} → ⟨ X ⟩ ≡ ⟨ Y ⟩ → X ≡ Y
TypeOfHLevel≡ n = Σ≡Prop (λ _ → isPropIsOfHLevel n)

-- Fillers for cubes from h-level

isSet→isSet' : isSet A → isSet' A
isSet→isSet' {A = A} Aset a₀₋ a₁₋ a₋₀ a₋₁ =
  transport⁻ (PathP≡Path (λ i → a₋₀ i ≡ a₋₁ i) a₀₋ a₁₋) (Aset _ _ _ _)

isSet'→isSet : isSet' A → isSet A
isSet'→isSet {A = A} Aset' x y p q = Aset' p q refl refl

isSet→SquareP :
  {A : I → I → Type ℓ}
  (isSet : (i j : I) → isSet (A i j))
  {a₀₀ : A i0 i0} {a₀₁ : A i0 i1} (a₀₋ : PathP (λ j → A i0 j) a₀₀ a₀₁)
  {a₁₀ : A i1 i0} {a₁₁ : A i1 i1} (a₁₋ : PathP (λ j → A i1 j) a₁₀ a₁₁)
  (a₋₀ : PathP (λ i → A i i0) a₀₀ a₁₀) (a₋₁ : PathP (λ i → A i i1) a₀₁ a₁₁)
  → SquareP A a₀₋ a₁₋ a₋₀ a₋₁
isSet→SquareP isset a₀₋ a₁₋ a₋₀ a₋₁ =
  transport (sym (PathP≡Path _ _ _))
            (isOfHLevelPathP' 1 (isset _ _) _ _ _ _ )

isGroupoid→isGroupoid' : isGroupoid A → isGroupoid' A
isGroupoid→isGroupoid' {A = A} Agpd a₀₋₋ a₁₋₋ a₋₀₋ a₋₁₋ a₋₋₀ a₋₋₁ =
  transport⁻ (PathP≡Path (λ i → Square (a₋₀₋ i) (a₋₁₋ i) (a₋₋₀ i) (a₋₋₁ i)) a₀₋₋ a₁₋₋)
    (isGroupoid→isPropSquare _ _ _ _ _ _)
  where
  isGroupoid→isPropSquare :
    {a₀₀ a₀₁ : A} (a₀₋ : a₀₀ ≡ a₀₁)
    {a₁₀ a₁₁ : A} (a₁₋ : a₁₀ ≡ a₁₁)
    (a₋₀ : a₀₀ ≡ a₁₀) (a₋₁ : a₀₁ ≡ a₁₁)
    → isProp (Square a₀₋ a₁₋ a₋₀ a₋₁)
  isGroupoid→isPropSquare a₀₋ a₁₋ a₋₀ a₋₁ =
    transport⁻
      (cong isProp (PathP≡Path (λ i → a₋₀ i ≡ a₋₁ i) a₀₋ a₁₋))
      (Agpd _ _ _ _)

isGroupoid'→isGroupoid : isGroupoid' A → isGroupoid A
isGroupoid'→isGroupoid Agpd' x y p q r s = Agpd' r s refl refl refl refl

-- hlevels are preserved by retracts (and consequently equivalences)

isContrRetract
  : ∀ {B : Type ℓ}
  → (f : A → B) (g : B → A)
  → (h : retract f g)
  → (v : isContr B) → isContr A
fst (isContrRetract f g h (b , p)) = g b
snd (isContrRetract f g h (b , p)) x = (cong g (p (f x))) ∙ (h x)

isPropRetract
  : {B : Type ℓ}
  (f : A → B) (g : B → A)
  (h : (x : A) → g (f x) ≡ x)
  → isProp B → isProp A
isPropRetract f g h p x y i =
  hcomp
    (λ j → λ
      { (i = i0) → h x j
      ; (i = i1) → h y j})
    (g (p (f x) (f y) i))

isSetRetract
  : {B : Type ℓ}
  (f : A → B) (g : B → A)
  (h : (x : A) → g (f x) ≡ x)
  → isSet B → isSet A
isSetRetract f g h set x y p q i j =
  hcomp (λ k → λ { (i = i0) → h (p j) k
                 ; (i = i1) → h (q j) k
                 ; (j = i0) → h x k
                 ; (j = i1) → h y k})
        (g (set (f x) (f y)
                (cong f p) (cong f q) i j))

isGroupoidRetract
  : {B : Type ℓ}
  (f : A → B) (g : B → A)
  (h : (x : A) → g (f x) ≡ x)
  → isGroupoid B → isGroupoid A
isGroupoidRetract f g h grp x y p q P Q i j k =
  hcomp ((λ l → λ { (i = i0) → h (P j k) l
                  ; (i = i1) → h (Q j k) l
                  ; (j = i0) → h (p k) l
                  ; (j = i1) → h (q k) l
                  ; (k = i0) → h x l
                  ; (k = i1) → h y l}))
       (g (grp (f x) (f y) (cong f p) (cong f q)
                           (cong (cong f) P) (cong (cong f) Q) i j k))

is2GroupoidRetract
  : {B : Type ℓ}
  (f : A → B) (g : B → A)
  (h : (x : A) → g (f x) ≡ x)
  → is2Groupoid B → is2Groupoid A
is2GroupoidRetract f g h grp x y p q P Q R S i j k l =
  hcomp (λ r → λ { (i = i0) → h (R j k l) r
                 ; (i = i1) → h (S j k l) r
                 ; (j = i0) → h (P k l) r
                 ; (j = i1) → h (Q k l) r
                 ; (k = i0) → h (p l) r
                 ; (k = i1) → h (q l) r
                 ; (l = i0) → h x r
                 ; (l = i1) → h y r})
       (g (grp (f x) (f y) (cong f p) (cong f q)
               (cong (cong f) P) (cong (cong f) Q)
               (cong (cong (cong f)) R) (cong (cong (cong f)) S) i j k l))

isOfHLevelRetract
  : (n : HLevel) {B : Type ℓ}
  (f : A → B) (g : B → A)
  (h : (x : A) → g (f x) ≡ x)
  → isOfHLevel n B → isOfHLevel n A
isOfHLevelRetract 0 = isContrRetract
isOfHLevelRetract 1 = isPropRetract
isOfHLevelRetract 2 = isSetRetract
isOfHLevelRetract 3 = isGroupoidRetract
isOfHLevelRetract 4 = is2GroupoidRetract
isOfHLevelRetract (suc (suc (suc (suc (suc n))))) f g h ofLevel x y p q P Q R S =
  isOfHLevelRetract (suc n) (cong (cong (cong (cong f))))
                    (λ s i j k l →
                      hcomp (λ r → λ { (i = i0) → h (R j k l) r
                                     ; (i = i1) → h (S j k l) r
                                     ; (j = i0) → h (P k l) r
                                     ; (j = i1) → h (Q k l) r
                                     ; (k = i0) → h (p l) r
                                     ; (k = i1) → h (q l) r
                                     ; (l = i0) → h x r
                                     ; (l = i1) → h y r})
                            (g (s i j k l)))
                    (λ s i j k l m →
                    hcomp (λ n → λ { (i = i1) → s j k l m
                                   ; (j = i0) → h (R k l m) (i ∨ n)
                                   ; (j = i1) → h (S k l m) (i ∨ n)
                                   ; (k = i0) → h (P l m) (i ∨ n)
                                   ; (k = i1) → h (Q l m) (i ∨ n)
                                   ; (l = i0) → h (p m) (i ∨ n)
                                   ; (l = i1) → h (q m) (i ∨ n)
                                   ; (m = i0) → h x (i ∨ n)
                                   ; (m = i1) → h y (i ∨ n) })
                          (h (s j k l m) i))
                    (ofLevel (f x) (f y)
                             (cong f p) (cong f q)
                             (cong (cong f) P) (cong (cong f) Q)
                             (cong (cong (cong f)) R) (cong (cong (cong f)) S))

isOfHLevelRetractFromIso : {A : Type ℓ} {B : Type ℓ'} (n : HLevel) → Iso A B → isOfHLevel n B → isOfHLevel n A
isOfHLevelRetractFromIso n e hlev = isOfHLevelRetract n (Iso.fun e) (Iso.inv e) (Iso.leftInv e) hlev

isOfHLevelRespectEquiv : {A : Type ℓ} {B : Type ℓ'} → (n : HLevel) → A ≃ B → isOfHLevel n A → isOfHLevel n B
isOfHLevelRespectEquiv n eq = isOfHLevelRetract n (invEq eq) (eq .fst) (retEq eq)

isContrRetractOfConstFun : {A : Type ℓ} {B : Type ℓ'} (b₀ : B)
   → Σ[ f ∈ (B → A) ] ((x : A) → (f ∘ (λ _ → b₀)) x ≡ x)
   → isContr A
fst (isContrRetractOfConstFun b₀ ret) = ret .fst b₀
snd (isContrRetractOfConstFun b₀ ret) y = ret .snd y

-- h-level of Σ-types

isContrΣ : isContr A → ((x : A) → isContr (B x)) → isContr (Σ A B)
isContrΣ {A = A} {B = B} (a , p) q =
  let h : (x : A) (y : B x) → (q x) .fst ≡ y
      h x y = (q x) .snd y
  in (( a , q a .fst)
     , ( λ x i → p (x .fst) i
       , h (p (x .fst) i) (transp (λ j → B (p (x .fst) (i ∨ ~ j))) i (x .snd)) i))

isContrΣ′ : (ca : isContr A) → isContr (B (fst ca)) → isContr (Σ A B)
isContrΣ′ ca cb = isContrΣ ca (λ x → subst _ (snd ca x) cb)

section-Σ≡Prop
  : (pB : (x : A) → isProp (B x)) {u v : Σ A B}
  → section (Σ≡Prop pB {u} {v}) (cong fst)
section-Σ≡Prop {A = A} pB {u} {v} p j i =
  (p i .fst) , isProp→PathP (λ i → isOfHLevelPath 1 (pB (fst (p i)))
                                       (Σ≡Prop pB {u} {v} (cong fst p) i .snd)
                                       (p i .snd) )
                                       refl refl i j

isEquiv-Σ≡Prop
  : (pB : (x : A) → isProp (B x)) {u v : Σ A B}
  → isEquiv (Σ≡Prop pB {u} {v})
isEquiv-Σ≡Prop {A = A} pB {u} {v} = isoToIsEquiv (iso (Σ≡Prop pB) (cong fst) (section-Σ≡Prop pB) (λ _ → refl))

isPropΣ : isProp A → ((x : A) → isProp (B x)) → isProp (Σ A B)
isPropΣ pA pB t u = Σ≡Prop pB (pA (t .fst) (u .fst))

isOfHLevelΣ : ∀ n → isOfHLevel n A → ((x : A) → isOfHLevel n (B x))
                  → isOfHLevel n (Σ A B)
isOfHLevelΣ 0 = isContrΣ
isOfHLevelΣ 1 = isPropΣ
isOfHLevelΣ {B = B} (suc (suc n)) h1 h2 x y =
  isOfHLevelRetractFromIso (suc n)
    (invIso (IsoΣPathTransportPathΣ _ _))
    (isOfHLevelΣ (suc n) (h1 (fst x) (fst y)) λ x → h2 _ _ _)

isSetΣ : isSet A → ((x : A) → isSet (B x)) → isSet (Σ A B)
isSetΣ = isOfHLevelΣ 2

isGroupoidΣ : isGroupoid A → ((x : A) → isGroupoid (B x)) → isGroupoid (Σ A B)
isGroupoidΣ = isOfHLevelΣ 3

is2GroupoidΣ : is2Groupoid A → ((x : A) → is2Groupoid (B x)) → is2Groupoid (Σ A B)
is2GroupoidΣ = isOfHLevelΣ 4

-- h-level of ×

isProp× : {A : Type ℓ} {B : Type ℓ'} → isProp A → isProp B → isProp (A × B)
isProp× pA pB = isPropΣ pA (λ _ → pB)

isProp×2 : {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''}
         → isProp A → isProp B → isProp C → isProp (A × B × C)
isProp×2 pA pB pC = isProp× pA (isProp× pB pC)

isProp×3 : {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''} {D : Type ℓ'''}
         → isProp A → isProp B → isProp C → isProp D → isProp (A × B × C × D)
isProp×3 pA pB pC pD = isProp×2 pA pB (isProp× pC pD)

isOfHLevel× : ∀ {A : Type ℓ} {B : Type ℓ'} n → isOfHLevel n A → isOfHLevel n B
                                             → isOfHLevel n (A × B)
isOfHLevel× n hA hB = isOfHLevelΣ n hA (λ _ → hB)

isSet× : ∀ {A : Type ℓ} {B : Type ℓ'} → isSet A → isSet B → isSet (A × B)
isSet× = isOfHLevel× 2

isGroupoid× : ∀ {A : Type ℓ} {B : Type ℓ'} → isGroupoid A → isGroupoid B
                                           → isGroupoid (A × B)
isGroupoid× = isOfHLevel× 3

is2Groupoid× : ∀ {A : Type ℓ} {B : Type ℓ'} → is2Groupoid A → is2Groupoid B
                                            → is2Groupoid (A × B)
is2Groupoid× = isOfHLevel× 4

-- h-level of Π-types

isOfHLevelΠ : ∀ n → ((x : A) → isOfHLevel n (B x))
                  → isOfHLevel n ((x : A) → B x)
isOfHLevelΠ 0 h = (λ x → fst (h x)) , λ f i y → snd (h y) (f y) i
isOfHLevelΠ 1 h f g i x = (h x) (f x) (g x) i
isOfHLevelΠ 2 h f g F G i j z = h z (f z) (g z) (funExt⁻ F z) (funExt⁻ G z) i j
isOfHLevelΠ 3 h f g p q P Q i j k z =
  h z (f z) (g z)
      (funExt⁻ p z) (funExt⁻ q z)
      (cong (λ f → funExt⁻ f z) P) (cong (λ f → funExt⁻ f z) Q) i j k
isOfHLevelΠ 4 h f g p q P Q R S i j k l z =
  h z (f z) (g z)
      (funExt⁻ p z) (funExt⁻ q z)
      (cong (λ f → funExt⁻ f z) P) (cong (λ f → funExt⁻ f z) Q)
      (cong (cong (λ f → funExt⁻ f z)) R) (cong (cong (λ f → funExt⁻ f z)) S) i j k l
isOfHLevelΠ (suc (suc (suc (suc (suc n))))) h f g p q P Q R S =
  isOfHLevelRetract (suc n)
    (cong (cong (cong funExt⁻))) (cong (cong (cong funExt))) (λ _ → refl)
    (isOfHLevelΠ (suc (suc (suc (suc n)))) (λ x → h x (f x) (g x))
                  (funExt⁻ p) (funExt⁻ q)
                  (cong funExt⁻ P) (cong funExt⁻ Q)
                  (cong (cong funExt⁻) R) (cong (cong funExt⁻) S))

isPropΠ : (h : (x : A) → isProp (B x)) → isProp ((x : A) → B x)
isPropΠ = isOfHLevelΠ 1

isPropΠ2 : (h : (x : A) (y : B x) → isProp (C x y))
         → isProp ((x : A) (y : B x) → C x y)
isPropΠ2 h = isPropΠ λ x → isPropΠ λ y → h x y

isPropΠ3 : (h : (x : A) (y : B x) (z : C x y) → isProp (D x y z))
         → isProp ((x : A) (y : B x) (z : C x y) → D x y z)
isPropΠ3 h = isPropΠ λ x → isPropΠ λ y → isPropΠ λ z → h x y z

isPropΠ4 : (h : (x : A) (y : B x) (z : C x y) (w : D x y z) → isProp (E x y z w))
            → isProp ((x : A) (y : B x) (z : C x y) (w : D x y z) → E x y z w)
isPropΠ4 h = isPropΠ λ _ → isPropΠ3 λ _ → h _ _

isPropImplicitΠ : (h : (x : A) → isProp (B x)) → isProp ({x : A} → B x)
isPropImplicitΠ h f g i {x} = h x (f {x}) (g {x}) i

isProp→ : {A : Type ℓ} {B : Type ℓ'} → isProp B → isProp (A → B)
isProp→ pB = isPropΠ λ _ → pB

isSetΠ : ((x : A) → isSet (B x)) → isSet ((x : A) → B x)
isSetΠ = isOfHLevelΠ 2

isSetΠ2 : (h : (x : A) (y : B x) → isSet (C x y))
        → isSet ((x : A) (y : B x) → C x y)
isSetΠ2 h = isSetΠ λ x → isSetΠ λ y → h x y

isSetΠ3 : (h : (x : A) (y : B x) (z : C x y) → isSet (D x y z))
         → isSet ((x : A) (y : B x) (z : C x y) → D x y z)
isSetΠ3 h = isSetΠ λ x → isSetΠ λ y → isSetΠ λ z → h x y z

isGroupoidΠ : ((x : A) → isGroupoid (B x)) → isGroupoid ((x : A) → B x)
isGroupoidΠ = isOfHLevelΠ 3

isGroupoidΠ2 : (h : (x : A) (y : B x) → isGroupoid (C x y)) → isGroupoid ((x : A) (y : B x) → C x y)
isGroupoidΠ2 h = isGroupoidΠ λ _ → isGroupoidΠ λ _ → h _ _

isGroupoidΠ3 : (h : (x : A) (y : B x) (z : C x y) → isGroupoid (D x y z))
            → isGroupoid ((x : A) (y : B x) (z : C x y) → D x y z)
isGroupoidΠ3 h = isGroupoidΠ λ _ → isGroupoidΠ2 λ _ → h _ _

isGroupoidΠ4 : (h : (x : A) (y : B x) (z : C x y) (w : D x y z) → isGroupoid (E x y z w))
            → isGroupoid ((x : A) (y : B x) (z : C x y) (w : D x y z) → E x y z w)
isGroupoidΠ4 h = isGroupoidΠ λ _ → isGroupoidΠ3 λ _ → h _ _

is2GroupoidΠ : ((x : A) → is2Groupoid (B x)) → is2Groupoid ((x : A) → B x)
is2GroupoidΠ = isOfHLevelΠ 4

isOfHLevelΠ⁻ : ∀ {A : Type ℓ} {B : Type ℓ'} n
             → isOfHLevel n (A → B) → (A → isOfHLevel n B)
isOfHLevelΠ⁻ 0 h x = fst h x , λ y → funExt⁻ (snd h (const y)) x
isOfHLevelΠ⁻ 1 h x y z = funExt⁻ (h (const y) (const z)) x
isOfHLevelΠ⁻ (suc (suc n)) h x y z =
  isOfHLevelΠ⁻ (suc n) (subst (isOfHLevel (suc n)) (sym funExtPath) (h (const y) (const z))) x

-- h-level of A ≃ B and A ≡ B

isOfHLevel≃
  : ∀ n {A : Type ℓ} {B : Type ℓ'}
  → (hA : isOfHLevel n A) (hB : isOfHLevel n B) → isOfHLevel n (A ≃ B)
isOfHLevel≃ zero {A = A} {B = B} hA hB = isContr→Equiv hA hB , contr
  where
  contr : (y : A ≃ B) → isContr→Equiv hA hB ≡ y
  contr y = Σ≡Prop isPropIsEquiv (funExt (λ a → snd hB (fst y a)))

isOfHLevel≃ (suc n) {A = A} {B = B} hA hB =
  isOfHLevelΣ (suc n) (isOfHLevelΠ _ λ _ → hB)
              λ a → isOfHLevelPlus' 1 (isPropIsEquiv a)

isOfHLevel≡ : ∀ n → {A B : Type ℓ} (hA : isOfHLevel n A) (hB : isOfHLevel n B) →
  isOfHLevel n (A ≡ B)
isOfHLevel≡ n hA hB = isOfHLevelRetract n (fst univalence) ua (secEq univalence) (isOfHLevel≃ n hA hB)

isOfHLevel⁺≃ₗ
  : ∀ n {A : Type ℓ} {B : Type ℓ'}
  → isOfHLevel (suc n) A → isOfHLevel (suc n) (A ≃ B)
isOfHLevel⁺≃ₗ zero pA e = isOfHLevel≃ 1 pA (isOfHLevelRespectEquiv 1 e pA) e
isOfHLevel⁺≃ₗ (suc n) hA e = isOfHLevel≃ m hA (isOfHLevelRespectEquiv m e hA) e
  where
  m = suc (suc n)

isOfHLevel⁺≃ᵣ
  : ∀ n {A : Type ℓ} {B : Type ℓ'}
  → isOfHLevel (suc n) B → isOfHLevel (suc n) (A ≃ B)
isOfHLevel⁺≃ᵣ zero pB e
  = isOfHLevel≃ 1 (isPropRetract (e .fst) (invEq e) (secEq e) pB) pB e
isOfHLevel⁺≃ᵣ (suc n) hB e
  = isOfHLevel≃ m (isOfHLevelRetract m (e .fst) (invEq e) (secEq e) hB) hB e
  where
  m = suc (suc n)

isOfHLevel⁺≡ₗ
  : ∀ n → {A B : Type ℓ}
  → isOfHLevel (suc n) A → isOfHLevel (suc n) (A ≡ B)
isOfHLevel⁺≡ₗ zero pA P = isOfHLevel≡ 1 pA (subst isProp P pA) P
isOfHLevel⁺≡ₗ (suc n) hA P
  = isOfHLevel≡ m hA (subst (isOfHLevel m) P hA) P
  where
  m = suc (suc n)

isOfHLevel⁺≡ᵣ
  : ∀ n → {A B : Type ℓ}
  → isOfHLevel (suc n) B → isOfHLevel (suc n) (A ≡ B)
isOfHLevel⁺≡ᵣ zero pB P = isOfHLevel≡ 1 (subst⁻ isProp P pB) pB P
isOfHLevel⁺≡ᵣ (suc n) hB P
  = isOfHLevel≡ m (subst⁻ (isOfHLevel m) P hB) hB P
  where
  m = suc (suc n)

-- h-level of TypeOfHLevel

isPropHContr : isProp (TypeOfHLevel ℓ 0)
isPropHContr x y = Σ≡Prop (λ _ → isPropIsContr) (isOfHLevel≡ 0 (x .snd) (y .snd) .fst)

isOfHLevelTypeOfHLevel : ∀ n → isOfHLevel (suc n) (TypeOfHLevel ℓ n)
isOfHLevelTypeOfHLevel zero = isPropHContr
isOfHLevelTypeOfHLevel (suc n) (X , a) (Y , b) =
  isOfHLevelRetract (suc n) (cong fst) (Σ≡Prop λ _ → isPropIsOfHLevel (suc n))
    (section-Σ≡Prop λ _ → isPropIsOfHLevel (suc n))
    (isOfHLevel≡ (suc n) a b)

isSetHProp : isSet (hProp ℓ)
isSetHProp = isOfHLevelTypeOfHLevel 1

-- h-level of lifted type

isOfHLevelLift : ∀ {ℓ ℓ'} (n : HLevel) {A : Type ℓ} → isOfHLevel n A → isOfHLevel n (Lift {j = ℓ'} A)
isOfHLevelLift n = isOfHLevelRetract n lower lift λ _ → refl

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

-- More consequences of isProp and isContr

inhProp→isContr : A → isProp A → isContr A
inhProp→isContr x h = x , h x

extend : isContr A → (∀ φ → (u : Partial φ A) → Sub A φ u)
extend (x , p) φ u = inS (hcomp (λ { j (φ = i1) → p (u 1=1) j }) x)

isContrPartial→isContr : ∀ {ℓ} {A : Type ℓ}
                       → (extend : ∀ φ → Partial φ A → A)
                       → (∀ u → u ≡ (extend i1 λ { _ → u}))
                       → isContr A
isContrPartial→isContr {A = A} extend law
  = ex , λ y → law ex ∙ (λ i → Aux.v y i) ∙ sym (law y)
    where ex = extend i0 empty
          module Aux (y : A) (i : I) where
            φ = ~ i ∨ i
            u : Partial φ A
            u = λ { (i = i0) → ex ; (i = i1) → y }
            v = extend φ u

-- Dependent h-level over a type

isOfHLevelDep : HLevel → {A : Type ℓ} (B : A → Type ℓ') → Type (ℓ-max ℓ ℓ')
isOfHLevelDep 0 {A = A} B = {a : A} → Σ[ b ∈ B a ] ({a' : A} (b' : B a') (p : a ≡ a') → PathP (λ i → B (p i)) b b')
isOfHLevelDep 1 {A = A} B = {a0 a1 : A} (b0 : B a0) (b1 : B a1) (p : a0 ≡ a1)  → PathP (λ i → B (p i)) b0 b1
isOfHLevelDep (suc (suc  n)) {A = A} B = {a0 a1 : A} (b0 : B a0) (b1 : B a1) → isOfHLevelDep (suc n) {A = a0 ≡ a1} (λ p → PathP (λ i → B (p i)) b0 b1)

isOfHLevel→isOfHLevelDep : (n : HLevel)
  → {A : Type ℓ} {B : A → Type ℓ'} (h : (a : A) → isOfHLevel n (B a)) → isOfHLevelDep n {A = A} B
isOfHLevel→isOfHLevelDep 0 h {a} =
  (h a .fst , λ b' p → isProp→PathP (λ i → isContr→isProp (h (p i))) (h a .fst) b')
isOfHLevel→isOfHLevelDep 1 h = λ b0 b1 p → isProp→PathP (λ i → h (p i)) b0 b1
isOfHLevel→isOfHLevelDep (suc (suc n)) {A = A} {B} h {a0} {a1} b0 b1 =
  isOfHLevel→isOfHLevelDep (suc n) (λ p → helper a1 p b1)
  where
  helper : (a1 : A) (p : a0 ≡ a1) (b1 : B a1) →
    isOfHLevel (suc n) (PathP (λ i → B (p i)) b0 b1)
  helper a1 p b1 = J (λ a1 p → ∀ b1 → isOfHLevel (suc n) (PathP (λ i → B (p i)) b0 b1))
                     (λ _ → h _ _ _) p b1

isContrDep→isPropDep : isOfHLevelDep 0 B → isOfHLevelDep 1 B
isContrDep→isPropDep {B = B} Bctr {a0 = a0} b0 b1 p i
  = comp (λ k → B (p (i ∧ k))) (λ k → λ where
        (i = i0) → Bctr .snd b0 refl k
        (i = i1) → Bctr .snd b1 p k)
      (c0 .fst)
  where
  c0 = Bctr {a0}

isPropDep→isSetDep : isOfHLevelDep 1 B → isOfHLevelDep 2 B
isPropDep→isSetDep {B = B} Bprp b0 b1 b2 b3 p i j
  = comp (λ k → B (p (i ∧ k) (j ∧ k))) (λ k → λ where
        (j = i0) → Bprp b0 b0 refl k
        (i = i0) → Bprp b0 (b2 j) (λ k → p i0 (j ∧ k)) k
        (i = i1) → Bprp b0 (b3 j) (λ k → p k (j ∧ k)) k
        (j = i1) → Bprp b0 b1 (λ k → p (i ∧ k) (j ∧ k)) k)
      b0

isOfHLevelDepSuc : (n : HLevel) → isOfHLevelDep n B → isOfHLevelDep (suc n) B
isOfHLevelDepSuc 0 = isContrDep→isPropDep
isOfHLevelDepSuc 1 = isPropDep→isSetDep
isOfHLevelDepSuc (suc (suc n)) Blvl b0 b1 = isOfHLevelDepSuc (suc n) (Blvl b0 b1)

isPropDep→isSetDep'
  : isOfHLevelDep 1 B
  → {p : w ≡ x} {q : y ≡ z} {r : w ≡ y} {s : x ≡ z}
  → {tw : B w} {tx : B x} {ty : B y} {tz : B z}
  → (sq : Square p q r s)
  → (tp : PathP (λ i → B (p i)) tw tx)
  → (tq : PathP (λ i → B (q i)) ty tz)
  → (tr : PathP (λ i → B (r i)) tw ty)
  → (ts : PathP (λ i → B (s i)) tx tz)
  → SquareP (λ i j → B (sq i j)) tp tq tr ts
isPropDep→isSetDep' {B = B} Bprp {p} {q} {r} {s} {tw} sq tp tq tr ts i j
  = comp (λ k → B (sq (i ∧ k) (j ∧ k))) (λ k → λ where
        (i = i0) → Bprp tw (tp j) (λ k → p (k ∧ j)) k
        (i = i1) → Bprp tw (tq j) (λ k → sq (i ∧ k) (j ∧ k)) k
        (j = i0) → Bprp tw (tr i) (λ k → r (k ∧ i)) k
        (j = i1) → Bprp tw (ts i) (λ k → sq (k ∧ i) (j ∧ k)) k)
      tw

isOfHLevelΣ' : ∀ n → isOfHLevel n A → isOfHLevelDep n B → isOfHLevel n (Σ A B)
isOfHLevelΣ' 0 Actr Bctr .fst = (Actr .fst , Bctr .fst)
isOfHLevelΣ' 0 Actr Bctr .snd (x , y) i
  = Actr .snd x i , Bctr .snd y (Actr .snd x) i
isOfHLevelΣ' 1 Alvl Blvl (w , y) (x , z) i .fst = Alvl w x i
isOfHLevelΣ' 1 Alvl Blvl (w , y) (x , z) i .snd = Blvl y z (Alvl w x) i
isOfHLevelΣ' {A = A} {B = B} (suc (suc n)) Alvl Blvl (w , y) (x , z)
  = isOfHLevelRetract (suc n)
      (λ p → (λ i → p i .fst) , λ i → p i .snd)
      ΣPathP
      (λ x → refl)
      (isOfHLevelΣ' (suc n) (Alvl w x) (Blvl y z))

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
-- {-# OPTIONS -v interaction.case:10 -v tc.cover:40 #-}
module Issue635 where

record Pointed : Set₁ where
  field
    Carrier : Set
    empty : Carrier
    equal : Carrier → Carrier → Set

record PointedMorphism (M₁ M₂ : Pointed) : Set where
  constructor morph
  module M₁ = Pointed M₁
  module M₂ = Pointed M₂
  field
    f : M₁.Carrier → M₂.Carrier
    .identity : M₂.equal (f M₁.empty) M₂.empty

g : ∀ (M₁ M₂ : Pointed) → PointedMorphism M₁ M₂ → PointedMorphism M₁ M₂
g M₁ M₂ (morph f identity) = morph f identity

f : ∀ {M₁ M₂ : Pointed} → PointedMorphism M₁ M₂ → PointedMorphism M₁ M₂
f x = {!x!}

{- WAS:
case splitting on x in that hole produces this monstrosity:

f {.Splitting.recCon-NOT-PRINTED Carrier empty times equal} {.Splitting.recCon-NOT-PRINTED Carrier₁ empty₁ times₁ equal₁} (morph f identity) = ?
-}

-- Andreas, 2013-03-21
-- NOW: case splitting on x yields pattern (morph f identity)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Termination.Sized.DeBruijnBase where

open import Data.Maybe
open import Data.Maybe.Effectful
open import Function -- composition, identity
open import Relation.Binary.PropositionalEquality hiding ( subst )
open ≡-Reasoning

open import Effect.Functor

fmap : {A B : Set} -> (A -> B) -> Maybe A -> Maybe B
fmap = RawFunctor._<$>_ functor

-- OR:
-- open RawFunctor MaybeFunctor using () renaming (_<$>_ to fmap)

fmapExt : {A B : Set}{f g : A -> B} ->
          (forall a -> f a ≡ g a) -> forall m -> fmap f m ≡ fmap g m
fmapExt f≡g nothing  = refl
fmapExt f≡g (just a) = cong just (f≡g a)

fmapLaw1 : {A : Set}(a : Maybe A) -> fmap id a ≡ a
fmapLaw1 nothing  = refl
fmapLaw1 (just a) = refl

fmapLaw2 : {A B C : Set}(f : B -> C)(g : A -> B) ->
          forall m -> fmap f (fmap g m) ≡ fmap (f ∘ g) m
fmapLaw2 f g nothing  = refl
fmapLaw2 f g (just a) = refl

-- untyped de Bruijn terms
data Lam (A : Set) : Set where
    var : A -> Lam A
    app : Lam A -> Lam A -> Lam A
    abs : Lam (Maybe A) -> Lam A

-- functoriality of Lam
lam : {A B : Set} -> (A -> B) -> Lam A -> Lam B
lam f (var a)     = var (f a)
lam f (app t1 t2) = app (lam f t1) (lam f t2)
lam f (abs r)     = abs (lam (fmap f) r)

lamExt : {A B : Set}{f g : A -> B} ->
         (forall a -> f a ≡ g a) -> forall t -> lam f t ≡ lam g t
lamExt f≡g (var a)   = cong var (f≡g a)
lamExt f≡g (abs r)   = cong abs (lamExt (fmapExt f≡g) r)
lamExt f≡g (app r s) = cong₂ app (lamExt f≡g r) (lamExt f≡g s)

lamLaw1 : {A : Set}(t : Lam A) -> lam id t ≡ t
lamLaw1 (var a) = refl
lamLaw1 (app r s) = begin
  lam id (app r s)
     ≡⟨ refl ⟩
  app (lam id r) (lam id s)
     ≡⟨ cong (app (lam id r)) (lamLaw1 s) ⟩
  app (lam id r) s
     ≡⟨ cong (\ x -> app x s) (lamLaw1 r) ⟩
  app r s
     ∎
lamLaw1 (abs t) = begin
  lam id (abs t)
     ≡⟨ refl ⟩
  abs (lam (fmap id) t)
     ≡⟨ cong abs (lamExt {g = id} fmapLaw1 t) ⟩
  abs (lam id t)
     ≡⟨ cong abs (lamLaw1 t) ⟩
  abs t
     ∎

lamLaw2 : {A B C : Set}(f : B -> C)(g : A -> B) ->
          forall t -> lam f (lam g t) ≡ lam (f ∘ g) t
lamLaw2 f g (var a)   = refl
lamLaw2 f g (app r s) = cong₂ app (lamLaw2 f g r) (lamLaw2 f g s)
lamLaw2 f g (abs t)   = begin
  lam f (lam g (abs t))
     ≡⟨ refl ⟩
  lam f (abs (lam (fmap g) t))
     ≡⟨ refl ⟩
  abs (lam (fmap f) (lam (fmap g) t))
     ≡⟨ cong abs (lamLaw2 (fmap f) (fmap g) t) ⟩
  abs (lam (fmap f ∘ fmap g) t)
     ≡⟨ cong abs (lamExt (fmapLaw2 f g) t) ⟩
  abs (lam (fmap (f ∘ g)) t)
     ≡⟨ refl ⟩
  lam (f ∘ g) (abs t)
     ∎

-- lifting a substitution A -> Lam B under a binder
lift : {A B : Set} -> (A -> Lam B) -> Maybe A -> Lam (Maybe B)
lift f nothing  = var nothing
lift f (just a) = lam just (f a)

-- extensionality of lifting
liftExt : {A B : Set}{f g : A -> Lam B} ->
   ((a : A) -> f a ≡ g a) -> (t : Maybe A) -> lift f t ≡ lift g t
liftExt H nothing  = refl
liftExt H (just a) = cong (lam just) $ H a

-- simultaneous substitution
subst : {A B : Set} -> (A -> Lam B) -> Lam A -> Lam B
subst f (var a)     = f a
subst f (app t1 t2) = app (subst f t1) (subst f t2)
subst f (abs r)     = abs (subst (lift f) r)

-- extensionality of subst
substExt : {A B : Set}{f g : A -> Lam B} ->
   ((a : A) -> f a ≡ g a) -> (t : Lam A) -> subst f t ≡ subst g t
substExt H (var a)     = H a
substExt {f = f}{g = g} H (app t1 t2) = begin
  subst f (app t1 t2)
     ≡⟨ refl ⟩
  app (subst f t1) (subst f t2)
     ≡⟨ cong (\ x -> app x (subst f t2)) (substExt H t1) ⟩
  app (subst g t1) (subst f t2)
     ≡⟨ cong (\ x -> app (subst g t1) x) (substExt H t2) ⟩
  app (subst g t1) (subst g t2)
     ∎
substExt {f = f}{g = g} H (abs r) = begin
  subst f (abs r)
     ≡⟨ refl ⟩
  abs (subst (lift f) r)
     ≡⟨ cong abs (substExt (liftExt H) r) ⟩
  abs (subst (lift g) r)
     ≡⟨ refl ⟩
  subst g (abs r)
     ∎

-- Lemma: lift g ∘ fmap f = lift (g ∘ f)
liftLaw1 : {A B C : Set}(f : A -> B)(g : B -> Lam C)(t : Maybe A) ->
  lift g (fmap f t) ≡ lift (g ∘ f) t
liftLaw1 f g nothing = begin
  lift g (fmap f nothing)
     ≡⟨ refl ⟩
  lift g nothing
     ≡⟨ refl ⟩
  var nothing
     ≡⟨ refl ⟩
  lift (g ∘ f) nothing
     ∎
liftLaw1 f g (just a) = begin
  lift g (fmap f (just a))
     ≡⟨ refl ⟩
  lift g (just (f a))
     ≡⟨ refl ⟩
  lam just (g (f a))
     ≡⟨ refl ⟩
  lift (g ∘ f) (just a)
     ∎

-- Lemma: subst g ∘ lam f t = subst (g ∘ f)
substLaw1 : {A B C : Set}(f : A -> B)(g : B -> Lam C)(t : Lam A) ->
  subst g (lam f t) ≡ subst (g ∘ f) t

substLaw1 f g (var a) = refl

substLaw1 f g (app t1 t2) = begin
  subst g (lam f (app t1 t2))
     ≡⟨ refl ⟩
  subst g (app (lam f t1) (lam f t2))
     ≡⟨ refl ⟩
  app (subst g (lam f t1)) (subst g (lam f t2))
     ≡⟨ cong (\ x -> app x (subst g (lam f t2))) (substLaw1 f g t1) ⟩
  app (subst (g ∘ f) t1) (subst g (lam f t2))
     ≡⟨ cong (\ x -> app (subst (g ∘ f) t1) x) (substLaw1 f g t2) ⟩
  app (subst (g ∘ f) t1) (subst (g ∘ f) t2)
     ∎

substLaw1 f g (abs r) =
  begin subst g (lam f (abs r))
     ≡⟨ refl ⟩
  subst g (abs (lam (fmap f) r))
     ≡⟨ refl ⟩
  abs (subst (lift g) (lam (fmap f) r))
     ≡⟨ cong abs (substLaw1 (fmap f) (lift g) r) ⟩
  abs (subst (lift g ∘ fmap f) r)
     ≡⟨ cong abs (substExt {f = lift g ∘ fmap f} {g = lift (g ∘ f)} (liftLaw1 f g) r) ⟩
  abs (subst (lift (g ∘ f)) r)
     ∎

-- Lemma: lift (lam f ∘ g) = lam f ∘ subst g
liftLaw2 : {A B C : Set}(f : B -> C)(g : A -> Lam B)(t : Maybe A) ->
  lift (lam f ∘ g) t ≡ lam (fmap f) (lift g t)
liftLaw2 f g nothing = begin
  lift (lam f ∘ g) nothing
     ≡⟨ refl ⟩
  var nothing
     ≡⟨ refl ⟩
  var (fmap f nothing)
     ≡⟨ refl ⟩
  lam (fmap f) (var nothing)
     ≡⟨ refl ⟩
  lam (fmap f) (lift g nothing)
     ∎
liftLaw2 f g (just a) = begin
  lift (lam f ∘ g) (just a)
     ≡⟨ refl ⟩
  lam just (lam f (g a))
     ≡⟨ lamLaw2 just f (g a) ⟩
  lam (just ∘ f) (g a)
     ≡⟨ lamExt (\ a -> refl) (g a) ⟩
  lam (fmap f ∘ just) (g a)
     ≡⟨ sym (lamLaw2 (fmap f) just (g a)) ⟩
  lam (fmap f) (lam just (g a))
     ≡⟨ refl ⟩
  lam (fmap f) (lift g (just a))
     ∎

-- Lemma: subst (lam f ∘ g) = lam f ∘ subst g
substLaw2 : {A B C : Set}(f : B -> C)(g : A -> Lam B)(t : Lam A) ->
  subst (lam f ∘ g) t ≡ lam f (subst g t)

substLaw2 f g (var a) = refl

substLaw2 f g (app r s) = begin
  subst (lam f ∘ g) (app r s)
     ≡⟨ refl ⟩
  app (subst (lam f ∘ g) r) (subst (lam f ∘ g) s)
     ≡⟨ cong (app (subst (lam f ∘ g) r)) (substLaw2 f g s) ⟩
  app (subst (lam f ∘ g) r) (lam f (subst g s))
     ≡⟨ cong (\ x -> app x (lam f (subst g s))) (substLaw2 f g r) ⟩
  app (lam f (subst g r)) (lam f (subst g s))
     ≡⟨ refl ⟩
  lam f (app (subst g r) (subst g s))
     ≡⟨ refl ⟩
  lam f (subst g (app r s))
     ∎

substLaw2 f g (abs t) = begin
  subst (lam f ∘ g) (abs t)
     ≡⟨ refl ⟩
  abs (subst (lift (lam f ∘ g)) t)
     ≡⟨ cong abs (substExt (liftLaw2 f g) t) ⟩
  abs (subst (lam (fmap f) ∘ (lift g)) t)
     ≡⟨ cong abs (substLaw2 (fmap f) (lift g) t) ⟩
  abs (lam (fmap f) (subst (lift g) t))
     ≡⟨ refl ⟩
  lam f (abs (subst (lift g) t))
     ≡⟨ refl ⟩
  lam f (subst g (abs t))
     ∎


text:
{-# OPTIONS --without-K  #-}
module sum where

open import level using (Level; _⊔_)
open import function.core

infixr 4 _,_
infixr 2 _×_
infixr 1 _⊎_

record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

open Σ public

_×_ : {l k : Level} (A : Set l) (B : Set k) → Set (l ⊔ k)
A × B = Σ A λ _ → B

uncurry : ∀ {a b c} {A : Set a} {B : A → Set b} {C : (x : A) → (B x) → Set c}
        → ((x : A) → (y : B x) → C x y) → ((xy : Σ A B) → C (proj₁ xy) (proj₂ xy))
uncurry f (a , b) = f a b

uncurry' : ∀ {i j k}{X : Set i}{Y : Set j}{Z : Set k}
        → (X → Y → Z)
        → (X × Y) → Z
uncurry' f (x , y) = f x y

data _⊎_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  inj₁ : (x : A) → A ⊎ B
  inj₂ : (y : B) → A ⊎ B

[_,⊎_] : ∀ {i i' j}{A : Set i}{A' : Set i'}{B : Set j}
      → (A → B) → (A' → B)
      → A ⊎ A' → B
[ f ,⊎ f' ] (inj₁ a) = f a
[ f ,⊎ f' ] (inj₂ a') = f' a'

map-⊎ : ∀ {i i' j j'}{A : Set i}{A' : Set i'}
      → {B : Set j}{B' : Set j'}
      → (A → B) → (A' → B')
      → A ⊎ A' → B ⊎ B'
map-⊎ g g' = [ inj₁ ∘' g ,⊎ inj₂ ∘' g' ]

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: HoTT/M-types


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Abstractions used in the reflection machinery
------------------------------------------------------------------------

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

module Reflection.Abstraction where

open import Data.List.Base as List using (List)
open import Data.Product using (_×_; _,_; uncurry; <_,_>)
import Data.String as String
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Product using (_×-dec_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

private
  variable
    A B : Set

------------------------------------------------------------------------
-- Re-exporting the builtins publically

open import Agda.Builtin.Reflection public using (Abs)
open Abs public

-- Pattern synonyms

------------------------------------------------------------------------
-- Operations

map : (A → B) → Abs A → Abs B
map f (abs s x) = abs s (f x)

------------------------------------------------------------------------
-- Decidable equality

abs-injective₁ : ∀ {i i′} {a a′ : A} → abs i a ≡ abs i′ a′ → i ≡ i′
abs-injective₁ refl = refl

abs-injective₂ : ∀ {i i′} {a a′ : A} → abs i a ≡ abs i′ a′ → a ≡ a′
abs-injective₂ refl = refl

abs-injective : ∀ {i i′} {a a′ : A} → abs i a ≡ abs i′ a′ → i ≡ i′ × a ≡ a′
abs-injective = < abs-injective₁ , abs-injective₂ >

-- We often need decidability of equality for Abs A when implementing it
-- for A. Unfortunately ≡-dec makes the termination checker unhappy.
-- Instead, we can match on both Abs A and use unAbs-dec for an obviously
-- decreasing recursive call.

unAbs : Abs A → A
unAbs (abs s a) = a

unAbs-dec : {x y : Abs A} → Dec (unAbs x ≡ unAbs y) → Dec (x ≡ y)
unAbs-dec {x = abs i a} {abs i′ a′} a≟a′ =
  Dec.map′ (uncurry (cong₂ abs)) abs-injective ((i String.≟ i′) ×-dec a≟a′)

≡-dec : Decidable {A = A} _≡_ → Decidable {A = Abs A} _≡_
≡-dec _≟_ x y = unAbs-dec (unAbs x ≟ unAbs y)


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

open import Setoids.Setoids
open import Functions.Definition
open import Groups.Definition
open import Sets.EquivalenceRelations
open import Groups.Homomorphisms.Definition
open import Groups.Lemmas

module Groups.Homomorphisms.Lemmas {a b c d : _} {A : Set a} {S : Setoid {a} {c} A} {B : Set b} {T : Setoid {b} {d} B} {_+A_ : A → A → A} {_+B_ : B → B → B} {G : Group S _+A_} {H : Group T _+B_} {f : A → B} (hom : GroupHom G H f) where

imageOfIdentityIsIdentity : Setoid._∼_ T (f (Group.0G G)) (Group.0G H)
imageOfIdentityIsIdentity = Equivalence.symmetric (Setoid.eq T) t
  where
    open Group H
    open Setoid T
    id2 : Setoid._∼_ S (Group.0G G) ((Group.0G G) +A (Group.0G G))
    id2 = Equivalence.symmetric (Setoid.eq S) (Group.identRight G)
    r : f (Group.0G G) ∼ f (Group.0G G) +B f (Group.0G G)
    s : 0G +B f (Group.0G G) ∼ f (Group.0G G) +B f (Group.0G G)
    t : 0G ∼ f (Group.0G G)
    t = groupsHaveRightCancellation H (f (Group.0G G)) 0G (f (Group.0G G)) s
    s = Equivalence.transitive (Setoid.eq T) identLeft r
    r = Equivalence.transitive (Setoid.eq T) (GroupHom.wellDefined hom id2) (GroupHom.groupHom hom)

groupHomsCompose : {o t : _} {C : Set o} {U : Setoid {o} {t} C} {_+C_ : C → C → C} {I : Group U _+C_} {g : B → C} (gHom : GroupHom H I g) → GroupHom G I (g ∘ f)
GroupHom.wellDefined (groupHomsCompose {I} {f} gHom) {x} {y} pr = GroupHom.wellDefined gHom (GroupHom.wellDefined hom pr)
GroupHom.groupHom (groupHomsCompose {U = U} {_+C_ = _·C_} {I} {g} gHom) {x} {y} = answer
  where
    open Group I
    answer : (Setoid._∼_ U) ((g ∘ f) (x +A y)) ((g ∘ f) x ·C (g ∘ f) y)
    answer = (Equivalence.transitive (Setoid.eq U)) (GroupHom.wellDefined gHom (GroupHom.groupHom hom {x} {y}) ) (GroupHom.groupHom gHom {f x} {f y})

homRespectsInverse : {x : A} → Setoid._∼_ T (f (Group.inverse G x)) (Group.inverse H (f x))
homRespectsInverse {x} = rightInversesAreUnique H {f x} {f (Group.inverse G x)} (transitive (symmetric (GroupHom.groupHom hom)) (transitive (GroupHom.wellDefined hom (Group.invLeft G)) imageOfIdentityIsIdentity))
  where
    open Setoid T
    open Equivalence eq

zeroImpliesInverseZero : {x : A} → Setoid._∼_ T (f x) (Group.0G H) → Setoid._∼_ T (f (Group.inverse G x)) (Group.0G H)
zeroImpliesInverseZero {x} fx=0 = transitive homRespectsInverse (transitive (inverseWellDefined H fx=0) (invIdent H))
  where
    open Setoid T
    open Equivalence eq

homRespectsInverse' : {a b : A} → Setoid._∼_ T (f (Group.inverse G a) +B f (Group.inverse G b)) (Group.inverse H (f (b +A a)))
homRespectsInverse' {a} {b} = transitive (symmetric (GroupHom.groupHom hom)) (transitive (GroupHom.wellDefined hom (Equivalence.symmetric (Setoid.eq S) (invContravariant G))) (homRespectsInverse))
  where
    open Setoid T
    open Equivalence eq


text:
-- Some proposition constructors.

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

module Tools.Nullary where

open import Relation.Nullary using (¬_; Dec; yes; no) public
open import Relation.Nullary.Decidable using (isYes) public

-- If A and B are logically equivalent, then so are Dec A and Dec B.

map : ∀ {ℓ₁ ℓ₂} {A : Set ℓ₁} {B : Set ℓ₂} → (A → B) → (B → A) → Dec A → Dec B
map f g (yes p) = yes (f p)
map f g (no ¬p) = no (λ x → ¬p (g x))